direct_rh_from_vectorC_bridge
plain-language theorem explainer
A Vector C bridge converts honest zeta phase data into a zero composition witness and thereby forces every witnessed defect sensor to carry zero charge. Analytic number theorists pursuing an axiom-free proof of the Riemann Hypothesis would cite the result to close the pure analytic route once the bridge is supplied. The proof is a one-line term application of the zero-free criterion theorem to the criterion extracted from the bridge.
Claim. Suppose a Vector C charge-zero bridge exists, i.e., a structure that maps honest zeta-derived phase data for any witnessed defect sensor to a zero composition witness. Then every witnessed defect sensor has charge zero.
background
The Analytic Trace module builds an axiom-free interface to the Riemann Hypothesis from sampled Euler carriers, contour winding, and honest phase data. Central definitions are the VectorCChargeZeroBridge (a structure that turns honest zeta phase data into a ZeroCompositionWitness) and the WitnessedDefectSensor (a sensor carrying a charge value). The module proves floor coverage holds if and only if charge is zero and eliminates prior axioms by deriving zero winding from holomorphy plus nonvanishing. Upstream results include the zero-free criterion theorem and the honest-phase cost bridges that supply the phase data contract.
proof idea
The proof is a term-mode one-liner: it applies rh_from_zero_free_criterion directly to the zero-free criterion produced by zeroFreeCriterion_of_vectorC vc.
why it matters
The theorem closes the pure analytic route to the Riemann Hypothesis once a Vector C bridge is instantiated, feeding the zero-free criterion and the direct RH statement in the same module. It supports the Recognition Science analytic path that avoids the deprecated defect_annular_cost_bounded axiom and the ontology route via UnifiedRH.unified_rh. The result touches the open instantiation question for the Vector C bridge from zeta phase data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.