eulerSampledFloorCovered_iff_charge_zero
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.