Foundation Dalembert Unconditional P Determined Nonneg

The determined composition law

The declaration P_determined_nonneg is a theorem in the machine-checked library of formal theorems that Recognition Science uses to build its framework. It concerns a function called the cost, which in this framework is a measure of the price reality pays to register a recognition event, a discrete record of an occurrence. The theorem states that if a certain consistency equation holds for all positive numbers, then the function P that combines two costs must take a specific algebraic form: P(u, v) = 2uv + 2u + 2v, for all nonnegative values u and v.

To understand what this means, consider the equation that defines the consistency condition: F(xy) + F(x/y) = P(F(x), F(y)), where F is the cost function. This equation says that the cost of a product and a quotient can be expressed in terms of the costs of the individual factors. The theorem proves that any function P satisfying this equation with the known cost function J(x) = (x + 1/x)/2 - 1 must be exactly the polynomial 2uv + 2u + 2v. The proof works by showing that the cost function J maps positive numbers onto all nonnegative numbers, so every pair of nonnegative costs corresponds to some pair of positive inputs.

The importance of this result is that it removes a potential loophole. Earlier versions of the framework assumed P was a polynomial, which critics said limited the validity. This theorem makes no such assumption. It only requires that F exists and satisfies basic properties like symmetry and normalization. From those, P is computed, not chosen. The theorem P_uniqueness goes further: it shows that any two functions satisfying the consistency equation with J must agree on all nonnegative inputs, ruling out all alternative forms, polynomial or not.

In Recognition Science, this result is part of a chain that forces the golden ratio, an eight-tick cycle, and three spatial dimensions. But the theorem itself does not claim to derive those consequences. It only establishes the form of the composition law on the first quadrant. It does not say anything about negative costs, nor does it prove that the cost function J is the only possible function satisfying the basic properties; that is a separate theorem. The declaration is a precise, limited result about the algebra of combining costs.

/-- Since J is surjective onto [0, ∞), P is determined on [0, ∞)². -/
theorem P_determined_nonneg (P : ℝ → ℝ → ℝ)
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y →
      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y)) :
    ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2*u*v + 2*u + 2*v := by
  intro u v hu hv
  obtain ⟨x, hx_pos, hx_eq⟩ := J_surjective_nonneg u hu
  obtain ⟨y, hy_pos, hy_eq⟩ := J_surjective_nonneg v hv
  have h := P_determined_on_range P hCons x y hx_pos hy_pos
  rw [hx_eq, hy_eq] at h
  exact h

/-- J : (0, ∞) → [0, ∞) is surjective onto [0, ∞). -/
theorem J_surjective_nonneg :
    ∀ v : ℝ, 0 ≤ v → ∃ x : ℝ, 0 < x ∧ Cost.Jcost x = v := by
  intro v hv
  -- J(x) = (x + 1/x)/2 - 1
  -- J(1) = 0
  -- J(x) → ∞ as x → ∞ or x → 0⁺
  -- J is continuous on (0, ∞)
  -- By IVT, J takes all values in [0, ∞)
  -- For v = 0, take x = 1
  -- For v > 0, solve (x + 1/x)/2 - 1 = v
  --   => x + 1/x = 2v + 2
  --   => x² - (2v + 2)x + 1 = 0
  --   => x = (2v + 2 + √((2v+2)² - 4)) / 2 = v + 1 + √(v² + 2v)
  by_cases hv0 : v = 0
  · use 1
    constructor
    · exact one_pos
    · simp [Cost.Jcost, hv0]
  · -- v > 0 case
    have hv_pos : 0 < v := lt_of_le_of_ne hv (Ne.symm hv0)
    let discriminant := (2*v + 2)^2 - 4
    have h_disc_pos : 0 < discriminant := by
      simp only [discriminant]
      have h1 : (2*v + 2)^2 = 4*v^2 + 8*v + 4 := by ring
      rw [h1]
      have h2 : 4*v^2 + 8*v + 4 - 4 = 4*v^2 + 8*v := by ring
      rw [h2]
      have h3 : 4*v^2 + 8*v = 4*v*(v + 2) := by ring
      rw [h3]
      apply mul_pos
      · linarith
      · linarith
    let x := (2*v + 2 + Real.sqrt discriminant) / 2
    have hx_pos : 0 < x := by
      simp only [x]
      apply div_pos
      · have h1 : 0 < 2*v + 2 := by linarith
        have h2 : 0 ≤ Real.sqrt discriminant := Real.sqrt_nonneg _
        linarith
      · linarith
    use x
    constructor
    · exact hx_pos
    · -- Prove J(x) = v
      simp only [Cost.Jcost, x]
      -- Need to show: ((2v+2+√disc)/2 + 2/(2v+2+√disc))/2 - 1 = v
      -- This is algebraic manipulation
      have hx_ne : x ≠ 0 := hx_pos.ne'
      have h_quad : x^2 - (2*v + 2)*x + 1 = 0 := by
        simp only [x]
        have h_sqrt_sq : Real.sqrt discriminant ^ 2 = discriminant :=
          Real.sq_sqrt (le_of_lt h_disc_pos)
        field_simp
        simp only [discriminant] at h_sqrt_sq ⊢
        ring_nf
        ring_nf at h_sqrt_sq
        linarith
      -- From quadratic: x + 1/x = 2v + 2
      have h_sum : x + x⁻¹ = 2*v + 2 := by
        have h1 : x^2 + 1 = (2*v + 2)*x := by linarith [h_quad]
        field_simp at h1 ⊢
        linarith
      calc (x + x⁻¹) / 2 - 1 = (2*v + 2) / 2 - 1 := by rw [h_sum]
        _ = v + 1 - 1 := by ring
        _ = v := by ring

/-- If any P satisfies the consistency equation with J, it must be the RCL.
    This rules out ALL alternatives, polynomial or not. -/
theorem P_uniqueness (P Q : ℝ → ℝ → ℝ)
    (hP : ∀ x y : ℝ, 0 < x → 0 < y →
      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y))
    (hQ : ∀ x y : ℝ, 0 < x → 0 < y →
      Cost.Jcost (x * y) + Cost.Jcost (x / y) = Q (Cost.Jcost x) (Cost.Jcost y)) :
    ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = Q u v := by
  intro u v hu hv
  have hP' := rcl_unconditional P hP u v hu hv
  have hQ' := rcl_unconditional Q hQ u v hu hv
  rw [hP', hQ']

What this page does not claim

The theorem does not prove that the cost function J is the only possible function satisfying the basic properties. It does not apply to negative costs, only to nonnegative ones. It does not by itself derive the golden ratio or three spatial dimensions.

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/Unconditional.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: