def
definition
turingBridgeCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Complexity.TuringBridge on GitHub at line 154.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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