summary
plain-language theorem explainer
The summary theorem collects the three concrete conditions that turn abstract inevitability into a uniqueness statement for the golden-ratio fixed point under the defect functional. A researcher closing the Recognition Science forcing chain would invoke it to confirm that the cost foundation admits no alternatives once J is fixed. The proof is a direct term that packages the uniqueness of the positive quadratic root, the zero characterization of the defect, and the divergence of the defect near zero.
Claim. There exists a unique positive real number $x$ satisfying $x^2 = x + 1$. For every positive real $x$, the defect functional vanishes if and only if $x = 1$. For every real bound $C$ there exists a positive $ε$ such that the defect exceeds $C$ for all positive arguments smaller than $ε$.
background
This module bridges abstract inevitability slogans such as zero-parameter and no-alternatives to concrete CPM/cost definitions, with the key equivalence Abstract Inevitability ⟺ Concrete Cost/CPM Conditions. The defect functional is defined to equal J for positive arguments, where J is the cost that satisfies the Recognition Composition Law. The local setting is the concrete side of INEV_DIMLESS, INEV_ABSOLUTE, and INEV_CLOSURE, in which J-minima determine existence with a unique φ fixed point.
proof idea
The proof is a one-line term that directly assembles the three conjuncts by applying phi_unique_pos for the uniqueness of the positive root of x² = x + 1, the lambda fun x hx => defect_zero_iff_one hx for the zero characterization, and nothing_cannot_exist for the statement that defect diverges to infinity near zero.
why it matters
This declaration closes the concrete side of the inevitability equivalence, confirming that any cost satisfying the axioms equals J and that no free parameters remain. It connects to T5 J-uniqueness in the forcing chain by establishing the unique positive fixed point and to the module claim that no alternatives means any alternative must violate a necessity or add parameters. It touches the open question of full chain closure from CPM/cost through the eight-tick octave to D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.