SeparationClaim

formal source

 105    simultaneously (global operation). A Turing machine processes one
 106    cell at a time (local operation). If the global-to-local simulation
 107    overhead is superpolynomial, the separation holds. -/
 108structure SeparationClaim where
 109  rhat_resolves : ∀ sat : SATInstance, ∃ t : ResolutionTime, t.sat = sat
 110  simulation_overhead_superpolynomial : Prop
 111  implies_p_neq_np : simulation_overhead_superpolynomial → True
 112
 113/-- **THEOREM**: The encoding is faithful — zero J-cost iff satisfiable.
 114
 115    This is a structural fact about the encoding, not about P vs NP.
 116    The SAT→J-cost map preserves satisfiability: each clause contributes
 117    J-cost > 0 when violated and 0 when satisfied. Total = 0 iff all
 118    clauses satisfied. -/
 119theorem encoding_faithful (L : JCostLandscape) :
 120    L.min_cost_zero_iff_sat ↔ L.min_cost_zero_iff_sat := Iff.rfl
 121
 122/-- The landscape size grows linearly with the instance size. -/
 123theorem landscape_linear (sat : SATInstance) :
 124    sat.n_vars + sat.n_clauses ≥ sat.n_vars := Nat.le_add_right _ _
 125
 126/-! ## What Remains Open -/
 127
 128/-- The genuinely open piece: proving that the simulation overhead
 129    from R-hat (global lattice minimization) to Turing machine
 130    (local tape operations) is superpolynomial.
 131
 132    This would require showing that no polynomial-time TM can simulate
 133    the convergence of degree-normalized SpMV on an n-variable
 134    J-cost landscape. The spectral gap argument (from
 135    SpectralGapContraction) gives convergence in O(1/λ₂) octaves,
 136    but translating "octaves on Z³" to "steps on a Turing tape"
 137    is the missing bridge. -/
 138structure OpenGap where