floorCovered_iff_charge_zero
plain-language theorem explainer
The theorem establishes that the defect topological floor is covered by the sampled Euler package precisely when the sensor charge vanishes. Analysts pursuing the pure analytic route to the Riemann hypothesis cite this equivalence to link coverage directly to charge zero. The proof is a one-line wrapper applying the sampled Euler floor coverage lemma.
Claim. Let $σ_0 > 1/2$ be real and let $S$ be a defect sensor. The topological floor of the defect is covered by the sampled Euler package at $σ_0$ if and only if the charge of $S$ equals zero.
background
The Analytic Trace module assembles an axiom-free RH bridge via the sampled Euler package, which carries zero budget from zero-winding certification in the Euler carrier complex. The defect functional equals J at positive arguments, with the property that defect at unity is zero. Upstream results set the carrier frequency to 5φ Hz and the active edge count A to 1, satisfying the φ-power balance identity at D = 3. The module replaces prior axioms with proved equivalences from holomorphy and nonvanishing.
proof idea
This is a one-line wrapper that applies the sampled Euler floor coverage equivalence to obtain the bidirectional statement between topological floor coverage and sensor charge zero.
why it matters
The result supports the downstream implication that floor coverage forces zero charge, as stated in charge_zero_of_covered: 'If floor coverage holds for the sampled package, the charge must be 0.' It advances the carrier-side infrastructure by proving the equivalence, closing the former axiom on the argument principle. This contributes to the pure analytic route targeting a ZeroFreeCriterion from honest phase data within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.