Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcmonotone Dalembert Composition Law

ARTICLE 3 claims 3 theorems

Foundation Primitive Recognition Calculus Prcmonotone Dalembert Composition Law

A machine-checked proof shows that a simple monotonicity condition, not continuity, forces the recognition cost into a single family of curves.

Verify this page

The order-only cost theorem

The declaration composition_law_monotone_forces_cosh_family proves a structural fact about functions that describe the cost of recognition, the framework's term for the price reality pays to register an event. The theorem starts with a function F that satisfies three plain conditions: reciprocal symmetry (F(1/x) = F(x)), normalization (F(1) = 0), and a forced composition law that ties the cost of combined events to the costs of the parts. The fourth hypothesis is not continuity, the usual analytic assumption, but a purely order-theoretic one: a certain logarithmic transform of F, written H_F, is monotone, meaning it never decreases as its input grows. Under these four hypotheses, the theorem concludes that H_F must equal cosh(c·t) for some real constant c. In plain words, the cost function's shape is forced into the hyperbolic cosine family, with a single free scale parameter c.

The classical d'Alembert equation, H(s+t) + H(s−t) = 2H(s)H(t), is the engine. The composition law delivers this equation, reciprocal symmetry gives evenness, and normalization sets H(0) = 1. The proof then shows that monotonicity alone, without any continuity or smoothness assumption, pins the sign of the square root that distinguishes the cosh branch from the cosine branch. The cosine solution dips below 1, while monotonicity forces H ≥ 1, isolating the unbounded cosh family. The argument uses only field operations, square roots, the order structure, and the density of rationals in an Archimedean field. It never invokes a least-upper-bound axiom, so the statement transfers verbatim to any Archimedean real-closed field. This is the completeness-free replacement for the older continuity-based route, and it is the load-bearing brick the framework's forcing chain now cites.

What the theorem does not claim is just as important. It does not fix the value of c; that requires a separate calibration step, which identifies c² as the log-coordinate curvature at the unit and sets it to 1, yielding the specific cost function J(x) = (x + 1/x)/2 − 1. The theorem also does not prove that the cost function exists; that non-vacuity is a separate witness showing J itself satisfies the monotonicity hypothesis. And it does not claim that monotonicity is the only possible substitute for continuity, only that it is a sufficient one. The theorem is a structural result about a family of functions, not a derivation of any particular physical constant.

THEOREM composition_law_monotone_forces_cosh_family · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
composition_law_monotone_forces_cosh_family · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean:455 
/-- **§9 payoff: the cost FORM is forced by monotonicity alone (no continuity).**

The cost function `F` (reciprocal-symmetric, normalized, satisfying the
composition law) is forced into the cosh log-shape `H_F t = cosh (c·t)` by the
single regularity hypothesis that `H_F = F∘exp + 1` is monotone on `[0,∞)`. This
is the completeness-free replacement for the `ContinuousOn`/Aczél-smoothness
hypothesis of `Cost.FunctionalEquation.law_of_logic_forces_jcost`: the composition
law gives the d'Alembert equation on `H_F`, reciprocal symmetry gives evenness,
normalization gives `H_F 0 = 1`, and `dAlembert_cosh_of_monotone` finishes using
only order + field + sqrt + Archimedean density. -/
theorem composition_law_monotone_forces_cosh_family (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 : ℝ))) :
    ∃ c : ℝ, ∀ t, Cost.FunctionalEquation.H F t = Real.cosh (c * t) := by
  have hCoshAdd := (Cost.FunctionalEquation.composition_law_equiv_coshAdd F).mp hComp
  have h_direct := Cost.FunctionalEquation.CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
  have h_dAlembert : ∀ t u,
      Cost.FunctionalEquation.H F (t + u) + Cost.FunctionalEquation.H F (t - u)
        = 2 * Cost.FunctionalEquation.H F t * Cost.FunctionalEquation.H F u := by
    intro t u
    simp only [Cost.FunctionalEquation.H]
    linear_combination (h_direct t u)
  have h0 : Cost.FunctionalEquation.H F 0 = 1 := by
    simp only [Cost.FunctionalEquation.H]
    rw [Cost.FunctionalEquation.G_zero_of_unit F hNorm]; norm_num
  have heven : Function.Even (Cost.FunctionalEquation.H F) := by
    intro t
    simp only [Cost.FunctionalEquation.H]
    rw [Cost.FunctionalEquation.G_even_of_reciprocal_symmetry F (fun {x} hx => hRecip x hx) t]
  exact dAlembert_cosh_of_monotone h_dAlembert h0 heven hMono
