module module high

`IndisputableMonolith.NumberTheory.ZetaLedgerBridge`

The ZetaLedgerBridge module links the zeta function's Euler product to the RS ledger through defect sensors. It establishes that a zetaDefectSensor of multiplicity one carries charge one. Downstream modules for the RH proof chain import this bridge. The construction rests on the EulerInstantiation and UnifiedRH modules.

claimA sensor constructed via the zeta defect sensor with multiplicity 1 has charge 1.

background

The module sits inside the NumberTheory domain and imports EulerInstantiation, which shows that the Euler product of ζ(s) instantiates the abstract RS carrier/sensor framework from AnnularCost.lean and CostCoveringBridge.lean. It also imports UnifiedRH, whose T1-Bounded Realizability Architecture replaces the former OntologicalPrimeLedger with a structured three-component system for bounded annular cost. The local setting therefore combines the Euler product sensor construction with the realizability architecture to produce ledger-compatible zeta sensors.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds ArgumentPrincipleSensor (which isolates zeros as annular winding charge), ProxyPhysicalizationBridge (which closes the gap after the Euler ledger), RH_Certificate (which assembles the full RS-to-RH chain), and RSPhysicalThesisDecomposition (which replaces the opaque RSPhysicalThesis dependency). It supplies the concrete zeta-to-ledger link required by the five-line RH proof outline in RH_Certificate.

scope and limits

Does not prove the Riemann Hypothesis.
Does not treat the left half-plane.
Does not compute explicit zero locations.
Does not bound total annular cost.

used by (4)

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

IndisputableMonolith.NumberTheory.ArgumentPrincipleSensor module_import
IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge module_import
IndisputableMonolith.NumberTheory.RH_Certificate module_import
IndisputableMonolith.NumberTheory.RSPhysicalThesisDecomposition module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.NumberTheory.EulerInstantiation module_import
IndisputableMonolith.Unification.UnifiedRH module_import

declarations in this module (17)

theorem zetaDefectSensor_charge_one L52
theorem zetaDefectSensor_charge_ne_zero L58
theorem nonzero_charge_not_physical L66
theorem unit_sensor_not_physical L75
theorem strip_zero_gives_nonphysical_sensor L87
def RSPhysicalThesis L115
theorem no_strip_zeros_from_rs L131
theorem zeta_ne_zero_re_ge_one L141
theorem rh_right_half_from_rs L154
theorem gammaR_ne_zero_of_nontrivial_zero L165
theorem completedZeta_zero_of_nontrivial_zero L177
theorem zeta_one_sub_zero_of_zero L191
theorem rh_from_rs_thesis L213
theorem rh_certificate L250
theorem rh_right_half_certificate L258
theorem witnessed_sensor_not_physical L278
theorem witnessed_physical_contradiction L286