Measurement C2 Abridge Weight Equals Born

The weight bridge

The Born rule is the standard quantum-mechanical recipe that turns a wavefunction's amplitude into a probability: the probability of an outcome equals the squared magnitude of its amplitude. In the Recognition Science framework, the declaration weight_equals_born proves that, for a specific two-branch rotation, the framework's own recognition weight equals exactly that squared amplitude. This is a formal equivalence, not an approximation or a numerical coincidence.

The framework's recognition cost, a measure of how much effort reality's discrete record of events spends on a transition, is linked to a rate action through the C = 2A bridge theorem. The weight is then defined as exp(-C). The weight_equals_born theorem shows that this weight, built entirely from the framework's cost functional, is identical to the squared initial amplitude of the rotation. In plain terms, the framework's internal accounting for a two-branch process reproduces the Born rule's probability assignment.

The proof is a short chain of equalities: it unfolds the definitions of weight and amplitude, applies the C = 2A bridge, and uses a prior lemma that connects the rate action to the squared amplitude. The result is a theorem in the machine-checked library of formal theorems, meaning the equivalence is verified by a computer, not just argued in a written exposition. This is a structural result: it says the framework's cost functional and the Born rule agree for this class of rotations.

What the declaration does not claim is broader scope. It applies only to a two-branch geodesic rotation, a specific setup with exactly two possible outcomes. It does not prove the Born rule for general quantum systems, nor does it derive the full measurement postulate of quantum mechanics. It establishes a precise correspondence for one constructed path, not a universal law. The theorem is a bridge, not a replacement for the standard quantum formalism.

/-- 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

/-- 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

What this page does not claim

The theorem does not apply to general quantum systems with more than two outcomes. It does not derive the full measurement postulate of quantum mechanics. It does not claim the framework's cost functional is the only way to obtain the Born rule.

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: