MeasurementBridgeCert
plain-language theorem explainer
Certificate packaging the two-branch measurement bridge: for every two-branch rotation the recognition path action equals twice the rate action, and the path weight is exp(-2A). Cite it when you need a single verified bundle of the C=2A and Born-weight identities without quantum scaffolds. Discharge is a one-line And.intro of the two C2ABridge theorems.
Claim. A measurement-bridge certificate is a unit record whose verification predicate asserts: for every two-branch rotation $\mathrm{rot}$, if $\gamma$ is the recognition path built from $\mathrm{rot}$, then the path action satisfies $C[\gamma]=2A(\mathrm{rot})$ and the path weight satisfies $w[\gamma]=\exp(-2A(\mathrm{rot}))$. Every such certificate is verified.
background
The module packages the two-branch measurement bridge proved in C2ABridge, and deliberately imports neither Quantum scaffolds nor a measurement-axioms typeclass.
Recognition action on a path is $C[\gamma]=\int_0^{T} J(r(t)),dt$ (pathAction), with positive weight $w[\gamma]=\exp(-C[\gamma])$ (pathWeight). From a two-branch rotation one builds a canonical path via pathFromRotation: duration $T=\pi/2-\theta_s$ and rate equal to the recognition profile shifted by the split angle.
Upstream, measurement_bridge_C_eq_2A states that this constructed path has $C[\gamma]=2A(\mathrm{rot})$ ("the recognition action for the constructed path equals twice the rate action"). weight_bridge then rewrites $w[\gamma]=\exp(-C)=\exp(-2A)$.
proof idea
The structure itself is empty (unit certificate). The simp predicate verified is the conjunction of the two universal statements over TwoBranchRotation.
verified_any is a two-goal And.intro: the first intro applies measurement_bridge_C_eq_2A; the second applies weight_bridge. No extra algebra is done at this layer.
why it matters
This is a Verification-domain certificate: a single Prop that auditors can point at when they need both halves of the two-branch bridge (action doubling and the exponential weight that yields the Born weight) without dragging in quantum measurement axioms.
It sits directly on the C2ABridge landmarks $C=2A$ and $w=\exp(-2A)$. Downstream use count is currently zero; the certificate is an export surface for the measurement stack rather than an intermediate lemma. In the broader RS picture it records that the path-integral cost built from the J-cost on the recognition profile doubles the rate action on two-branch rotations, which is the classical-to-weight step before any amplitude phase is attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.