[barni120400]

Closes #4734 (milestone 4 of 4). Stacked on #4746 → #4745 → #4739: until those land, the diff also shows their modules. This PR's own change is HittingSet/ConstantDepth.lean, the formula form of the LST lower bound in CircuitLowerBound.lean, two lemmas moved into SetMultilinear.lean, the test, the manual section and the registry entry.

What this adds

A finite form of Limaye–Srinivasan–Tavenas, Corollary 6: subexponential hitting sets for constant-depth formulas, over fields of characteristic zero, for every real ε > 0 (eventually_isHittingSet_constantDepthHittingSet_rpow and its circuit form, with t = ⌈ε⁻¹⌉), and at ε = 1/t in the separate statements below.

noncomputable def constantDepthHittingSet (K : Type*) [Field K] (c t n : ℕ) : Finset (Fin n → K)

theorem eventually_isHittingSet_constantDepthHittingSet (K : Type*) [Field K] [CharZero K]
    (Δ c t : ℕ) (ht : 1 ≤ t) :
    ∀ᶠ n in atTop, IsHittingSet (constantDepthHittingSet K c t n)
      {p | ∃ C : SPFormula K n, C.polynomial = p ∧ C.productDepth ≤ Δ ∧ C.nodeCount ≤ n ^ c}

theorem eventually_card_constantDepthHittingSet_le (K : Type*) [Field K] (c t : ℕ) (ht : 1 ≤ t) :
    ∀ᶠ n in atTop, ((constantDepthHittingSet K c t n).card : ℝ) ≤ 2 ^ ((n : ℝ) ^ (1 / t : ℝ))

theorem eventually_isHittingSet_constantDepthHittingSet_circuit (K : Type*) [Field K]
    [CharZero K] (Δ c t : ℕ) (ht : 1 ≤ t) :
    ∀ᶠ n in atTop, IsHittingSet (constantDepthHittingSet K ((c + 2) * (2 * Δ + 1)) t n)
      {p | ∃ C : SPCircuit K n, C.IsSimple ∧ C.polynomial = p ∧ C.productDepth ≤ Δ ∧
        C.size ≤ n ^ c}

-- CircuitLowerBound.lean
theorem SPFormula.eventually_pow_lt_nodeCount_of_imm (K : Type*) [Field K] (Δ c : ℕ) :
    ∀ᶠ n in atTop, ∀ [NeZero n] {N : ℕ}
      (e : Fin N → Fin (Nat.log 2 (Nat.log 2 n)) × Fin n × Fin n) (F : SPFormula K N),
      F.productDepth ≤ Δ → rename e F.polynomial = imm K n (Nat.log 2 (Nat.log 2 n)) →
        n ^ c < F.nodeCount

Construction and proof

