The cutwidth lower bound

This umbrella collects the (4 - ε) n lower bound for rectangle-free functions over the full binary basis. FourN combines cut counting, circuit wiring, compression, and the proved sharp cubic bisection and pathwidth bounds. Nondeterministic extends the conclusion to arbitrarily many witness inputs; AverageCase gives the agreement bound for balanced functions. SingleCut proves the single-cut criterion: one split of a circuit's wires, crossed by |A| forward and |B| backward signals with i inputs on one side, bounds the accepted inputs of a K-rectangle-free function by K (2 ^ (i + |B|) + 2 ^ (n - i + |A|)). MultiOutput.Ordering transfers the graph-ordering hypothesis to programs over any signature with fan-in two and any number of outputs: a ranking of the wires whose prefixes are crossed by at most (A + η) (s - n)⁺ + O(log (n + s)) signals, component by component. MultiOutput.Rank bounds the signals crossing any split of a circuit computing a linear map x ↦ M x over a finite field below by rank M[Y_T, X_S] + rank M[Y_S, X_T]. MultiOutput.TotallyRegular combines the two: a fan-in-two circuit over a finite field computing a totally regular N × N map, such as an explicit Cauchy matrix over ZMod q, has more than (1 + 1/(2 κ_E) - ε) N ≥ (41/9 - ε) N gates for all large N. MultiOutput.Quadratic proves the single-output analogue for quadratic forms x ↦ xᵀ M x: every split is crossed by at least rank (M + Mᵀ)[X_S, X_T] signals, so a fan-in-two circuit over a finite field computing such a form with M + Mᵀ totally regular, such as the Hankel Cauchy matrix 1 / (i + j + 2) over ZMod q, has more than (1 + 1/(4 κ_E) - ε) N ≥ (25/9 - ε) N gates for all large N. The rank-cut bound also holds when a combination of several outputs is the quadratic form. MultiOutput.Restrict restricts the fibre bound to product domains and to the inputs with some coordinates fixed. MultiOutput.FieldMul applies it to multiplication in a degree-n extension of a finite field, written in a basis: fixing one factor makes it linear, and averaging over the fixed factor shows that a fan-in-two circuit over any signature has more than (2 + 1/(2 κ_E) - ε) n ≥ (50/9 - ε) n gates for all large n, in particular for GF(2 ^ n) over the full binary basis. MultiOutput.MatMul.Tripartite proves the charging combinatorics of the terminal graph of n × n matrix multiplication, the complete tripartite graph on the three index sets, and the threshold prefix of a ranking. MultiOutput.MatMul bounds each of the three charges of a split by its crossing signals, through the restricted rank-cut bound with one factor fixed and the rank-cut bound for the Hessian of a combination of the outputs, so a fan-in-two circuit over any finite field computing the n × n matrix product has more than (2 + 1/(4 κ_E) - ε) n² ≥ (34/9 - ε) n² gates for all large n, in particular over the full binary basis for the product over GF(2). MultiOutput.Taylor proves the algebraic counterpart for polynomial gates over every field: evaluating the circuit over L[s, t]/(s², t²) at a + s v + t u, cut and paste shows that every split is crossed by at least rank J[O_T, X_S] + rank J[O_S, X_T] signals, J the Jacobian of the outputs at any point, and by at least rank H[X_S, X_T] signals, H the Hessian of any linear combination of the outputs. MultiOutput.PolyMul applies the Hessian bound to polynomial multiplication with Hankel weights t ^ (m²) over K(t), totally regular in every characteristic: a fan-in-two circuit with polynomial gates over any field formally computing the product of two polynomials with n coefficients has more than (2 + 1/(2 κ_E) - ε) n ≥ (50/9 - ε) n gates for all large n; the same holds for arithmetic circuits over infinite fields with free constants and for arbitrary gates over ZMod q, q > 2n prime. MultiOutput.Quadratic.Polynomial transfers the quadratic-form bound to polynomial gates over every field: the Hessian of xᵀ M x is M + Mᵀ, so the same (25/9 - ε) N bound holds, for example for xᵀ (1 / (i + j + 2)) x over every field of characteristic zero.

