IndisputableMonolith.Complexity.CircuitLowerBound
CircuitLowerBound states the algebraic restriction hypothesis: d'Alembert structure on J-cost differences forces any Boolean circuit computing a high-frustration function to access Ω(n) input bits at once. Researchers resolving P vs NP inside Recognition Science cite it to convert J-frustration ≥ τ into a depth lower bound log₂(τ/S). The module assembles the claim from the circuit ledger, J-cost Laplacian, and RSatEncoding without supplying an unconditional proof.
claimFor any Boolean circuit $C$ of size $S$ computing a function $f$ whose J-frustration (on the J-cost landscape of its truth table) satisfies $JFrust(f) ≥ τ$, the depth of $C$ is at least $log₂(τ/S)$.
background
The module operates inside the Complexity domain and imports CircuitLedger (Boolean circuits viewed as restricted sub-ledgers of the global J-cost gradient), JCostLaplacian (weighted hypercube graph whose edge weights are absolute differences of satJCost), JFrustration (topological depth of the barrier around satisfying assignments), RSatEncoding (R̂ reaches zero J-cost in O(n) steps for satisfiable instances and leaves a non-contractible obstruction for unsatisfiable ones), and Constants (τ₀ = 1 tick). These supply the J-cost landscape and the non-natural character of frustration that the algebraic restriction hypothesis then constrains.
proof idea
This is a definition module, no proofs. It declares AlgebraicRestrictionHyp together with the two concrete lower-bound statements circuit_lower_bound_algebraic and circuit_lower_bound_topological, plus the auxiliary objects exp_dominates_poly and p_neq_np_conditional that package the hypothesis for downstream use.
why it matters in Recognition Science
The module supplies the Phase-3 conditional step in PvsNPAssembly: high J-frustration implies exponential circuit size once the uniform topological obstruction is granted. It therefore closes the algebraic half of the P ≠ NP resolution path that begins from the non-natural character of J-frustration established in RSatEncoding and JFrustration.
scope and limits
- Does not prove the algebraic restriction unconditionally.
- Does not treat quantum or non-Boolean circuit models.
- Does not quantify the precise constant hidden in the Ω(n) access requirement.
- Does not address average-case rather than worst-case frustration.
used by (2)
depends on (5)
declarations in this module (11)
-
structure
AlgebraicRestrictionHyp -
structure
TopologicalObstructionHyp -
theorem
circuit_lower_bound_algebraic -
theorem
circuit_lower_bound_topological -
structure
UniformTopologicalObstructionHyp -
theorem
exp_dominates_poly -
theorem
p_neq_np_conditional -
structure
AlgebraicRestrictionProofSketch -
def
the_proof_sketch -
structure
CircuitLowerBoundCert -
def
circuitLowerBoundCert