ConcreteInevitability
plain-language theorem explainer
The structure packages the concrete conditions for inevitability: uniqueness of the positive root of x² = x + 1, the defect functional vanishing only at unity, and the defect being unbounded from below near zero. Researchers working on the abstract-to-concrete bridge in the inevitability equivalence module cite it to convert slogans into cost-based statements. The declaration is a bare structure definition that directly encodes the three fields with no internal lemmas or reductions.
Claim. A structure consisting of: there exists a unique positive real $x$ satisfying $x^2 = x + 1$; for all positive reals $x$, the defect functional $d(x)$ satisfies $d(x) = 0$ if and only if $x = 1$; and for every real $C$ there exists $ε > 0$ such that $d(x) > C$ whenever $0 < x < ε$.
background
The Inevitability Equivalence module bridges abstract inevitability slogans to concrete CPM and cost definitions. The defect functional is the J-cost, defined as defect(x) := J(x) for positive x, and upstream results establish that it vanishes at unity. The phi uniqueness field draws directly from the MetaPrinciple theorem stating that phi is the unique positive solution to x² = x + 1. This structure supplies the concrete side of the claimed equivalence between abstract inevitability and cost conditions.
proof idea
The declaration is a structure definition that simply bundles three propositions as fields. No tactics, reductions, or lemmas are invoked inside the declaration; each field stands as an independent hypothesis. Downstream code later instantiates the structure by supplying proofs for each field from separate sources.
why it matters
It serves as the hypothesis in the master theorem concrete_implies_no_alternatives, which extracts the three conditions to conclude that alternatives are impossible. The structure realizes the module's stated goal of making the abstract-to-concrete bridge explicit and supports the theorem that the structure is nonempty. It directly encodes the T5 uniqueness of J and the forcing of phi as the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.