floorCovered_iff_charge_zero
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.
claimLet $σ_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 in Recognition Science
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.
scope and limits
- Does not prove the Riemann hypothesis.
- Does not apply for real part at or below 1/2.
- Does not extend to sensors outside the defect class.
- Does not address the ontology route or empirical programs.
Lean usage
theorem charge_zero_of_covered (σ₀ : ℝ) (hσ : 1/2 < σ₀) (sensor : DefectSensor) (hcover : DefectTopologicalFloorCovered (eulerSampledCoveringPackage σ₀ hσ) sensor) : sensor.charge = 0 := (floorCovered_iff_charge_zero σ₀ hσ sensor).mp hcoverformal statement (Lean)
69theorem floorCovered_iff_charge_zero (σ₀ : ℝ) (hσ : 1/2 < σ₀)
70 (sensor : DefectSensor) :
71 DefectTopologicalFloorCovered (eulerSampledCoveringPackage σ₀ hσ) sensor ↔
72 sensor.charge = 0 :=
proof body
Term-mode proof.
73 eulerSampledFloorCovered_iff_charge_zero σ₀ hσ sensor
74
75/-! ### §3. Carrier-side RH obstruction (no axioms) -/
76
77/-- A DefectSensor with charge ≠ 0 can never have its floor covered by
78the sampled Euler package. The defect floor grows as m² log N while the
79carrier budget is 0. -/