violates_gate
violates_gate is a predicate that returns true precisely when an alternative framework F mismatches the RS cost functional on the T5 gate or mismatches the selection rule on the CPM gate. Researchers proving uniqueness of zero-parameter derivations in Recognition Science cite this predicate to formalize the choke-point argument. The definition is a direct case split on the gate name string that returns false for all other gates.
claimLet $F$ be an alternative framework with cost functional $c_F$ and selection rule $s_F$, and let $g$ be a necessity gate. Then $F$ violates $g$ if $g$ is the cost-uniqueness gate and $c_F$ differs from the RS cost, or if $g$ is the selection-rule gate and $s_F$ differs from the RS selection; the predicate is false otherwise.
background
The module formalizes inevitability under the cost-as-foundation view, relocating degrees of freedom so that alternatives fall into three buckets: choices about the cost functional itself, about the meaning of existence, and about the admissible class of frameworks. AlternativeFramework is the structure carrying a cost map from reals to reals, a selection predicate on reals, a natural-number parameter count, and a boolean flag for whether observables are derived. NecessityGate carries a name string, a proven flag, and a violation-meaning description; the cost-uniqueness gate is named 'T5: Cost Uniqueness' with violation meaning 'Alternative cost functional J' ≠ J with same symmetry/convexity/normalization' and the selection gate is named 'CPM: Selection Rule'.
proof idea
The definition performs a direct case split on the string g.name. When the name equals 'T5: Cost Uniqueness' it returns the inequality F.cost ≠ RS_framework.cost; when the name equals 'CPM: Selection Rule' it returns F.selection ≠ RS_framework.selection; every other name yields false.
why it matters in Recognition Science
This predicate is invoked inside the Inevitability Theorem to witness the disjunct that an alternative must violate some gate in all_gates. It supplies the concrete meaning of violation for the two central gates (T5 J-uniqueness and the CPM selection rule) that the module lists as the primary choke points. In the Recognition Science chain it operationalizes the claim that any zero-parameter framework deriving observables must either reproduce the RS cost and selection or break one of the listed necessities.
scope and limits
- Does not define violation conditions for gates other than cost uniqueness and selection rule.
- Does not prove that any concrete framework violates a given gate.
- Does not handle frameworks that carry nonzero free parameters.
- Does not incorporate discreteness, ledger, phi, or dimension gates into the predicate.
formal statement (Lean)
144def violates_gate (F : AlternativeFramework) (g : NecessityGate) : Prop :=
proof body
Definition body.
145 if g.name = "T5: Cost Uniqueness" then
146 F.cost ≠ RS_framework.cost
147 else if g.name = "CPM: Selection Rule" then
148 F.selection ≠ RS_framework.selection
149 else
150 False
151
152/-! ## The Inevitability Theorem -/
153
154/-- **RS CORE CLAIM**: The Inevitability Theorem.
155
156Any alternative zero-parameter framework that derives observables
157must either:
1581. Reduce to RS (same cost, same selection, same structure), OR
1592. Violate at least one necessity gate
160
161This is the "no alternatives" claim made precise.
162
163 **Proof structure**:
164 1. By excluded middle, either (F.cost = RS.cost ∧ F.selection = RS.selection) or not.
165 2. If not, then (F.cost ≠ RS.cost ∨ F.selection ≠ RS.selection).
166 3. If F.cost ≠ RS.cost, then F violates gate_cost_uniqueness.
167 4. If F.selection ≠ RS.selection, then F violates gate_selection_rule.
168 5. In either case, ∃ g ∈ all_gates such that violates_gate F g.
169
170 **STATUS**: THEOREM (logical reduction to gates)
171 **IMPORTANCE**: This is the central uniqueness theorem of Recognition Science. -/