VectorCChargeZeroBridge
plain-language theorem explainer
VectorCChargeZeroBridge defines the interface that converts honest zeta-derived phase family data for a witnessed defect sensor into a ZeroCompositionWitness at the corresponding point. Analytic number theorists following the pure analytic route to the Riemann hypothesis would cite this structure to close the Vector C pathway. The declaration is a structure definition with no proof body, serving as an interface contract for later instantiation.
Claim. A structure is a Vector C charge zero bridge when, for every witnessed defect sensor $s$, the existence of zeta phase family data $z$ satisfying $z$ sensor equals the defect sensor of $s$ and $z$ phase family sensor equals the defect sensor of $s$ implies a zero composition witness exists for the complex point $s$.rho.
background
WitnessedDefectSensor records a complex point rho in the strip (1/2 < Re rho < 1), its integer charge, and the meromorphic order witness from zeta reciprocal at that point. ZetaPhaseFamilyData records phase samples obtained from the Weierstrass factorization of zeta reciprocal near such a point, together with the matching sensor and order. ZeroCompositionWitness supplies a concrete law at the zero deviation of rho whose value equals 1, forcing the point onto the critical line. The module assembles axiom-free carrier-side infrastructure for the analytic trace, with former axioms replaced by proved statements such as floor coverage iff charge zero.
proof idea
This declaration is a structure definition. It encodes the interface contract without any proof steps or lemmas applied.
why it matters
This structure feeds charge_zero_of_honest_phase_of_vectorC and direct_rh_from_vectorC_bridge, which establish that any successful instantiation yields the Riemann hypothesis via the analytic route. It completes the pure analytic pathway targeting ZeroFreeCriterion without external bridges or cost contradictions. The declaration touches the open question of realizing an honest phase family from actual zeta data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.