structure
definition
TuringBridgeCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.TuringBridge on GitHub at line 148.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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