THEOREM dAlembert_diff_eq_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
dAlembert_diff_eq_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean:251 
/-- **§9 sign crux, RESOLVED: monotonicity fixes the sign.** For `0 ≤ t ≤ s`,
both `s+t` and `s−t` lie in `[0,∞)`, so monotonicity of `H` there forces
`H(s+t) ≥ H(s−t)`; the difference is the NONNEGATIVE root of the square computed
in `dAlembert_diff_sq`:

`H(s+t) − H(s−t) = 2 √(H(s)²−1) · √(H(t)²−1)`.

This is the cosh addition formula `cosh(a+b) − cosh(a−b) = 2 sinh a sinh b` with
`sinh = √(cosh²−1) ≥ 0`. The sign — the one place the analytic proof used
continuity — is here pinned by ORDER ALONE. So the answer to the §9 sub-question
"can monotonicity fix the sign?" is YES. Completeness is not needed for this
step; only the order structure of the field is. -/
theorem dAlembert_diff_eq_of_monotone {H : ℝ → ℝ}
    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1)
    (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) :
    ∀ s t, 0 ≤ t → t ≤ s →
      H (s + t) - H (s - t)
        = 2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1) := by
  intro s t ht hts
  have hs0 : 0 ≤ s := le_trans ht hts
  have hge1s : 1 ≤ H s := dAlembert_ge_one_of_monotone h0 hmono s hs0
  have hge1t : 1 ≤ H t := dAlembert_ge_one_of_monotone h0 hmono t ht
  have hSs : 0 ≤ (H s) ^ 2 - 1 := by nlinarith [hge1s]
  have hSt : 0 ≤ (H t) ^ 2 - 1 := by nlinarith [hge1t]
  have hsmt_nonneg : 0 ≤ s - t := by linarith
  have hspt_nonneg : 0 ≤ s + t := by linarith
  have hdiff_nonneg : 0 ≤ H (s + t) - H (s - t) := by
    have hle : H (s - t) ≤ H (s + t) :=
      hmono (Set.mem_Ici.mpr hsmt_nonneg) (Set.mem_Ici.mpr hspt_nonneg) (by linarith)
    linarith
  have hrhs_nonneg :
      0 ≤ 2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1) := by positivity
  have hsq := dAlembert_diff_sq hd h0 s t
  have hrhs_sq :
      (2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1)) ^ 2
        = 4 * ((H s) ^ 2 - 1) * ((H t) ^ 2 - 1) := by
    rw [show (2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1)) ^ 2
          = 4 * (Real.sqrt ((H s) ^ 2 - 1)) ^ 2 * (Real.sqrt ((H t) ^ 2 - 1)) ^ 2 by ring,
       Real.sq_sqrt hSs, Real.sq_sqrt hSt]
  have hsquares :
      (H (s + t) - H (s - t)) ^ 2
        = (2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1)) ^ 2 := by
    rw [hsq, hrhs_sq]
  have hsqrt := congrArg Real.sqrt hsquares
  rwa [Real.sqrt_sq hdiff_nonneg, Real.sqrt_sq hrhs_nonneg] at hsqrt
THEOREM dAlembert_cosh_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
dAlembert_cosh_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean:366 
/-- **§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]

What this page does not claim

The theorem does not fix the value of the free parameter c; that requires a separate calibration step. The theorem does not prove the existence of a cost function satisfying the hypotheses; non-vacuity is shown separately. The theorem does not claim monotonicity is the only possible substitute for continuity.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND