Two-half Nechiporuk-style lower bounds for MCSP #
This module extends the left-half Nechiporuk infrastructure in
Complexitylib.Algebraic.LowerBound.MCSP.SubcubeRepetition with reusable infrastructure and
two-half lower bounds.
Reusable infrastructure #
- Exact-cost persistence under subcube duplication.
costComplexity_pairTruthTable_selfis thepairTruthTableform ofcostComplexity_muxTarget_self. Iterating it (iterPairTruthTable) embedsexactCostSet ... n sinjectively intoexactCostSet ... (n + k) s(iterPairTruthTable_mem_exactCostSet,card_exactCostSet_le_add). - Coordinate-translation symmetry of subfunction counts. A Boolean function invariant under a
coordinate permutation
ehas the same number of Nechiporuk subfunctions onY.map eas onY(card_subfunctions_map_equiv), specialized totableTranslate afor the De Morgan cost and binary MCSP scalars. - Right-half blocks.
rightBlock Y₀embedsY₀ ⊆ Fin (2 ^ n)into the upper half ofFin (2 ^ (n + 1)). It is the translate ofleftBlock Y₀by flipping the leading input bit (rightBlock_eq_map_tableTranslate), so the left-half subfunction bounds transfer to it (mcsp_card_image_restrictTo_le_subfunctions_rightBlock), and it is disjoint from every left-half block (disjoint_leftBlock_rightBlock).
Two-half lower bounds #
Combining the disjoint left and right halves gives (exactCostSet ... n s).card ^ 2 ≤ 4 * 16 ^ F.leaves for Binary.Formula (mcsp_binaryFormula_leaves_lower_bound) and analogous
trade-offs for Binary.signature circuits with bounded sharing
(mcsp_binary_circuit_active_sharing_lower_bound, mcsp_binary_circuit_sharing_lower_bound).
These bounds are linear in the input length N = 2 ^ (n + 1): since
(exactCostSet ... n s).card ≤ 2 ^ (2 ^ n), they yield at most about N / 4 leaves (and, for
circuits, about N / 4 - O(k + f) gates). They are therefore not stronger than the
Khrapchenko-style De Morgan formula bound mcsp_formula_leaves_lower_bound (at least N leaves)
or the trivial N - 1 circuit bound coming from full input support in
Complexitylib.Algebraic.LowerBound.MCSP.NonVacuity. Their interest is that they are proved
over the full binary basis by the Nechiporuk subfunction-counting method, which also tolerates
bounded sharing.
Exact-cost persistence under iterated subcube duplication #
Repeating a truth table tt across both halves of the (n + 1)-cube preserves its
DeMorgan.binaryCost complexity. This is the pairTruthTable form of
costComplexity_muxTarget_self.
pairTruthTable tt tt has exact DeMorgan.binaryCost complexity s if and only if tt
does.
Duplicating an exact-cost truth table across both halves of the (n + 1)-cube preserves
membership in exactCostSet.
The diagonal map tt ↦ pairTruthTable tt tt injects exactCostSet ... n s into
exactCostSet ... (n + 1) s, so (exactCostSet ... n s).card is non-decreasing in n.
iterPairTruthTable k tt belongs to exactCostSet ... (n + k) s if and only if tt belongs to
exactCostSet ... n s.
Iterated subcube duplication preserves membership in exactCostSet.
Non-emptiness of exactCostSet persists across k subcube doublings.
(exactCostSet ... n s).card is monotonically non-decreasing across k subcube doublings.
Coordinate-permutation and tableTranslate invariance of subfunction counts #
If a Boolean function f : Cslib.BooleanFunction N is invariant under a coordinate permutation
e : Fin N ≃ Fin N (∀ x, f (x ∘ e) = f x), then for every block Y : Finset (Fin N), the
number of Nechiporuk subfunctions of f on Y.map e.toEmbedding equals the number on Y.
Right-half coordinate blocks #
Any left-half block leftBlock Y₀ is disjoint from any right-half block rightBlock Y₁.
Flipping the leading input bit (tableTranslate (Fin.cons true fun _ => false)) sends the
left-half embedding to the right-half embedding.
The right-half block rightBlock Y₀ is the translate of the left-half block leftBlock Y₀
by flipping the leading input bit.
Nechiporuk subfunction lower bound for MCSP on arbitrary right-half blocks:
For 1 ≤ s and any subset Y₀ : Finset (Fin (2 ^ n)), distinct restrictions restrictTo Y₀ tt
of truth tables tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s induce
distinct subfunctions of mcspCostScalar ... (n + 1) s on rightBlock Y₀. Transferred from
mcsp_card_image_restrictTo_le_subfunctions_leftBlock by rightBlock_eq_map_tableTranslate.
Full-right-half Nechiporuk subfunction lower bound for MCSP: For 1 ≤ s, every truth table
tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s induces a distinct subfunction
of mcspCostScalar ... (n + 1) s on the right-half coordinate block rightBlock Finset.univ.
Right-block Binary.Formula leaf lower bound for MCSP: For 1 ≤ s, any binary formula
F : Binary.Formula (2 ^ (n + 1)) computing
mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s satisfies
((exactCostSet ... n s).image (restrictTo Y₀)).card ≤ 2 * 16 ^ F.leavesIn (rightBlock Y₀)
for every coordinate subset Y₀ : Finset (Fin (2 ^ n)).
Full-right-half Binary.Formula leaf lower bound for MCSP: For 1 ≤ s, any binary formula
F : Binary.Formula (2 ^ (n + 1)) computing
mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s satisfies
(exactCostSet ... n s).card ≤ 2 * 16 ^ F.leavesIn (rightBlock Finset.univ).
Two-half Binary.Formula leaf lower bound for MCSP #
Since leftBlock Y₀ and rightBlock Y₁ are disjoint, the leaves of any formula F in
leftBlock Y₀ and in rightBlock Y₁ sum to at most F.leaves.
Two-half Binary.Formula leaf lower bound for MCSP: For 1 ≤ s, any binary formula
F : Binary.Formula (2 ^ (n + 1)) computing
mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s satisfies
(exactCostSet ... n s).card ^ 2 ≤ 4 * 16 ^ F.leaves.
Since (exactCostSet ... n s).card ≤ 2 ^ (2 ^ n), this forces at most about
2 ^ (n + 1) / 4 leaves: it is linear in the input length and weaker than the De Morgan
Khrapchenko bound mcsp_formula_leaves_lower_bound.
Bounded-sharing Binary.signature circuit lower bounds for MCSP #
Since leftBlock Y₀ and rightBlock Y₁ are disjoint, the primary input leaves of any
SharedProgram in leftBlock Y₀ and rightBlock Y₁ sum to at most
P.inputLeaves (2 ^ (n + 1)).
Active-block bounded-sharing Binary.signature circuit lower bound for MCSP:
For 1 ≤ s, any single-output circuit c : Circuit Binary.signature (2 ^ (n + 1)) 1 computing
mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s satisfies
(exactCostSet ... n s).card ^ 2 ≤ 2 ^ (activeSharedGateCount c (leftBlock univ) + activeSharedGateCount c (rightBlock univ) + 2) * 16 ^ (c.size + KW.sharedGateCount c + 1 + activeSharedFanOut c (leftBlock univ) + activeSharedFanOut c (rightBlock univ)).
Like mcsp_binaryFormula_leaves_lower_bound, this yields only a size bound linear in the input
length (about 2 ^ (n + 1) / 4 minus sharing terms), weaker than the trivial full-support bound.
Global bounded-sharing Binary.signature circuit lower bound for MCSP:
For 1 ≤ s, any single-output circuit c : Circuit Binary.signature (2 ^ (n + 1)) 1 computing
mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s with
KW.sharedGateCount c ≤ k and Nechiporuk.sharedFanOut c ≤ f satisfies
(exactCostSet ... n s).card ^ 2 ≤ 2 ^ (2 * k + 2) * 16 ^ (c.size + k + 1 + 2 * f).
This gives c.size ≥ about 2 ^ (n + 1) / 4 - O(k + f), linear in the input length and weaker than
the trivial full-support bound.