direct_rh_from_EBBA_via_analytic
plain-language theorem explainer
Under the EulerBoundaryBridgeAssumption, no witnessed defect sensor can carry nonzero charge. This yields the Riemann Hypothesis directly through the analytic trace route from the ontology bridge. Number theorists and physicists linking physical realizability proxies to zeta-function zeros would cite the result for its axiom-free closure of the ontology path. The proof is a one-line term application of rh_from_zero_free_criterion to the ZeroFreeCriterion built from the bridge.
Claim. Let $B$ be the EulerBoundaryBridgeAssumption (collapse of realized defect families transports to boundary approach for the realizability proxy). Then for every witnessed defect sensor $s$ (a structure with complex center $rho$ in the strip $1/2 < Re(rho) < 1$, integer charge, and meromorphic-order witness for $zeta^{-1}$ at $rho$), $s.charge neq 0$ implies a contradiction.
background
The AnalyticTrace module supplies an axiom-free interface that assembles the full RH bridge from analytic trace infrastructure. It replaces former axioms with proved statements such as contour winding from holomorphy and floor coverage iff charge zero. WitnessedDefectSensor records a point $rho$ in the critical strip together with its charge and the explicit meromorphic-order witness for $zetaReciprocal$ at that point. EulerBoundaryBridgeAssumption is the proposition that every defect sensor equipped with its physically realizable ledger satisfies collapse boundary transport.
proof idea
The proof is a term-mode one-liner that applies rh_from_zero_free_criterion to the ZeroFreeCriterion obtained by zeroFreeCriterion_of_EBBA bridge. The latter definition first invokes honestPhaseCostBridge_of_EBBA and then zeroFreeCriterion_of_honestPhaseCostBridge, after which rh_from_zero_free_criterion extracts the honest-phase family and concludes charge zero.
why it matters
The declaration supplies the direct witnessed-sensor RH statement along the ontology route, feeding the preferred path in UnifiedRH.unified_rh. It closes the analytic-trace contribution to the Recognition Science framework by converting the external bridge hypothesis into a concrete ZeroFreeCriterion, thereby eliminating the need for separate axioms on winding or argument principle. The result sits downstream of the forcing chain (T5 J-uniqueness through T8 D=3) and the Recognition Composition Law, while leaving open the physical verification of the bridge assumption itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.