Registry · Proposition III.P18 tau-effective formalized

III.P18 — Hodge Requires E₁

At E₀, all characters are NF-addressable (Book II Central Theorem). The Hodge question becomes non-trivial only at E₁, where sector admissibility predicates distinguish addressable-within-sector from addressable-globally.

Book III Part 5 Ch. 41

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookIII.Physics.Hodge

Symbol: char_sector_check