Registry · Proposition IV.P81 tau-effective formalized

IV.P81 — Finiteness and decidability

For each primorial stage n >= 3, the strong loop class L_s[n] is finite (inherited from finite-dimensionality of H_partial[n]) and membership is decidable from the boundary holonomy data.

Book IV Part 5 Ch. 37

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookIV.Strong.StrongVacuum

Symbol: Tau.BookIV.Strong.FinitenessAndDecidability