ZeroInducedProxyPhysicalizationBridge
plain-language theorem explainer
ZeroInducedProxyPhysicalizationBridge packages the claim that every Riemann zeta zero in the open critical strip yields a defect sensor satisfying the proxy physicalization bridge. Number theorists and physicists exploring physical interpretations of the Riemann Hypothesis cite this definition to reduce the conjecture to a sensor-level existence statement. It is introduced directly as a universal quantification over zeta zeros using the zetaDefectSensor constructor and the ProxyPhysicalizationBridge predicate.
Claim. Let $Z$ be the proposition that for every complex number $ρ$ with $ζ(ρ)=0$ and $1/2 < Re(ρ) < 1$, the sensor-level bridge holds for the defect sensor constructed from $Re(ρ)$ with multiplicity one. Here the sensor is built by zetaDefectSensor and the bridge is the implication from bounded T1 defect in the realizability proxy to PhysicallyExists.
background
The module isolates the transport from the T1-bounded realizability proxy supplied by PhysicallyRealizableLedger to the PhysicallyExists predicate. Upstream, zetaDefectSensor takes a real part in (1/2,1) and multiplicity to produce a DefectSensor carrying that charge and the in_strip flag. ProxyPhysicalizationBridge for a sensor requires that if the defect of the scalar state remains bounded over all N then PhysicallyExists holds for the same sensor. The Physical structure from DataCore supplies the minimal positive constants c, ħ, G for bridge anchors.
proof idea
This is a definition that directly encodes the universal quantification: for each strip zero ρ it applies zetaDefectSensor with multiplicity 1 and asserts ProxyPhysicalizationBridge on the resulting sensor. No lemmas or tactics are applied beyond the upstream constructors zetaDefectSensor and ProxyPhysicalizationBridge.
why it matters
This definition supplies the hypothesis that feeds rsPhysicalThesis_of_ZeroInducedProxyPhysicalizationBridge and thereby yields RiemannHypothesis via rh_from_ZeroInducedProxyPhysicalizationBridge. It is equivalent to the Riemann Hypothesis by zeroInducedBridge_iff_rh. In the Recognition framework it completes the bridge from the directed Euler ledger to the RS Physical Thesis, showing that the remaining gap after realizability is precisely the absence of strip zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.