Polynomial-gate lower bounds for the explicit rational Cauchy family

One rational matrix family works over every characteristic-zero field, including the rationals, reals, and complexes. The coefficient applies to arbitrary binary polynomial gates, with unrestricted degree, coefficients, depth, and fanout. Explicit nullary gate occurrences are counted in the circuit size.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.eventually_lt_size_cauchyCharZero {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [CharZero F] (σ : Signature) (I : Interpretation σ F), IsPolynomial I → ∀ (c : Circuit σ N N), c.FanInAtMost 2 → (c.Computes I fun (x : Fin N → F) => (cauchyCharZero F N).mulVec x) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑N < ↑c.size

The rational Cauchy map requires the Gaussian linear coefficient over any polynomial basis.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.eventually_lt_size_cauchyCharZero_full {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [CharZero F] (c : Circuit (signature F) N N), c.FanInAtMost 2 → (c.Computes (interpretation F) fun (x : Fin N → F) => (cauchyCharZero F N).mulVec x) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑N < ↑c.size

The canonical polynomial signature permits arbitrary coefficients inside each gate.