From 46c41460670d7fdd455a10377ac36ae37e1bdb98 Mon Sep 17 00:00:00 2001 From: OxBenji Date: Sat, 1 Aug 2026 15:53:58 -0400 Subject: [PATCH] research(proximity): add G316 antipodal closed formula --- .../CodingTheory/ProximityGap/DISPROOF_LOG.md | 25 ++ ...316-antipodal-closed-formula-2026-08-01.md | 67 +++++ .../probes/g316_antipodal_closed_formula.py | 263 ++++++++++++++++++ 3 files changed, 355 insertions(+) create mode 100644 docs/kb/deltastar-466-g316-antipodal-closed-formula-2026-08-01.md create mode 100644 scripts/probes/g316_antipodal_closed_formula.py diff --git a/ArkLib/Data/CodingTheory/ProximityGap/DISPROOF_LOG.md b/ArkLib/Data/CodingTheory/ProximityGap/DISPROOF_LOG.md index 0fc0518f39..e3d09dd7a7 100644 --- a/ArkLib/Data/CodingTheory/ProximityGap/DISPROOF_LOG.md +++ b/ArkLib/Data/CodingTheory/ProximityGap/DISPROOF_LOG.md @@ -53380,3 +53380,28 @@ prove both a positive sponsor-two odd-cubic value and a transfer theorem using a adjacent-rank row structure. Formal payload `_G309TargetOrientedCubicGenericRowNoGo.lean`; exact probe `g309_target_oriented_cubic_generic_row_nogo.py`; full note `docs/kb/deltastar-466-g309-target-oriented-cubic-generic-row-nogo-2026-07-14.md`. CORE OPEN / ON-BGK. + +--- + +### [466-G316-antipodal-closed-formula] coefficient one vanishes by parity and coefficient two has a two-term formula in the antipodal model (2026-08-01) + +G316 turns the G314/G315 antipodal-pair model into a compact formula. Let `n=2h`, pair roots as +`{e_j,-e_j}`, and let `u,v` mark the subset sizes on the adjacent-rank pair `(r,r-1)`. The local +balanced-choice polynomials are +`N=1+2uv+u^2+v^2+u^2v^2`, `U=u+v+u^2v+uv^2`, and `D=uv`. + +For coefficient 1, the possible global cases are `N^h`, `D*N^(h-1)`, and `U^2*N^(h-2)`. Each has +even `deg_u-deg_v`, so the adjacent-rank coefficient is always zero. For coefficient 2, with +`T_m(r)=[u^r v^(r-1)] U*N^m`, the antipodal-model dot is +`D_2(h,r)=2h*T_{h-1}(r)+4h(h-1)*T_{h-2}(r-1)`, separating the same-pair `z=y` case from the +different-pair case. + +The probe checks the formula against the brute antipodal model for `n=16` at every rank and for +`n=32` at ranks `5,6`. At the live ranks this specializes to +`D_2(h,5)=2h*(11*C(h-1,2)+161*C(h-1,3)+406*C(h-1,4))` and +`D_2(h,6)=2h*(C(h-1,2)+81*C(h-1,3)+786*C(h-1,4)+1722*C(h-1,5))`. It then emits the +rank-five/six predictions: +`n=64: (864230400,20331698688)` and `n=128: (31776632832,1609610978304)`. +This is a formula for the model, not a proof that finite-field cells have no extra modular +relations. Exact probe `g316_antipodal_closed_formula.py`; full note +`docs/kb/deltastar-466-g316-antipodal-closed-formula-2026-08-01.md`. CORE OPEN / ON-BGK. diff --git a/docs/kb/deltastar-466-g316-antipodal-closed-formula-2026-08-01.md b/docs/kb/deltastar-466-g316-antipodal-closed-formula-2026-08-01.md new file mode 100644 index 0000000000..978897358b --- /dev/null +++ b/docs/kb/deltastar-466-g316-antipodal-closed-formula-2026-08-01.md @@ -0,0 +1,67 @@ +# G316: closed formula for the antipodal-pair model + +Date: 2026-08-01 +Issue: #466 +Branch: `research/proximity-prize` + +## Result + +G314 and G315 identified an antipodal-pair model behind the certified large-field toy tables. G316 +turns that model into a compact formula. + +Let `n=2h` and pair the roots as `{e_j,-e_j}`. Let `u` mark the size of the `r`-subset `A`, and `v` +mark the size of the `(r-1)`-subset `B`. The local balanced-choice polynomials are: + +```text +N = 1 + 2uv + u^2 + v^2 + u^2v^2 neutral pair +U = u + v + u^2v + uv^2 unit-forced pair +D = uv double-forced pair +``` + +For coefficient 1, every contributing case has even `deg_u-deg_v`, while adjacent ranks require +`deg_u-deg_v = 1`. Hence the coefficient-1 antipodal-model dot is zero for every adjacent rank. + +For coefficient 2, define + +```text +T_m(r) = [u^r v^(r-1)] U N^m. +``` + +Then the antipodal-model dot is + +```text +D_2(h,r) = 2h*T_{h-1}(r) + 4h(h-1)*T_{h-2}(r-1). +``` + +The first term is the same-pair case `z=y`; the second term is the different-pair case +`pair(y) != pair(z)`. The opposite same-pair case `z=-y` contributes zero for coefficient 2. + +For the live ranks this coefficient extraction simplifies to: + +```text +D_2(h,5) = 2h*(11*C(h-1,2) + 161*C(h-1,3) + 406*C(h-1,4)) +D_2(h,6) = 2h*(C(h-1,2) + 81*C(h-1,3) + 786*C(h-1,4) + 1722*C(h-1,5)) +``` + +The script checks this formula against the brute antipodal model for `n=16` at every rank and for +`n=32` at ranks `5,6`. It also emits the next closed-form predictions: + +```text +n=16: r=5 dot=321216, r=6 dot=1064448 +n=32: r=5 dot=20115200, r=6 dot=200992512 +n=64: r=5 dot=864230400, r=6 dot=20331698688 +n=128: r=5 dot=31776632832, r=6 dot=1609610978304 +``` + +## Scope + +This is a formula for the antipodal-pair model, not a proof that every finite-field cell has no +extra modular relations. The certified field computations already matched this model for `n=16` all +ranks and `n=32` ranks `5,6`; G316 isolates the exact combinatorial highway those checks were +following. The next production-facing question is to prove when the finite-field relation count +equals this antipodal model, or to bound the extra relations. + +## Artifact + +- Probe: `scripts/probes/g316_antipodal_closed_formula.py` +- Output: platform temp directory `arklib-reports/g316_antipodal_closed_formula.out` diff --git a/scripts/probes/g316_antipodal_closed_formula.py b/scripts/probes/g316_antipodal_closed_formula.py new file mode 100644 index 0000000000..bcfa0c8c23 --- /dev/null +++ b/scripts/probes/g316_antipodal_closed_formula.py @@ -0,0 +1,263 @@ +#!/usr/bin/env python3 +"""G316 closed formula for the coefficient-2 antipodal-pair model. + +G314/G315 identified an antipodal-pair model behind the certified large-field +toy tables. This probe turns that model into a compact coefficient formula. + +Let n=2h and pair the roots as {e_j,-e_j}. With u marking the A-subset rank +and v marking the B-subset rank, the local balanced-choice polynomials are + + N = 1 + 2uv + u^2 + v^2 + u^2v^2 (neutral pair) + U = u + v + u^2v + uv^2 (unit-forced pair) + D = uv (double-forced pair) + +For coefficient 1, every contributing case has even (deg_u-deg_v), so the +adjacent-rank coefficient [u^r v^(r-1)] is zero. + +For coefficient 2, define + + T_m(r) = [u^r v^(r-1)] U N^m. + +Then the antipodal model dot is + + D_2(h,r) = 2h*T_{h-1}(r) + 4h(h-1)*T_{h-2}(r-1). + +The two terms are exactly the same-pair case z=y and the different-pair case +pair(y) != pair(z). This is a formula for the model only, not a proof that a +finite-field cell has no extra modular relations. + +For the live ranks, coefficient extraction simplifies further: + + D_2(h,5) = 2h*(11*C(h-1,2) + 161*C(h-1,3) + 406*C(h-1,4)) + D_2(h,6) = 2h*(C(h-1,2) + 81*C(h-1,3) + 786*C(h-1,4) + 1722*C(h-1,5)). +""" +from __future__ import annotations + +from collections import defaultdict +from math import comb +from pathlib import Path +from tempfile import gettempdir + + +NEUTRAL = {(0, 0): 1, (1, 1): 2, (2, 0): 1, (0, 2): 1, (2, 2): 1} +UNIT = {(1, 0): 1, (0, 1): 1, (2, 1): 1, (1, 2): 1} +DOUBLE = {(1, 1): 1} + +EXPECTED_N16_ALL_RANKS = [ + 16, + 576, + 8064, + 64064, + 321216, + 1064448, + 2369472, + 3544608, + 3544608, + 2369472, + 1064448, + 321216, + 64064, + 8064, + 576, +] + +EXPECTED_R56 = { + 16: {5: 321_216, 6: 1_064_448}, + 32: {5: 20_115_200, 6: 200_992_512}, + 64: {5: 864_230_400, 6: 20_331_698_688}, + 128: {5: 31_776_632_832, 6: 1_609_610_978_304}, +} + + +def neutral_coeff(m: int, a_degree: int, b_degree: int) -> int: + """Return [u^a_degree v^b_degree] N^m for N=1+2uv+u^2+v^2+u^2v^2.""" + if m < 0 or a_degree < 0 or b_degree < 0: + return 0 + total = 0 + # x counts 2uv choices, y counts u^2, z counts v^2, w counts u^2v^2. + for w in range(min(a_degree, b_degree) // 2 + 1): + max_x = min(a_degree - 2 * w, b_degree - 2 * w) + for x in range(max_x + 1): + if (a_degree - x - 2 * w) % 2: + continue + if (b_degree - x - 2 * w) % 2: + continue + y = (a_degree - x - 2 * w) // 2 + z = (b_degree - x - 2 * w) // 2 + used = x + y + z + w + if used > m: + continue + total += ( + comb(m, x) + * comb(m - x, y) + * comb(m - x - y, z) + * comb(m - x - y - z, w) + * (2 ** x) + ) + return total + + +def unit_tail(m: int, r: int) -> int: + """Return T_m(r) = [u^r v^(r-1)] U N^m.""" + if m < 0: + return 0 + return ( + neutral_coeff(m, r - 1, r - 1) + + neutral_coeff(m, r, r - 2) + + neutral_coeff(m, r - 2, r - 2) + + neutral_coeff(m, r - 1, r - 3) + ) + + +def coeff1_antipodal_dot(_h: int, _r: int) -> int: + return 0 + + +def coeff2_antipodal_dot(h: int, r: int) -> int: + same_pair = 2 * h * unit_tail(h - 1, r) + different_pair = 4 * h * (h - 1) * unit_tail(h - 2, r - 1) + return same_pair + different_pair + + +def coeff2_r56_closed(n: int, r: int) -> int: + assert n % 2 == 0 + h = n // 2 + if r == 5: + return n * ( + 11 * comb(h - 1, 2) + + 161 * comb(h - 1, 3) + + 406 * comb(h - 1, 4) + ) + if r == 6: + return n * ( + comb(h - 1, 2) + + 81 * comb(h - 1, 3) + + 786 * comb(h - 1, 4) + + 1722 * comb(h - 1, 5) + ) + raise ValueError("closed form currently recorded only for ranks 5 and 6") + + +def signed_coordinate(index: int, pair: int, n: int) -> int: + half = n // 2 + if index == pair: + return 1 + if index == pair + half: + return -1 + return 0 + + +def local_balanced_choices(n: int, pair: int, y: int, z: int, coefficient: int) -> list[tuple[int, int]]: + base = coefficient * signed_coordinate(y, pair, n) - signed_coordinate(z, pair, n) + out: list[tuple[int, int]] = [] + for a_mask in range(4): + for b_mask in range(4): + delta = base + a_count = 0 + b_count = 0 + if a_mask & 1: + delta -= 1 + a_count += 1 + if a_mask & 2: + delta += 1 + a_count += 1 + if b_mask & 1: + delta += 1 + b_count += 1 + if b_mask & 2: + delta -= 1 + b_count += 1 + if delta == 0: + out.append((a_count, b_count)) + return out + + +def brute_antipodal_dot(n: int, r: int, coefficient: int) -> int: + half = n // 2 + total = 0 + for y in range(n): + for z in range(n): + dp: dict[tuple[int, int], int] = {(0, 0): 1} + for pair in range(half): + choices = local_balanced_choices(n, pair, y, z, coefficient) + next_dp: defaultdict[tuple[int, int], int] = defaultdict(int) + for (a_rank, b_rank), value in dp.items(): + for a_count, b_count in choices: + aa = a_rank + a_count + bb = b_rank + b_count + if aa <= r and bb <= r - 1: + next_dp[(aa, bb)] += value + dp = dict(next_dp) + total += dp.get((r, r - 1), 0) + return total + + +def emit(handle, line: str = "") -> None: + print(line, flush=True) + handle.write(line + "\n") + handle.flush() + + +def verify_parity(handle) -> None: + assert all((a - b) % 2 == 0 for a, b in NEUTRAL) + assert all((a - b) % 2 == 0 for a, b in DOUBLE) + assert all((a - b) % 2 == 1 for a, b in UNIT) + emit(handle, "parity check: N,D are even and U is odd in deg_u-deg_v") + emit(handle, "coefficient 1 cases N^h, D*N^(h-1), U^2*N^(h-2) cannot hit adjacent rank") + + +def verify_against_brute_model(handle) -> None: + emit(handle, "formula vs brute antipodal model") + for r, expected in enumerate(EXPECTED_N16_ALL_RANKS, start=1): + formula = coeff2_antipodal_dot(8, r) + brute = brute_antipodal_dot(16, r, 2) + zero = brute_antipodal_dot(16, r, 1) + assert formula == brute == expected + assert coeff1_antipodal_dot(8, r) == zero == 0 + emit(handle, f"n=16 coefficient=2 all ranks: {EXPECTED_N16_ALL_RANKS}") + + for n in (32,): + h = n // 2 + for r in (5, 6): + formula = coeff2_antipodal_dot(h, r) + brute = brute_antipodal_dot(n, r, 2) + zero = brute_antipodal_dot(n, r, 1) + assert formula == brute == EXPECTED_R56[n][r] + assert coeff1_antipodal_dot(h, r) == zero == 0 + emit(handle, f"n={n} r={r} formula=brute={formula}") + + +def emit_r56_formula_table(handle) -> None: + emit(handle, "closed-form coefficient-2 predictions for ranks 5 and 6") + for n, rows in EXPECTED_R56.items(): + h = n // 2 + r5 = coeff2_antipodal_dot(h, 5) + r6 = coeff2_antipodal_dot(h, 6) + assert coeff2_r56_closed(n, 5) == r5 + assert coeff2_r56_closed(n, 6) == r6 + assert r5 == rows[5] + assert r6 == rows[6] + emit(handle, f"n={n} h={h} r=5 dot={r5} r=6 dot={r6}") + + +def main() -> None: + out_dir = Path(gettempdir()) / "arklib-reports" + out_dir.mkdir(parents=True, exist_ok=True) + out_path = out_dir / "g316_antipodal_closed_formula.out" + + with out_path.open("w", encoding="utf-8") as handle: + emit(handle, "G316 antipodal closed formula") + verify_parity(handle) + verify_against_brute_model(handle) + emit_r56_formula_table(handle) + emit( + handle, + "PASS: coefficient 1 vanishes by parity in the antipodal model, and " + "coefficient 2 is given by D_2(h,r)=2h*T_{h-1}(r)+4h(h-1)*T_{h-2}(r-1).", + ) + + print(f"wrote {out_path}", flush=True) + + +if __name__ == "__main__": + main()