diff --git a/notes/proof-613-bridge-scope-review-20260908.md b/notes/proof-613-bridge-scope-review-20260908.md new file mode 100644 index 00000000..831f6758 --- /dev/null +++ b/notes/proof-613-bridge-scope-review-20260908.md @@ -0,0 +1,272 @@ +# #613 — independent scope review of the #276 critical-point bridge + +2026-09-08. WorkBuddy CLI (local machine). Bounded proof/literature task: +discharge the five verification items of #613 against the proof in +`docs/astra/ANSWER-610-20260907.md` (Q4, commit `65f5db1f`) and the +repository's digital Alexander duality +(`notes/digital-alexander-duality-proof.md`, workspace commit `8b5bc840`). +The note `notes/p613-quantile-convergence-20260907.md` (commit `f0981a98`, +merged via PR #614) already delivers Theorem L; this review re-derives and +checks its five verification items independently from the primary sources, +and records two scope corrections. + +Verdict in one line: **the bridge survives — all five items discharge, with +two scope clarifications that must travel with the theorem.** + +--- + +## Item 1 — the local lift/embedded-ball argument, with explicit radius + +**Claim to check.** A nonzero ambient cycle (a loop representing a nonzero +class of `H_1(T_N; Q)`) has a lift exiting an embedded ball; inside such a +ball the occupation law coincides with the infinite-graph product law; a +union bound over `N` starting vertices gives +`P_p(r_G > 0) <= C(p) N exp[-c(p) ell_N] -> 0` for `p < p_c(G)`. + +**Discharged.** Let `T_N = R^2/P_N Z^2` with shortest nonzero Euclidean +period `ell_N`. Because `pi_1(T^2)` is abelian, a loop is null-homologous +iff null-homotopic, so a nonzero class has a lift to the universal cover +with distinct endpoints `x, x+v`, `v in P_N Z^2 \ {0}`. + +*Graph vs Euclidean distance (NN).* An NN path from `x` to `x+v` in the +cover has `l^1`-length at least `|v|_2 >= ell_N`, so it reaches +NN-graph distance `>= ell_N` from its start. + +*Graph vs Euclidean distance (matching, NN+NNN).* A diagonal step covers +Euclidean distance `sqrt(2)`, so a matching path reaches Ghat-graph +distance `>= |v|_2/sqrt(2) >= ell_N/sqrt(2)`. + +*Conservative embedded radius.* Take `R_N = floor(ell_N/4)`. An +NN-ball of graph radius `R` lies in the Euclidean ball of radius `R` +(since `|y|_1 <= R => |y|_2 <= R`), diameter `<= 2R_N <= ell_N/2 < ell_N`, +so the covering projection is injective on it. A Ghat-ball of graph +radius `R` lies in the Euclidean ball of radius `sqrt(2) R`, diameter +`<= 2 sqrt(2) R_N <= 0.708 ell_N < ell_N` — also injective. The escaped +distances (`ell_N` and `ell_N/sqrt(2)`) both exceed `2 R_N`, so any lifted +nonzero cycle exits the ball. One radius serves both graphs; any +`R_N <= 0.35 ell_N` would do. + +*The bound.* On the embedded ball the restricted measure is the product +measure of the infinite graph (independence is local; embeddedness makes +the identification legitimate). For `p < p_c(G)`, exponential decay +(Item 2) gives `P^{Z^2}_p(0 <-> dist n) <= A(p) e^{-c(p) n}`; union bound +over the `N` starting vertices: + +```text +P_p(r_G > 0) <= N A(p) e^{-c(p) R_N} + <= C(p) N exp[-(c(p)/4) ell_N], +``` + +which tends to zero exactly when `ell_N/log N -> infinity`. The rate is +per-fixed-`p` and degenerates as `p ↑ p_c` — no uniformity up to `p_c` is +claimed, and none is needed for fixed quantiles. + +**Scope correction 1 (sufficient, not necessary).** `ell_N/log N -> infinity` +is a *sufficient* condition for this fixed-off-critical union-bound +argument, not a proved *necessary* condition for quantile convergence. A +fixed-width torus genuinely fails (quasi-one-dimensional behaviour, no +transition at `p_c(Z^2)`), but a failure at one width `O(log N)` does not +establish failure for every width `O(log N)`; closing that would need a +separate argument and is out of scope. Keep the hypothesis as stated, but +label it sufficient. + +*Honest quotients.* The cellwise digital Alexander proof requires each +periodic unit square to be an embedded cell with four distinct corners; +`ell_N > sqrt(2)` guarantees this. Tiny quotients with local +identifications are covered only by the separate finite oracle +(`scripts/digital_alexander_*_oracle.py`), not by the cellwise argument. +Short-period degeneracies are correctly outside the theorem. + +## Item 2 — exponential decay for site percolation on both graphs + +**Claim to check.** Subcritical site connection probabilities decay +exponentially on both the NN graph `G = Z^2` and the NN+NNN matching graph +`Ghat`, with no unqualified bond theorem substituted. + +**Discharged.** Primary source: + +> H. Duminil-Copin, V. Tassion, *A new proof of the sharpness of the phase +> transition for Bernoulli percolation and the Ising model*, +> Commun. Math. Phys. **343** (2016) 725–745; arXiv:1502.03050; +> DOI 10.1007/s00220-015-2480-z. + +* **Theorem 1.1, item 3** (finite-range case, 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`." The main theorem is + stated for **bond** percolation with general transitive couplings. +* **§1.2, remark "Site percolation"** (verbatim): "As in [AB87], the proof + may be adapted to site percolation on transitive graphs", with the + modified crossing functional `φ_p(S) = Σ_{x∈S} Σ_{y∉S, {x,y}∈E} + P_p[0 ↔ x]`. This is the site adaptation #613 asked to be discharged, + and it is a remark, not a separately numbered theorem — the citation + should say so. +* The remark's `[AB87]` is M. Aizenman & D. J. Barsky, *Sharpness of the + phase transition in percolation models*, Commun. Math. Phys. **108** + (1987) 489–526, which treats general finite-range independent percolation + (site included) directly; M. V. Menshikov, Dokl. Akad. Nauk SSSR **288** + (1986) 1308–1311 is the classical companion. Either route covers both + `G` and `Ghat`: both are locally finite, transitive, finite-range, so + the site adaptation applies to each at every `p` below its own site + critical point. + +The DCT statement is a **graph**-distance bound; Item 1's embedded-ball +conversion turns it into the Euclidean `ell_N` form. No unqualified bond +theorem is used anywhere. + +## Item 3 — the amenable matching critical-point relation + +**Claim to check.** `p_c^site(G) + p_c^site(Ghat) = 1` for `G = Z^2`, +sourced from a probability theorem, not from Mertens–Ziff's analyticity +heuristic. + +**Discharged, with a citation precision the issue's pointer does not +capture.** The issue points at Grimmett–Li, DOI 10.1002/rsa.21226 +(G. R. Grimmett, Z. Li, *Percolation critical probabilities of matching +lattice-pairs*, Random Structures & Algorithms **65** (2024), arXiv:2205.02734; +Crossref-verified: received 6 May 2022, accepted 15 Feb 2024). That paper's +Theorem 3.1 proves the **strict inequality** criterion +(`p_c(G*) < p_c(G)` iff `G` is not a triangulation, for transitive `G`) and +states (1.1)–(1.3) in its introduction, where (1.1) is +`p_c^site(G) + p_c^site(G*) = 1` — but (1.1) is presented there as the +Sykes–Essam relation "verified in a number of cases when `G` is amenable", +not as that paper's theorem. + +The theorem actually proving the equality is the companion: + +> G. R. Grimmett, Z. Li, *Hyperbolic site percolation*, +> Random Structures & Algorithms (2024, accepted v3); arXiv:2203.00981. + +Its abstract: "If `(G1,G2)` is a matching pair derived from some +quasi-transitive mosaic `M`, then `p_u(G1) + p_c(G2) = 1`", and "when `G` +is amenable we have `p_c(G) = p_u(G)`". The discharge chain is: + +```text +p_u^site(G) + p_c^site(G*) = 1 [Grimmett–Li, arXiv:2203.00981] +p_c^site(G) = p_u^site(G) for amenable G + [uniqueness of the infinite cluster; + Burton–Keane, Comm. Math. Phys. 121 + (1989) 501–505] +=> p_c^site(Z^2) + p_c^site(Ghat) = 1, + with G* = Z^2 + face diagonals = Ghat. +``` + +Classical alternative: J. van den Berg, *Percolation theory on pairs of +matching lattices*, J. Math. Phys. **22**(1) (1981) 152–157, +DOI 10.1063/1.524747, derives the relation for a restricted class under the +(finite mean cluster size) assumption later proved by Menshikov/Aizenman– +Barsky — so van den Berg plus sharpness also yields the equality for `Z^2`. + +**Warning that must stay in the record.** van den Berg's abstract records +that Sykes–Essam's suggested general relation has a constructed +counterexample outside the restricted (amenable) class. So (H3) is a +genuine hypothesis with known failures in greater generality; it holds here +specifically because `Z^2` is amenable, transitive and one-ended. Do not +carry (H3) to an arbitrary planar matching pair. Mertens–Ziff +(arXiv:1603.07289) supply the *finite* matching identity used in the +repository's duality note; their introduction's analyticity motivation is, +as the issue says, not the probability theorem and is not used as one. + +## Item 4 — scope against the existing literature; lemma, not new theorem + +The matching-root / homological-percolation comparison: + +> P. Duncan, M. Kahle, B. Schweinhart, *Homological percolation on a torus: +> plaquettes and permutohedra*, arXiv:2011.11903 (v4 2023); published, +> Ann. Inst. H. Poincaré Probab. Statist. (2025). + +Their giant cycles are exactly the event `im[H_i(S) -> H_i(T^d)] ≠ 0` that +the repository calls `r_G > 0`. They prove a sharp transition from +nonexistence of giant cycles to giant cycles spanning the ambient homology, +and — directly relevant — "we also prove convergence of the threshold +function to a constant in certain cases", with `p_c = 1/2` at middle +dimension. In `d = 2, i = 1`, their plaquette model **is** bond percolation +on the square torus, so the union-bound mechanism reconstructed in Item 1 +is already in the literature for square-bond tori. Their site model is the +**triangular** lattice, not the square; the square-site NN/matching-pair +instance is not literally in DKS. + +**Classification.** Theorem L is a **scoped repository lemma**: the +sharp-threshold mechanism is Duncan–Kahle–Schweinhart / standard finite-size +percolation theory (Margulis–Russo for strict monotonicity; the quantile +squeezing is elementary); the genuinely repository-specific additions are +(i) the square-site matching instance, which additionally consumes (H3), +and (ii) the digital Alexander duality (H1) that converts the vacant-set +matching rank into the complementary rank — the 16-pattern regular- +neighbourhood certificate in `notes/digital-alexander-duality-proof.md` is +the piece with no literature counterpart. No novelty claim is supportable, +and none should be made. Cite as: a corollary of Duminil-Copin–Tassion +(site sharpness/exponential decay), Grimmett–Li (matching critical-point +equality), Duncan–Kahle–Schweinhart (giant-cycle threshold mechanism), and +the repository's digital Alexander duality. + +## Item 5 — what fails, and stays outside + +1. **Thin tori (`ell_N = O(log N)` or bounded width).** The union bound no + longer tends to zero; at bounded width the model is quasi-one-dimensional + and has no transition at `p_c(Z^2)` at all. Also `ell_N <= sqrt(2)` + breaks the honest-cell hypothesis, so (H1) itself is not stated there. + Both the growth hypothesis and `ell_N > sqrt(2)` are load-bearing. + (Cf. Scope correction 1: sufficiency, not necessity.) +2. **Unbounded extrapolation weights.** A weighted quantile combination + `Σ_k w_k Q_N^{(k)}` with `Σ_k w_k = 1` converges iff + `sup_N max_k |w_k| < ∞` (each `Q_N^{(k)}` is covered individually; + mixed signs are fine because quantile functions, not CDFs, are + combined). With unbounded weights the `O(1)` finite-size error can be + amplified without bound — boundedness is not cosmetic. +3. **A u-grid approaching 0 or 1 with `N`.** The squeeze needs a *fixed* + `eps` with `F_N(p_c - eps) < u_N < F_N(p_c + eps)`. For `u_N -> 0` no + such `eps` exists; `Q_N(u_N)` is then only constrained to the correct + side of `p_c` and can converge to anything in `[0, p_c]`. A quantified + extension would need a lower bound on `u_N` against the + super-exponentially small tail `N C e^{-c' ell_N}` — a separate estimate, + not claimed. + +Non-claims restated: no rate at or near criticality (`c'(p) -> 0` as +`p ↑ p_c`; `F_N(p_c)` unconstrained in `[0,1]`); no numerical value or +certified interval for `p_c^site(Z^2)` (that is #112's separate finite-event +route); no correction-to-scaling shape, CFT operator content, or the value +3/4 for square-site thermal scaling. + +--- + +## Verdict + +All five items discharge: + +| item | status | carrier | +|---|---|---| +| 1. lift/embedded-ball union bound | **proved**, explicit `R_N = floor(ell_N/4)` | this note §Item 1; consistent with Theorem L §1 | +| 2. site exponential decay, both graphs | **cited**: DCT Thm 1.1(3) + §1.2 site remark (Aizenman–Barsky/Menshikov route) | this note §Item 2 | +| 3. amenable matching relation | **cited**: Grimmett–Li *Hyperbolic site percolation* (equality) + Burton–Keane amenability; RSA 2024 paper states but does not prove (1.1) | this note §Item 3 | +| 4. novelty scope | **repository lemma, not a new theorem**; DKS holds the giant-cycle threshold (bond case) | this note §Item 4 | +| 5. failure modes | thin tori, unbounded weights, `u_N -> {0,1}` all correctly excluded | this note §Item 5 | + +**Expected result confirmed, not falsified.** The #276 Phase A/B bridge now +rests on stated, sourced inputs: qualitative `Q_N(u) -> p_c^site(Z^2)` for +honest square-cell tori with `ell_N/log N -> infinity`, no CFT input, no +fitted exponent. Two scope corrections travel with it: (a) +`ell_N/log N -> infinity` is sufficient, not proved necessary, for the +quantile conclusion; (b) the RSA-paper pointer for item 3 should be cited +through the *Hyperbolic site percolation* theorem, with the van den Berg +counterexample caveat attached to any generalization beyond amenable pairs. + +No Monte Carlo was run; no simulation artifact is touched. STATUS.md +untouched; nothing merged; no ticket closed. + +## Sources + +| ref | item | +|---|---| +| [DCT16] | Duminil-Copin & Tassion, CMP **343** (2016) 725–745; arXiv:1502.03050; DOI 10.1007/s00220-015-2480-z. Thm 1.1(3); §1.2 "Site percolation". | +| [AB87] | Aizenman & Barsky, CMP **108** (1987) 489–526. | +| [Men86] | Menshikov, Dokl. Akad. Nauk SSSR **288** (1986) 1308–1311. | +| [GL24a] | Grimmett & Li, *Matching lattice-pairs*, Random Struct. Alg. **65** (2024); DOI 10.1002/rsa.21226; arXiv:2205.02734. States (1.1)–(1.3); proves strict-inequality criterion (Thm 3.1). | +| [GL24b] | Grimmett & Li, *Hyperbolic site percolation*, Random Struct. Alg. (2024); arXiv:2203.00981. Proves `p_u(G1)+p_c(G2)=1` and `p_c=p_u` for amenable `G`. | +| [vdB81] | van den Berg, J. Math. Phys. **22**(1) (1981) 152–157; DOI 10.1063/1.524747. Restricted-class derivation; records the Sykes–Essam counterexample. | +| [SE64] | Sykes & Essam, J. Math. Phys. **5** (1964) 1117–1127. | +| [BK89] | Burton & Keane, CMP **121** (1989) 501–505. | +| [DKS25] | Duncan, Kahle & Schweinhart, arXiv:2011.11903; Ann. Inst. H. Poincaré Probab. Statist. (2025). | +| [MZ17] | Mertens & Ziff, arXiv:1603.07289 (finite matching identity). | +| repo | `notes/digital-alexander-duality-proof.md` (H1, 16-pattern certificate). | +| repo | `notes/p613-quantile-convergence-20260907.md` (Theorem L, commit `f0981a98`). | +| repo | `docs/astra/ANSWER-610-20260907.md` Q4 (the proof under review, commit `65f5db1f`). |