def definition def or abbrev

`satJCost`

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

formal statement (Lean)

  81noncomputable def satJCost {n : ℕ} (f : CNFFormula n) (a : Assignment n) : ℝ :=

Definition body.

  82  (f.clauses.filter (fun c => !c.satisfiedBy a)).length
  83
  84/-- J-cost is nonneg (number of unsatisfied clauses ≥ 0). -/

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

CircuitLedgerCert in IndisputableMonolith.Complexity.CircuitLedger decl_use
CircuitSeparation in IndisputableMonolith.Complexity.CircuitLedger decl_use
moat_width_unsat in IndisputableMonolith.Complexity.CircuitLedger decl_use
moat_zero_sat in IndisputableMonolith.Complexity.CircuitLedger decl_use
jcostEdgeWeight in IndisputableMonolith.Complexity.JCostLaplacian decl_use
jcostEdgeWeight_le_clauses in IndisputableMonolith.Complexity.JCostLaplacian decl_use
LandscapeDepth in IndisputableMonolith.Complexity.JFrustration decl_use
landscapeDepth_unsat in IndisputableMonolith.Complexity.JFrustration decl_use
PvsNPDissolution in IndisputableMonolith.Complexity.PvsNPAssembly decl_use
RSATSeparation in IndisputableMonolith.Complexity.RSatEncoding decl_use
satJCost_nonneg in IndisputableMonolith.Complexity.RSatEncoding decl_use
satJCost_zero_iff in IndisputableMonolith.Complexity.RSatEncoding decl_use
sat_reaches_zero in IndisputableMonolith.Complexity.RSatEncoding decl_use
sat_recognition_time_bound in IndisputableMonolith.Complexity.RSatEncoding decl_use
unsat_cost_lower_bound in IndisputableMonolith.Complexity.RSatEncoding decl_use
unsat_positive_jcost in IndisputableMonolith.Complexity.RSatEncoding decl_use
empty_formula_flat_landscape in IndisputableMonolith.Complexity.SpectralGap decl_use

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Assignment in IndisputableMonolith.Complexity.RSatEncoding decl_use
CNFFormula in IndisputableMonolith.Complexity.RSatEncoding decl_use
Assignment in IndisputableMonolith.Complexity.SAT.CNF decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use