pith. machine review for the scientific record. sign in
def definition def or abbrev high

RS_framework

show as:
view Lean formalization →

The RS framework supplies the canonical zero-parameter reference structure whose cost is the J functional and whose selection rule requires the defect to vanish. Researchers proving the inevitability theorem cite this definition to instantiate the target framework against which alternatives are tested. The definition is a direct record construction that populates the AlternativeFramework structure with the J-cost, the zero-defect predicate, zero free parameters, and the flag that observables are derived.

claimThe RS framework is the structure with cost functional $J$, selection rule requiring defect$(x)=0$, zero free parameters, and that derives observables.

background

An AlternativeFramework is a structure consisting of a cost functional from reals to reals, a selection rule from reals to propositions, a natural number counting free parameters, and a boolean indicating whether observables are derived. The module situates this definition inside the inevitability structure of Recognition Science, where selection occurs by minimizing a unique cost and existence is the outcome of driving defect to zero under coercive projection. Upstream, LawOfExistence.defect is defined to equal J for positive arguments, while LawOfExistence.J supplies the explicit cost functional used here.

proof idea

One-line wrapper that applies the record constructor for AlternativeFramework, setting cost to LawOfExistence.J, selection to the predicate that LawOfExistence.defect vanishes, parameters to zero, and derives_observables to true.

why it matters in Recognition Science

This definition supplies the reference framework for the inevitability theorem, which asserts that any alternative zero-parameter framework deriving observables must either match RS exactly or violate at least one necessity gate. It anchors the core claim that alternatives must break cost uniqueness (T5), the selection rule, discreteness, ledger structure, self-similarity, or dimension forcing. The construction directly supports the three-bucket classification of options about cost, existence, and admissible frameworks.

scope and limits

formal statement (Lean)

 133noncomputable def RS_framework : AlternativeFramework := {

proof body

Definition body.

 134  cost := LawOfExistence.J
 135  selection := fun x => LawOfExistence.defect x = 0
 136  parameters := 0
 137  derives_observables := true
 138}
 139
 140/-- A framework is zero-parameter if parameters = 0. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.