def
definition
gate_cost_uniqueness
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.InevitabilityStructure on GitHub at line 73.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
70 violation_meaning : String
71
72/-- Gate 1: Cost Uniqueness (T5) -/
73def gate_cost_uniqueness : NecessityGate := {
74 name := "T5: Cost Uniqueness"
75 proven := true -- Proven in Cost/T5Uniqueness.lean
76 violation_meaning := "Alternative cost functional J' ≠ J with same symmetry/convexity/normalization"
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