  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
 111  violation_meaning := "Non-trivial linking in D ≠ 3"
 112}
 113
 114/-- All necessity gates. -/
 115def all_gates : List NecessityGate :=
 116  [gate_cost_uniqueness, gate_selection_rule, gate_discreteness,
 117   gate_ledger, gate_phi, gate_dimension]
 118
 119/-! ## The Alternative Framework Structure -/
 120
 121/-- An alternative framework to RS. -/
 122structure AlternativeFramework where
 123  /-- The cost functional -/
 124  cost : ℝ → ℝ
 125  /-- The selection rule -/
 126  selection : ℝ → Prop
 127  /-- Number of free parameters -/
 128  parameters : ℕ
 129  /-- Whether it derives observables -/
 130  derives_observables : Bool
 131

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.