single_scalar_obstruction
plain-language theorem explainer
The theorem shows that any DefectSensor with nonzero charge forces the T1 defect of its realized collapse scalar family to be unbounded. Unification researchers cite it to demonstrate that the Euler boundary bridge cannot be closed by equating the realizability proxy to a single scalar observable. The proof is a direct term application of the not_realizedDefectCollapseScalar_t1_bounded lemma.
Claim. Let $s$ be a defect sensor with $s.charge ≠ 0$. There does not exist a real $K$ such that for every natural number $n$ the defect of the realized collapse scalar of $s$ at $n$ is at most $K$.
background
The Unified RH module replaces an earlier bounded-total-cost ledger with a three-component architecture: CostDivergent (nonzero charge forces annular cost to diverge), EulerTraceAdmissible (Euler carrier is convergent with bounded log derivative), and PhysicallyRealizableLedger (T1 defect remains uniformly bounded for Euler instances). The defect function is the T1 cost from LawOfExistence.defect. Upstream results include the structure of nuclear densities in NucleosynthesisTiers.of and the dimensionless bridge ratio $K = φ^{1/2}$ from Constants.K.
proof idea
One-line wrapper that applies not_realizedDefectCollapseScalar_t1_bounded sensor hm.
why it matters
It closes the single-scalar discharge route for the bridge hypothesis, supporting the module's claim that EulerBoundaryBridgeAssumption is equivalent to RH. The result sits inside the T1 cost barrier step of the forcing chain and rules out identifying the collapse observable with a bounded scalar proxy. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.