all_choke_points
plain-language theorem explainer
The definition assembles a list of four ChokePoint records that mark the necessity gates any zero-parameter alternative to Recognition Science must violate. Researchers tracking framework uniqueness cite the list when counting closed versus open bottlenecks. It is a direct enumeration of the individually defined choke point structures.
Claim. Let $C$ be the list of choke points $C = [U, A, E, D]$ where $U$ records universality of the cost-projection model, $A$ the cost axiom bundle with status closed, $E$ framework exclusivity with status scaffold, and $D$ dimension forcing with status scaffold; each entry is a record containing a name string, status string, and consequence string.
background
A ChokePoint is a structure with three fields: a name string identifying the gate, a status string taking values closed, scaffold or open, and a consequence string stating what closure would establish. The module formalizes inevitability under the cost-projection model by relocating degrees of freedom into a unique J-cost minimization; alternatives must break one of the listed gates rather than rely on an empty-set tautology. Upstream, choke_cost_axioms records that T5 forces J uniqueness via symmetry, convexity and normalization, while choke_dimension records the incomplete link from ledger self-similarity to D = 3.
proof idea
One-line definition that constructs the list literal from the four sibling choke point definitions already present in the same module.
why it matters
The list supplies the single source of truth for the two downstream counters closed_count and scaffold_count that measure progress toward the inevitability theorem. It directly encodes the six-step chain in the module documentation: cost uniqueness (T5), selection rule, discreteness, ledger structure, self-similarity and dimension forcing. The definition therefore anchors the claim that any alternative zero-parameter framework must violate at least one of these gates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.