weight_bridge
plain-language theorem explainer
The weight bridge equates the path weight of any rotation-derived recognition path to the exponential of minus twice the rate action. Researchers connecting recognition costs to Born-rule probabilities in quantum measurement would cite this step. The proof is a short algebraic reduction that unfolds the weight definition, substitutes the C-equals-2A bridge, and normalizes the resulting expression.
Claim. For any two-branch geodesic rotation $ρ$, the path weight $w[γ_ρ] = e^{-2A(ρ)}$, where $γ_ρ$ is the recognition path constructed from $ρ$ and $A(ρ)$ denotes the associated rate action.
background
This theorem belongs to the C=2A Measurement Bridge module, which proves that recognition action C for a two-branch geodesic rotation equals twice the rate action A, so that quantum measurement and recognition share the same cost functional J. The path weight is defined as the positive quantity $w[γ] = exp(-C[γ])$. The rotation-to-path constructor builds a RecognitionPath whose duration and rate profile are taken directly from the input rotation bounds and recognition profile. Upstream results fix the active edge count A at 1 per fundamental tick and recover probabilities via the squared modulus of state amplitudes.
proof idea
The proof is a term-mode reduction. It unfolds the pathWeight definition to expose the exponential of the negative path action, rewrites via the measurement_bridge_C_eq_2A theorem that equates path action to twice the rate action, then applies congruences and ring normalization to finish the equality.
why it matters
This declaration converts the central C-equals-2A bridge into an explicit weight formula, allowing direct comparison with Born probabilities in the quantum ledger. It supports the framework claim that measurement is governed by the unique J-cost functional. The result sits immediately before the weight-equals-Born sibling and inherits the module's setting of two-branch geodesics under the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.