violates_gate
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.