eulerSampledFloorCovered_iff_charge_zero
The equivalence shows that the Euler-sampled cost-covering package satisfies the topological floor condition precisely when the defect sensor has zero charge. Researchers deriving conditional Riemann Hypothesis statements from the Recognition Science carrier framework would cite this result. The proof splits the biconditional, using contradiction via the general nonzero-charge non-coverage lemma in one direction and the zero-charge annular floor identity plus budget nonnegativity in the other.
claimLet $P$ be the cost-covering package obtained by sampling the Euler carrier at real part $σ_0 > 1/2$. For any defect sensor $s$ with integer charge $m$, the statement that the annular topological floor of $m$ is bounded above by the carrier budget scale of $P$ for every mesh depth $N$ holds if and only if $m = 0$.
background
The EulerInstantiation module instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge using the Euler product for ζ(s). A DefectSensor records the multiplicity (charge) and real part of a potential zero of ζ. The predicate DefectTopologicalFloorCovered pkg sensor asserts ∀ N : ℕ, annularTopologicalFloor N sensor.charge ≤ carrierBudgetScale pkg.carrier. The eulerSampledPackage constructs a CostCoveringPackage whose carrier is the sampled Euler budgeted carrier at σ₀ > 1/2.
proof idea
The term proof opens the biconditional with constructor. The forward direction assumes coverage and obtains a contradiction from nonzero charge by applying not_DefectTopologicalFloorCovered. The reverse direction assumes zero charge, rewrites the floor via annularTopologicalFloor_zero, and concludes by carrierBudgetScale_nonneg.
why it matters in Recognition Science
This result closes the sampled Euler instantiation of the cost-covering axiom and is invoked directly by floorCovered_iff_charge_zero in AnalyticTrace. It sits in the module chain that converts the Euler product into a concrete carrier satisfying the hypotheses of the conditional Riemann Hypothesis bridge after convergence and nonvanishing of the regularized determinant. The downstream statement records the same equivalence for the covering package.
scope and limits
- Does not establish the Riemann Hypothesis unconditionally.
- Does not apply to carriers other than the sampled Euler product.
- Does not bound charges for sensors with real part outside the critical strip.
- Does not compute an explicit numerical value for the carrier budget scale.
formal statement (Lean)
979theorem eulerSampledFloorCovered_iff_charge_zero (σ₀ : ℝ) (hσ : 1/2 < σ₀)
980 (sensor : DefectSensor) :
981 DefectTopologicalFloorCovered (eulerSampledPackage σ₀ hσ) sensor ↔
982 sensor.charge = 0 := by
proof body
Term-mode proof.
983 constructor
984 · intro hcover
985 by_contra hm
986 exact not_DefectTopologicalFloorCovered (eulerSampledPackage σ₀ hσ) sensor hm hcover
987 · intro hzero
988 intro N
989 rw [hzero, annularTopologicalFloor_zero]
990 exact carrierBudgetScale_nonneg _
991
992end NumberTheory
993end IndisputableMonolith