def
definition
gate_selection_rule
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.InevitabilityStructure on GitHub at line 80.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
77}
78
79/-- Gate 2: Selection Rule (CPM) -/
80def gate_selection_rule : NecessityGate := {
81 name := "CPM: Selection Rule"
82 proven := true -- Proven in CPM/LawOfExistence.lean
83 violation_meaning := "Alternative selection criterion not based on defect → 0"
84}
85
86/-- Gate 3: Discreteness Forcing -/
87def gate_discreteness : NecessityGate := {
88 name := "Discreteness Forcing"
89 proven := true -- Proven in DiscretenessForcing.lean
90 violation_meaning := "Continuous configuration space with stable minima"
91}
92
93/-- Gate 4: Ledger Structure -/
94def gate_ledger : NecessityGate := {
95 name := "Ledger Forcing"
96 proven := true -- Proven in LedgerForcing.lean
97 violation_meaning := "Asymmetric recognition without double-entry conservation"
98}
99
100/-- Gate 5: φ Forcing -/
101def gate_phi : NecessityGate := {
102 name := "φ Forcing"
103 proven := true -- Proven in PhiForcing.lean
104 violation_meaning := "Self-similar discrete ledger with ratio ≠ φ"
105}
106
107/-- Gate 6: Dimension Forcing -/
108def gate_dimension : NecessityGate := {
109 name := "D = 3 Forcing"
110 proven := false -- Scaffold: requires linking + gap-45 proof