SATInstance

formal source

  51/-! ## SAT Instance as J-Cost Landscape -/
  52
  53/-- A SAT instance: n variables, m clauses. -/
  54structure SATInstance where
  55  n_vars : ℕ
  56  n_clauses : ℕ
  57  n_pos : 0 < n_vars
  58  m_pos : 0 < n_clauses
  59
  60/-- A J-cost landscape encoding of a SAT instance.
  61    Each clause becomes a local J-cost contribution.
  62    Total J-cost = 0 iff all clauses satisfied. -/
  63structure JCostLandscape where
  64  sat : SATInstance
  65  landscape_size : ℕ := sat.n_vars + sat.n_clauses
  66  min_cost_zero_iff_sat : Prop
  67
  68/-- R-hat resolution time: the number of octaves for R-hat to reach
  69    defect below ε on the SAT landscape. -/
  70structure ResolutionTime where
  71  sat : SATInstance
  72  octaves : ℕ
  73  reaches_minimum : Prop
  74
  75/-! ## The Non-Naturality Argument -/
  76
  77/-- A natural property (Razborov-Rudich) has two characteristics:
  78    1. Constructivity: computable in polynomial time from the truth table.
  79    2. Largeness: satisfied by a random function with probability ≥ 1/poly(n).
  80
  81    R-hat's certificate is non-natural because it operates on the full Z³
  82    lattice topology, not on polynomial-size truth tables. -/
  83structure NaturalProperty where
  84  constructive : Prop