closed_count
plain-language theorem explainer
closed_count tallies the choke points marked closed inside the all_choke_points list of the inevitability structure. Researchers summarizing the CPM/cost foundation would cite this count when stating that exactly one necessity gate is resolved while three remain scaffolded. The definition performs a direct filter on status equality followed by a length operation.
Claim. Let $C$ be the list of all choke points. Then closed_count equals the number of elements $c$ in $C$ such that status$(c)$ equals closed.
background
The InevitabilityStructure module formalizes how any zero-parameter alternative to Recognition Science must violate one of the CPM/cost necessities. These necessities are organized as choke points: cost uniqueness (T5: $J(x) = ½(x + x^{-1}) - 1$), selection by defect minimization, discreteness, ledger double-entry from J-symmetry, self-similarity forcing phi, and dimension forcing to $D=3$. The list all_choke_points enumerates four concrete instances: choke_universality, choke_cost_axioms, choke_exclusivity, and choke_dimension.
proof idea
One-line definition that applies filter for status equality to all_choke_points and then computes the length of the resulting list.
why it matters
The definition supplies the left-hand side of the inevitability_structure_summary theorem, which asserts closed_count = 1 and scaffold_count = 3. It thereby anchors the claim that the cost-uniqueness gate (T5) is closed while the remaining gates stay scaffolded. This placement directly supports the module's inevitability story that alternatives must break a necessity gate derived from the forcing chain T5 through T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.