pith. sign in
module module high

IndisputableMonolith.NumberTheory.EulerCarrierComplex

show as:
view Lean formalization →

The module defines the open half-plane Re(s) > 1/2 as the carrier domain for the Euler product in the Recognition Science number theory layer. Researchers constructing analytic traces or contour arguments from the RS cost structure would cite it when replacing prior axioms with explicit certificates. The module supplies only definitions and certificates, with no internal proofs.

claimLet $H = { s : ℂ | Re(s) > 1/2 }$. This open half-plane is the domain on which the Euler carrier complex is defined and on which holomorphic nonvanishing functions are certified to have zero winding.

background

Recognition Science derives number-theoretic objects from the J-functional and the phi-ladder cost structure imported from Constants (τ₀ = 1 tick) and Cost. The module introduces the open half-plane Re(s) > 1/2 as the geometric carrier for the Euler product instantiation of the abstract RS carrier/sensor framework. This half-plane is the classical region of absolute convergence for the zeta Euler product, now repurposed to host contour-winding data and sampled traces.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds AnalyticTrace, which assembles the axiom-free RH bridge by replacing zeroWindingOfHolNonvanishing with the explicit contourWinding construction. It also supplies the domain for EulerInstantiation (Euler product of ζ(s) as RS carrier) and for SampledTrace (bridge from continuous contours to discrete AnnularMesh). The half-plane definition therefore closes the geometric layer between Cost and the full analytic trace infrastructure.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)