FullUnconditionalHypotheses
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.