Measurement C2 Abridge Amplitude Modulus Bridge

The amplitude bridge

Quantum mechanics describes measurement through complex numbers called amplitudes. The probability of a particular outcome equals the squared magnitude of the amplitude, a rule known as the Born rule. This page concerns a theorem inside the Recognition Science framework that connects that amplitude magnitude to a cost function. The framework models a measurement as a two-branch rotation, a geometric object with a defined rate action A. The theorem, named amplitude_modulus_bridge, states that for any such rotation, the magnitude of the path amplitude equals exp(-A).

In plainer terms, the size of the quantum amplitude is an exponential decay of a cost. The cost is not a free parameter; it is the same unique functional J that the framework derives from five conditions on recognition. The bridge theorem depends on a prior result, measurement_bridge_C_eq_2A, which shows that the recognition action C for the constructed path is exactly twice the rate action A. From C = 2A, the weight bridge follows: the path weight equals exp(-2A), which the framework identifies with the Born probability |α₂|². The amplitude modulus bridge then takes the square root of that weight to get exp(-A).

The theorem is proved in the machine-checked library of formal theorems, meaning the derivation is verified step by step. It establishes a structural identity within the framework: the amplitude magnitude is not an independent quantity but is fixed by the cost. This is a formal result about the framework's own definitions. It does not claim that this is the only way to derive the Born rule, nor does it assert that the framework's model of measurement is the correct physical one. The bridge connects two quantities within the model; it does not by itself prove that the model matches experiment.

What the theorem changes is the status of the amplitude within the framework. Previously, one might have taken amplitude as a primitive. Now it is derived from the cost, which itself is forced by the five conditions. This makes the amplitude magnitude a consequence of the framework's foundational axioms, not an additional assumption. The reader can see that, inside this account, the exponential form of the amplitude is not a choice but a result.

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

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

What this page does not claim

The theorem does not assert that the Born rule is universally true in all interpretations of quantum mechanics. The theorem does not claim that the framework's model of measurement is the correct physical description of nature. The theorem does not derive the value of any physical constant or predict a specific experimental outcome.

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: