OpenGap

formal source

 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
 154def turingBridgeCert : TuringBridgeCert where
 155  encoding_faithful := encoding_faithful
 156  non_natural := rhat_is_non_natural
 157  landscape_linear := landscape_linear
 158  gap_identified := the_open_gap
 159
 160end
 161
 162end IndisputableMonolith.Complexity.TuringBridge