Encyclopedia Foundation Foundation Dalembert Inevitability Bilinear Family Reduction

ARTICLE 3 claims 3 theorems

Foundation Dalembert Inevitability Bilinear Family Reduction

A single equation governs how the cost of a ratio must combine, and the proof shows only one family of such equations can exist.

Verify this page

The forced family

The d'Alembert functional equation is a classical object in mathematics, studied since Jean le Rond d'Alembert's work in the 18th century. It asks for functions that satisfy a particular relation between values at products and quotients. The equation appears in geometry and probability, and its solutions are well understood. The Recognition Science framework, a system that derives physical structure from the cost of recognition events, encounters this equation in a specific way: as the unique form of a consistency condition on a cost function.

In the framework, a cost function (a rule that assigns a nonnegative number to a deviation from unity) must satisfy a multiplicative consistency condition. This condition says that the cost of a product plus the cost of a quotient must equal some polynomial function of the costs of the two inputs. The framework's library of formal theorems proves that this consistency requirement forces the polynomial to belong to a single family: P(u, v) = 2u + 2v + c·u·v, for some constant c. This is the bilinear family, so named because the only nonlinear term is the product u·v. The theorem bilinear_family_reduction then shows that any equation in this family can be transformed, by an affine change of variables, into the standard d'Alembert equation.

The proof proceeds in steps. First, symmetry and normalization of the cost function force the polynomial to satisfy P(0, v) = 2v. Second, symmetry of the cost function forces the polynomial to be symmetric in its arguments. Third, a symmetric quadratic polynomial with that boundary condition must have the form 2u + 2v + k·u·v. The constant k is not determined by consistency alone; it is fixed later by a calibration condition that sets the natural scale. The choice c = 2 recovers the specific equation used in the framework's core cost function.

In Recognition Science, this result matters because it closes a gap in the framework's foundations. The framework's axioms include a composition law for costs; this theorem proves that the law is not an arbitrary assumption but the unique polynomial form consistent with the stated conditions. The framework's library states this as the theorem bilinear_family_forced, which requires continuity of the cost function and non-triviality. The proof relies on classical results in functional equations, particularly the classification of solutions to additive-type equations.

What the theorem does not claim is just as important. It does not determine the constant c; that is left to a separate normalization step. It does not prove that the cost function itself is unique, only that the polynomial combining costs must lie in this family. And it does not assert that the d'Alembert equation is the only functional equation worth studying; it says that within the framework's specific assumptions, this is the only consistent form. The framework's claim is that this family is forced, not that it was chosen.

THEOREM bilinear_family_forced · IndisputableMonolith/Foundation/DAlembert/Inevitability.lean
bilinear_family_forced · IndisputableMonolith/Foundation/DAlembert/Inevitability.lean:275 
/-- **THEOREM: The consistency requirement forces the unique bilinear family.**

Given:
1. F : ℝ₊ → ℝ is a cost functional
2. F is symmetric: F(x) = F(1/x)
3. F is normalized: F(1) = 0
4. F has multiplicative consistency: F(xy) + F(x/y) = P(F(x), F(y)) for some **symmetric quadratic polynomial** P
5. F is non-trivial (not constant 0)

Then:
P(u, v) = 2u + 2v + c*u*v for some constant c.

