concrete_implies_no_alternatives
plain-language theorem explainer
The theorem shows that the three concrete conditions on the cost function suffice to recover the defect characterization, the unboundedness of defect near zero, and the uniqueness of the positive golden-ratio root. Researchers closing the inevitability chain from CPM axioms to the absence of free parameters would cite this result. The proof is a one-line term that directly assembles the conjunction from the three fields of the input structure.
Claim. Assume the cost function satisfies the defect characterization, the condition that defect is unbounded near zero, and the uniqueness of the positive root of $x^2 = x + 1$. Then defect vanishes precisely at unity for positive reals, defect exceeds any real bound in every neighborhood of zero, and the equation $x^2 = x + 1$ has a unique positive real solution.
background
The module bridges abstract inevitability slogans with concrete CPM and cost definitions, establishing equivalence between layers such as INEV_DIMLESS and specific cost conditions. ConcreteInevitability is the structure whose fields are exactly the defect characterization (defect vanishes only at unity), the no-infinite-cost condition, and the unique positive golden-ratio root. Upstream results include the reciprocal automorphism from CostAlgebra, which encodes the symmetry that forces these properties, and the Chain structure that supplies the minimal relational axioms supporting the ledger.
proof idea
The proof is a term-mode construction that returns the conjunction of the defect_char, nothing_infinite, and phi_unique fields extracted from the supplied ConcreteInevitability instance.
why it matters
This is the master theorem realizing the abstract-concrete equivalence for the inevitability chain, showing that concrete cost conditions suffice for the no-alternatives claim. It connects directly to T5 J-uniqueness in the forcing chain and supports the RS thesis that any alternative satisfying the same properties either equals J or breaks reciprocity. The module positions the result as the mathematical heart of zero-parameter inevitability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.