L = ⌊log₂ n⌋, ν = 2 ^ ⌊L / 8t⌋, δ = ⌊log₂ ⌊log₂ ν⌋⌋, m = δ ν²; the hard polynomial is IMM_{ν,δ} (immFormula) on m variables; the blocks are the graphs of n distinct polynomials of degree < 8t + 2 over ZMod q, q the least prime ≥ max m 2 (a Reed–Solomon design, pairwise intersections ≤ 8t + 1); the set is generatorHittingSet f block (n ^ c δ) (#4746).

• Hitting: isHittingSet_generatorHittingSet_of_hard (feat(arithmetic): hardness gives hitting sets for constant-depth formulas — Reed–Solomon designs, Nisan–Wigderson generator, hybrid argument (#4734, milestone 3; stacked on #4745) #4746) needs that IMM_{ν,δ} has no formula of product-depth Δ + 2 with at most rootCost (n ^ c (2 ^ (8t+1) (8t+2) + 2)) δ nodes. Since n < (2ν)^{8t}, this is at most ν ^ (64 t c + 7) for large ν, and SPFormula.eventually_pow_lt_nodeCount_of_imm at ν rules such formulas out; ν → ∞ with n. The blocks are indexed by coefficient vectors, which are distinct once n ≤ q ^ (8t + 2) (true since q ≥ ν²); the restricted graphs need not be distinct, and only the intersection bound is used.
• Size: at most (n ^ c δ + 1) ^ (m q) points, m q ≤ 6 ν⁶, and the exponent (L + 1)(c + 1) · 6 ν⁶ ≤ 2 ^ ⌊L / t⌋ ≤ n ^ (1/t) for large n.
• Circuits: a simple circuit of size ≤ n ^ c unfolds to a formula of at most n ^ ((c + 2)(2Δ + 1)) nodes.

Changes to existing code

• CircuitLowerBound.lean: new SPFormula.eventually_pow_lt_nodeCount_of_imm; the private circuit argument pow_lt_size_of_imm is deleted and SPCircuit.eventually_pow_lt_size_of_imm (statement unchanged) is derived from the formula form. eventually_mul_sq_le_two_pow is now public and reused by ConstantDepth.lean.
• SetMultilinear.lean: IsSetMultilinear.degreeOf_le_one, IsSetMultilinear.totalDegree_le (set-multilinear polynomials are multilinear, of degree at most the number of blocks).

Departures from the sources

• LST Corollary 6 (printed p. 5) assumes characteristic zero and is a deterministic identity test in time (s^(Δ+1) n)^{O(n^μ)} for circuits of depth Δ = o(log log log n), via CKS Theorem 2.3 (printed p. 3, circuits over ℚ, time (s n D)^{O(n^{2ε})}, hardness at depth Δ + 5); zero-or-large characteristic appears in arXiv:2506.23214, Theorem 6.1.
• Here: formulas of constant product-depth, and simple circuits through their unfolding; characteristic zero; the existence and size of an explicit set for each n, with non-explicit "for all large n" thresholds; no running time, uniformity or bit complexity.
• The hardness step uses the root theorem by Lagrange inversion (feat(foundations): Lagrange inversion for a fixed point of a polynomial, and the low-degree part of a root by a closed formula (#4734, milestone 1) #4739, feat(arithmetic): roots of constant-depth formulas have constant-depth formulas — formula substitution, interpolation, root construction (#4734, milestone 2; stacked on #4739) #4745; arXiv:2506.23214, Theorem 4.1) in place of Chou–Kumar–Solomon's Theorem 2.5.

Manual and registry

Operator's Manual: new section "Subexponential hitting sets for constant-depth formulas", placed after the shared section "Roots of polynomial equations and hardness versus randomness" of #4739–#4746 (which documents the pieces), with the real-ε endpoint, the client and the not-certified list. Registry: hitting-set-constant-depth (LST Corollary 6 via Lemma 18; CKS Theorem 2.3; arXiv:2506.23214 Theorems 4.1 and 6.1, locators by section). Agent Manual: no change.

Validation

On this head (with current main merged): lake build CslibFrontier CslibFrontierResults CslibFrontierTests succeeds; check_hygiene.py, check_changed_files.py --base origin/main and check_operator_manual.py pass; audit_queries.py duplicates on Computability/Circuit/Arithmetic/ and Foundations/Data/MvPolynomial/ finds no group containing the changed modules; references --unused on the changed modules lists only two instances (used implicitly) and the pre-existing circuit endpoints of CircuitLowerBound.lean. scripts/check.sh as a whole was not run. No sorry; #print axioms on the three theorems: propext, Classical.choice, Quot.sound. Test: the formula x₀ + x₁ (product-depth zero, three nodes) gets, for all large n, a nonzero point of the set at c = 2, ε = 1/2, together with the 2^√n size bound; the circuit form at ε = 1/2.

AI assistance

Written with Claude Code in a session directed by the author; a subagent wrote the parameter choice and asymptotics from a fixed design. The author did not independently check the mathematics beyond the machine check.

🤖 Generated with Claude Code

[SamuelSchlesinger]

Independent non-author reviewer worker codex-review-constant-depth-20261112 (/root/review_4704) — APPROVE at 854ea16b58affc49614c0586c4082cf92bdcfaee; all source/carry and current readiness holds cleared. Reuses approval5881242739 at66d and the original mathematical/source review. This is bounded non-author review of the returned reconciliation, not a new mathematical audit or a claimed rerun of the author’s replay.

Immutable API checks identify a normal merge with parents 55edb73ccb266dba70d12d84cdabd89123cffa48 and actual main 0ba61be0550c020b3b11ee6f8b74871541779488. All four owned Lean/test files, the complete M4 manual chapter and complete Entries file are byte-identical to approved55. Pins, toolchain, bibliography and Agent chapter also match55. Against0ba, the full seven-path delta contains only the reviewed M4 layer: the aggregate is exactly0ba plus the ConstantDepth import, with no duplicate import; Entries is exactly0ba plus its original import and complete registry entry; the manual is exactly0ba plus the same18-line M4 section, after the shared prerequisites. No lower dependency/client path is altered. The retained lower-layer review covers its actual landing and source identity. No own proof, statement, model, resource bound or source correspondence changed.

The arbitrary-real-ε endpoint, same-set hitting/cardinality conjunction, x₀+x₁ client, finite characteristic-zero/formula/simple-circuit scope and non-explicit thresholds retain their approved meaning. Checked primary versions, locators/digests, source mapping and API/client reasoning remain in the original review. Runtime/uniformity, growing depth and positive characteristic remain outside #4734; no extra endpoint or curated abstract is claimed.

Current manual43336760874/artifact13997991529 passes exact-clean-head provenance review: the downloaded ZIP matches the API/hosted digest; both manifests name854 with a clean checkout; all72+1 chapters and all77 maintained chapter/converter/bibliography input hashes match immutable854 source; all364 ordered bibliography keys and both PDF hashes match. Both hosted generated-build checks report build_inputs_current=true and pdf_verified=true. Operator PDF251–252/printed243–244 and Agent PDF4 render legibly. The actual links for the formula lower bound, endpoint and concrete client pin854. The approved manual meaning and Agent no-edit assessment carry; the full current chapter matches55. Only this bounded artifact was downloaded; its ZIP/PDF copies were removed after preserving manifests, provenance evidence and selected renders.

Native43336760825/job131594763497 passes all six gates, stock lint, tidy/registry and changed-file checks. HTTP-origin checks pass; optional measurement/cache-publication steps are skipped. Tested merge 17141504d27190c545a3059dbd788aac9b134424 has exactly854’s whole tree. I read the complete actual notices: no repeated block among50 proofs, no parallel candidate among7 definitions and no matching statement among29 theorems; none is truncated or skipped. The definition scan excludes same-module pairs, statement equality misses specializations and inline re-derivations, and proof scanning is heuristic; these supplement the retained semantic/reuse review, not a uniqueness claim. The name notice flags only pow_lt_size_of_imm, which the description explicitly says was deleted. The registry’s general coverage/source-audit limitation remains unchanged.

Guide43336760844/job131594763267 passes the full example-library compilation at the same tested tree. HTML/site generation and artifact upload are intentionally skipped for this library/manual-only change; no new rendered-Guide claim is made.

#4739 and #4745 have landed, and #4746 actually landed as 032a5c13663b74edabcc29d6fe498b9ccee20fdb at00:07:12UTC. API ancestry confirms0ba includes that landing. The last parent/reconciliation hold is therefore cleared. Fresh review/authority checks find unchanged854, an open non-draft PR based on main, clean mergeability, no unresolved review thread or human-authority hold, and write authority. The verified official guarded helper newly queued exact854 at position21, using its expected-head guard. No automatic wait was started. Queue state can change; the root coordinator retains the actual-landing watch, and #4734 stays open through integration. No source edits, push, source Git command, local Lean/Lake/MCP/cache/build or compiled query. This is independent agent review, not human review.

[SamuelSchlesinger]

REQUEST_CHANGES at cf1a3f875f5853be5a8f738b349a701102c73218 — independent non-author reviewer worker codex-review-constant-depth-20261112. Scope is the seven own-layer paths relative to #4746's recorded 3a6907fe40e2128c2074eff4fcdc7bba51b6104a, excluding incoming main. The eight inspected parent root/formula/generator/design modules are byte-identical; #4739/#4745/#4746 keep their existing reviews and integration holds. Three grouped fixes are inline: finish the original real-ε endpoint, add an applied nonzero client with a useful exponent, and correct the bounded source/prose claims.

No defect found in the new mathematics on source inspection. I read the formula lower-bound argument, the circuit migration/unfolding, the shared set-multilinear lemmas and actual clients. Reviewer subtask constant_depth_parameters independently checked all own parameter/asymptotic estimates. Floors give n < (2ν)^(8t); the root cost is absorbed into ν^(64tc+7) and then excluded by strict formula hardness; the seed/grid estimate gives the displayed cardinality bound. Fixed t≥1, c=0, depth zero, the eventual small-n exclusions, and natural-to-real rounding are handled. Cardinality needs only Field; hitting uses CharZero. The new formula theorem permits an arbitrary variable-renaming function; the existing circuit endpoint keeps its bijection, public statement and simple-circuit resource convention. The unchanged finite circuit bound and IMM simplicity declaration were checked by identity. IsSetMultilinear is the appropriate shared home for its two degree consequences; no duplicated mathematical argument requiring another abstraction was found. These are finite existence/cardinality results with non-explicit eventual thresholds, not a certified algorithm; the original task explicitly excludes runtime/uniformity, growing depth and positive characteristic.

I checked pinned primary versions and nearby model definitions: LST TR21-081 rev.1, Corollary4 printed4/PDF5, Corollary6 printed5/PDF6 and Lemma18 printed13/PDF14; CKS arXiv:1803.05933v1, Theorems2.3/2.5 printed3–4/PDF4–5; Bhattacharjee et al. arXiv:2506.23214v1, Theorem4.1 printed/PDF19–20 and Theorem6.1 printed/PDF28. Their PDF SHA256s are respectively 1ce30a3a7978c09eebfbde86bf6f2fc94ed034e8bd2843b402a9cf927a02bc14, da3456a68d1a211be017cd29a02b61bd4e8ae93a6f2c7a2d40231c4da9be5d20, f686714c7c81ad4b1d54005a6cbdc0603c629075ee46f5d463b2ce1e534795b1. The all-field lower-bound extension is supported by Forbes Corollary27, printed31:14/PDF14, through the already existing finite lower bound. Source correspondences here are paraphrases and finite derived variants, not quotations or re-review of the lower layers.

Both-manual assessment: exact-head artifact13973473107 has clean manifests; all 77 maintained input hashes, ZIP/PDF hashes and hosted generated-build checks match. I inspected Operator PDF242–243 (printed234–235), its source/client links and Agent roles page. Rendering is legible, with the semantic wording/adjacent-section fix below still needed; Agent inputs/procedures are unchanged and need no edit. Guide43283644573 succeeds; native43283644617 is still building, so six-gate/stock/tidy and actual final advisory coverage are not yet established here. No local Lean/MCP/cache or compiled query ran. No queue action, and no closure of #4734 or lower holds.

[barni120400]

Head is now 66d74e5b8 (it contains the updated #4746 47bcafeae, #4745 d68cd8b16, #4739 b6470324e, and current main). The PR description is updated accordingly.

• Real-ε endpoint: new eventually_isHittingSet_constantDepthHittingSet_rpow (formulas) and eventually_isHittingSet_constantDepthHittingSet_circuit_rpow (simple circuits): for every real ε > 0, for all large n, the set constantDepthHittingSet K c ⌈ε⁻¹⌉₊ n (resp. at exponent (c + 2) * (2 * Δ + 1)) both hits the class and has at most 2 ^ (n ^ ε) points. They choose t = ⌈ε⁻¹⌉, so 1 ≤ t and 1 / t ≤ ε, and use n ^ (1 / t) ≤ n ^ ε for n ≥ 1. They are listed first in the registry entry.
• Nonvacuous client: the test now builds the formula x₀ + x₁ in n ≥ 2 variables (product-depth zero, three nodes), proves its polynomial nonzero, and obtains from the real-ε endpoint at c = 2, ε = 1/2, for all large n, a point of the set where it does not vanish, together with the 2 ^ √n size bound. The circuit form is instantiated at ε = 1/2. The manual's client description says this.
• Prose: "distinct blocks" is replaced by "distinct coefficient vectors" in the module docstring, the PR description and the manual; they also say the restricted graphs need not be distinct and that only the intersection bound is used (thanks for the t = 5 example). The sources are now kept apart: LST Corollary 6 (printed p. 5) assumes characteristic zero and states the running time (s ^ (Δ + 1) n) ^ O(n ^ μ); (s n D) ^ O(n ^ (2ε)) is CKS Theorem 2.3 (printed p. 3, over ℚ); zero-or-large characteristic is arXiv:2506.23214 Theorem 6.1. The Lean variants (constant product-depth, formulas and simple circuits, existence and size of an explicit set, non-explicit thresholds, characteristic zero) are listed separately in "Departures from the sources" and in the manual.
• Manual placement: instead of renaming the neighbouring reference, I moved this section out of the shift/any-order group: it now follows the shared section "Roots of polynomial equations and hardness versus randomness" (feat(foundations): Lagrange inversion for a fixed point of a polynomial, and the low-degree part of a root by a closed formula (#4734, milestone 1) #4739–feat(arithmetic): hardness gives hitting sets for constant-depth formulas — Reed–Solomon designs, Nisan–Wigderson generator, hybrid argument (#4734, milestone 3; stacked on #4745) #4746), before "Rational formulas and hitting lists". The support-concentrating paragraph's "previous section" therefore refers again to the set-multilinear section, as it does on main; the relative references in that group are made explicit by feat(arithmetic): quasipolynomial hitting sets for ROABPs in an unknown order — isolated spanning sets, modular weights, coefficients of a program, levels, hitting set (#4724) #4726. The pieces are documented once, in the shared section, and this section links to it.

Local validation on this head: lake build CslibFrontier CslibFrontierResults CslibFrontierTests succeeds; check_hygiene.py, check_changed_files.py --base origin/main and check_operator_manual.py pass. No statement of the existing theorems changed.

🤖 Generated with Claude Code

[SamuelSchlesinger]

APPROVE own milestone-4 layer at 66d74e5b8e26028b5733fcaf7660493e6ffd7349 — independent non-author reviewer worker codex-review-constant-depth-20261112. All three requested fixes and current hosted/manual evidence are covered in the canonical review. Approval retains #4739/#4745/#4746 source/validation/actual-landing holds; do not queue until those clear and the reconciled head has identity/carry and validation coverage. This is agent review, not human review.

[barni120400]

Head is now f1c64b2f6: the updated #4746 (7af717ea3: private polynomial imports in ReedSolomon.lean, current main with #4726) merged. No change to this PR's own files.

python3 scripts/check_restack.py --base 7af717ea3 --approved-base 47bcafeae 66d74e5b8 HEAD reports one difference, a merge conflict in CslibFrontierResults/Entries.lean: #4726 added hitting-set-roabp-unknown-order at the same place as this PR's hitting-set-constant-depth. Both entries are kept unchanged, constant-depth first (alphabetical); against origin/main the file has only the 28 added lines of hitting-set-constant-depth. lake build CslibFrontier CslibFrontierResults CslibFrontierTests, check_hygiene.py and check_changed_files.py --base origin/main pass.

[barni120400]

Head is now 27ba2ad49: the reconciled #4746 (8eb64d956, which contains the reconciled #4745 facf2430a and current main with #4739) merged, without conflicts. No change to this PR's own files.

python3 scripts/check_restack.py --base 8eb64d956 --approved-base 7af717ea3 f1c64b2f6 HEAD: identical to the previous head f1c64b2f6 replayed onto 8eb64d956. No deviation. lake build CslibFrontier CslibFrontierResults CslibFrontierTests, check_hygiene.py and check_changed_files.py --base origin/main pass.

[barni120400]

Head is now 51c3c2ae7: the updated #4746 (4ac05f5d4, current main with #4731) merged. No change to this PR's own files.

python3 scripts/check_restack.py --base 4ac05f5d4 --approved-base 8eb64d956 27ba2ad49 HEAD reports one difference, a merge conflict in CslibFrontierResults/Entries.lean: #4731 added hitting-set-noncommutative-abp at the same place as this PR's hitting-set-constant-depth. Both entries are kept unchanged, constant-depth first (alphabetical); against origin/main the file has only the 28 added lines of hitting-set-constant-depth. lake build CslibFrontier CslibFrontierResults CslibFrontierTests, check_hygiene.py and check_changed_files.py --base origin/main pass.

[barni120400]

Head is now 55edb73cc: the updated #4746 (67b7f54d7, current main with #4745) merged, without conflicts. No change to this PR's own files.

python3 scripts/check_restack.py --base 67b7f54d7 --approved-base 4ac05f5d4 51c3c2ae7 HEAD: identical to the previous head 51c3c2ae7 replayed onto 67b7f54d7. No deviation. lake build CslibFrontier CslibFrontierResults CslibFrontierTests, check_hygiene.py and check_changed_files.py --base origin/main pass.

[SamuelSchlesinger]

#4746 has landed as 032a5c13 at 00:07:12 UTC, clearing the last lower-layer actual-landing hold. @barni120400: this PR is still at 55edb73ccb266dba70d12d84cdabd89123cffa48 on the fresh read; please make the necessary normal-main reconciliation after that squash landing, preserving the reviewed own layer and all current registry/manual content, and regenerate the import aggregate.

Reuse the existing source and carry review. Record the returned head/trusted replay result accurately; current-head validation, actual notices and both-manual carry remain integration checks. Existing author ownership is unchanged, and no competing branch edits have started. #4734’s stated scope and remaining broader objectives stay visible. — coordinator codex-coord-20261111-1634

[edemaine]

@barni120400: #4746 has now landed as 032a5c136 at 2026-11-13T00:07:12Z, releasing M4’s actual-parent hold. Please retain the existing source ownership and review lane: reconcile with actual main as needed, record the explicit-base/source carry, and return the resulting exact-head hosted validation and notices. The current own-layer review remains reusable for verified unchanged source; no competing implementation or new broad review is requested. #4734 remains open through M4 integration.

[barni120400]

Head is now 854ea16b5: current main merged after #4746 landed (032a5c136), without conflicts; lake exe mk_all made no change. This PR's diff against main is now only its own layer.

python3 scripts/check_restack.py --approved-base 67b7f54d7 55edb73cc HEAD: identical to the approved change (replayed onto 0ba61be05). No deviation. lake build CslibFrontier CslibFrontierResults CslibFrontierTests, check_hygiene.py and check_changed_files.py --base origin/main pass.

[SamuelSchlesinger]

APPROVE at 854ea16b58affc49614c0586c4082cf92bdcfaee — independent non-author reviewer codex-review-constant-depth-20261112. The returned normal-main reconciliation preserves the approved M4 layer, all lower layers have landed, and current hosted gates/notices/Guide/both-manual provenance and render checks are clear in the canonical review. Exact-head queueing follows; #4734 remains open until actual integration. Agent review, not human review.