This means F satisfies the generalized d'Alembert equation.
If we choose the canonical cost normalization c = 2, we recover the RCL. -/
theorem bilinear_family_forced (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
    (hNorm : IsNormalized F)
    (hCons : HasMultiplicativeConsistency F P)
    (hPoly : ∃ (a b c d e f : ℝ), ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2)
    (hSymP : ∀ u v, P u v = P v u) -- Explicit symmetry of P
    (hNonTriv : ∃ x : ℝ, 0 < x ∧ F x ≠ 0)
    (hCont : ContinuousOn F (Set.Ioi 0)) -- Regularity: F is continuous on (0, ∞)
    : ∃ c : ℝ, (∀ u v, P u v = 2*u + 2*v + c*u*v) ∧
               (c = 2 → ∀ u v, P u v = 2*u + 2*v + 2*u*v) := by
  -- Derived reciprocity from symmetry of P
  have hSym : IsSymmetric F := F_symmetric_of_P_symmetric F P hCons hSymP
  -- Step 1: Normalization forces P(0, v) = 2v
  have hP0 : ∀ y : ℝ, 0 < y → P 0 (F y) = 2 * F y :=
    symmetry_and_normalization_constrain_P F P hSym hNorm hCons

  -- Use the polynomial form lemma
  -- We need to satisfy the hypotheses of `polynomial_form_forced`.
  -- `hNorm0`: ∀ v, P 0 v = 2 * v.
  -- We only have `P 0 (F y) = 2 F y`.
  -- However, since P is a polynomial and F is non-trivial (has range with at least 0 and some non-zero value),
  -- we can determine the coefficients.
  -- P(0, v) = a + c*v + f*v^2.
  -- P(0, 0) = a = 2*0 = 0 (from F(1)=0).
  -- P(0, F y) = c*(F y) + f*(F y)^2 = 2*(F y).
  -- This holds for y=1 (0=0) and some y where F y ≠ 0.
  -- If we only have two points, we can't uniquely determine a quadratic.
  -- But wait, `polynomial_form_forced` derived `a=0, c=2, f=0`.
  -- Let's reproduce that logic but being careful about the domain.

  obtain ⟨a, b, c, d, e, f, hP⟩ := hPoly

  -- 1. a = 0
  have ha : a = 0 := by
    have hCons1 := hCons 1 1 one_pos one_pos
    simp only [one_mul, one_div] at hCons1
    -- hCons1 : F 1 + F 1⁻¹ = P (F 1) (F 1)
    -- inv_one : 1⁻¹ = 1
    rw [inv_one, hNorm] at hCons1
    -- hCons1 : 0 + 0 = P 0 0
    simp only [add_zero] at hCons1
    -- hCons1 : 0 = P 0 0
    rw [hP 0 0] at hCons1
    simp at hCons1
    exact hCons1.symm

  -- 2. From hSymP: P(u,v) = P(v,u)
  -- a + bu + cv + duv + eu^2 + fv^2 = a + bv + cu + duv + ev^2 + fu^2
  -- (b-c)u + (c-b)v + (e-f)u^2 + (f-e)v^2 = 0
  -- This implies b=c and e=f.
  have hb_c : b = c := by
    have h1 := hSymP 1 0
    rw [hP 1 0, hP 0 1] at h1
    -- h1 : a + b*1 + c*0 + d*0 + e*1 + f*0 = a + b*0 + c*1 + d*0 + e*0 + f*1
    -- i.e., a + b + e = a + c + f
    -- Using ha: a = 0, we get b + e = c + f
    simp only [ha, mul_zero, mul_one, add_zero, zero_add] at h1
    -- We need another equation to separate b, e, c, f
    have h2 := hSymP 2 0
    rw [hP 2 0, hP 0 2] at h2
    simp only [ha, mul_zero, add_zero, zero_add] at h2
    -- h1: b + e = c + f
    -- h2: 2b + 4e = 2c + 4f
    -- From h2: b + 2e = c + 2f
    -- Subtracting h1: e = f
    -- So b = c
    linarith
  have he_f : e = f := by
    have h1 := hSymP 1 0
    have h2 := hSymP 2 0
    rw [hP 1 0, hP 0 1] at h1
    rw [hP 2 0, hP 0 2] at h2
    simp only [ha, mul_zero, mul_one, add_zero, zero_add] at h1 h2
    linarith

  -- Now P(0, v) = c*v + f*v^2 (using a=0, b=c, e=f).
  -- And P(0, F y) = 2 * F y.
  -- So c*(F y) + f*(F y)^2 = 2*(F y).
  -- (c - 2)*(F y) + f*(F y)^2 = 0.
  -- This must hold for all y > 0.
  -- Since F is non-trivial, there exists y such that F y ≠ 0.
  obtain ⟨y0, hy0_pos, hy0_ne⟩ := hNonTriv
  have hc_2 : c = 2 ∧ f = 0 := by
    -- Let k = F y0 (a nonzero value in the range).
    let k : ℝ := F y0
    have hk_ne : k ≠ 0 := by
      -- hy0_ne : F y0 ≠ 0
      simpa [k] using hy0_ne

    -- The polynomial identity on the range: (c - 2) * F(y) + f * (F(y))^2 = 0.
    have poly_identity : ∀ y : ℝ, 0 < y → (c - 2) * (F y) + f * (F y)^2 = 0 := by
      intro y hy
      have h := hP0 y hy
      rw [hP 0 (F y)] at h
      simp [ha, hb_c, he_f] at h
      linarith

    -- Use IVT to find y1 with F y1 = k/2 (since F(1)=0 and F(y0)=k).
    have hF1 : F 1 = 0 := hNorm
    have hInterval_pos : Set.uIcc 1 y0 ⊆ Set.Ioi 0 := by
      intro x hx
      rcases hx with ⟨hx_lo, _hx_hi⟩
      have hmin_pos : 0 < min 1 y0 := lt_min one_pos hy0_pos
      exact lt_of_lt_of_le hmin_pos hx_lo
    have hContInterval : ContinuousOn F (Set.uIcc 1 y0) :=
      hCont.mono hInterval_pos
    have h1_mem : 1 ∈ Set.uIcc 1 y0 := Set.left_mem_uIcc
    have hy0_mem : y0 ∈ Set.uIcc 1 y0 := Set.right_mem_uIcc
    have hk2_in_image : k / 2 ∈ F '' Set.uIcc 1 y0 := by
      have hPreconn := isPreconnected_uIcc (a := 1) (b := y0)
      by_cases hk : 0 ≤ k
      · -- monotone direction: 0 ≤ k, so k/2 ∈ Icc 0 k
        have hIVT : Set.Icc 0 k ⊆ F '' Set.uIcc 1 y0 := by
          simpa [hF1, k] using hPreconn.intermediate_value h1_mem hy0_mem hContInterval
        have hk2_between : k / 2 ∈ Set.Icc 0 k := by
          constructor <;> linarith
        exact hIVT hk2_between
      · -- reverse direction: k < 0, so k/2 ∈ Icc k 0
        have hk_lt : k < 0 := lt_of_not_ge hk
        have hIVT : Set.Icc k 0 ⊆ F '' Set.uIcc 1 y0 := by
          simpa [hF1, k] using hPreconn.intermediate_value hy0_mem h1_mem hContInterval
        have hk2_between : k / 2 ∈ Set.Icc k 0 := by
          constructor <;> linarith
        exact hIVT hk2_between
    obtain ⟨y1, hy1_mem, hFy1⟩ := hk2_in_image
    have hy1_pos : 0 < y1 := hInterval_pos hy1_mem

    -- Evaluate the polynomial identity at y0 and y1, then solve for c and f.
    have h_y0 : (c - 2) * k + f * k^2 = 0 := by
      have h := poly_identity y0 hy0_pos
      simpa [k] using h
    have h_y1 : (c - 2) * (k / 2) + f * (k / 2)^2 = 0 := by
      have h := poly_identity y1 hy1_pos
      -- rewrite F y1 = k/2
      simpa [hFy1, k] using h

    -- Multiply the y1 equation by 4 to align it with the y0 equation.
    have h_y1_4 : 2 * (c - 2) * k + f * k^2 = 0 := by
      have h' := congrArg (fun z => 4 * z) h_y1
      -- simplify 4*(...) and 4*0
      ring_nf at h'
      -- `ring_nf` chooses its own normal form; bridge to our preferred one.
      have hrew : c * k * 2 - k * 4 + k ^ 2 * f = 2 * (c - 2) * k + f * k ^ 2 := by ring
      -- h' : c*k*2 - k*4 + k^2*f = 0
      calc
        2 * (c - 2) * k + f * k ^ 2
            = c * k * 2 - k * 4 + k ^ 2 * f := by simpa [hrew] using (Eq.symm hrew)
        _ = 0 := h'

    -- Subtract to get (c - 2) * k = 0, hence c = 2 (since k ≠ 0).
    have hk_mul : (c - 2) * k = 0 := by
      linarith [h_y0, h_y1_4]
    have hc : c = 2 := by
      rcases mul_eq_zero.mp hk_mul with hc0 | hk0
      · linarith
      · exact False.elim (hk_ne hk0)

    -- Plug back to get f = 0.
    have hf : f = 0 := by
      have hk2_ne : k^2 ≠ 0 := pow_ne_zero 2 hk_ne
      have hfk2 : f * k^2 = 0 := by
        -- from h_y0 with c=2
        simpa [hc] using h_y0
      rcases mul_eq_zero.mp hfk2 with hf0 | hk20
      · exact hf0
      · exact False.elim (hk2_ne hk20)

    exact ⟨hc, hf⟩

  have hc : c = 2 := hc_2.1
  have hf : f = 0 := hc_2.2
  have hb : b = 2 := by rw [hb_c, hc]
  have he : e = 0 := by rw [he_f, hf]

  -- So P(u, v) = 2u + 2v + d*u*v.
  use d
  constructor
  · intro u v
    rw [hP, ha, hb, hc, he, hf]
    ring
  · intro hd u v
    rw [hP, ha, hb, hc, he, hf, hd]
    ring
THEOREM bilinear_family_reduction · IndisputableMonolith/Foundation/DAlembert/Inevitability.lean
bilinear_family_reduction · IndisputableMonolith/Foundation/DAlembert/Inevitability.lean:198 
/-- Any bilinear consistency equation reduces to the standard d'Alembert equation
    via an affine transformation H(t) = 1 + (c/2)G(t). -/
theorem bilinear_family_reduction (F : ℝ → ℝ) (c : ℝ)
    (_hc : c ≠ 0)
    (h_bilinear : ∀ x y, F (x * y) + F (x / y) = 2 * F x + 2 * F y + c * F x * F y)
    : let G := fun t => F (Real.exp t)
      let H := fun t => 1 + (c/2) * G t
      ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u := by
  intro G H t u
  simp only [H, G]
  -- We need to prove:
  -- (1 + c/2*F(exp(t+u))) + (1 + c/2*F(exp(t-u))) = 2 * (1 + c/2*F(exp t)) * (1 + c/2*F(exp u))
  -- LHS = 2 + c/2 * (F(xy) + F(x/y))  where x=exp t, y=exp u
  -- RHS = 2 * (1 + c/2*Fx + c/2*Fy + c^2/4*Fx*Fy)
  --     = 2 + c*Fx + c*Fy + c^2/2*Fx*Fy
  --
  -- LHS using bilinear:
  -- LHS = 2 + c/2 * (2Fx + 2Fy + c*Fx*Fy)
  --     = 2 + c*Fx + c*Fy + c^2/2*Fx*Fy
  --
  -- LHS = RHS. QED.
  let x := Real.exp t
  let y := Real.exp u
  have h_eq := h_bilinear x y
  -- Transform using exp_add and exp_sub
  have hxy : Real.exp t * Real.exp u = Real.exp (t + u) := (Real.exp_add t u).symm
  have hxy' : Real.exp t / Real.exp u = Real.exp (t - u) := by
    rw [Real.exp_sub]
  -- The goal is: H(t+u) + H(t-u) = 2 * H(t) * H(u)
  -- where H(t) = 1 + (c/2) * F(exp(t))
  -- LHS = (1 + c/2*F(exp(t+u))) + (1 + c/2*F(exp(t-u)))
  --     = 2 + c/2*(F(exp(t+u)) + F(exp(t-u)))
  --     = 2 + c/2*(F(x*y) + F(x/y))
  --     = 2 + c/2*(2Fx + 2Fy + c*Fx*Fy)  [by h_eq]
  --     = 2 + c*Fx + c*Fy + c²/2*Fx*Fy
  -- RHS = 2*(1 + c/2*Fx)*(1 + c/2*Fy)
  --     = 2*(1 + c/2*Fx + c/2*Fy + c²/4*Fx*Fy)
  --     = 2 + c*Fx + c*Fy + c²/2*Fx*Fy
  -- LHS = RHS ✓
  -- The goal involves H and G which are let-bindings
  -- We need to show: H(t+u) + H(t-u) = 2 * H(t) * H(u)
  -- With H(s) = 1 + (c/2) * G(s) = 1 + (c/2) * F(exp(s))
  -- Note: x = exp(t), y = exp(u), so x*y = exp(t+u), x/y = exp(t-u)
  -- h_eq : F(x*y) + F(x/y) = 2Fx + 2Fy + c*Fx*Fy
  -- Rewrite the goal using hxy and hxy'
  have goal_lhs : F (Real.exp (t + u)) = F (x * y) := by rw [hxy]
  have goal_lhs' : F (Real.exp (t - u)) = F (x / y) := by rw [hxy']
  rw [goal_lhs, goal_lhs']
  -- Now the goal is in terms of F(x*y), F(x/y), F(x), F(y)
  -- Use h_eq to substitute F(x*y) + F(x/y)
  -- Actually, we need to prove an algebraic identity
  -- LHS = 1 + c/2*F(xy) + 1 + c/2*F(x/y) = 2 + c/2*(F(xy) + F(x/y))
  -- RHS = 2*(1 + c/2*Fx)*(1 + c/2*Fy)
  --     = 2 + c*Fx + c*Fy + c²/2*Fx*Fy
  -- Using h_eq: F(xy) + F(x/y) = 2Fx + 2Fy + c*Fx*Fy
  -- LHS = 2 + c/2*(2Fx + 2Fy + c*Fx*Fy)
  --     = 2 + c*Fx + c*Fy + c²/2*Fx*Fy
  --     = RHS ✓
  calc 1 + c / 2 * F (x * y) + (1 + c / 2 * F (x / y))
      = 2 + c / 2 * (F (x * y) + F (x / y)) := by ring
    _ = 2 + c / 2 * (2 * F x + 2 * F y + c * F x * F y) := by rw [h_eq]
    _ = 2 * (1 + c / 2 * F x) * (1 + c / 2 * F y) := by ring
THEOREM axiom_bundle_necessary · IndisputableMonolith/Foundation/DAlembert/Inevitability.lean
axiom_bundle_necessary · IndisputableMonolith/Foundation/DAlembert/Inevitability.lean:474 
/-- **COROLLARY: The Recognition Science axiom bundle (A1, A2, A3) is transcendentally necessary.**

- A1 (Normalization): F(1) = 0
  → Definitional for "cost of deviation from unity"

- A2 (RCL): F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)
  → PROVED: The unique polynomial form for multiplicative consistency (up to scale)

