pith. machine review for the scientific record. sign in
theorem proved term proof high

charge_zero_of_covered

show as:
view Lean formalization →

If the Euler sampled covering package at real part σ₀ > 1/2 topologically covers the floor for a defect sensor, then the sensor charge is zero. Analysts closing the pure analytic route to the Riemann hypothesis in Recognition Science cite this to obtain charge vanishing from coverage data. The proof is a one-line term application of the floor-coverage equivalence via modus ponens.

claimLet σ₀ > 1/2 be real and let S be a defect sensor. If the Euler sampled covering package at σ₀ satisfies the topological floor coverage condition for S, then the charge of S equals zero.

background

The Analytic Trace module assembles an axiom-free bridge from meromorphic factorization of ζ⁻¹ to the Riemann hypothesis. The Euler sampled covering package packages honest phase data from the carrier complex and contour winding, with annular excess fixed at zero by the zero-winding certificate. A DefectSensor records net charge as the integrated defect functional J(x) = (x + x⁻¹)/2 - 1 drawn from the Law of Existence. The topological floor covered predicate asserts that the sampled package exhausts the phase budget exactly on the eight-tick octave without excess cost.

proof idea

The proof is a one-line term wrapper that applies the left-to-right direction of the floorCovered_iff_charge_zero equivalence to the coverage hypothesis.

why it matters in Recognition Science

This result replaces the former axiom argument_principle_forces_charge_zero and supplies the final implication needed for the ZeroFreeCriterion structure in the pure analytic route. It feeds direct_rh_from_honestPhaseCostBridge and honestPhase_routeC_bottleneck by converting floor coverage into charge zero once honest phase data from zetaDerivedPhaseFamily is in place. In the Recognition framework it closes the analytic trace without external hypotheses, supporting the T5 J-uniqueness and the eight-tick phase periodicity while leaving the ontology route via EulerBoundaryBridgeAssumption untouched.

scope and limits

formal statement (Lean)

  86theorem charge_zero_of_covered (σ₀ : ℝ) (hσ : 1/2 < σ₀)
  87    (sensor : DefectSensor)
  88    (hcover : DefectTopologicalFloorCovered (eulerSampledCoveringPackage σ₀ hσ) sensor) :
  89    sensor.charge = 0 :=

proof body

Term-mode proof.

  90  (floorCovered_iff_charge_zero σ₀ hσ sensor).mp hcover
  91
  92/-! ### §4. Zero-free criterion (analytic route target) -/
  93
  94/-- The zero-free criterion for the pure analytic route.
  95
  96This structure packages the honest analytic target: witnessed ζ⁻¹ defect data
  97in the strip gives an honest phase-family package, and analytic estimates then
  98force the corresponding defect charge to vanish.
  99
 100**Field status (April 2026):**
 101- `logDeriv_bounded_on_strip`: **PROVED** (`carrierDerivBound_pos`).
 102- `carrier_nonvanishing_on_strip`: **PROVED** (`carrier_nonvanishing`).
 103- `honest_phase_family`: **PROVED** via `honest_argument_principle_phase_family`,
 104  now using `zetaDerivedPhaseFamily` (genuine phase data from meromorphic
 105  factorization) rather than the former `trivialDefectPhaseFamily` scaffold.
 106- `charge_zero_of_honest_phase`: **NARROWED TARGET**. Honest phase data now
 107  comes with a canonical perturbation witness, and the present sampled family
 108  sits exactly on the topological floor (`annularExcess = 0`). The remaining
 109  content is to upgrade the honest sampled family to bounded total cost / floor
 110  coverage, forcing charge = 0.
 111
 112This replaces the deprecated `defect_annular_cost_bounded` as the proper
 113analytic-route target. -/

depends on (32)

Lean names referenced from this declaration's body.

… and 2 more