NoFreeParameters
plain-language theorem explainer
NoFreeParameters encodes the claim that any cost function on positive reals obeying normalization at 1, reciprocal symmetry, non-negativity, C^2 smoothness, unit second derivative of the log-lift at zero, and the d'Alembert gate must equal the J-cost. Researchers establishing uniqueness of the recognition cost in zero-parameter frameworks would cite this when closing the abstract layer of inevitability. The definition directly packages the quantified statement as a Prop with no attached reduction or tactics.
Claim. Any twice continuously differentiable function $c:(0,∞)→ℝ$ satisfying $c(1)=0$, $c(x)=c(1/x)$ for $x>0$, $c(x)≥0$, with second derivative of $t↦c(e^t)$ equal to 1 at $t=0$, and obeying the d'Alembert condition on the shifted log-lift, coincides with the J-cost $J(x)=(x+x^{-1})/2-1$.
background
The module bridges abstract inevitability slogans such as 'no free parameters' to concrete cost conditions. J-cost is the function $J(x)=cosh(log x)-1$, the self-similar fixed point forced by the recognition axioms. HasDAlembert requires that the shifted log-lift $H(t)=c(e^t)+1$ satisfies the d'Alembert functional equation, as defined in FourthGate. Upstream, the inevitability theorem asserts that any zero-parameter alternative framework either reduces to the RS cost and selection or violates at least one necessity gate.
proof idea
This is a definition that directly states the uniqueness proposition as a Prop; it contains no proof body, lemmas, or tactics.
why it matters
It supplies the abstract 'no free parameters' claim that feeds the inevitability_chain theorem, which establishes the concrete equivalence between abstract and concrete layers. This realizes the T5 J-uniqueness step in the forcing chain, confirming that all constants derive from the J-structure with no adjustable parameters. The downstream noFreeParameters theorem discharges the claim using concrete_inevitability.defect_char, nothing_infinite, and phi_unique.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.