defect_realizedDefectCollapseScalar
plain-language theorem explainer
The theorem supplies the closed-form T1 defect for the realized collapse scalar built from any nonzero-charge sensor and index N. Workers on the T1-bounded realizability architecture cite this identity when tracking how annular cost maps to defect values on the collapse scalar. The proof is a one-line wrapper that instantiates the defect_one_div_one_add lemma after binding the annular cost to a nonnegative real t.
Claim. Let $J$ be the defect functional. For a sensor $s$ with nonzero charge and natural number $n$, $J$ of the realized collapse scalar at $s$ and $n$ equals $a^2 / (2(1+a))$, where $a$ is the annular cost of the mesh from the canonical defect sampled family at $s$.
background
The module develops the unified RH architecture with three components: cost divergence forced by nonzero charge, Euler trace admissibility, and physically realizable ledgers whose T1 defect stays bounded. The defect functional equals the J-cost, which is zero at unity. Annular cost is the sum of ring costs over an annular mesh. The upstream defect definition states it equals J for positive arguments. This supplies the explicit scalar computation inside the boundary transport step of the module's proof chain.
proof idea
The proof binds t to the annular cost of the sampled family mesh at N, records nonnegativity via annularCost_nonneg, then applies simpa to reduce directly to the defect_one_div_one_add identity at t.
why it matters
This identity supplies the precise T1 defect value needed to analyze boundary approach in the DivergenceWitnessesBoundary step. It connects the proved cost divergence for nonzero charges to the T1 prohibition on boundary approach for realizable ledgers. The result fills the explicit scalar defect computation in the module's architecture, supporting that realizable Euler ledgers cannot approach the T1 boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.