EulerCarrier
plain-language theorem explainer
EulerCarrier encodes the abstract Fredholm-Carleman carrier tied to the Euler product, requiring a regularity half-plane strictly above 1/2, a real-valued logarithmic derivative bound finite on that half-plane, and an explicit nonvanishing proposition. Recognition Science researchers and number theorists working on the Riemann hypothesis through cost-covering bridges cite this interface to construct concrete witnesses such as the zeta carrier. The declaration is a plain structure definition whose fields directly package the half-plane, bound, f
Claim. An Euler carrier consists of a real number $h > 1/2$, a function $B:ℝ→ℝ$, a proof that $B$ remains finite for every $σ > h$, and a proposition asserting that the associated carrier $C(s) = det_2(I-A(s))^2 = ∏_p (1-p^{-s})^2 exp(2p^{-s})$ is nonvanishing on the half-plane Re$(s) > h$.
background
The Cost-Covering Bridge module packages the RS cost-covering architecture for the Riemann hypothesis once the budget interface is realized. It rests on the unconditional annular analysis of AnnularCost.lean, which supplies phiCost properties, Jensen bounds, coercivity, topological floor, annular excess, and trace-based carrier budget. The carrier is defined as the Fredholm-Carleman determinant $C(s) = det_2(I-A(s))^2 = ∏_p (1-p^{-s})^2 exp(2p^{-s})$, holomorphic and nonvanishing for Re$(s) > 1/2$. Any zero of zeta at $ρ$ with Re$(ρ) > 1/2$ induces a pole of order $m ≥ 1$ in the sensor $D(s) = zeta(s)^{-1}$, driving the topological floor to diverge as $m^2 log N$.
proof idea
The declaration is a structure definition that directly introduces the five fields (halfPlane, halfPlane_gt, logDerivBound, logDerivBound_finite, nonvanishing) with no lemmas, tactics, or reduction steps required.
why it matters
EulerCarrier supplies the abstract interface instantiated by zetaCarrier and by eulerCarrierInstance in EulerInstantiation. It is used by not_DefectTopologicalFloorCovered, which isolates the nontrivial step that a finite carrier scale cannot dominate the defect topological floor of a nonzero-charge sensor. Within the Recognition framework the structure advances the cost-covering argument that forces $m = 0$ for zeros with Re$(s) > 1/2$, connecting to the T5 J-uniqueness, T7 eight-tick octave, and annular excess bounds independent of mesh refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.