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

scaffold_count

show as:
view Lean formalization →

The definition scaffold_count tallies the number of choke points marked as scaffolds in the inevitability structure. Researchers assessing the completeness of the Recognition Science foundation cite this count when evaluating remaining gaps before the inevitability theorem is fully closed. It arises from a direct filter on the all_choke_points list followed by a length computation.

claimLet $C$ be the list of all choke points. Then scaffold_count equals the cardinality of the sublist of $C$ consisting of those $c$ for which status$(c)=$``scaffold''.

background

The InevitabilityStructure module organizes Recognition Science claims into necessity gates called choke points. These gates cover cost uniqueness (T5: J(x) = ½(x + x⁻¹) - 1), selection by defect minimization, discreteness, ledger symmetry, self-similarity forcing phi, and dimension D=3. Each choke point carries a status string that is either closed or scaffold.

proof idea

One-line definition that filters all_choke_points for entries whose status equals ``scaffold'' and returns the length of the resulting list.

why it matters in Recognition Science

The count is invoked by the inevitability_structure_summary theorem, which states closed_count = 1 and scaffold_count = 3. It therefore quantifies the open steps in the inevitability theorem: any zero-parameter framework deriving observables must either match RS or violate at least one gate. The module doc identifies the three option buckets (cost, existence, admissible frameworks) that this count helps track.

scope and limits

formal statement (Lean)

 246def scaffold_count : ℕ := (all_choke_points.filter (fun c => c.status = "scaffold")).length

proof body

Definition body.

 247
 248/-! ## The Inevitability Upgrade Path -/
 249
 250/-- The upgrade path: what needs to happen to make inevitability complete. -/

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.