No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
157structure SATGadget where
158 /-- Number of variables -/
159 n : ℕ
160 /-- Number of clauses -/
161 m : ℕ
162 /-- Clause gadgets -/
163 clauses : List (ClauseGadget n)
164 /-- Variable assignment cells -/
165 var_positions : Fin n → ℤ
166 /-- Output cell position -/
167 output_position : ℤ
168 /-- Total tape width used -/
169 total_width : ℕ := n + 3 * m + 10
proof body
Definition body.
170
171/-- The evaluation time for a SAT instance with n variables and m clauses -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
H_SATCARuntime
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
depends on (11)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
ClauseGadget
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
-
Clause
in IndisputableMonolith.Complexity.RSatEncoding
decl_use
-
Clause
in IndisputableMonolith.Complexity.SAT.CNF
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
width
in IndisputableMonolith.Recognition.Certification
decl_use