[chris-ai1]

Part of #4640, milestone M4 (two address blocks, $k=2$). Based on main.

Mathematical progress. For two address blocks, both sign-coherent bounds are linear in $m$:

• (a) Lower bound. Every circuit of depth $\le 2$ computing andreev 2 m whose bottom gates are sign-coherent has at least $m-1$ bottom gates read by the output gate (sub_one_le_card_outputBottomGates_andreev_two; for depthTwoInputs circuits, sub_one_le_of_depthTwoInputs_andreev_two).
• (b) Upper bound. andreevTwoBlocksCircuit m is an explicit depthTwoInputs circuit that computes andreev 2 m on every input. It has exactly $4\lceil m/2\rceil+m$ bottom gates. Each bottom gate gives every bit of a block the same weight, $0$ or $1$, so it sees the block only through its count; in particular it is sign-coherent. All weights are integers.

Proof of (a). Fix the table $x_c=c_0\oplus c_1$. On each unit square of block counts (M3's cube restriction), the circuit computes XOR or its negation. Restricted to the square, the circuit is an upper level set of its live form. If no bottom gate had a nonzero mixed difference there, the live form would be separable; the output gate's direct input wires are literals and fit in. No upper level set of a separable form is XOR, so every square needs a gate that cuts a corner.

With the table fixed, a sign-coherent gate is a threshold of $F_0(s_0)+F_1(s_1)$, and each $F_i$ is monotone or antitone (M3's monotone_or_antitone_blockForm). The ring lemma (new, Cslib.Combinatorics.card_filter_cutsCorner_gridBorder_le) says such a gate cuts a corner of at most $4$ of the $4(m-1)$ border squares. After reflecting coordinates, cut squares split into outer and inner corners. Two cut squares of the same kind are incomparable in the product order, and the border is the union of two chains. So $4(m-1)\le 4G$.

Lemma 15's count of $2m-1$ split squares per gate only gives about $m/2$; the corner condition plus the border is what gives $m-1$.

Proof of (b). It follows the draft, with all weights doubled to make them integers. The even staircases (sum_decide_two_mul_succ_le) give $\lfloor (s+y)/2\rfloor$, so the top sum depends on the counts only through their parities (andreevTwoBlocksTopSum_eq). The remaining finite check is proved for all $m$ (thirteen_le_andreevTwoBlocksTopSum_iff); the draft checks it numerically for $m\le 40$.

Source and provenance. The remark "Two address blocks" in the author's unpublished working draft eccc_draft/paper.tex, lines 873–877. I read the version with SHA-256 71f5738c239b3600c02b2d8aa5ad20a57d61d8af6d4d0cd2b5f862a79215089b. The fuller sketch and construction are in prop:k2 of the companion draft threshold_paper/paper.tex (SHA-256 2802eff9…). Neither draft is publicly accessible, so third parties cannot verify the correspondence. The mathematics is original, AI-assisted work under #4640.

Draft (remark "Two address blocks" / prop:k2)	Lean
(a) at least $m-1$ bottom gates	sub_one_le_card_outputBottomGates_andreev_two, sub_one_le_of_depthTwoInputs_andreev_two
table $x_c=c_1\oplus c_2$; "on every square some gate cuts off exactly one corner"	andreevXorTable, andreev_andreevCubePoint_xorTable, exists_cutsCorner_andreevGateGrid, circuitLiveForm_mixed_eq
"after reflecting, the 1-region is an up-set"	andreevGateGrid_orientation, cutsCorner_reflect_fst/_snd
Ring Lemma (at most four turns on the $4(m-1)$ border squares)	card_filter_cutsCorner_gridBorder_le, le_card_gridBorder
(b) circuit, $\lceil m/2\rceil$ and $m$ staircases, top $\Psi$	andreevTwoBlocksCircuit, AndreevTwoBlocksIndex, andreevTwoBlocksTopSum
identity $t-2\sum_j[t+y\ge 2j]=(-1)^y(t\bmod 2)$	sum_decide_two_mul_succ_le, andreevTwoBlocksTopSum_eq
correctness (draft: checked for $m\le 40$)	thirteen_le_andreevTwoBlocksTopSum_iff, computes_andreevTwoBlocksCircuit
$4\lceil m/2\rceil+m$ gates; block-symmetric	card_andreevTwoBlocksIndex, size_andreevTwoBlocksCircuit; weight_andreevTwoBlocksBottomOp_blockVar, isSignCoherent_andreevTwoBlocksBottomOp

Differences from the draft. "Cuts off exactly one corner" is formalized as a nonzero mixed difference (CutsCorner). For a threshold function of two bits, that means it is not constant and not a literal. The ring lemma is proved for all $m$; the draft checks it by brute force for $m\le 11$. The weights of (b) are doubled: top weights $-8,-4,-8,-4,-8$, input coefficients $10,10,16,4,3,2$ and threshold $13$, instead of the draft's $-4,-2,\dots$, $5,5,8,2,\tfrac32,1$ and $\tfrac{13}2$. Preprint gaps: none found. Both claims hold as stated, for every $m$.

Infrastructure.

• New Foundations/Combinatorics/CornerCutting.lean: CutsCorner, gridBorder, the chain and ring lemmas. It sits beside CubeSplitting, which holds Lemma 15.
• circuitLiveForm_mixed_eq goes in SplitCounting.lean, because circuitLiveForm is not exposed outside that module. Its only importer is AndreevSignCoherent.
• M1's AndreevSharp.lean gains interpretation_andreevFormWeight, the evaluation of a gate with andreevFormWeight weights. interpretation_andreevSharpBottomOp is now a one-line instance of it, and the new circuit uses it too, so the proof is not duplicated.

Docs. The Operator's Manual circuits chapter now has the requested sentences in the "Depth-two threshold bounds for Andreev's function" bullet: one for M1's andreevSharpCircuit and one for M4. The reference paragraph gains the M4 API. ROADMAP is unchanged (scope-only; status stays on #4640). The Agent Operator's Manual needs no change, since no workflow changed. Original results are deliberately absent from the results registry. Checked examples are in CslibFrontierTests/WeightedThresholdAndreevTwoBlocks.lean:

• CutsCorner on AND versus a literal;
• the ring lemma for a staircase and a reflected staircase;
• correctness and size $13$ at $m=4$, and size below andreevSharpCircuit 2 8;
• a concrete parity case of the finite check;
• block symmetry;
• the lower bound applied to both this circuit and M1's circuit at $b=2$.

Validation (local).

• lake build --wfail --iofail passes on the changed modules (CornerCutting, SplitCounting, AndreevSharp, AndreevSignCoherent, AndreevTwoBlocks, AndreevTwoBlocksLowerBound), their direct importers and the tests WeightedThresholdAndreevTwoBlocks, WeightedThresholdSignCoherent and WeightedThresholdAndreevSharp.
• lake exe mk_all --check, lake exe lint-style and scripts/check_operator_manual.py pass. No line exceeds 100 characters.
• scripts/proof_copies.py --base origin/main flags two small candidate pairs: the two coordinate reflections in CornerCutting, and the four parity cases of the finite check. I left both because a shared lemma would not be shorter.
• Not run locally: the root CslibFrontier build and scripts/parallel_defs.py. The host had 18G free, below the 30G needed for a full build, and the duplicate-definition scan needs one. CI covers both.

AI disclosure: written by Claude Code (Claude Opus 5.5) as the M4 worker for #4640. Requesting coordinator review.

🤖 Generated with Claude Code

[chris-ai1]

Independent agent review by this T3 delegated-task session, Codex codex-review-4774-20261112, on exact head 6fec765a9321b52eea8e461d7e35b62280238da2. I did not author, implement or design this change, and reviewed its source and evidence in a separate context. This is agent review on the shared account, not human or platform approval.

Verdict: no blocking mathematical or API defect found in the full diff; approval is held pending the required CI advisory and rendered-manual review. I read origin/main:AGENTS.md first and the pinned CSLib guidance. No local Lean build or full check was run; disk space was 42G free.

Source fidelity: I read the current ECCC draft, SHA-256 abadbd2fd22232a0af72dd53fa78dd63b02d8886a73100deb9dac7ad4ed39f50, remark “Two address blocks”, now lines 875–879, rather than claiming to have read the author's earlier 71f5738c… version. I also read the companion draft, SHA-256 2802eff9b095af2f52d81359333cdbd7a3a963ec4a608b2be15b0cd5a9d7f68e, prop:k2 and its proofs/reproduction paragraph. Both endpoints match: for $k=2$, $m-1$ bottom gates below, and $4\lceil m/2\rceil+m$ above. The Lean model permits direct input wires at the top, arbitrary real weights in the lower bound, and sign coherence only for the bottom gates actually read. It uses exactly M3's outputBottomGates: nonzero aggregated gate weights at the designated output, excluding dead/cancelled connections. No extra positivity or balance hypothesis is imposed; natural subtraction correctly makes $m=0,1$ trivial. The explicit upper-bound circuit and the test applications to both constructions witness non-vacuity.

The lower proof is sound on inspection. The XOR-table restriction forces nonzero mixed difference in some splitting gate, since the direct input contribution is separable and no threshold of a zero-mixed-difference form realizes XOR or its complement. circuitSplitGates_subset transfers the witness to the same output-gate count. The ring lemma is usefully more general than separable threshold gates: any Boolean grid function with uniform monotone/antitone orientation in each coordinate. Same-kind cut squares form an antichain; the border is covered by two product-order chains; the reflection bijections preserve the border and cut count. The border-cover/union-cardinality argument then gives $4(m-1)\le4G$. For $m=1$ the border has one square rather than $4(m-1)$; the formal statement correctly uses a lower bound on its size.

The upper construction's five staircase families, opposite-block unit addresses, top coefficients and threshold match the draft. Its index cardinality counts bottom gates, while size_andreevTwoBlocksCircuit includes the additional top gate. Equal integer block weights establish block symmetry and sign coherence; integer weights/thresholds are visible in the construction. I inspected the staircase reduction and four parity branches, plus the checked test clients (including size 13 at $m=4$ and both lower-bound applications). An independent Python arithmetic check of the displayed construction passed for all tables and count pairs at $m=0,\ldots,12$, including the empty-block edge case; this supplements source inspection, not Lean validation. The existing M1 theorem statement is unchanged: its evaluation proof now specializes the new shared interpretation_andreevFormWeight, also used by M4. SplitCounting adds a linearity lemma without changing old statements.

I accept the two source-level repeated-block dispositions described in the PR: the coordinate-specific reflection bijections contain short arithmetic bookkeeping, and the four parity branches make the actual finite truth-table cases explicit. They do not duplicate a substantial mathematical argument requiring another abstraction here. This assessment does not substitute for inspecting the pending CI candidates.

Manual/provenance source review: the Operator's Manual correctly distinguishes bottom count from total circuit size, names the M1 and M4 APIs, links complete test clients, and identifies these as original AI-assisted results from an unpublished draft. The Agent Operator's Manual needs no edit because roles/workflow are unchanged. Keeping ROADMAP scope-only, the broader issue open, candidate upstream markers and the original-results registry exclusion is consistent with repository policy. Nonblocking wording nit: “all weights doubled” should say the top affine coefficients and threshold are doubled; the bottom gates retain their draft weights and thresholds.

Readiness hold: Lean CI is still in progress. Its repeated-proof step has succeeded, but gh run view --log reports that logs are unavailable until completion, so I have not read that actual notice or the Parallel-definition/Duplicate-statement notice. The manual PDF build and Guide are also pending. Title and HTTP-cache tests pass. Before approval, inspect all three actual advisories and resolve relevant candidates/coverage limits, confirm final-head validation, and inspect the affected rendered manual pages. No queue or merge action, per the user's explicit instruction.

[chris-ai1]

Coordinator integration record at 6fec765a9321b52eea8e461d7e35b62280238da2:

• Independent review: T3 delegated-task session node:delegated-task:command:mcp:209b45c0-6ec8-4d3a-9adb-bbb62207cefe:delegate-task:0d0cbd80-2a38-4711-ac54-7e57886ce355, review of this exact head. It found no blocking mathematical or API defect: both bounds match the drafts, and the ring argument, gate count, M1 refactor and repeated-proof dispositions are sound. One optional wording nit about the doubled weights is left as is.
  • The reviewer did not author, implement or design the change, and reviewed it in a separate context.
  • The PR's author was a different session: …delegate-task:95a5a871-fd00-4cfb-bb98-28338822588a.
• CI: Lean CI 43281670655 passed; Guide, manual build and title pass.
• Advisory notices (read):
  • no parallel definitions (14 examined);
  • no duplicate statements (32 theorems);
  • 2 repeated-proof candidates: the gridBorder fst/snd reflection pair and the two thirteen_le_andreevTwoBlocksTopSum_iff parity cases, 5 lines each. These are exactly the two dispositions the PR explains and the review accepted.
• Rendered manual: in the PDF artifact, the M4 API paragraph (PDF p. 214) and the Andreev summary bullet (printed p. 213, now naming M1's andreevSharpCircuit and M4) render cleanly.
• Integration check: a replay of the current queue prefix (refactor(Graph): finish named input records and current clients #4618 … doc(results): audit Arora–Barak chapters 8–10 #4769) followed by this PR, built with real merge commits, is clean.

Queueing.