abbrev definition def or abbrev

`Clause`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  17abbrev Clause (n : Nat) := List (Lit n)

Definition body.

  18
  19/-- CNF: conjunction of clauses, parameterized by number of variables. -/

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

SATGadget in IndisputableMonolith.Complexity.CellularAutomata decl_use
SATLedger in IndisputableMonolith.Complexity.ComputationBridge decl_use
clause_unchanged_by_flip in IndisputableMonolith.Complexity.JCostLaplacian decl_use
containsVar in IndisputableMonolith.Complexity.JCostLaplacian decl_use
Clause in IndisputableMonolith.Complexity.RSatEncoding decl_use
Clause in IndisputableMonolith.Complexity.RSatEncoding decl_use
CNFFormula in IndisputableMonolith.Complexity.RSatEncoding decl_use
rhat_is_non_natural in IndisputableMonolith.Complexity.RSatEncoding decl_use
BPStep in IndisputableMonolith.Complexity.SAT.Backprop decl_use
clauseUnit in IndisputableMonolith.Complexity.SAT.Backprop decl_use
clauseUnit_correct in IndisputableMonolith.Complexity.SAT.Backprop decl_use
valueOfClause in IndisputableMonolith.Complexity.SAT.Backprop decl_use
CNF in IndisputableMonolith.Complexity.SAT.CNF decl_use
evalClause in IndisputableMonolith.Complexity.SAT.CNF decl_use
consistent_completeStateFrom in IndisputableMonolith.Complexity.SAT.Completeness decl_use
Constraint in IndisputableMonolith.Complexity.SAT.PC decl_use
mentionsVarClause in IndisputableMonolith.Complexity.SAT.PC decl_use

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Clause in IndisputableMonolith.Complexity.RSatEncoding decl_use
CNF in IndisputableMonolith.Complexity.SAT.CNF decl_use
Lit 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
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use