SATLedger

formal source

  89    ¬(∀ b R, measure (encode (BalancedParityHidden.enc b R).toList) M = b)
  90
  91/-- SAT instance in ledger representation -/
  92structure SATLedger where
  93  /-- Number of variables -/
  94  n : ℕ
  95  /-- Number of clauses -/
  96  m : ℕ
  97  /-- Clause structure encoded in ledger -/
  98  clauses : List (List (Bool × ℕ))
  99  /-- Result encoded using balanced-parity across n cells -/
 100  result_encoding : Fin n → Bool
 101
 102/-- A recognition scenario packages the demonstration data for the separation story. -/
 103structure RecognitionScenario where
 104  rc : RecognitionComplete
 105  /-- Demonstration bound relating computation and recognition costs for each SAT instance. -/
 106  sat_bound : ∀ inst : SATLedger,
 107    (rc.Tc inst.n : ℝ) ≤ inst.n^(1/3 : ℝ) * Real.log inst.n ∧
 108    (rc.Tr inst.n : ℝ) ≥ inst.n / 2
 109  /-- Eventual growth gap used to witness the recognition/computation split. -/
 110  eventual_gap : ∀ ⦃n : ℕ⦄, 100 ≤ n → (rc.Tc n : ℝ) < n ∧ (rc.Tr n : ℝ) ≥ n
 111
 112/-- Concrete scenario used by downstream demos: Tc = 0 and Tr = id. -/
 113noncomputable def demoRecognitionScenario : RecognitionScenario :=
 114  let rc : RecognitionComplete := {
 115    Tc := fun _ => 0
 116    Tr := fun n => n
 117    Tc_subpoly := by
 118      use 1, (1 / 3 : ℝ)
 119      constructor <;> norm_num
 120      intro n hn
 121      have hlog : 0 ≤ Real.log (n : ℝ) := by
 122        cases n with