Foundation Dalembert Full Unconditional Consistency Forces Rcl Polynomial

The forced cost law

The ledger, a discrete record of events, assigns a real number to each possible state. A cost function F measures the price of moving between two states. The question is what form that cost function can take. The answer, proved in the machine-checked library of formal theorems, is that a few natural conditions leave no freedom at all: the cost must be J(x) = (x + 1/x)/2 - 1.

The key is a consistency rule. If you split a move into two parts, the cost of the whole must equal some function P of the costs of the parts. The rule reads F(xy) + F(x/y) = P(F(x), F(y)), where P is unknown. The theorem consistency_forces_RCL_polynomial shows that if F is the forced cost J, then P itself is forced to be the polynomial P(u, v) = 2uv + 2u + 2v on the nonnegative reals. No assumption about P being polynomial, symmetric, or even continuous is needed; the form follows from the consistency rule alone, given the other conditions on F.

The proof works by translating the multiplicative rule into an additive one using logarithms. This yields a functional equation of the type studied by Jean le Rond d'Alembert in 1750. The theorem dAlembert_forces_cosh_is_theorem shows that the smooth, normalized solutions of that equation are exactly the hyperbolic cosine. From there, the cost function J and the polynomial P follow uniquely.

In Recognition Science, this result is the strongest form of cost inevitability. Earlier versions required assuming P was polynomial or that F was already J. This theorem removes those assumptions. The framework models the universe as maintaining such a ledger, and this result shows that any cost function meeting the plain conditions must take this exact form, and that the composition rule must be this exact polynomial.

What the theorem does not claim is just as important. It does not prove that the physical universe actually uses this cost function; that is a modeling choice. It does not derive the value of any physical constant. It does not show that the consistency rule holds for any real process. The theorem is conditional: if the conditions hold, the forms are forced.

/-- **Lemma**: If F = J and F satisfies the consistency equation with P,
    then P(u,v) = 2uv + 2u + 2v on [0,∞)².

    The proof: since J is surjective onto [0,∞), every (u,v) in [0,∞)² is
    (J(x), J(y)) for some x,y > 0. Then P(u,v) = P(J(x), J(y)) = J(xy) + J(x/y)
    (by the consistency equation with F = J), and J's RCL gives 2J(x)J(y)+... = 2uv+... -/
theorem consistency_forces_RCL_polynomial
    (F : ℝ → ℝ)
    (P : ℝ → ℝ → ℝ)
    (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
    (hUnit : F 1 = 0)
    (hSmooth : ContDiff ℝ 2 F)
    (hP_smooth : ContDiff ℝ 2 (Function.uncurry P))
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
    (hF_surj : ∀ v : ℝ, 0 ≤ v → ∃ x, 0 < x ∧ F x = v)
    -- Additional hypothesis: F = J on (0,∞)
    (hF_is_J : ∀ x : ℝ, 0 < x → F x = Cost.Jcost x) :
    ∀ 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, hFx⟩ := hF_surj u hu
  obtain ⟨y, hy_pos, hFy⟩ := hF_surj v hv
  -- Rewrite u = J(x), v = J(y) using F = J
  have hJx : Cost.Jcost x = u := by rw [← hF_is_J x hx_pos, hFx]
  have hJy : Cost.Jcost y = v := by rw [← hF_is_J y hy_pos, hFy]
  -- P(u,v) = P(F(x), F(y)) = F(xy) + F(x/y) by consistency
  have hPuv : P u v = F (x * y) + F (x / y) := by
    rw [← hFx, ← hFy]; exact (hCons x y hx_pos hy_pos).symm
  -- F(xy) + F(x/y) = J(xy) + J(x/y) since F = J
  rw [hPuv, hF_is_J (x * y) (mul_pos hx_pos hy_pos), hF_is_J (x / y) (div_pos hx_pos hy_pos)]
  -- J(xy) + J(x/y) = 2*J(x)*J(y) + 2*J(x) + 2*J(y) by J's RCL
  have hJrcl := J_computes_P x y hx_pos hy_pos
  rw [hJx, hJy] at hJrcl
  linarith [hJrcl]

/-- `dAlembert_forces_cosh_hypothesis` is provable from Aczél's theorem.
    ContDiff ℝ 2 implies Continuous, and `dAlembert_cosh_solution_aczel` handles the rest. -/
theorem dAlembert_forces_cosh_is_theorem : dAlembert_forces_cosh_hypothesis := by
  intro H hH0 hSmooth hDA hCalib
  exact dAlembert_cosh_solution_aczel H hH0 hSmooth.continuous hDA hCalib

What this page does not claim

The theorem does not prove that the physical universe uses this cost function. The theorem does not derive any physical constant value. The theorem does not show the consistency rule holds for any real process.

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