module module

`IndisputableMonolith.Complexity.RSatEncoding`

show as: view Lean formalization →

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

generate prose now

used by (8)

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

IndisputableMonolith.Complexity.CircuitLedger module_import
IndisputableMonolith.Complexity.CircuitLowerBound module_import
IndisputableMonolith.Complexity.JCostLaplacian module_import
IndisputableMonolith.Complexity.JFrustration module_import
IndisputableMonolith.Complexity.NonNaturalness module_import
IndisputableMonolith.Complexity.PvsNPAssembly module_import
IndisputableMonolith.Complexity.SpectralGap module_import
IndisputableMonolith.Core.Complexity module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Complexity.BalancedParityHidden module_import
IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.LedgerForcing module_import

declarations in this module (14)

structure Clause L41
structure CNFFormula L48
def Assignment L54
def satJCost L81
theorem satJCost_nonneg L85
theorem satJCost_zero_iff L90
theorem sat_reaches_zero L123
theorem sat_recognition_time_bound L129
theorem unsat_positive_jcost L139
theorem unsat_cost_lower_bound L151
theorem rs_adversarial_lower_bound L169
theorem rhat_is_non_natural L178
structure RSATSeparation L247
theorem rsatSeparation L261