FullUnconditionalHypotheses
FullUnconditionalHypotheses packages the d'Alembert-derived cosh hypothesis with the consistency-derived RCL-form hypothesis into one record. Recognition Science researchers cite it when invoking the strongest unconditional inevitability result for the J-cost function. The definition is a direct structure constructor with no further computation.
claimThe structure consists of two fields: dAlembert_cosh, the hypothesis that d'Alembert's equation forces $G(t) = F(e^t) = (e^t + e^{-t})/2 - 1$, and consistency_RCL, the hypothesis that multiplicative consistency forces $P(u,v) = 2uv + 2u + 2v$ for all $u,v$.
background
The module proves the strongest form of RCL inevitability: both F and P are forced with no assumption on P. The local setting requires F : positive reals to reals satisfying F(1)=0, F(x)=F(1/x), twice continuous differentiability, the calibration G''(0)=1 where G(t)=F(exp t), and existence of some P such that F(xy)+F(x/y)=P(F(x),F(y)). Upstream results include the log reparametrization G from Cost.FunctionalEquation and the partial unconditional theorem from Unconditional.lean. Key definitions: J(x)=(x + x^{-1})/2 -1 (T5 self-similar fixed point) and the Recognition Composition Law J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y).
proof idea
The declaration is a one-line structure definition that bundles dAlembert_forces_cosh_hypothesis and consistency_forces_RCL_form_hypothesis as its two fields.
why it matters in Recognition Science
This bundle supplies the input to the downstream theorem full_unconditional_inevitability, which concludes F equals J and P equals the bilinear RCL form. It completes the T0-T8 forcing chain by removing every prior assumption on P, enabling derivation of RS-native constants (c=1, hbar=phi^{-5}, G=phi^5/pi, alpha^{-1} in (137.030,137.039)) and the eight-tick octave. It touches the open question of relaxing C2 smoothness.
scope and limits
- Does not derive the d'Alembert or consistency hypotheses from more primitive axioms.
- Does not extend the result to functions lacking C2 smoothness.
- Does not apply if the calibration condition G''(0)=1 is dropped.
- Does not treat non-multiplicative or non-symmetric cases.
formal statement (Lean)
269structure FullUnconditionalHypotheses where
270 dAlembert_cosh : dAlembert_forces_cosh_hypothesis
271 consistency_RCL : consistency_forces_RCL_form_hypothesis
272
273/-- **THEOREM (Full Unconditional Inevitability)**
274
275If F : ℝ₊ → ℝ satisfies:
2761. F(1) = 0 (normalization)
2772. F(x) = F(1/x) (symmetry)
2783. F ∈ C² (smoothness)
2794. G''(0) = 1 where G(t) = F(exp(t)) (calibration)
2805. F(xy) + F(x/y) = P(F(x), F(y)) for SOME function P
281
282Then:
283- F(x) = J(x) = (x + 1/x)/2 - 1
284- P(u, v) = 2uv + 2u + 2v for all u, v ≥ 0
285
286**NO ASSUMPTION ON P IS MADE.**
287-/