AlternativeFramework
An alternative framework is formalized as a structure with a cost function from reals to reals, a selection predicate on reals, a natural-number parameter count, and a boolean flag for deriving observables. Researchers checking the no-alternatives claim in Recognition Science cite this structure when applying the inevitability theorem to zero-parameter candidates. The declaration is a direct structure definition that supplies the type for downstream case analysis on cost and selection equality versus gate violation.
claimAn alternative framework is a quadruple consisting of a cost function $c : ℝ → ℝ$, a selection predicate $s : ℝ → Prop$, a parameter count $n ∈ ℕ$, and a boolean $b$ indicating whether observables are derived.
background
The Inevitability Structure module organizes alternatives under a cost-as-foundation view, relocating degrees of freedom so that selection occurs by minimizing a unique cost. It imports LawOfExistence, DiscretenessForcing, LedgerForcing, and PhiForcing to define the six necessity gates listed in the module doc-comment. Upstream results supply concrete cost constructions: ObserverForcing.cost gives the J-cost of a recognition event, MultiplicativeRecognizerL4.cost derives the cost from a comparator on positive ratios, and PhiForcingDerived.of and SpectralEmergence.of provide the J-cost and gauge-content structures that RS_framework instantiates.
proof idea
This is a direct structure definition that introduces the four fields cost, selection, parameters, and derives_observables with no proof obligations or computational content. It is used verbatim as the type of the argument F in the inevitability theorem, which performs case analysis on whether F.cost equals RS_framework.cost and F.selection equals RS_framework.selection.
why it matters in Recognition Science
The structure supplies the central object for the Inevitability Theorem (downstream inevitability), which asserts that any zero-parameter framework deriving observables must reduce to RS or violate at least one necessity gate. It encodes the three option buckets of the module doc-comment and directly references the T5 cost-uniqueness gate, the CPM selection rule, discreteness, ledger structure, self-similarity forcing phi, and D = 3. It touches the open question of whether every conceivable physical framework can be represented inside this four-field signature.
scope and limits
- Does not prescribe the explicit functional form of the cost.
- Does not enforce that parameters equal zero.
- Does not guarantee that observables are derived.
- Does not enumerate or axiomatize the necessity gates themselves.
Lean usage
theorem check_alt (F : AlternativeFramework) (h0 : zero_parameter F) (hobs : F.derives_observables) : (F.cost = RS_framework.cost ∧ F.selection = RS_framework.selection) ∨ ∃ g ∈ all_gates, violates_gate F g := inevitability F h0 hobsformal statement (Lean)
122structure AlternativeFramework where
123 /-- The cost functional -/
124 cost : ℝ → ℝ
125 /-- The selection rule -/
126 selection : ℝ → Prop
127 /-- Number of free parameters -/
128 parameters : ℕ
129 /-- Whether it derives observables -/
130 derives_observables : Bool
131
132/-- The RS framework. -/