Measurement C2 Abridge Measurement Bridge C Eq 2 A

The C = 2A bridge

In quantum mechanics, the probability of an outcome is given by the Born rule: the squared magnitude of a probability amplitude. The declaration measurement_bridge_C_eq_2A is a theorem in the machine-checked library of formal theorems that connects this probabilistic rule to a deeper cost structure. It states that for any two-branch geodesic rotation, the recognition cost C exactly equals twice a rate action A, written as C = 2A. The rate action is a quantity that accumulates along a path, and the recognition cost is the framework's measure of the effort required to register an event.

The theorem is proved by constructing a recognition path from a rotation and showing that the path action equals twice the rate action. The proof uses an integral of the cotangent function, which evaluates to a logarithm of a sine. This is not a numerical approximation; it is an exact equality. The result is then used to derive two further statements. First, the weight of a path, defined as exp(-C), equals exp(-2A). Second, this weight equals the squared initial amplitude, which is precisely the Born probability. In plain terms, the framework shows that the probability of a measurement outcome is governed by the same cost functional that governs recognition.

The theorem does not claim that all measurements are described by this bridge, nor that the rate action is observable. It applies specifically to two-branch geodesic rotations, a restricted class of paths. The connection to the full Born rule for arbitrary measurements is not established. The framework's own library states the equivalence for this constructed path, and the weight bridge and amplitude modulus bridge follow from it. The declaration does not assert that the cost functional J is the only possible one; that uniqueness is a separate theorem. It also does not claim that the rate action is the physical action of any known field; the identification is a structural one within the framework.

/-- Main C=2A Bridge Theorem:
    The recognition action for the constructed path equals twice the rate action -/
theorem measurement_bridge_C_eq_2A (rot : TwoBranchRotation) :
  pathAction (pathFromRotation rot) = 2 * rateAction rot := by
  unfold pathAction pathFromRotation rateAction
  simp
  have hkernel : ∫ ϑ in (0)..(π/2 - rot.θ_s),
                   Jcost (recognitionProfile (ϑ + rot.θ_s)) =
                2 * ∫ ϑ in (0)..(π/2 - rot.θ_s), Real.cot (ϑ + rot.θ_s) :=
    kernel_integral_match rot.θ_s rot.θ_s_bounds
  rw [hkernel]
  have h_subst :
      ∫ ϑ in (0)..(π/2 - rot.θ_s), Real.cot (ϑ + rot.θ_s)
        = ∫ θ in rot.θ_s..(π/2), Real.cot θ := by
    simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc]
      using
        (intervalIntegral.integral_comp_add_right
          (a := (0 : ℝ)) (b := π/2 - rot.θ_s)
          (f := fun θ => Real.cot θ) (d := rot.θ_s))
  have hI := integral_cot_from_theta rot.θ_s rot.θ_s_bounds
  have htan :
      ∫ ϑ in (0)..(π/2 - rot.θ_s), Real.cot (ϑ + rot.θ_s)
        = - Real.log (Real.sin rot.θ_s) := by
    simpa [h_subst] using hI
  simp [htan, two_mul, mul_left_comm, mul_assoc]

/-- Weight bridge: w = exp(-C) = exp(-2A) -/
theorem weight_bridge (rot : TwoBranchRotation) :
  pathWeight (pathFromRotation rot) = Real.exp (- 2 * rateAction rot) := by
  unfold pathWeight
  rw [measurement_bridge_C_eq_2A]
  congr 1
  ring

/-- Weight equals Born probability: exp(-2A) = |α₂|² -/
theorem weight_equals_born (rot : TwoBranchRotation) :
  pathWeight (pathFromRotation rot) = initialAmplitudeSquared rot := by
  unfold pathWeight initialAmplitudeSquared
  rw [measurement_bridge_C_eq_2A]
  have h := Measurement.born_weight_from_rate rot
  have hWeight :
      Real.exp (-(2 * rateAction rot)) = initialAmplitudeSquared rot := by
    simpa [rateAction, Measurement.initialAmplitudeSquared] using h
  simpa using hWeight

What this page does not claim

The theorem does not apply to arbitrary quantum measurements beyond two-branch geodesic rotations. The rate action A is not identified with the action of any known physical field. The uniqueness of the cost functional J is a separate theorem, not established by this bridge.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Measurement/C2ABridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: