full_inevitability_explicit
Any C² function F on positive reals obeying inversion symmetry, unit normalization at 1, and a multiplicative consistency relation F(xy) + F(x/y) = P(F(x), F(y)) for some combiner P must equal the J-cost function J(x) = (x + x^{-1})/2 - 1. The associated P is forced to the bilinear form 2uv + 2u + 2v on the nonnegative quadrant. Recognition Science researchers cite this as the explicit unconditional inevitability result. The argument lifts to G(t) = F(e^t), verifies the d'Alembert equation, and invokes cosh uniqueness under the given second-der
claimLet $F : ℝ → ℝ$ and $P : ℝ → ℝ → ℝ$ satisfy $F(1) = 0$, $F(x) = F(x^{-1})$ for $x > 0$, $F$ twice continuously differentiable, the second derivative of $G(t) := F(e^t)$ at zero equal to 1, and $F(xy) + F(x/y) = P(F(x), F(y))$ for $x, y > 0$. Assume moreover that $P(F(x), F(y)) = 2 F(x) F(y) + 2 F(x) + 2 F(y)$ and that any $H$ obeying the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$, $H(0)=1$, twice differentiable with $H''(0)=1$ equals the hyperbolic cosine. Then $F(x) = (x + x^{-1})/2 - 1$ for $x > 0$ and $P(u, v) = 2uv + 2u + 2v$ for $u, v ≥ 0$.
background
In Recognition Science the J-cost is the function J(x) = (x + x^{-1})/2 - 1. The auxiliary map G(t) = F(exp t) converts multiplicative consistency into an additive relation on the reals. The module establishes the strongest form of RCL inevitability by assuming only the existence of some combiner P and deriving both F and P uniquely from smoothness, symmetry, normalization, and calibration of G''(0) = 1. The shifted function H = G + 1 satisfies the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0) = 1. Upstream results include the verification that G satisfies this equation under the RCL hypothesis (H_dAlembert_of_G_RCL) and the uniqueness theorem forcing H to cosh under the calibration condition.
proof idea
The proof first derives that G satisfies the RCL form of the d'Alembert equation by substituting exponential variables into the consistency relation and applying the RCL hypothesis. It then defines Hloc = G + 1, verifies Hloc(0) = 1 via G_zero_of_unit, the d'Alembert relation via H_dAlembert_of_G_RCL, smoothness by composition with exp, and the second-derivative calibration by direct differentiation. Application of the dA_cosh hypothesis yields Hloc = cosh, hence G = cosh - 1. Inversion via the logarithm recovers F = Jcost on positives using Jcost_G_eq_cosh_sub_one. The P conclusion follows by surjectivity of J onto the nonnegatives (J_surjective_nonneg) and substitution into the RCL form.
why it matters in Recognition Science
This is the explicit form of the full unconditional inevitability theorem. It feeds the washburn_full_unconditional result that closes the forcing chain. The declaration shows that the Recognition Composition Law is the only combiner compatible with T5 J-uniqueness and the d'Alembert step under the given calibration. It removes all prior assumptions on P and thereby strengthens the link from the consistency hypothesis to the eight-tick octave and D = 3 spatial dimensions.
scope and limits
- Does not apply to functions lacking C² smoothness.
- Does not cover cases where the consistency relation fails for some positive x, y.
- Does not determine P outside the image of F.
- Does not address discrete or finite-domain analogues.
formal statement (Lean)
352theorem full_inevitability_explicit
353 (F : ℝ → ℝ)
354 (P : ℝ → ℝ → ℝ)
355 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
356 (hUnit : F 1 = 0)
357 (hSmooth : ContDiff ℝ 2 F)
358 (hCalib : deriv (deriv (G F)) 0 = 1)
359 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
360 -- Hypothesis: consistency forces RCL form
361 (h_RCL_form : ∀ x y : ℝ, 0 < x → 0 < y →
362 P (F x) (F y) = 2 * F x * F y + 2 * F x + 2 * F y)
363 -- Hypothesis: d'Alembert + calibration forces cosh
364 (h_dA_cosh : ∀ (H : ℝ → ℝ), H 0 = 1 → ContDiff ℝ 2 H →
365 (∀ t u : ℝ, H (t + u) + H (t - u) = 2 * H t * H u) →
366 deriv (deriv H) 0 = 1 → ∀ t, H t = Real.cosh t) :
367 -- Conclusion
368 (∀ x : ℝ, 0 < x → F x = Cost.Jcost x) ∧
369 (∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2 * u * v + 2 * u + 2 * v) := by
proof body
Tactic-mode proof.
370 -- G satisfies RCL consistency
371 have hG_RCL : ∀ t u : ℝ, G F (t + u) + G F (t - u) =
372 2 * G F t * G F u + 2 * G F t + 2 * G F u := by
373 intro t u
374 simp only [G]
375 have hexp_t : 0 < Real.exp t := Real.exp_pos t
376 have hexp_u : 0 < Real.exp u := Real.exp_pos u
377 have h := hCons (Real.exp t) (Real.exp u) hexp_t hexp_u
378 rw [h_RCL_form (Real.exp t) (Real.exp u) hexp_t hexp_u] at h
379 rw [← Real.exp_add, ← Real.exp_sub] at h
380 exact h
381 -- G(0) = 0
382 have hG0 : G F 0 = 0 := G_zero_of_unit F hUnit
383 -- H = G + 1 satisfies d'Alembert with H(0) = 1
384 let Hloc := fun t => G F t + 1
385 have hH0 : Hloc 0 = 1 := by
386 simp only [Hloc, G, Real.exp_zero]; rw [hUnit]; ring
387 have hH_dA : ∀ t u : ℝ, Hloc (t + u) + Hloc (t - u) = 2 * Hloc t * Hloc u :=
388 H_dAlembert_of_G_RCL (G F) hG0 hG_RCL
389 -- H is C²
390 have hH_smooth : ContDiff ℝ 2 Hloc := by
391 simp only [Hloc]
392 exact (hSmooth.comp Real.contDiff_exp).add contDiff_const
393 -- H''(0) = 1
394 have hH_calib : deriv (deriv Hloc) 0 = 1 := by
395 have h_deriv_G : deriv Hloc = deriv (G F) := by
396 ext t; change deriv (fun s => G F s + 1) t = deriv (G F) t
397 simpa using (deriv_add_const (f := G F) (x := t) (c := (1 : ℝ)))
398 have h_deriv2 : deriv (deriv Hloc) = deriv (deriv (G F)) := congrArg deriv h_deriv_G
399 rw [h_deriv2]; exact hCalib
400 -- Therefore H = cosh
401 have hH_cosh : ∀ t, Hloc t = Real.cosh t := h_dA_cosh Hloc hH0 hH_smooth hH_dA hH_calib
402 -- G = cosh - 1
403 have hG_cosh : ∀ t, G F t = Real.cosh t - 1 := by
404 intro t; have h := hH_cosh t; simp only [Hloc] at h; linarith
405 -- F = J on positive reals
406 have hF_eq_J : ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
407 intro x hx
408 rw [← Real.exp_log hx]
409 have h1 := hG_cosh (Real.log x)
410 simp only [G] at h1
411 have h2 := Jcost_G_eq_cosh_sub_one (Real.log x)
412 simp only [G] at h2
413 linarith
414 constructor
415 · exact hF_eq_J
416 · -- P = 2uv + 2u + 2v on [0, ∞)²
417 intro u v hu hv
418 -- Since F = J, and J is surjective onto [0, ∞), there exist x, y with J(x) = u, J(y) = v
419 obtain ⟨x, hx_pos, hx_eq⟩ := J_surjective_nonneg u hu
420 obtain ⟨y, hy_pos, hy_eq⟩ := J_surjective_nonneg v hv
421 -- F(x) = J(x) = u, F(y) = J(y) = v
422 have hFx : F x = u := by rw [hF_eq_J x hx_pos, hx_eq]
423 have hFy : F y = v := by rw [hF_eq_J y hy_pos, hy_eq]
424 -- P(u, v) = P(F(x), F(y)) = 2*F(x)*F(y) + 2*F(x) + 2*F(y) = 2uv + 2u + 2v
425 calc P u v = P (F x) (F y) := by rw [hFx, hFy]
426 _ = 2 * F x * F y + 2 * F x + 2 * F y := h_RCL_form x y hx_pos hy_pos
427 _ = 2 * u * v + 2 * u + 2 * v := by rw [hFx, hFy]
428
429/-- Concrete (no-hypothesis-bundle) full unconditional theorem.
430
431This version makes all assumptions explicit and uses:
4321) `consistency_forces_RCL_form_is_theorem` for the combiner shape, and
4332) `dAlembert_forces_cosh_is_theorem` for the d'Alembert/cosh step. -/