measurement_bridge_C_eq_2A
plain-language theorem explainer
The central bridge theorem equates the recognition path action C for any two-branch geodesic rotation to twice its rate action A. Measurement theorists in Recognition Science cite it to show that quantum probabilities arise from the same J-cost functional that governs classical rate models. The proof unfolds the action definitions, replaces the J-cost integral by twice a cotangent integral via kernel_integral_match, shifts the integration limits with arithmetic lemmas and integral_comp_add_right, then evaluates the definite integral with the -1
Claim. For any two-branch rotation ρ with starting angle θ_s ∈ (0, π/2), the integrated recognition cost along the geodesic path constructed from ρ equals twice the rate action of ρ: C(ρ) = 2 A(ρ).
background
The module proves the exact equivalence C = 2A between recognition cost and residual rate action for two-branch rotations. TwoBranchRotation packages an angle θ_s together with the open-interval bounds 0 < θ_s < π/2. pathFromRotation builds the corresponding geodesic path; pathAction integrates the J-cost (recognitionProfile) along that path; rateAction supplies the base rate whose doubling yields the total cost. The local setting is the C = 2A Measurement Bridge, whose purpose is to demonstrate that quantum measurement and recognition are governed by the same unique cost functional J. Upstream, integral_cot_from_theta states that ∫_θ_s^{π/2} cot θ dθ = -log(sin θ_s), while kernel_integral_match supplies the identity that converts the J-cost integral into twice the cotangent integral.
proof idea
The tactic proof first unfolds pathAction, pathFromRotation and rateAction, then applies kernel_integral_match to obtain the factor-of-two relation between the J-cost integral and the cotangent integral. A change-of-variable step invokes intervalIntegral.integral_comp_add_right together with add_assoc, add_comm and add_left_comm to shift the limits from (0, π/2 - θ_s) to (θ_s, π/2). The resulting integral is identified with integral_cot_from_theta, which evaluates it to -log(sin θ_s). Final simp steps with two_mul, mul_left_comm and mul_assoc close the equality.
why it matters
The result is invoked directly by weight_bridge (which obtains pathWeight = exp(-2A)), by weight_equals_born (which equates the weight to the Born probability |α₂|²) and by amplitude_modulus_bridge (which recovers the modulus |𝒜| = exp(-A)). It supplies the central C = 2A step inside the Measurement.C2ABridge module, thereby linking the J-cost functional of the Recognition Composition Law to observable measurement weights. In the broader framework it closes the bridge between the eight-tick octave and the phi-ladder on one side and the probabilistic structure of quantum measurement on the other.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.