Registry · Proposition III.P24 tau-effective formalized

III.P24 — Three-Reading Equivalence at E₁

The E₁ Mutual Determination instance admits exactly three non-trivial sector-restricted readings (NS, YM, Hodge)

Book III Part 6 Ch. 44

Dependency Graph

Depends on (2)

III.D57 III.D58

Depended on by (1)

III.T40

Lean Formalization

Module: TauLib.BookIII.Arithmetic.EnrFunctor01

Symbol: three_reading_check