Encyclopedia Foundation Foundation Dalembert Unconditional P Determined On Range

ARTICLE 3 claims 3 theorems

Foundation Dalembert Unconditional P Determined On Range

A single equation governs how the cost of two events combines, and a machine-checked proof shows only one rule can satisfy it.

Verify this page

What the consistency law forces

The declaration P_determined_on_range is a theorem in the framework's machine-checked library of formal theorems. It concerns the cost function J(x) = (x + 1/x)/2 - 1, which measures the price of a recognition event. The theorem states that if any two-variable function P satisfies the consistency law J(xy) + J(x/y) = P(J(x), J(y)) for all positive x and y, then P must equal 2uv + 2u + 2v on the range of J. In plain terms: once the cost function is fixed, the rule for combining costs is forced, not chosen.

The proof is direct. It starts from the d'Alembert identity for J, which shows that J(xy) + J(x/y) equals 2J(x)J(y) + 2J(x) + 2J(y). If P also satisfies the consistency law, then P(J(x), J(y)) must equal that same expression. The theorem P_determined_on_range formalizes this step. It does not assume P has any particular form, such as a polynomial. It only assumes P exists and obeys the consistency equation with J. From that single assumption, the value of P on the range of J follows.

The range of J is the set of nonnegative real numbers. A companion theorem, J_surjective_nonneg, proves that J maps the positive reals onto [0, ∞). This surjectivity matters because it extends the result: P is determined not just on the image of J, but on the entire first quadrant. The theorem P_determined_nonneg then states that P(u, v) = 2uv + 2u + 2v for all nonnegative u and v. The full result, rcl_unconditional, packages this as the unconditional inevitability of the consistency law.

What the declaration does not claim is equally precise. It does not assert that the cost function J itself is unique; that is a separate theorem resting on symmetry, normalization, calibration, and smoothness. It does not claim that P is unique for arguments outside the nonnegative quadrant, where J does not reach. And it does not claim that the consistency law holds for arbitrary functions F; it applies specifically when F equals J. The theorem is a statement about P given J, not a statement about all possible cost functions.

THEOREM P_determined_on_range · IndisputableMonolith/Foundation/DAlembert/Unconditional.lean
P_determined_on_range · IndisputableMonolith/Foundation/DAlembert/Unconditional.lean:78 
/-- P is uniquely determined on the range of (J, J). -/
theorem P_determined_on_range (P : ℝ → ℝ → ℝ)
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y →
      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y)) :
    ∀ x y : ℝ, 0 < x → 0 < y →
      P (Cost.Jcost x) (Cost.Jcost y) =
      2 * Cost.Jcost x * Cost.Jcost y + 2 * Cost.Jcost x + 2 * Cost.Jcost y := by
  intro x y hx hy
  rw [← hCons x y hx hy]
  exact J_computes_P x y hx hy
THEOREM J_surjective_nonneg · IndisputableMonolith/Foundation/DAlembert/Unconditional.lean
J_surjective_nonneg · IndisputableMonolith/Foundation/DAlembert/Unconditional.lean:91 
/-- 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
THEOREM P_determined_nonneg · IndisputableMonolith/Foundation/DAlembert/Unconditional.lean
P_determined_nonneg · IndisputableMonolith/Foundation/DAlembert/Unconditional.lean:158 
/-- 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

What this page does not claim

P_determined_on_range does not prove the uniqueness of the cost function J itself. It does not determine P for arguments outside the nonnegative quadrant. It does not apply the consistency law to arbitrary functions F, only to J.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND