LightChainr · LightChainr · Sep 12, 2026
diff --git a/notes/cross-check-pr718-root-20260912.md b/notes/cross-check-pr718-root-20260912.md
@@ -0,0 +1,196 @@
+# Round B cross-check of #718's aspect-uniform root note (root-vs-law half)
+
+2026-09-12. Ticket #722 (parent #650). ASSIGNED_MACHINE: local. Model:
+glm-5.3-flash (deepseek-v4.1-flash returned 429). Peer check of
+`notes/aspect-uniform-balance-consistency-20260912.md` on branch `pr718`
+(commit 72d2ee6). Peer check, not original retrieval: branches were read with
+`git show prNNN:path`; nothing merged; STATUS untouched; #613 is not weakened
+by anything below.
+
+## 0. Scope
+
+The root-vs-law half only: #718 §1–§7 (theorem (1), H profile, thin-sequence
+contrast, Fisher identity, executed checks). The P398 periodic identified-TL
+half of the same PR is out of scope for this round.
+
+## 1. The five required checks
+
+### 1.1 The #718 note itself — PRIMARY_TEXT_READ (branch pr718, full text)
+
+Claim under review: on axis rectangles m>=w>=2, the unique zero p_(w,m) of
+M=P_2-P_0 satisfies sup_(m>=w) |p_(w,m)-p_c^site(NN)| -> 0 as w->infinity,
+with NO m/w bound and NO w/log(wm) condition; H=P_2/(P_0+P_2) is a conditional
+rank profile, not the birth-time mixture F; #613's full-law theorem stays.
+
+### 1.2 #716's two-birth note — PRIMARY_TEXT_READ (branch pr716, full text)
+
+#716 proves law(T) => (delta_0+delta_1)/2 for fixed w as m->infinity (its §2)
+and extends it to super-thin sequences w_m = o(log m) (its §6). #718 §5 uses
+w_j=j, m_j=ceil(exp(j^2)); w_j/log m_j = 1/j -> 0, inside #716 §6's hypothesis,
+so the citation is legitimate. The three-way statement on that sequence —
+F(p)->1/2 while p_(w_j,m_j)->p_c and H(p)->1{p>p_c} — is exactly the root-vs-law
+distinction both notes claim, and the two notes' limits are orthogonal
+(#716's "mean -> 1/2, not q_w" remark concerns the fixed-w cylinder limit).
+KEEP.
+
+### 1.3 Duminil-Copin–Tassion site adaptation — PRIMARY_TEXT_READ [LIT]
+
+Read arXiv:1502.03050v3 (HTML): Theorem 1.1 and §1.2. Theorem 1.1(3) (verbatim):
+"If (J_{x,y}) is finite-range, then for any β<β_c, there exists c=c(β)>0 such
+that P_β[0<->Λ_n^c] <= e^{-cn} for all n>=0." Printed in bond language.
+
+§1.2 "Comments and consequences", paragraph "Site percolation" (verbatim):
+"As in [AB87], the proof may be adapted to site percolation on transitive
+graphs. In this context, one can obtain the inequality P_p[0<->∞] >=
+(1/(d-1))·(p-p_c)/(1-p_c) (d is the degree of G) for p>=p_c by introducing
+φ_p(S)=Σ_{x∈S}Σ_{y∉S,{x,y}∈E} P_p[0<->^S x]."
+
+Precision finding: §1.2 is an adaptation remark whose PRINTED site inequality
+is the supercritical mean-field bound with the modified φ_p; the subcritical
+one-arm exponential decay for site is obtained by running the same adapted
+proof, not printed as a numbered site theorem. It is not a bond result copied
+to site — the φ_p modification is genuinely site-specific — and [AB87]
+(Aizenman–Barsky 1987) inside that sentence, plus Menshikov (1986), cover site
+subcritical exponential decay on finite-range transitive graphs directly.
+#718 already flags "the main theorem there is printed in bond language; §1.2 is
+essential here" and "actual site sharpness on the degree-eight graph, not a
+bond result". KEEP, with a precision upgrade suggested in §5.
+
+### 1.4 Matching duality for the p_c relation — PRIMARY_TEXT_READ [LIT]
+
+This is the load-bearing citation and the direction must be stated correctly.
+The elementary crossing duality for a planar matching pair gives only
+p_c(G)+p_c(G*) <= 1 (closed matching crossings are subcritical exactly when
+1-p < p_c(G*)). The SUPERCRITICAL half of #718 §4 needs the opposite inclusion:
+p > p_c(NN) must force 1-p < p_c(NN+NNN), i.e. p_c(NN)+p_c(NN+NNN) >= 1 — the
+Sykes–Essam equality.
+
+Verified chain (arXiv:2205.02734v3, HTML intro, = RSA 65 (2024) 832–856,
+DOI 10.1002/rsa.21226): Eq (1.1) is Sykes–Essam motivation ("presented
+motivation ... verified in a number of cases when G is amenable"), NOT that
+paper's theorem; Eq (1.3) p_u^site(G)+p_c^site(G*)=1 IS proved, in the
+companion Grimmett–Li "Hyperbolic site percolation" (arXiv:2203.00981, accepted
+RSA) for quasi-transitive one-ended plane matching pairs derived from a
+mosaic; the intro states "When G is amenable, we have p_c^site(G)=p_u^site(G)";
+G = square lattice Z^2 (amenable, transitive, one-ended) with G* = Z^2 plus
+face diagonals is the paper's Figure 1.1 pair. Hence
+p_c^site(NN)+p_c^site(NN+NNN)=1 holds for exactly this pair. This matches #613's
+§(H3) reading of the published PDF, including its warning (van den Berg 1981
+counterexample in wider generality — do not carry (H3) beyond the amenable
+case). #718 cites "Eqs. (1.1),(1.3) and the amenable p_u=p_c discussion", which
+reproduces the provenance chain without overclaiming (1.1) as a theorem of the
+RSA paper. KEEP. Upgrade suggested in §5: cite arXiv:2203.00981 directly.
+
+### 1.5 Harris/FKG for the P_0 lower bound — verified
+
+#718 §2 supplies the induction proof of association for decreasing indicators
+and explicitly does not pretend the overlapping boxes A_v are independent; the
+overlap is handled by (3): intersection_v A_v^c ⊆ {r=0}, via the winding-lift
+escape argument under the embedding condition 2R+2<=w<=m (both graphs have all
+edges of sup-norm length <=1, so the same condition prevents edge
+identification and spurious boundary adjacency for the NN+NNN box). FKG then
+gives P_0 >= (1-a_R)^(wm). KEEP. The exact-rational FKG lower bound appears in
+the executed script output (see §3).
+
+## 2. Independent re-derivation of the proof skeleton
+
+Items checked by hand, no gap found:
+
+- Floor bound: floor(m/(R+1)) >= m/(2(R+1)) holds iff m >= 2(R+1), which the
+  hypotheses give (m >= w >= 2R+2). With R=floor(w/8), 2R+2 <= w for w >= 8,
+  and the L=floor(m/(R+1)) slabs k(R+1)..k(R+1)+R fit the m rows.
+- Rate split (7): exponent/m <= floor(m/(R+1))/m · log(w a_R) - w log(1-a_R),
+  so gamma_w = -log(w a_R)/(2(R+1)) + w log(1-a_R) with the second term
+  NEGATIVE and retained; (8) is exactly the exponentiation of gamma_w > 0.
+- §4 limits: a_R <= C e^{-cR} gives -log(w a_R)/(2(R+1)) -> c/2 (R ~ w/8) and
+  w log(1-a_R) ~ -w C e^{-cw/8} -> 0, so gamma_w >= c/4 eventually, uniformly
+  in m >= w. Same on the matching graph (finite-range transitive; diagonal
+  steps change y by at most 1, so the slab containment (5) survives).
+- Supercritical half: complementation interchanges P_0 and P_2 through the
+  rank-sum identity r_NN(ω)+r_match(ω^c)=2 (repository digital Alexander,
+  assumed as in #613's (H1)); the matching graph at 1-p is subcritical exactly
+  when p > p_c(NN) by the equality of §1.4.
+- Uniqueness: Margulis–Russo pivotality gives P_0' < 0, P_2' > 0, M' > 0 on
+  (0,1); M(0)=-1, M(1)=+1; unique zero trapped for every m >= w.
+- Fisher identity (11): re-derived symbolically from
+  P_0=E(1-H), P_2=EH, P_1=1-E; the cross terms 2E'H' cancel, giving
+  (E')^2/[E(1-E)] + E(H')^2/[H(1-H)]; at H=1/2 the second term is (M')^2/E
+  since M'=2EH' there. Confirmed.
+- H quantiles: H <= P_2/P_0 below p_c and 1-H <= P_0/P_2 above p_c trap all
+  interior quantiles uniformly in m >= w; H is not F (F=(1+M)/2, different
+  function; §5 shows the limits decouple on the thin sequence).
+
+## 3. Executed controls (reproduced on this machine)
+
+`git worktree` of pr718; pytest unavailable locally, run via unittest:
+
+- `tests/test_rectangular_rank_odds.py`: 8 tests, OK.
+- `tests/test_p398_tl_fattening.py`: 8 tests, OK (out of scope, ran anyway).
+- `scripts/rectangular_rank_odds.py`: reproduced §7 — 65,536 configurations
+  per graph (131,072 graph/configuration evaluations) on the 4x4 torus,
+  complementary rank sum checked on all 65,536 pairings, 236 structural
+  graph cases, exact probability versions of (4), (6), (11) at p=1/10, 1/3,
+  1/2 with `inequalities_exact: true` and `exact_decomposition: true`,
+  elapsed ~1.1 s.
+
+These are finite sign checks; the note correctly does not claim the asymptotic
+theorem from them (§7 of the note says the same).
+
+## 4. KEEP / CORRECT / DROP
+
+| # | Claim / citation in #718 | Verdict | Basis |
+|---|---|---|---|
+| 1 | uniform-in-m root consistency as w->infinity (theorem (1)) | KEEP | skeleton re-derived end-to-end; the needed matching-pair equality is rigorously sourced (§1.4); no gap found |
+| 2 | H is not the birth-time mixture F | KEEP | different functions ((1+M)/2 vs P_2/(P_0+P_2)); #718 §5 shows the limits decouple (F->1/2, H->step); not proposed as an independent observation |
+| 3 | #613 remains valid for the full law | KEEP | #613 Theorem L is scoped under (H0); #718 claims neither necessity of (H0) nor a sharp full-law condition; nothing here weakens #613 |
+| 4 | no tilted-torus claim | KEEP | skew quotients explicitly excluded ("does not extend the geometry to arbitrary skew quotients without an additional strip construction"); nothing in the proof implies one |
+| 5 | bond sharpness cited for site? | NO FLAG — KEEP | the note flags the bond language itself and relies on the §1.2 site adaptation plus [AB87]; see the precision upgrade below |
+
+No DROP entries. No CORRECT entries of substance; three non-blocking
+precision upgrades follow.
+
+## 5. Non-blocking precision upgrades
+
+1. Quote the §1.2 "Site percolation" passage (done in §1.3 above) when
+   relying on the site one-arm decay, or cite Aizenman–Barsky (1987) /
+   Menshikov (1986) directly for subcritical site exponential decay on
+   finite-range transitive graphs — §1.2's printed site inequality is the
+   supercritical mean-field bound, the subcritical decay being an adaptation
+   the reader runs.
+2. Cite Grimmett–Li arXiv:2203.00981 alongside rsa.21226 for (1.3); the RSA
+   paper's (1.1) is motivation, not theorem — exactly as #613's (H3) warning
+   already records.
+3. In §5, name #716 §6's hypothesis (w_m = o(log m)) explicitly when invoking
+   the super-thin sequence w_j=j, m_j=exp(j^2); "the previous full/empty-row
+   bounds" currently leaves the hypothesis implicit.
+
+## 6. Sources and read marks
+
+- pr718 `notes/aspect-uniform-balance-consistency-20260912.md`:
+  PRIMARY_TEXT_READ (branch pr718, full text).
+- pr716 `notes/thin-torus-two-birth-limits-20260912.md`:
+  PRIMARY_TEXT_READ (branch pr716, full text).
+- main `notes/p613-quantile-convergence-20260907.md`: PRIMARY_TEXT_READ.
+- Duminil-Copin & Tassion, arXiv:1502.03050v3 (HTML), Theorem 1.1 and §1.2:
+  PRIMARY_TEXT_READ. [LIT]
+- Grimmett & Li, "Percolation critical probabilities of matching
+  lattice-pairs", RSA 65 (2024) 832–856, DOI 10.1002/rsa.21226; read as
+  arXiv:2205.02734v3 (HTML introduction, Eqs (1.1)–(1.4), amenability
+  passage): PRIMARY_TEXT_READ; the Wiley page itself: ABSTRACT_ONLY.
+  [LIT]
+- Grimmett & Li, "Hyperbolic site percolation", arXiv:2203.00981v3:
+  ABSTRACT_ONLY — the p_u+p_c(G*)=1 theorem verified via its quotation as
+  Eq (1.3) in the primary text and via #613's published-PDF reading, not from
+  the companion's full text. [LIT]
+- Background, not read in this round: [LIT] Aizenman–Barsky, CMP 108 (1987)
+  489–526; Menshikov (1986); van den Berg, JMP 22 (1981) 152–157;
+  Burton–Keane, CMP 121 (1989) 501–505; Sykes–Essam, J. Math. Phys. 5 (1964)
+  1117–1127.
+
+## 7. Verdict
+
+Not falsified. KEEP x5, CORRECT 0, DROP 0, three non-blocking precision
+upgrades. The aspect-uniform root theorem's citation base (site one-arm decay
+via the DC–T adaptation; matching-pair equality via the Grimmett–Li pair;
+Harris/FKG with overlapping boxes handled honestly) supports the claim as
+stated; #613's full-law theorem and the root-vs-law distinction are preserved.