noFreeParameters
plain-language theorem explainer
The theorem confirms that the J-cost function is the unique solution satisfying normalization at 1, reciprocity under inversion, non-negativity, twice continuous differentiability, unit second derivative after logarithmic change of variables, and the d'Alembert fourth-gate condition. Researchers deriving physical constants from zero-parameter axioms would cite it to establish that the cost structure admits no free parameters. The proof is a direct term-mode instantiation of the inevitability_chain theorem using the defect-zero characterization,
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. Any function $C:ℝ→ℝ$ obeying $C(1)=0$, $C(x)=C(x^{-1})$ for all $x>0$, $C(x)≥0$ for $x>0$, $C∈C^2(ℝ)$, the second derivative of $t↦C(e^t)$ at $t=0$ equals 1, and the d'Alembert fourth-gate condition must satisfy $C=J$.
background
The module InevitabilityEquivalence equates abstract inevitability slogans with concrete cost conditions. NoFreeParameters is the abstract claim that J is fixed by the axiom bundle: normalization, reciprocity, non-negativity, smoothness, calibration derivative, and HasDAlembert. The concrete_inevitability structure supplies the three supporting facts: defect vanishes only at 1, nothing cannot exist at finite cost, and phi is the unique positive fixed point of $x^2=x+1$. Upstream, inevitability_chain states that these three facts together force any cost obeying the listed properties to equal J. The local setting is the bridge from abstract zero-parameter claims to CPM/cost definitions.
proof idea
Term-mode one-line wrapper that applies inevitability_chain to the three fields of concrete_inevitability: the defect characterization (defect x = 0 ↔ x = 1), the nothing-infinite bound, and the phi-uniqueness witness.
why it matters
It discharges the abstract half of the inevitability equivalence, confirming that the J-structure is uniquely determined by the axiom set. This supports the parent inevitability theorem in InevitabilityStructure, which asserts that any zero-parameter alternative either reduces to RS or violates a necessity gate. It directly realizes the T5 J-uniqueness step of the forcing chain and the INEV_DIMLESS slogan in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.