gate_selection_rule
plain-language theorem explainer
The gate_selection_rule records the second necessity gate asserting that physical existence is selected by driving the defect functional to zero under the unique cost J. Physicists exploring zero-parameter alternatives to Recognition Science would reference this gate when testing whether their framework obeys the cost-minimization selection rule. The definition is a straightforward record literal that hardcodes the gate name, its proven status from the Law of Existence, and the meaning of a violation.
Claim. The selection rule gate is the structure NecessityGate with fields name = ``CPM: Selection Rule'', proven = true, and violation_meaning = ``Alternative selection criterion not based on defect → 0''.
background
In the inevitability structure module, alternatives to Recognition Science are organized into necessity gates that must be violated for a framework to differ from RS. The NecessityGate structure captures each gate by its name, whether it has been proven, and the physical meaning of violating it. This particular gate encodes the selection rule from the Law of Existence, where the defect functional is defined as defect(x) := J(x) for positive x, with J the unique cost function forced by symmetry and convexity.
proof idea
The definition is a direct record construction that populates the three fields of NecessityGate. It sets the name to identify the gate as the CPM selection rule, marks it proven by reference to the LawOfExistence module, and specifies the violation condition as any selection not based on driving defect to zero.
why it matters
This gate supplies the second entry in the all_gates list used by the inevitability theorem, which states that any zero-parameter framework deriving observables must either match RS or violate at least one gate. It fills the selection bucket in the module's three-option classification, enforcing that existence equals defect minimization under the unique J. The gate connects to the broader chain by ensuring alternatives cannot introduce non-cost-based selection without breaking the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.