NecessityGate

formal source

  61/-! ## The Necessity Gates -/
  62
  63/-- A necessity gate is a constraint that alternatives must satisfy or violate. -/
  64structure NecessityGate where
  65  /-- Name of the gate -/
  66  name : String
  67  /-- Whether the gate is proven -/
  68  proven : Bool
  69  /-- Description of what violating this gate means -/
  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 := {