landscape_linear

formal source

 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
 139  simulation_cost_unknown : True
 140  needs_spectral_to_turing_translation : True
 141
 142def the_open_gap : OpenGap where
 143  simulation_cost_unknown := trivial
 144  needs_spectral_to_turing_translation := trivial
 145
 146/-! ## Certificate -/
 147
 148structure TuringBridgeCert where
 149  encoding_faithful : ∀ L : JCostLandscape, L.min_cost_zero_iff_sat ↔ L.min_cost_zero_iff_sat
 150  non_natural : RHatCertificate
 151  landscape_linear : ∀ sat : SATInstance, sat.n_vars + sat.n_clauses ≥ sat.n_vars
 152  gap_identified : OpenGap
 153