Bisection.Helpful completes the graph theorem. Its proof uses the first boundary normalization phase, a partition into bounded connected clusters, red-edge incidence counting, and the exact boundary lift. The resulting bounded helpful-set theorem combines with accumulation and logarithmic-cost rebalancing. The second normalization phase, thin-path systems, weighted core forests, and simultaneous restoration remain available as separate graph APIs.

Extractor transfers flat-source sumset extraction to the hard-family properties. Extractor.Padding permits any fixed error below one half by adding a balancing bit. Extractor.SourceReduction proves that the stated low-order parity bounds on enough good source fixings imply extraction with error 35/72, by composing the moment, majority, and conditioning arguments. Extractor.Sampler supplies the finite extractor-to-sampler conversion and amplification; SourceReduction.Selection proves the simultaneous choice of good parity coordinates from individual bad-seed bounds. Condenser.Polynomial defines the underlying modular polynomial map and proves its source linearity. Condenser.Expansion proves its finite neighbor expansion for a supplied irreducible modulus, using interpolation and quotient-field root counting. Condenser.Lossless.Polynomial converts this to flat-source lossless condensation while preserving the seed; the mixture layer extends it to all larger flat supports. Modulus.Binomial supplies a sparse irreducible family from a noncube coefficient, and its Extension module proves that the quotient root supplies another noncube. Modulus.Binary gives an explicit irreducible binary trinomial family, its fixed-width quotient codec, and a uniform encoded modular-powering program. Its Extension module identifies the binomial tower with a larger binary quotient. Condenser.Encoding.Correctness proves that the actual uniform FP program, using coefficient transposition and modular Horner evaluation, computes the polynomial condenser and preserves source addition. Source packing preserves all fixed-length inputs within capacity. Encoding.Lossless transfers the flat-source and mixture guarantees to this actual program. Parameters.Sparse proves that field bit lengths twice a power of three preserve the intended output rate with the appropriate powering exponent. Parameters.Explicit selects the dimensions from source length, entropy, inverse error, and rate; Encoding.Explicit computes them uniformly and proves error at most 2^(-e) for the resulting program. Strong retains the seed in its statistical comparison. Hashing proves the sharp leftover-hash bound and instantiates it with uniform binary field multiplication and truncation. Strong.Composition retains both independent seeds through a mixture-aware condenser-to-extractor argument. Strong.OneShot joins these results to an actual linear FP bit program, extracting ell bits with error 2^(-e) from sources of min-entropy at least ell + 2*e. Strong.FlatMixture decomposes arbitrary capped weights into exact-size flat sources. Strong.Weighted extends both extraction and lossless condensation to these weights with the same error. Strong.Weighted.Coupling repairs a marginal while retaining correlations. Strong.Weighted.Conditional completes null rows and retains the actual side-information law. Its Transport layer preserves conditional distance under tag-dependent output bijections. Strong.Weighted.Transcript factors the actual law after left, right, or adaptive observations. Its Envelope layer charges only source-side messages against the average entropy budget. Coupling.Conditional replaces a marginal at its exact average distance while retaining the transcript and the other coordinate jointly. Coupling.Factored repairs a distinguished right state to uniform while preserving both original sources and the factored law. Continuation costs one repair distance when the retained marginal is preserved, and at most two otherwise. Strong.Weighted.Leakage bounds extraction error using an average joint-mass envelope; individual conditional sources need not all retain the extractor's entropy threshold. Strong.Weighted.Merging combines this with a seed close to uniform given a right-side observation, retaining the entire right variable and charging its seed error once. Merging.Independence merges two possibly overlapping tampering sets with error 2*epsilon+delta under the explicit average-envelope budget. Strong.Weighted.Affine extracts from a source combined with a correlated right mask, retaining the full right state whenever fixed-mask output transport is bijective. Strong.Weighted.Alternating switches extraction sides after a message and composes an actual affine extraction with the next call, retaining the entire opposite source. Strong.Weighted.LookAhead proves the actual two-round, one-tampering transition, retaining the complete right state and both first outputs with explicit entropy charges. Its UniformState layer derives the next look-ahead from a nearly uniform refreshed state. Refresh proves both first refresh estimates with exact transcript factors and original-source envelopes. FixedTampering handles a left-only tampered seed in the next extraction and refresh, retaining the original left source. Its Second layer handles the second look-ahead output and proves that a normalized left observation preserves the original average seed discrepancy exactly. UniformRefresh handles either selected refresh from whole-state uniformity, with arbitrary correlated tampering and no pointwise current-state entropy premise. Strong.Weighted.Perturbation handles seeds close to jointly independent uniform seeds, including the extra distance needed to retain the actual tag-and-seed marginal. Strong.Block.Splitting repairs a two-block source with a quantified error. Strong.Block supplies the general prefix-based block-source invariant. Strong.Block.Splitting.Iterated splits every dependent pair into successive half-blocks at error at most t * 2^(-e), preserving the required conditional caps. Its family corollary retains the earlier seed with the same joint error. Strong.Block.Condenser applies one seed across dependent blocks with at most one condenser error per block. Its extraction corollary compares the entire output tuple with uniform; the scheduled condenser has the same shared-seed guarantee on actual decoded blocks. Strong.OneShot.Block similarly reuses one pair of field seeds across all leaves, with error at most t * 2^(-e). Strong.Weighted.SeedStep retains earlier randomness and adds a fresh seed without increasing a prior joint error. Strong.Block.Level combines condensation and splitting; Strong.Block.Recursion iterates the actual finite maps with an explicit error sum and one seed per level. Its extraction theorem joins an initial condenser, all levels, and a final block extractor, with the finite dyadic error budget. Fixed-seed additivity is preserved when the supplied component maps preserve addition. Condenser.Encoding.Explicit.Pair splits the actual condenser output into two equal Boolean-vector halves with the same entropy threshold and error. Its splitting budget supplies the two finite entropy inequalities for a level. Condenser.Encoding.Explicit.Block.Program computes one shared-seed block level uniformly in polynomial time, with exact fixed-width tuple semantics. Its correctness theorem identifies the result with the statistical level map. Strong.Block.Recursion.Scheduled specifies all component maps and a constant-rate integer schedule, discharges its entropy budgets, and proves the strong-extraction guarantee. Its seed cardinality and finite seed-bit bound are explicit, and its actual maps preserve source XOR for fixed seeds. Scheduled.Asymptotics supplies a fixed family with logarithmic seed length, sublinear source entropy, and any fixed power of logarithmic output length. Scheduled.Codec identifies its retained seed tuples with exact-length bit words. Scheduled.Program evaluates initial condensation, the bounded block loop, and the final shared extraction uniformly in polynomial time, including all parameter generation. Its correctness theorem identifies the full output with the statistical tuple. Program.Family gives one polynomial-time string evaluator for each fixed family and proves eventual agreement on all source inputs and canonical seeds. Scheduled.Boolean supplies the actual program on fixed-length Boolean sources and seeds, with the strong-extraction guarantee and fixed-seed XOR law. Its public statistical statements require no field enumeration instances. Scheduled.Affine applies this actual program to a source XOR a correlated right mask, with the full right state retained and an explicit average-entropy error budget. Scheduled.BoundedDepth bounds its actual seed width and entropy at fixed depths, providing finite parameters for matching the short alternating calls. Scheduled.Matched runs the actual bit program with those matched widths, retaining the full padded seed in its strong guarantee. Its Program layer gives a total uniform polynomial-time runtime and canonical agreement, including arbitrary seed tails. Matched.Growing supplies the statistical guarantee at variable depth under an explicit depth/error/logarithm budget. Its Program layer gives a total polynomial-time evaluator at depth clog 2 (t+1)+64, with polynomial block count in the unary parameter t, exact vector agreement, and ignored seed tails. Matched.Affine retains the full correlated right state when the source is XORed with its mask. CorrelationBreaker.FlipFlop.Program composes the actual three-call look-ahead and eight-call advice-bit step, with exact vector semantics and registered polytime proofs. Its LookAhead layer specializes the retained two-round statistical guarantee to these actual calls without supplied extractors or an intermediate-seed hypothesis. Its UniformState layer instantiates the repaired-state estimate for the actual program. FlipFlop.Opposite.False proves the complete honest-zero/tampered-one execution from original source envelopes and the initial seed error, retaining both histories, the tampered final output, and the full original left state. Opposite.True proves the other orientation from the original source and current-state envelopes and prefix error. Transcript factors the actual pair of executions for arbitrary advice bits into normalized original-source kernels. It gives exact envelope growth of D^8 on the left and C^4 on the right, before observing final outputs. Preservation.Half proves either selected refresh, retaining either tampered refresh, when the incoming tampered state is fixed by the transcript. Its premises are whole-state honest uniformity and the original source envelopes, with no current-state entropy cap. Opposite.UniformState supplies the first differing advice bit from whole-state uniformity. Preservation.Weak and Preservation.Step cover complete steps before and after that difference. Transcript.Output identifies their exact original-law factors, including the tampered final state in the separated phase. CorrelationBreaker.Advice.Program computes the complete advice fold and a final left-source extraction. Its uniform FP proof bounds the entire encoded loop state. Advice.Extraction constructs the complete invariant from the original sources and proves a strong finite bound for unequal equal-length advice, retaining the original right state and actual tampered output. Its explicit entropy reserve and local error schedule give any dyadic target. Advice.Parameters checks all finite program guards and reserves; Advice.Truncation preserves the guarantee for shorter requested outputs. Advice.Extraction.Parameters combines them into the actual requested-width guarantee with every numerical side condition discharged by the chooser. Advice.Extraction.Program computes that chooser and requested output in one total polynomial-time evaluator, with exact agreement on canonical source words. Advice.Extraction.Perturbed allows a jointly near-uniform honest right input and charges its discrepancy once because the actual retained marginal is preserved. Advice.Extraction.Alternating swaps source sides after a right observation, paying its alphabet size in the source envelope and requiring the preceding seed estimate. Affine.PhaseOne defines the actual three-call first phase and its complete transcript. Its Initial theorem derives the first extracted seed estimate from the original uniform right input and left envelope, retaining every first right message. Its Transcript theorems give exact original-law factors and envelope totals for all three observations, including normalized null rows. Second derives the advice-generated seed guarantee from those original hypotheses. Final and Extraction prove the complete actual first phase's pairwise guarantee, retaining the executed transcript, original right state, and one tampered output. The original-left contributions satisfy the same bound for later merging, and finite source reserves give any dyadic error target. No intermediate security witness is assumed. PhaseOne.Parameters supplies all finite component guards and entropy reserves with a total explicit chooser; its unary generators are uniformly polynomial-time. Extraction.Parameters proves the actual pairwise error 2^-target from the original source hypotheses and chosen mass bound, with no remaining numerical guard premise. PhaseOne.Program computes all three calls in one total polynomial-time evaluator. Canonical agreement needs the three finite component guards, with no statistical premises. Its Parameters wrapper computes the full chooser and normalizes the right word; canonical agreement then has no numerical or source-capacity premise. Strong.Weighted.Merging.Smooth constructs a conditional uniform-coordinate repair, preserving all original left observations and charging its distance once. It provides the smooth-source consumer needed by the next subset-doubling stage. NearHalving uses a rate increasing with depth and a near-halving entropy schedule. Its rounded parameters give an actual extractor on 8*b bits at entropy 2*b, with b output bits, error 1/4, and seed length at most a cubic logarithm, for all sufficiently large b. Exact seed codecs and payload invariants identify the complete bit program with this statistical map, including unused seed padding. Gamma.Padded reads this same total polynomial-time program on a seed whose width is the explicit cubic-logarithmic budget; the entire seed is uniform and retained in the strong guarantee. Affine.Iteration and its selected parameters complete the actual subset-doubling induction. SourceReduction.Construction composes the actual sampler, fixed affine tests, XOR, and majority. Its asymptotic layer proves sublinear source entropy and eventual numerical guards. Its uniform layer bounds every enumeration loop and provides one total polynomial-time evaluator for a fixed balanced family. SourceReduction.Construction.Hardness proves the unconditional (4-ε)n lower bound for that family, measured at the full input length; its language is in P. Aggregate preserves the Gaussian coefficient, about 4.5625, for binary circuits augmented by arbitrary finite commutative-monoid gates with sublinear total budget. The budget counts one output-guess bit and the ceiling logarithm of the register cardinality per special occurrence. It includes noninvertible AND, OR, and capped counting, as well as modular and symmetric gates. Superconcentrator applies the graph-ordering hypothesis to superconcentrators: every N-superconcentrator has at least (2 + 1/A - ε) N edges, about 5.5625 N for the edge-score coefficient, improving the 5 N of Lev and Valiant.