inevitability_chain
plain-language theorem explainer
The inevitability chain shows that under defect vanishing only at unity, a positive lower bound on defect near zero, and unique positive phi solving x^2 = x + 1, any cost obeying normalization at one, reciprocity symmetry, non-negativity, C^2 smoothness, unit log-curvature at zero, and d'Alembert structure must equal the J-cost. Recognition Science researchers cite it to close the uniqueness step from axioms to forced cost. The proof rewrites symmetry then invokes the d'Alembert forcing theorem directly.
Claim. Assume defect satisfies $x>0$ implies (defect$(x)=0$ iff $x=1$), that for every real $C$ there is $ε>0$ with $0<x<ε$ implying $C<$ defect$(x)$, and that there is a unique $φ>0$ solving $φ^2=φ+1$. Then any $F:ℝ^+→ℝ$ with $F(1)=0$, $F(x)=F(x^{-1})$ for $x>0$, $F≥0$, twice continuously differentiable, second derivative of $F(e^t)$ at $t=0$ equal to 1, and satisfying the d'Alembert condition on the shifted log-lift, equals the J-cost $J(x)=cosh(log x)-1$.
background
This theorem lives in the InevitabilityEquivalence module, which equates abstract inevitability slogans with concrete cost/CPM conditions. The defect hypothesis is drawn from LawOfExistence, where defect marks the sole zero-cost point. The nothing-infinite condition supplies a uniform positive lower bound on cost near zero. Phi uniqueness encodes the self-similar fixed point from the forcing chain T5-T6.
proof idea
The tactic proof first rewrites the symmetry hypothesis to cost x = cost x^{-1} via simpa on one_div. It then applies exactly the upstream theorem dAlembert_forces_Jcost from FourthGate, supplying the adjusted symmetry, smoothness, calibration, and HasDAlembert assumptions to conclude cost equals Jcost.
why it matters
This is the central uniqueness result realizing the RS core claim that cost is forced to J under the three constraints, feeding directly into noFreeParameters which asserts J is uniquely determined by the axiom bundle. It closes the abstract-to-concrete bridge noted in the module doc and sets full_chain_proven true in current_scaffold_status, linking to T5 J-uniqueness via the d'Alembert gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.