- A3 (Calibration): F''(1) = 1
  → Sets the natural scale (removes family degeneracy)

Therefore: The entire axiom bundle is not arbitrary but forced by the structure of comparison. -/
theorem axiom_bundle_necessary :
    -- A1: Normalization is definitional
    (∀ F : ℝ → ℝ, (∀ x : ℝ, 0 < x → F x = Cost.Jcost x) → F 1 = 0) ∧
    -- A2: RCL is the unique polynomial form (proven above)
    (∀ F P, IsNormalized F → HasMultiplicativeConsistency F P →
      (∃ a b c d e f, ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2) →
      (∀ u v, P u v = P v u) → -- Symmetry requirement
      (∃ x, 0 < x ∧ F x ≠ 0) → -- Non-triviality
      ContinuousOn F (Set.Ioi 0) → -- Regularity
      ∃ c, ∀ u v, P u v = 2*u + 2*v + c*u*v) ∧
    -- A3: Calibration pins down the scale (J''(1) = 1)
    (deriv (deriv (fun x => Cost.Jcost x)) 1 = 1) := by
  constructor
  · intro F hF
    have h := hF 1 one_pos
    simp only [Cost.Jcost, inv_one] at h
    linarith
  constructor
  · intro F P hNorm hCons hPoly hSymP hNonTriv hCont
    -- Use bilinear_family_forced and extract the first conjunct
    obtain ⟨c, hc, _⟩ := bilinear_family_forced F P hNorm hCons hPoly hSymP hNonTriv hCont
    exact ⟨c, hc⟩
  · -- Prove J''(1) = 1 (calibration)
    -- J(x) = x/2 + 1/(2x) - 1, so J''(x) = x⁻³, thus J''(1) = 1.
    exact Cost.deriv2_Jcost_one

What this page does not claim

The theorem does not determine the value of the constant c. The theorem does not prove the cost function itself is unique, only the polynomial family. The theorem does not claim the d'Alembert equation is the only functional equation of interest in mathematics.

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/Foundation/DAlembert/Inevitability.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND