Registry · Proposition IV.P85 tau-effective formalized

IV.P85 — Existence and uniqueness at each stage

For each n >= 3 the strong vacuum Gamma_s^*[n] exists (finite nonempty domain), is unique (NFMin tie-breaking), and is computable from the boundary holonomy algebra data at stage n.

Book IV Part 5 Ch. 37

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookIV.Strong.StrongVacuum

Symbol: Tau.BookIV.Strong.ExistenceAndUniquenessAtEachStage