pith. machine review for the scientific record. sign in
def definition def or abbrev high

circuitLowerBoundCert

show as:
view Lean formalization →

The circuitLowerBoundCert packages two conditional lower bounds on Boolean circuit size for unsatisfiable CNF formulas: a linear bound from algebraic restrictions on the J-cost landscape and an exponential bound from topological obstructions. Researchers formalizing the P versus NP separation in the Recognition Science framework would cite this certificate when assembling the master proof. The definition is a direct one-line wrapper that delegates each field to the corresponding conditional theorem.

claimThe certificate for circuit lower bounds is the structure whose algebraic linear field applies the algebraic restriction theorem to give gate count at least $n$ and whose topological exponential field applies the topological obstruction theorem to give gate count at least $2^{n/k}$ for some positive integer $k$, for any unsatisfiable formula on $n$ variables decided by the circuit.

background

The module formalizes circuit lower bounds from J-frustration, where the J-cost satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. High J-frustration for unsatisfiable formulas forces circuits to have large size through algebraic restrictions that prevent local computation and topological obstructions that require global access. The upstream theorem circuit_lower_bound_algebraic states that given AlgebraicRestrictionHyp any circuit deciding an UNSAT formula on $n$ variables has size at least $n$. Its companion circuit_lower_bound_topological states that given TopologicalObstructionHyp any such circuit has exponential size.

proof idea

The definition constructs the CircuitLowerBoundCert structure by assigning the algebraic_linear field to the direct application of circuit_lower_bound_algebraic and the topological_exp field to the direct application of circuit_lower_bound_topological. Each assignment is a one-line wrapper that passes the hypothesis, the formula, the unsatisfiability witness, the circuit, and the decision proof to the respective conditional theorem.

why it matters in Recognition Science

This declaration supplies the lower_bound component to pvsNPMasterCert in the PvsNPAssembly module, completing the assembly of the full P versus NP certificate that also includes Laplacian, spectral gap, frustration, and non-naturalness components. It realizes the core claim of the module that high J-frustration implies super-polynomial circuit size, advancing the Recognition Science program toward P ≠ NP. The open hypotheses AlgebraicRestrictionHyp and TopologicalObstructionHyp remain to be discharged.

scope and limits

Lean usage

  lower_bound := circuitLowerBoundCert

formal statement (Lean)

 251def circuitLowerBoundCert : CircuitLowerBoundCert where
 252  algebraic_linear := fun hyp n f hunsat c hdec =>

proof body

Definition body.

 253    circuit_lower_bound_algebraic hyp f hunsat c hdec
 254  topological_exp := fun hyp n f hunsat c hdec =>
 255    circuit_lower_bound_topological hyp f hunsat c hdec
 256
 257end -- noncomputable section
 258
 259end CircuitLowerBound
 260end Complexity
 261end IndisputableMonolith

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.