CNFFormula — Recognition explainer

formal statement (Lean)

  48structure CNFFormula (n : ℕ) where
  49  clauses : List (Clause n)
  50  var_count : ℕ
  51  var_count_eq : var_count = n
  52
  53/-- An assignment is a Boolean function on variables. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

CircuitDecides in IndisputableMonolith.Complexity.CircuitLedger decl_use
CircuitLedgerCert in IndisputableMonolith.Complexity.CircuitLedger decl_use
CircuitSeparation in IndisputableMonolith.Complexity.CircuitLedger decl_use
CircuitWithEvalDecides in IndisputableMonolith.Complexity.CircuitLedger decl_use
DefectMoat in IndisputableMonolith.Complexity.CircuitLedger decl_use
defect_moat_zero_iff_sat in IndisputableMonolith.Complexity.CircuitLedger decl_use
moat_width_unsat in IndisputableMonolith.Complexity.CircuitLedger decl_use
moat_zero_sat in IndisputableMonolith.Complexity.CircuitLedger decl_use
AlgebraicRestrictionHyp in IndisputableMonolith.Complexity.CircuitLowerBound decl_use
circuit_lower_bound_algebraic in IndisputableMonolith.Complexity.CircuitLowerBound decl_use
CircuitLowerBoundCert in IndisputableMonolith.Complexity.CircuitLowerBound decl_use
circuit_lower_bound_topological in IndisputableMonolith.Complexity.CircuitLowerBound decl_use
p_neq_np_conditional in IndisputableMonolith.Complexity.CircuitLowerBound decl_use
TopologicalObstructionHyp in IndisputableMonolith.Complexity.CircuitLowerBound decl_use
UniformTopologicalObstructionHyp in IndisputableMonolith.Complexity.CircuitLowerBound decl_use
CostConnected in IndisputableMonolith.Complexity.JCostLaplacian decl_use
costConnected_refl in IndisputableMonolith.Complexity.JCostLaplacian decl_use
jcostDegree in IndisputableMonolith.Complexity.JCostLaplacian decl_use
jcostDegree_nonneg in IndisputableMonolith.Complexity.JCostLaplacian decl_use
jcostEdgeWeight in IndisputableMonolith.Complexity.JCostLaplacian decl_use
jcostEdgeWeight_le_clauses in IndisputableMonolith.Complexity.JCostLaplacian decl_use
jcostEdgeWeight_le_varDegree_prop in IndisputableMonolith.Complexity.JCostLaplacian decl_use
jcostEdgeWeight_nonneg in IndisputableMonolith.Complexity.JCostLaplacian decl_use
jcostEdgeWeight_symm in IndisputableMonolith.Complexity.JCostLaplacian decl_use
JCostLaplacianCert in IndisputableMonolith.Complexity.JCostLaplacian decl_use
JCostLaplacianForm in IndisputableMonolith.Complexity.JCostLaplacian decl_use
laplacian_form_const_zero in IndisputableMonolith.Complexity.JCostLaplacian decl_use
laplacian_form_nonneg in IndisputableMonolith.Complexity.JCostLaplacian decl_use
laplacian_form_zero_imp in IndisputableMonolith.Complexity.JCostLaplacian decl_use
varDegree in IndisputableMonolith.Complexity.JCostLaplacian decl_use

… and 10 more

depends on (40)

Lean names referenced from this declaration's body.

all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Assignment in IndisputableMonolith.Complexity.RSatEncoding decl_use
Assignment in IndisputableMonolith.Complexity.RSatEncoding decl_use
Assignment in IndisputableMonolith.Complexity.RSatEncoding decl_use
Clause in IndisputableMonolith.Complexity.RSatEncoding decl_use
Assignment in IndisputableMonolith.Complexity.SAT.CNF decl_use
Assignment in IndisputableMonolith.Complexity.SAT.CNF decl_use
Assignment in IndisputableMonolith.Complexity.SAT.CNF decl_use
Clause in IndisputableMonolith.Complexity.SAT.CNF decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use

… and 10 more