all_gates
plain-language theorem explainer
The definition collects the six necessity gates that any zero-parameter alternative framework must either match or violate to derive observables. Researchers proving the no-alternatives claim in Recognition Science cite this enumeration when applying the inevitability theorem. It is a direct list construction referencing the individually defined gates for cost uniqueness, selection, discreteness, ledger, self-similarity, and dimension.
Claim. Let $G_1$ be the cost-uniqueness gate (T5), $G_2$ the selection-rule gate, $G_3$ the discreteness gate, $G_4$ the ledger-structure gate, $G_5$ the self-similarity gate, and $G_6$ the dimension-forcing gate. Then the complete list of necessity gates is $[G_1, G_2, G_3, G_4, G_5, G_6]$.
background
The module establishes the inevitability structure of Recognition Science by relocating degrees of freedom from an empty-set tautology to a physical claim that selection occurs by minimizing a unique cost. A NecessityGate records a constraint name, a proven flag, and the physical meaning of its violation. The three option buckets are: choices about the cost functional itself, choices about what existence means, and choices about the admissible class of zero-parameter frameworks.
proof idea
One-line definition that enumerates the six gate constants already constructed in the module: gate_cost_uniqueness, gate_selection_rule, gate_discreteness, gate_ledger, gate_phi, and gate_dimension.
why it matters
The list supplies the exhaustive set of gates required by the inevitability theorem, which asserts that any alternative zero-parameter framework deriving observables must reduce to RS or violate at least one gate. It directly implements the module's claim that alternatives must break a necessity gate or secretly add parameters. The dimension gate remains a scaffold, while the others rest on upstream results from Cost, DiscretenessForcing, LedgerForcing, and PhiForcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.