Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcmonotone Dalembert
ARTICLE 3 claims 3 theorems
Foundation Primitive Recognition Calculus Prcmonotone Dalembert
A classical functional equation gets a new proof that uses order instead of continuity, shrinking the assumptions behind a core cost function.
A regularity substitute
The d'Alembert equation, H(s+t) + H(s−t) = 2 H(s) H(t), is a classical functional equation whose solutions include hyperbolic cosine and cosine. It appears in physics wherever waves or oscillations are studied. A standard theorem says that if a solution is continuous, it must be a cosine or a hyperbolic cosine. The module PRCMonotoneDAlembert proves a sharper version: continuity can be replaced by the weaker, purely order-theoretic assumption of monotonicity, meaning the function never decreases as its input grows.
The classical proof of the d'Alembert classification relies on continuity, an analytic property that presupposes the real number continuum. The framework's central cost function, J(x) = (x + 1/x)/2 − 1, was originally derived using this analytic input. The new module asks whether that assumption can be dropped. It answers yes. A monotone additive function of a real variable is forced to be linear, f(x) = f(1)·x, a theorem proved using only the density of rational numbers in an Archimedean ordered field, never the least-upper-bound axiom. This single result powers the rest of the module.
From there, the module builds the full structure. A monotone solution of the d'Alembert equation, normalized so H(0) = 1, is shown to satisfy the hyperbolic cosine duplication formula, to stay above 1, and to obey the addition formula for cosh. The sign ambiguity that continuity used to resolve is pinned down by order alone. The final theorem, dAlembert_cosh_of_monotone, states that any even, normalized, monotone d'Alembert solution is exactly H(t) = cosh(c·t) for some real constant c.
In Recognition Science, this result has a direct payoff. The cost function F, which measures the price of a recognition event, satisfies the composition law. Its log transform, H(t) = F(e^t) + 1, then obeys the d'Alembert equation. The module proves that if this transform is monotone, the cost form is forced to be cosh, and the calibration condition c² = 1 selects the unique cost J. The theorem jcost_forced_by_order states this plainly: a reciprocal-symmetric, normalized, composition-law cost whose log transform is nondecreasing and which meets the unit calibration equals J on the positives. Continuity is never invoked, and no smoothness package is required.
The consequence is that the framework's arbitrary content drops from two nested posits to one. The continuum is no longer needed to force the cost form; monotonicity, an order property available on any ordered field, does all the work. The single residual constant c is the unit of scale. This is the positive resolution of a sharper target, and it makes the cost derivation available on any Archimedean ordered field, not just the real numbers.
THEOREM monotone_additive_isLinear · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
/-- **§9 regularity-substitute brick (completeness-free): a monotone additive
real function is linear.**
The classical J-uniqueness theorem (`law_of_logic_forces_jcost`) uses
`ContinuousOn`, an analytic hypothesis that presupposes the continuum. The §9
question asked whether that analytic input can be replaced by a purely
order-theoretic one available on any Archimedean ordered field *without*
completeness. That question is now CLOSED in the positive direction: the
completeness-free cost forcing is assembled below as `dAlembert_cosh_of_monotone`
(even, normalized, monotone d'Alembert solution is `cosh ∘ linear`) and
`composition_law_monotone_forces_costLambda` (the real cost hypotheses plus
`MonotoneOn` force the scale family), with faithfulness `costLambda_injOn_pos`.
This theorem is the load-bearing regularity brick those results consume: a
`Monotone` solution of Cauchy's additive equation `f (x+y) = f x + f y` is forced
to be linear, `f x = f 1 · x`. The proof uses only the density of `ℚ` in an
Archimedean field (`exists_rat_btwn`), never the least-upper-bound axiom. So
monotonicity is a genuine completeness-free substitute for continuity at the
additive layer that the d'Alembert reduction of the RCL lands on (set `g = F+1`,
`h(t) = g(e^t)`, then `h(s+t)+h(s−t) = 2 h(s) h(t)` with even `h` of the form
`cosh ∘ (additive)`; a monotone such `h` forces the inner additive map linear).
With the assembly complete, the continuum posit dissolves for the cost form:
the framework's arbitrary content on the cost side drops to one unit of scale. -/
theorem monotone_additive_isLinear {f : ℝ → ℝ}
(hadd : ∀ x y, f (x + y) = f x + f y) (hmono : Monotone f) :
∀ x, f x = f 1 * x := by
have hf0 : f 0 = 0 := by
have h := hadd 0 0
rw [add_zero] at h
linarith
let F : ℝ →+ ℝ := AddMonoidHom.mk' f (fun a b => hadd a b)
have hFcoe : ∀ y, F y = f y := fun _ => rfl
have hFq : ∀ q : ℚ, f (q : ℝ) = f 1 * (q : ℝ) := by
intro q
have h := map_ratCast_smul F ℝ ℝ q (1 : ℝ)
simp only [smul_eq_mul, mul_one, hFcoe] at h
rw [h]; ring
intro x
set c := f 1 with hc_def
have hc : 0 ≤ c := by
have hmle : f 0 ≤ f 1 := hmono (by norm_num)
rw [hf0] at hmle; exact hmle
rcases eq_or_lt_of_le hc with hc0 | hcpos
· -- c = 0: f is identically 0, and 0 = c * x
have hub : f x ≤ 0 := by
obtain ⟨r, hxr, -⟩ := exists_rat_btwn (lt_add_one x)
have hmr := hmono hxr.le
rw [hFq r, ← hc0, zero_mul] at hmr
exact hmr
have hlb : 0 ≤ f x := by
obtain ⟨q, -, hqx⟩ := exists_rat_btwn (sub_one_lt x)
have hmq := hmono hqx.le
rw [hFq q, ← hc0, zero_mul] at hmq
exact hmq
rw [← hc0, zero_mul]
linarith
· -- c > 0: Archimedean squeeze pins f x = c * x
refine le_antisymm ?_ ?_
· by_contra hcon
push_neg at hcon
have hxlt : x < f x / c := by
rw [lt_div_iff₀ hcpos]; linarith [mul_comm c x]
obtain ⟨r, hxr, hrlt⟩ := exists_rat_btwn hxlt
have h1 : f x ≤ c * (r : ℝ) := by
have hm := hmono hxr.le; rwa [hFq r] at hm
have h2 : c * (r : ℝ) < f x := by
have := (lt_div_iff₀ hcpos).mp hrlt; linarith [mul_comm (r : ℝ) c]
linarith
· by_contra hcon
push_neg at hcon
have hxlt : f x / c < x := by
rw [div_lt_iff₀ hcpos]; linarith [mul_comm c x]
obtain ⟨q, hqlt, hqx⟩ := exists_rat_btwn hxlt
have h1 : c * (q : ℝ) ≤ f x := by
have hm := hmono hqx.le; rwa [hFq q] at hm
have h2 : f x < c * (q : ℝ) := by
have := (div_lt_iff₀ hcpos).mp hqlt; linarith [mul_comm (q : ℝ) c]
linarith
THEOREM dAlembert_cosh_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
/-- **§9 RESOLVED, POSITIVE: the cosh cost form is forced WITHOUT completeness.**
A solution `H` of the d'Alembert equation that is even, normalized (`H 0 = 1`),
and monotone on `[0,∞)` is `H t = cosh (c · t)` for a single real `c`. The proof
uses no continuity, no smoothness, no Aczél package, and no least-upper-bound
axiom — only field operations, square roots, the order, and Archimedean density
(inside `monotone_additive_isLinear`). It therefore transfers verbatim to any
Archimedean real-closed field.
Consequence for the δ program (the §9 question): the continuum is NOT required to
force the cost form. Monotonicity — an order property present on any ordered
field — does everything continuity was doing. The single residual `c` is exactly
the known unit-of-scale posit. So the framework's arbitrary content drops from
two nested posits (continuum + unit) to one (unit), and the continuum posit for
the cost dissolves. This is the positive resolution of the sharper §9 target. -/
theorem dAlembert_cosh_of_monotone {H : ℝ → ℝ}
(hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1)
(heven : Function.Even H) (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) :
∃ c : ℝ, ∀ t, H t = Real.cosh (c * t) := by
have hφmul : ∀ a b, 0 ≤ a → 0 ≤ b →
(H (a + b) + Real.sqrt ((H (a + b)) ^ 2 - 1))
= (H a + Real.sqrt ((H a) ^ 2 - 1)) * (H b + Real.sqrt ((H b) ^ 2 - 1)) := by
intro a b ha hb
rcases le_total b a with hba | hab
· exact phi_mul_of_monotone hd h0 hmono a b hb hba
· have hp := phi_mul_of_monotone hd h0 hmono b a ha hab
rw [add_comm b a] at hp
rw [hp]; ring
have hφpos : ∀ x, 0 ≤ x → (1 : ℝ) ≤ H x + Real.sqrt ((H x) ^ 2 - 1) := by
intro x hx
have h1 := dAlembert_ge_one_of_monotone h0 hmono x hx
have h2 : 0 ≤ Real.sqrt ((H x) ^ 2 - 1) := Real.sqrt_nonneg _
linarith
have hφmono : MonotoneOn (fun x => Real.log (H x + Real.sqrt ((H x) ^ 2 - 1)))
(Set.Ici (0 : ℝ)) := by
intro x hx y hy hxy
have hx0 := Set.mem_Ici.mp hx
have hy0 := Set.mem_Ici.mp hy
have hHxy : H x ≤ H y := hmono hx hy hxy
have hge1x := dAlembert_ge_one_of_monotone h0 hmono x hx0
have hsqle : Real.sqrt ((H x) ^ 2 - 1) ≤ Real.sqrt ((H y) ^ 2 - 1) :=
Real.sqrt_le_sqrt (by nlinarith [hHxy, hge1x])
show Real.log (H x + Real.sqrt ((H x) ^ 2 - 1))
≤ Real.log (H y + Real.sqrt ((H y) ^ 2 - 1))
exact Real.log_le_log (by linarith [hφpos x hx0]) (by linarith)
have hγadd : ∀ a b, 0 ≤ a → 0 ≤ b →
Real.log (H (a + b) + Real.sqrt ((H (a + b)) ^ 2 - 1))
= Real.log (H a + Real.sqrt ((H a) ^ 2 - 1))
+ Real.log (H b + Real.sqrt ((H b) ^ 2 - 1)) := by
intro a b ha hb
rw [hφmul a b ha hb]
exact Real.log_mul (by have := hφpos a ha; linarith) (by have := hφpos b hb; linarith)
have hγ0 : Real.log (H 0 + Real.sqrt ((H 0) ^ 2 - 1)) = 0 := by
rw [h0]
have h01 : (1 : ℝ) ^ 2 - 1 = 0 := by norm_num
rw [h01, Real.sqrt_zero, add_zero, Real.log_one]
have hlin := monotone_additive_nonneg_isLinear
(f := fun x => Real.log (H x + Real.sqrt ((H x) ^ 2 - 1))) hγadd hφmono hγ0
refine ⟨Real.log (H 1 + Real.sqrt ((H 1) ^ 2 - 1)), ?_⟩
set c := Real.log (H 1 + Real.sqrt ((H 1) ^ 2 - 1)) with hc
have hcosh_nonneg : ∀ t, 0 ≤ t → H t = Real.cosh (c * t) := by
intro t ht
have hge1t := dAlembert_ge_one_of_monotone h0 hmono t ht
have hSt : 0 ≤ (H t) ^ 2 - 1 := by nlinarith [hge1t]
have hφtpos : 0 < H t + Real.sqrt ((H t) ^ 2 - 1) := by linarith [hφpos t ht]
have hloglin : Real.log (H t + Real.sqrt ((H t) ^ 2 - 1)) = c * t := hlin t ht
have hφexp : H t + Real.sqrt ((H t) ^ 2 - 1) = Real.exp (c * t) := by
rw [← hloglin]; exact (Real.exp_log hφtpos).symm
have hsqsq : (Real.sqrt ((H t) ^ 2 - 1)) ^ 2 = (H t) ^ 2 - 1 := Real.sq_sqrt hSt
have hprod :
(H t + Real.sqrt ((H t) ^ 2 - 1)) * (H t - Real.sqrt ((H t) ^ 2 - 1)) = 1 := by
have hexp :
(H t + Real.sqrt ((H t) ^ 2 - 1)) * (H t - Real.sqrt ((H t) ^ 2 - 1))
= (H t) ^ 2 - (Real.sqrt ((H t) ^ 2 - 1)) ^ 2 := by ring
rw [hexp, hsqsq]; ring
have hinv : H t - Real.sqrt ((H t) ^ 2 - 1) = (H t + Real.sqrt ((H t) ^ 2 - 1))⁻¹ :=
eq_inv_of_mul_eq_one_right hprod
have hHt : H t = (Real.exp (c * t) + (Real.exp (c * t))⁻¹) / 2 := by
have e : H t
= ((H t + Real.sqrt ((H t) ^ 2 - 1)) + (H t - Real.sqrt ((H t) ^ 2 - 1))) / 2 := by
ring
rw [e, hinv, hφexp]
rw [hHt, Real.cosh_eq, Real.exp_neg]
intro t
rcases le_or_lt 0 t with ht | ht
· exact hcosh_nonneg t ht
· have hnt : H t = H (-t) := (heven t).symm
rw [hnt, hcosh_nonneg (-t) (by linarith), show c * (-t) = -(c * t) by ring, Real.cosh_neg]
THEOREM jcost_forced_by_order · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
/-- **The recognition cost is forced by order.**
A reciprocal-symmetric, normalized, composition-law cost whose log transform is
nondecreasing on `[0, ∞)` and which meets the unit calibration equals
`Cost.Jcost` on the positives. Continuity is never invoked, no smoothness
package is required, and nothing in the proof needs a least upper bound, so the
statement is available on any Archimedean ordered field.
This is the theorem the forcing chain's T5 rung now cites. The older route
through the scale family, `law_of_logic_forces_jcost_monotone`, proves the same
thing and stays where it is; it just cannot be named from below the completion
layer, which is what this version fixes. -/
theorem jcost_forced_by_order (F : ℝ → ℝ)
(hRecip : Cost.FunctionalEquation.IsReciprocalCost F)
(hNorm : Cost.FunctionalEquation.IsNormalized F)
(hComp : Cost.FunctionalEquation.SatisfiesCompositionLaw F)
(hMono : MonotoneOn (Cost.FunctionalEquation.H F) (Set.Ici (0 : ℝ)))
(hCalib : Cost.FunctionalEquation.IsCalibrated F) :
∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
obtain ⟨c, hc⟩ :=
composition_law_monotone_forces_cosh_family F hRecip hNorm hComp hMono
have hGpt : ∀ t : ℝ,
Cost.FunctionalEquation.G F t = Real.cosh (c * t) - 1 := by
intro t
have ht := hc t
simp only [Cost.FunctionalEquation.H] at ht
linarith
have hG : Cost.FunctionalEquation.G F = fun t : ℝ => Real.cosh (c * t) - 1 :=
funext hGpt
have hc2 : c ^ 2 = 1 := by
have hcal : deriv (deriv (Cost.FunctionalEquation.G F)) 0 = 1 := hCalib
rw [hG, cosh_scale_curvature c] at hcal
exact hcal
-- `c² = 1` leaves the sign free, and `cosh` cannot see it.
have hcosh_eq : ∀ t : ℝ, Real.cosh (c * t) = Real.cosh t := by
intro t
have hfac : (c - 1) * (c + 1) = 0 := by nlinarith [hc2]
rcases mul_eq_zero.mp hfac with h | h
· rw [show c = 1 by linarith, one_mul]
· rw [show c = -1 by linarith, show (-1 : ℝ) * t = -t by ring, Real.cosh_neg]
intro x hx
have hgx : Cost.FunctionalEquation.G F (Real.log x) = F x := by
simp only [Cost.FunctionalEquation.G]
rw [Real.exp_log hx]
have hval : F x = Real.cosh (Real.log x) - 1 := by
have h1 := hGpt (Real.log x)
rw [hgx, hcosh_eq] at h1
exact h1
rw [hval, Cost.Jcost, Real.cosh_eq, Real.exp_log hx, Real.exp_neg, Real.exp_log hx]
What this page does not claim
The module does not prove the original continuity-based theorem; it proves a new, order-based version. The module does not derive the value of the constant c; it remains a unit-of-scale posit. The module does not apply to non-Archimedean ordered fields, where the density argument fails.
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/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.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:
- What is the precise statement of the d'Alembert equation and its classical solution families?
- How does the density of rational numbers in an Archimedean field replace the least-upper-bound axiom in the proof of linearity?
- What is the composition law for the cost function and how does it lead to the d'Alembert equation?
- What does the calibration condition c² = 1 mean physically in the framework?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM monotone_additive_isLinear · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
/-- **§9 regularity-substitute brick (completeness-free): a monotone additive real function is linear.** The classical J-uniqueness theorem (`law_of_logic_forces_jcost`) uses `ContinuousOn`, an analytic hypothesis that presupposes the continuum. The §9 question asked whether that analytic input can be replaced by a purely order-theoretic one available on any Archimedean ordered field *without* completeness. That question is now CLOSED in the positive direction: the completeness-free cost forcing is assembled below as `dAlembert_cosh_of_monotone` (even, normalized, monotone d'Alembert solution is `cosh ∘ linear`) and `composition_law_monotone_forces_costLambda` (the real cost hypotheses plus `MonotoneOn` force the scale family), with faithfulness `costLambda_injOn_pos`. This theorem is the load-bearing regularity brick those results consume: a `Monotone` solution of Cauchy's additive equation `f (x+y) = f x + f y` is forced to be linear, `f x = f 1 · x`. The proof uses only the density of `ℚ` in an Archimedean field (`exists_rat_btwn`), never the least-upper-bound axiom. So monotonicity is a genuine completeness-free substitute for continuity at the additive layer that the d'Alembert reduction of the RCL lands on (set `g = F+1`, `h(t) = g(e^t)`, then `h(s+t)+h(s−t) = 2 h(s) h(t)` with even `h` of the form `cosh ∘ (additive)`; a monotone such `h` forces the inner additive map linear). With the assembly complete, the continuum posit dissolves for the cost form: the framework's arbitrary content on the cost side drops to one unit of scale. -/ theorem monotone_additive_isLinear {f : ℝ → ℝ} (hadd : ∀ x y, f (x + y) = f x + f y) (hmono : Monotone f) : ∀ x, f x = f 1 * x := by have hf0 : f 0 = 0 := by have h := hadd 0 0 rw [add_zero] at h linarith let F : ℝ →+ ℝ := AddMonoidHom.mk' f (fun a b => hadd a b) have hFcoe : ∀ y, F y = f y := fun _ => rfl have hFq : ∀ q : ℚ, f (q : ℝ) = f 1 * (q : ℝ) := by intro q have h := map_ratCast_smul F ℝ ℝ q (1 : ℝ) simp only [smul_eq_mul, mul_one, hFcoe] at h rw [h]; ring intro x set c := f 1 with hc_def have hc : 0 ≤ c := by have hmle : f 0 ≤ f 1 := hmono (by norm_num) rw [hf0] at hmle; exact hmle rcases eq_or_lt_of_le hc with hc0 | hcpos · -- c = 0: f is identically 0, and 0 = c * x have hub : f x ≤ 0 := by obtain ⟨r, hxr, -⟩ := exists_rat_btwn (lt_add_one x) have hmr := hmono hxr.le rw [hFq r, ← hc0, zero_mul] at hmr exact hmr have hlb : 0 ≤ f x := by obtain ⟨q, -, hqx⟩ := exists_rat_btwn (sub_one_lt x) have hmq := hmono hqx.le rw [hFq q, ← hc0, zero_mul] at hmq exact hmq rw [← hc0, zero_mul] linarith · -- c > 0: Archimedean squeeze pins f x = c * x refine le_antisymm ?_ ?_ · by_contra hcon push_neg at hcon have hxlt : x < f x / c := by rw [lt_div_iff₀ hcpos]; linarith [mul_comm c x] obtain ⟨r, hxr, hrlt⟩ := exists_rat_btwn hxlt have h1 : f x ≤ c * (r : ℝ) := by have hm := hmono hxr.le; rwa [hFq r] at hm have h2 : c * (r : ℝ) < f x := by have := (lt_div_iff₀ hcpos).mp hrlt; linarith [mul_comm (r : ℝ) c] linarith · by_contra hcon push_neg at hcon have hxlt : f x / c < x := by rw [div_lt_iff₀ hcpos]; linarith [mul_comm c x] obtain ⟨q, hqlt, hqx⟩ := exists_rat_btwn hxlt have h1 : c * (q : ℝ) ≤ f x := by have hm := hmono hqx.le; rwa [hFq q] at hm have h2 : f x < c * (q : ℝ) := by have := (div_lt_iff₀ hcpos).mp hqlt; linarith [mul_comm (q : ℝ) c] linarithA monotone additive function of a real variable is forced to be linear, f(x) = f(1)·x. monotone_additive_isLinear · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.leanTHEOREM dAlembert_cosh_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
/-- **§9 RESOLVED, POSITIVE: the cosh cost form is forced WITHOUT completeness.** A solution `H` of the d'Alembert equation that is even, normalized (`H 0 = 1`), and monotone on `[0,∞)` is `H t = cosh (c · t)` for a single real `c`. The proof uses no continuity, no smoothness, no Aczél package, and no least-upper-bound axiom — only field operations, square roots, the order, and Archimedean density (inside `monotone_additive_isLinear`). It therefore transfers verbatim to any Archimedean real-closed field. Consequence for the δ program (the §9 question): the continuum is NOT required to force the cost form. Monotonicity — an order property present on any ordered field — does everything continuity was doing. The single residual `c` is exactly the known unit-of-scale posit. So the framework's arbitrary content drops from two nested posits (continuum + unit) to one (unit), and the continuum posit for the cost dissolves. This is the positive resolution of the sharper §9 target. -/ theorem dAlembert_cosh_of_monotone {H : ℝ → ℝ} (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1) (heven : Function.Even H) (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) : ∃ c : ℝ, ∀ t, H t = Real.cosh (c * t) := by have hφmul : ∀ a b, 0 ≤ a → 0 ≤ b → (H (a + b) + Real.sqrt ((H (a + b)) ^ 2 - 1)) = (H a + Real.sqrt ((H a) ^ 2 - 1)) * (H b + Real.sqrt ((H b) ^ 2 - 1)) := by intro a b ha hb rcases le_total b a with hba | hab · exact phi_mul_of_monotone hd h0 hmono a b hb hba · have hp := phi_mul_of_monotone hd h0 hmono b a ha hab rw [add_comm b a] at hp rw [hp]; ring have hφpos : ∀ x, 0 ≤ x → (1 : ℝ) ≤ H x + Real.sqrt ((H x) ^ 2 - 1) := by intro x hx have h1 := dAlembert_ge_one_of_monotone h0 hmono x hx have h2 : 0 ≤ Real.sqrt ((H x) ^ 2 - 1) := Real.sqrt_nonneg _ linarith have hφmono : MonotoneOn (fun x => Real.log (H x + Real.sqrt ((H x) ^ 2 - 1))) (Set.Ici (0 : ℝ)) := by intro x hx y hy hxy have hx0 := Set.mem_Ici.mp hx have hy0 := Set.mem_Ici.mp hy have hHxy : H x ≤ H y := hmono hx hy hxy have hge1x := dAlembert_ge_one_of_monotone h0 hmono x hx0 have hsqle : Real.sqrt ((H x) ^ 2 - 1) ≤ Real.sqrt ((H y) ^ 2 - 1) := Real.sqrt_le_sqrt (by nlinarith [hHxy, hge1x]) show Real.log (H x + Real.sqrt ((H x) ^ 2 - 1)) ≤ Real.log (H y + Real.sqrt ((H y) ^ 2 - 1)) exact Real.log_le_log (by linarith [hφpos x hx0]) (by linarith) have hγadd : ∀ a b, 0 ≤ a → 0 ≤ b → Real.log (H (a + b) + Real.sqrt ((H (a + b)) ^ 2 - 1)) = Real.log (H a + Real.sqrt ((H a) ^ 2 - 1)) + Real.log (H b + Real.sqrt ((H b) ^ 2 - 1)) := by intro a b ha hb rw [hφmul a b ha hb] exact Real.log_mul (by have := hφpos a ha; linarith) (by have := hφpos b hb; linarith) have hγ0 : Real.log (H 0 + Real.sqrt ((H 0) ^ 2 - 1)) = 0 := by rw [h0] have h01 : (1 : ℝ) ^ 2 - 1 = 0 := by norm_num rw [h01, Real.sqrt_zero, add_zero, Real.log_one] have hlin := monotone_additive_nonneg_isLinear (f := fun x => Real.log (H x + Real.sqrt ((H x) ^ 2 - 1))) hγadd hφmono hγ0 refine ⟨Real.log (H 1 + Real.sqrt ((H 1) ^ 2 - 1)), ?_⟩ set c := Real.log (H 1 + Real.sqrt ((H 1) ^ 2 - 1)) with hc have hcosh_nonneg : ∀ t, 0 ≤ t → H t = Real.cosh (c * t) := by intro t ht have hge1t := dAlembert_ge_one_of_monotone h0 hmono t ht have hSt : 0 ≤ (H t) ^ 2 - 1 := by nlinarith [hge1t] have hφtpos : 0 < H t + Real.sqrt ((H t) ^ 2 - 1) := by linarith [hφpos t ht] have hloglin : Real.log (H t + Real.sqrt ((H t) ^ 2 - 1)) = c * t := hlin t ht have hφexp : H t + Real.sqrt ((H t) ^ 2 - 1) = Real.exp (c * t) := by rw [← hloglin]; exact (Real.exp_log hφtpos).symm have hsqsq : (Real.sqrt ((H t) ^ 2 - 1)) ^ 2 = (H t) ^ 2 - 1 := Real.sq_sqrt hSt have hprod : (H t + Real.sqrt ((H t) ^ 2 - 1)) * (H t - Real.sqrt ((H t) ^ 2 - 1)) = 1 := by have hexp : (H t + Real.sqrt ((H t) ^ 2 - 1)) * (H t - Real.sqrt ((H t) ^ 2 - 1)) = (H t) ^ 2 - (Real.sqrt ((H t) ^ 2 - 1)) ^ 2 := by ring rw [hexp, hsqsq]; ring have hinv : H t - Real.sqrt ((H t) ^ 2 - 1) = (H t + Real.sqrt ((H t) ^ 2 - 1))⁻¹ := eq_inv_of_mul_eq_one_right hprod have hHt : H t = (Real.exp (c * t) + (Real.exp (c * t))⁻¹) / 2 := by have e : H t = ((H t + Real.sqrt ((H t) ^ 2 - 1)) + (H t - Real.sqrt ((H t) ^ 2 - 1))) / 2 := by ring rw [e, hinv, hφexp] rw [hHt, Real.cosh_eq, Real.exp_neg] intro t rcases le_or_lt 0 t with ht | ht · exact hcosh_nonneg t ht · have hnt : H t = H (-t) := (heven t).symm rw [hnt, hcosh_nonneg (-t) (by linarith), show c * (-t) = -(c * t) by ring, Real.cosh_neg]Any even, normalized, monotone d'Alembert solution is exactly H(t) = cosh(c·t) for some real constant c. dAlembert_cosh_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.leanTHEOREM jcost_forced_by_order · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
/-- **The recognition cost is forced by order.** A reciprocal-symmetric, normalized, composition-law cost whose log transform is nondecreasing on `[0, ∞)` and which meets the unit calibration equals `Cost.Jcost` on the positives. Continuity is never invoked, no smoothness package is required, and nothing in the proof needs a least upper bound, so the statement is available on any Archimedean ordered field. This is the theorem the forcing chain's T5 rung now cites. The older route through the scale family, `law_of_logic_forces_jcost_monotone`, proves the same thing and stays where it is; it just cannot be named from below the completion layer, which is what this version fixes. -/ theorem jcost_forced_by_order (F : ℝ → ℝ) (hRecip : Cost.FunctionalEquation.IsReciprocalCost F) (hNorm : Cost.FunctionalEquation.IsNormalized F) (hComp : Cost.FunctionalEquation.SatisfiesCompositionLaw F) (hMono : MonotoneOn (Cost.FunctionalEquation.H F) (Set.Ici (0 : ℝ))) (hCalib : Cost.FunctionalEquation.IsCalibrated F) : ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by obtain ⟨c, hc⟩ := composition_law_monotone_forces_cosh_family F hRecip hNorm hComp hMono have hGpt : ∀ t : ℝ, Cost.FunctionalEquation.G F t = Real.cosh (c * t) - 1 := by intro t have ht := hc t simp only [Cost.FunctionalEquation.H] at ht linarith have hG : Cost.FunctionalEquation.G F = fun t : ℝ => Real.cosh (c * t) - 1 := funext hGpt have hc2 : c ^ 2 = 1 := by have hcal : deriv (deriv (Cost.FunctionalEquation.G F)) 0 = 1 := hCalib rw [hG, cosh_scale_curvature c] at hcal exact hcal -- `c² = 1` leaves the sign free, and `cosh` cannot see it. have hcosh_eq : ∀ t : ℝ, Real.cosh (c * t) = Real.cosh t := by intro t have hfac : (c - 1) * (c + 1) = 0 := by nlinarith [hc2] rcases mul_eq_zero.mp hfac with h | h · rw [show c = 1 by linarith, one_mul] · rw [show c = -1 by linarith, show (-1 : ℝ) * t = -t by ring, Real.cosh_neg] intro x hx have hgx : Cost.FunctionalEquation.G F (Real.log x) = F x := by simp only [Cost.FunctionalEquation.G] rw [Real.exp_log hx] have hval : F x = Real.cosh (Real.log x) - 1 := by have h1 := hGpt (Real.log x) rw [hgx, hcosh_eq] at h1 exact h1 rw [hval, Cost.Jcost, Real.cosh_eq, Real.exp_log hx, Real.exp_neg, Real.exp_log hx]A reciprocal-symmetric, normalized, composition-law cost whose log transform is nondecreasing and which meets the unit calibration equals J on the positives. jcost_forced_by_order · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean