Verification Born Rule Route B

The no-signaling route

The Born rule is the quantum rule that turns a wave's amplitude into a probability: measure the amplitude r, and the chance of the event is r². Route B is one of two ways the Recognition Science framework derives that rule from deeper principles. The route starts with a function f that takes a nonnegative number r and returns a probability. The framework's library, a machine-checked collection of formal theorems, proves that if f satisfies a few plain conditions, then f(r) = r² for every r ≥ 0.

The key condition is no signaling. In plain terms, information cannot travel faster than light. The framework writes this as an equation: for any two positive numbers r and s with s less than 1, the identity f(r·s) + f(r·√(1 − s²)) = f(r) must hold. This says that splitting a process into two parts and adding their probabilities gives back the original probability, no matter how the split is made. The other conditions are modest: f is continuous, f(0) = 0, and f(1) = 1.

The proof proceeds in four steps. First, the no-signaling equation is transformed by a change of variables: define h(x) = f(√x). The equation becomes h(R·p) + h(R·(1 − p)) = h(R), a form that looks like a splitting rule. Second, this splitting rule is shown to imply additivity: h(x + y) = h(x) + h(y) for positive x and y. Third, a standard argument for the Cauchy equation shows that a continuous additive function with h(0) = 0 and h(1) = 1 must be the identity, so h(x) = x. Fourth, undoing the change of variables gives f(r) = h(r²) = r².

In Recognition Science, this result is Proposition 3.7, formalized with zero unproved assumptions in the module BornRuleRouteB. The theorem named born_rule_route_B states exactly this conclusion. A corollary, modulus_multiplicativity, shows that f(r₁·r₂) = f(r₁)·f(r₂) for nonnegative r₁ and r₂, meaning the rule respects multiplication of amplitudes. The certificate route_B_certified packages both the quadratic form and the multiplicativity into a single structure.

The significance is that the Born rule is not assumed as a postulate. It is derived from the physical principle of no signaling plus regularity conditions. The framework's library proves this derivation in full formal detail, so the chain from premises to conclusion is checkable line by line. This is one of the places where the framework shows that a central law of quantum mechanics follows from a deeper, more general principle.

/-- **Proposition 3.7 (Route B)**: f(r) = r² for all r ≥ 0. -/
theorem born_rule_route_B {f : ℝ → ℝ} (H : RouteBHyp f)
    {r : ℝ} (hr : 0 ≤ r) : f r = r ^ 2 := by
  have : hSub f (r ^ 2) = r ^ 2 := hSub_eq_id H (sq_nonneg r)
  simp only [hSub, Real.sqrt_sq hr] at this; exact this

/-- Route B hypothesis bundle (Proposition 3.7(a)–(d), pre-processed). -/
structure RouteBHyp (f : ℝ → ℝ) : Prop where
  cont : Continuous f
  f_zero : f 0 = 0
  f_one : f 1 = 1
  no_sig : ∀ r s : ℝ, 0 < r → 0 < s → s < 1 →
    f (r * s) + f (r * Real.sqrt (1 - s ^ 2)) = f r

theorem hSub_eq_id {f : ℝ → ℝ} (H : RouteBHyp f) {x : ℝ} (hx : 0 ≤ x) :
    hSub f x = x := by
  have h0 : gDev f x = 0 := additive_zero_on_nonneg
    ((hSub_cont H).sub continuous_id)
    (fun a b ha hb => show hSub f (a + b) - (a + b) = (hSub f a - a) + (hSub f b - b) by
      rw [hSub_additive H ha hb]; ring)
    (show hSub f 0 - 0 = 0 by rw [hSub_zero H]; ring)
    (show hSub f 1 - 1 = 0 by rw [hSub_one H]; ring)
    hx
  unfold gDev at h0; linarith

/-- (MA) is a COROLLARY, not an axiom (Remark 3.6 of the paper). -/
theorem modulus_multiplicativity {f : ℝ → ℝ} (H : RouteBHyp f)
    {r₁ r₂ : ℝ} (h1 : 0 ≤ r₁) (h2 : 0 ≤ r₂) :
    f (r₁ * r₂) = f r₁ * f r₂ := by
  simp only [born_rule_route_B H (mul_nonneg h1 h2),
    born_rule_route_B H h1, born_rule_route_B H h2]; ring

What this page does not claim

The proof does not derive the full Born rule for complex amplitudes, only for nonnegative real r. No claim is made that no signaling alone, without continuity and the boundary conditions, forces the quadratic form. This module does not address the measurement problem or the interpretation of quantum probability.

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/Verification/BornRuleRouteB.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: