pith. machine review for the scientific record. sign in
def

gate_selection_rule

definition
show as:
view math explainer →
module
IndisputableMonolith.Foundation.InevitabilityStructure
domain
Foundation
line
80 · github
papers citing
none yet

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

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

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