Foundation Dalembert Full Unconditional Washburn Full Unconditional

The unconditional result

The ledger, a discrete record of events, assigns a cost to each recognition. The question is whether that cost is forced or chosen. The declaration washburn_full_unconditional answers: forced, and without assuming anything about the combining rule.

Classically, this is a d'Alembert equation. In 1750, Jean le Rond d'Alembert studied functions satisfying H(t+u) + H(t-u) = 2H(t)H(u). The framework's theorem takes this equation, adds three plain conditions (normalization, symmetry, smoothness) and one calibration condition, and proves the only solution is H(t) = cosh(t).

The full theorem then lifts this to the cost function F. Given F(1) = 0, F(x) = F(1/x), F twice continuously differentiable, and a calibration condition, the multiplicative consistency equation F(xy) + F(x/y) = P(F(x), F(y)) forces both F and P. The unique F is J(x) = (x + 1/x)/2 - 1, and the unique P is P(u,v) = 2uv + 2u + 2v. The declaration proves this with no assumption on P beyond its existence.

In Recognition Science, this is the strongest form of inevitability. Earlier versions assumed P was polynomial, or assumed F was already J. This version assumes neither. The proof shows P must be symmetric, P(u,0) = 2u, and the functional equation forces an ODE whose uniqueness gives cosh, hence J.

What this does not claim: it does not claim the physical universe uses this ledger, nor that the calibration condition is physically realized. It establishes a mathematical uniqueness result under stated hypotheses. The step from this theorem to physical constants, such as the golden ratio or three spatial dimensions, is a separate chain of arguments.

/-- Concrete (no-hypothesis-bundle) full unconditional theorem.

This version makes all assumptions explicit and uses:
1) `consistency_forces_RCL_form_is_theorem` for the combiner shape, and
2) `dAlembert_forces_cosh_is_theorem` for the d'Alembert/cosh step. -/
theorem washburn_full_unconditional
    (F : ℝ → ℝ)
    (P : ℝ → ℝ → ℝ)
    (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
    (hUnit : F 1 = 0)
    (hSmooth : ContDiff ℝ 2 F)
    (hCalib : deriv (deriv (G F)) 0 = 1)
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
    (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)
    (hNonTriv : ∃ x : ℝ, 0 < x ∧ F x ≠ 0)
    (hCont : ContinuousOn F (Set.Ioi 0))
    (hP11 : P 1 1 = 6) :
    (∀ 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
  refine full_inevitability_explicit F P hSymm hUnit hSmooth hCalib hCons ?_ ?_
  · exact consistency_forces_RCL_form_is_theorem F P hSymm hUnit hSmooth
      hCons hPoly hSymP hNonTriv hCont hP11
  · exact dAlembert_forces_cosh_is_theorem

/-- Concrete (no-hypothesis-bundle) full unconditional theorem.

This version makes all assumptions explicit and uses:
1) `consistency_forces_RCL_form_is_theorem` for the combiner shape, and
2) `dAlembert_forces_cosh_is_theorem` for the d'Alembert/cosh step. -/
theorem washburn_full_unconditional
    (F : ℝ → ℝ)
    (P : ℝ → ℝ → ℝ)
    (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
    (hUnit : F 1 = 0)
    (hSmooth : ContDiff ℝ 2 F)
    (hCalib : deriv (deriv (G F)) 0 = 1)
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
    (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)
    (hNonTriv : ∃ x : ℝ, 0 < x ∧ F x ≠ 0)
    (hCont : ContinuousOn F (Set.Ioi 0))
    (hP11 : P 1 1 = 6) :
    (∀ 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
  refine full_inevitability_explicit F P hSymm hUnit hSmooth hCalib hCons ?_ ?_
  · exact consistency_forces_RCL_form_is_theorem F P hSymm hUnit hSmooth
      hCons hPoly hSymP hNonTriv hCont hP11
  · exact dAlembert_forces_cosh_is_theorem

/-- `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 claim the physical universe implements this ledger. It does not claim the calibration condition is physically realized. It does not claim the step from this theorem to physical constants is proved in this declaration.

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: