Measurement C2 Abridge

The C = 2A bridge

Measurement c2 abridge is the name of a formal result inside the Recognition Science framework. The name encodes its content: the recognition cost C equals twice the rate action A. In plain language, the module proves that the price the framework assigns to a recognition event is not an independent quantity. It is locked to another quantity, the residual-model rate action, by an exact factor of two. The result is a theorem in the framework's machine-checked library of formal theorems, meaning a computer verified every step of the proof.

The setting is a two-branch geodesic rotation, a geometric object with two paths that split and rejoin. The framework defines a recognition path from such a rotation and assigns it a cost. Separately, it defines a rate action for the rotation itself. The bridge theorem states that for any such rotation, the recognition path's action equals exactly twice the rate action. The proof uses a standard integral: the integral of cotangent from an angle to π/2 equals minus the natural logarithm of the sine of that angle. This integral is the technical engine that makes the factor of two appear.

The consequence is a chain of equalities. Since the path weight is exp(-C) and C = 2A, the weight becomes exp(-2A). The module then proves this weight equals the squared amplitude of the initial branch, which is the Born probability. A further theorem shows the amplitude modulus itself is exp(-A). The upshot: quantum measurement, expressed as a probability from an amplitude, is the same thing as recognition cost, expressed as a weight from an action. The framework's unique cost functional J governs both.

In Recognition Science, this is the bridge that connects the framework's core cost concept to the familiar Born rule of quantum mechanics. It does not introduce a new physical constant or a new rule. It shows that the rule already present in the framework, the forced cost J, reproduces the Born probability when applied to a two-branch rotation. The module is a formal proof, not a numerical fit. It establishes an exact equality, not an approximation.

What this changes for a reader is the status of the Born rule inside the framework. The rule is not assumed as an axiom. It is derived from the same cost function that governs recognition. The factor of two is not adjustable. It falls out of the integral. The module is one more link in the chain that starts from the cost function and reaches familiar physics.

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

/-- Amplitude bridge modulus: |𝒜| = exp(-A) -/
theorem amplitude_modulus_bridge (rot : TwoBranchRotation) (φ : ℝ) :
  ‖pathAmplitude (pathFromRotation rot) φ‖ = Real.exp (- rateAction rot) := by
  unfold pathAmplitude
  have hExpReal :
      ‖Complex.exp (-(pathAction (pathFromRotation rot)) / 2)‖ =
        Real.exp (-(pathAction (pathFromRotation rot)) / 2) := by
    simpa using Complex.norm_exp_ofReal (-(pathAction (pathFromRotation rot)) / 2)
  have hExpI :
      ‖Complex.exp (φ * Complex.I)‖ = 1 := by
    simpa using Complex.norm_exp_ofReal_mul_I φ
  have hAction :
      -(pathAction (pathFromRotation rot)) / 2 = - rateAction rot := by
    have h := measurement_bridge_C_eq_2A rot
    calc
      -(pathAction (pathFromRotation rot)) / 2
          = -(2 * rateAction rot) / 2 := by simpa [h]
      _ = - rateAction rot := by ring
  calc
    ‖Complex.exp (-(pathAction (pathFromRotation rot)) / 2)
        * Complex.exp (φ * Complex.I)‖
        = ‖Complex.exp (-(pathAction (pathFromRotation rot)) / 2)‖ *
          ‖Complex.exp (φ * Complex.I)‖ := by simpa using norm_mul _ _
    _ = Real.exp (-(pathAction (pathFromRotation rot)) / 2) * 1 := by
        simpa [hExpReal, hExpI]
    _ = Real.exp (- rateAction rot) := by
        simpa [hAction]

What this page does not claim

This module does not define the Born rule from scratch; it assumes the framework's cost function and derives the probability from it. The theorem applies to two-branch rotations only, not to all possible recognition paths. The result does not assign a numerical value to any physical constant.

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: