pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.NumberTheory.ArgumentPrincipleSensor

show as:
view Lean formalization →

A zero of the Riemann zeta function in the right half of the critical strip produces a nonphysical nonzero-charge sensor through the already-proved ontological dichotomy. Researchers formalizing the Riemann Hypothesis inside the Recognition Science framework cite this module to link analytic number theory directly to physical existence constraints. The module assembles the proved argument principle sampling with the zeta-ledger bridge to derive the sensor implication without new axioms.

claimIf there exists $s$ with $Re(s) > 1/2$ such that $zeta(s) = 0$, then a nonphysical nonzero-charge sensor exists, by the ontological dichotomy.

background

The module operates inside the NumberTheory domain of the Recognition Science formalization. It imports ArgumentPrincipleProved, which eliminates the argument_principle_sampling axiom and upgrades the analytic route to witnessed zeta inverse phase-family data, and ZetaLedgerBridge, which closes the formalization gap between the abstract DefectSensor and PhysicallyExists framework from UnifiedRH and Mathlib's concrete riemannZeta function. The doc comment states that a zero of zeta in the right half of the critical strip gives a nonphysical nonzero-charge sensor by the already-proved ontological dichotomy.

proof idea

This is a definition module, no proofs. It defines the charged sensor implication by direct reference to the imported results from ArgumentPrincipleProved and ZetaLedgerBridge.

why it matters in Recognition Science

The module supplies the explicit sensor construction required by RSPhysicalThesisDecomposition, which replaces the opaque RSPhysicalThesis dependency with a structured bundle of ingredients for the RH proof. It advances the Recognition framework by converting zeta zero data into a concrete nonphysicality constraint, supporting the chain that rules out right-half zeros. This closes the formalization gap identified in the upstream ZetaLedgerBridge doc comment.

scope and limits

used by (1)

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 (3)