diff --git a/research/eps-halo-exponent-check/README.md b/research/eps-halo-exponent-check/README.md new file mode 100644 index 0000000000..6d17bc7df9 --- /dev/null +++ b/research/eps-halo-exponent-check/README.md @@ -0,0 +1,65 @@ +# Independent check of #4439 and #4442: halo exponents under ε = 1/(16p²) + +**Claim type:** an independent check of conditional exponent arithmetic, by separate code with exact +rationals. **No new κ.** It covers jwr404's +[#4439](https://github.com/CrocSwap/integer-mult-bounds/pull/4439) (within one cell, head `26af8afb`) +and [#4442](https://github.com/CrocSwap/integer-mult-bounds/pull/4442) (across cells under the downward +reading, head `d079c2b0`). It is the ε-route counterpart of my #4460, which covers the δ route. + +## What is checked + +- **The ceiling.** The split identity `(1−ε)[T_in/(1−ε) + T_out] − T = −ε·T_out` is proved as a + polynomial identity on a 3×3×3 grid. It gives `off ≤ (1−g)/(1−ε) = (16p²−2)/(16p²−1)`, so the gap is + exactly `1/(16p²−1)` and the absolute sums are below 2. Exact for `p` in 2..64. +- **The exponents**, with `B = 16p²−1`. Exact for `p` in 2..64, plus all-`p` arguments. + + | Role | Value | Reason | + | --- | --- | --- | + | spectral endpoint | 12 | `B² ≤ p^{12}`; for `p ≥ 3`, `(16p²)² < p^{12}` | + | series length | 26 | error `< B·e^{−p²} < p⁶e^{−p²}` | + | bandwidth and agreement distance | 28 | `(2p^{26} ± 1)(p−1) < p^{28}` | + | normalizer | 6 | `B < p⁶`; 7 also works | + +- **The "fails" entries.** + + | Exponent | Where it fails | Reason | + | --- | --- | --- | + | endpoint 11 | `p = 2` | `63² > 2^{11}` | + | length 25 | `p = 2` | certified lower bound `(1−x)^L ≥ e^{−xL−x²L}` | + | 27 | `p = 2` (loose count) and `p ≥ 3` (sharp count) | | + | normalizer 5 | `p = 2` | `63 > 32` | + +- **#4442's tightness at `p = 2`.** An overshoot of 1/64 exceeds the ceiling, since + `63·63 = 3969 > 3968 = 62·64`. +- **#4442's bare-kernel example.** With `θ = β = 1/4`, `h = 1`, `g = 2`, the next phase is `−1/2`. + The square gap is `2 = 32/16`, against `ρh² = 5/4 = 20/16`. + +All statements check out. + +## Not covered + +- The ideal gaps. +- The rounding contract, which is #4449. +- The δ route, which is my #4460 and #4462. +- Any new κ. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/eps-halo-exponent-check --check-only +python3.12 -B scripts/research_package.py --package research/eps-halo-exponent-check +``` + +The verifier prints `PASS_EPS_HALO_EXPONENT_CHECK` in under a second, using only the standard library. + +## Open next questions + +1. **None specific to the ε route.** It is superseded by the δ route (#4452, #4460, #4462). + +## Credit + +- The lemmas and exponents are James Reed's (jwr404: #4439 and #4442). +- The entry law is LOG-A's. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/eps-halo-exponent-check/SOURCES.json b/research/eps-halo-exponent-check/SOURCES.json new file mode 100644 index 0000000000..6a28c347a0 --- /dev/null +++ b/research/eps-halo-exponent-check/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md", + "usage": "input", + "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73", + "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272" + } + ] +} diff --git a/research/eps-halo-exponent-check/TASK.json b/research/eps-halo-exponent-check/TASK.json new file mode 100644 index 0000000000..712a517431 --- /dev/null +++ b/research/eps-halo-exponent-check/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Independent check of #4439/#4442's epsilon-route halo exponents.", + "scope_change_reason": "Independent check of open author-checked lemmas.", + "bottleneck_link": "Side result on the #4100 precision/conditioning obligation.", + "budget_minutes": 25, + "stop_rule": "Stop at the stated arithmetic.", + "outcome": "completed", + "evidence": "All #4439/#4442 statements confirmed exactly for p=2..64 with all-p arguments; fails entries and p=2 tightness confirmed.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "None specific; superseded by the delta route.", + "why_it_matters": "n/a", + "first_step": "See #4460/#4462.", + "blocked_by": "None." + } + ] +} diff --git a/research/eps-halo-exponent-check/VERIFY.json b/research/eps-halo-exponent-check/VERIFY.json new file mode 100644 index 0000000000..88ed7e9c48 --- /dev/null +++ b/research/eps-halo-exponent-check/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "#4439/#4442 epsilon route: split identity (grid-proved), exact gap 1/(16p^2-1), exponents 12/26/28/28 and normalizer 6 for p=2..64 plus all-p arguments, every 'fails' entry, p=2 tightness 63*63>62*64, bare-kernel example." + } + ] +} diff --git a/research/eps-halo-exponent-check/verify.py b/research/eps-halo-exponent-check/verify.py new file mode 100644 index 0000000000..18a1a24dbf --- /dev/null +++ b/research/eps-halo-exponent-check/verify.py @@ -0,0 +1,81 @@ +#!/usr/bin/env python3 +"""Independent check of #4439 and #4442: halo exponents under the relative weight budget eps = 1/(16p^2). + +Ceiling. Ideal off-sums T <= 1 - g (g = 1/(8p^2)); within-cell entries <= ideal/(1-eps); across-cell entries in [0, n]. +Split T = T_in + T_out: off <= T_in/(1-eps) + T_out <= T/(1-eps) <= (16p^2-2)/(16p^2-1), so the gap is 1/(16p^2-1), +||H^-1||_2 <= B = 16p^2 - 1 and ||H||_2 < 2. Exponents: endpoint 12 (B^2 <= p^12), length 26 (error < B e^-p^2 < p^6 e^-p^2), +bandwidth/agreement 28, normalizer 6 (B < p^6; 7 also works). Fails: 11 (B^2 > p^11 at p = 2), 25 (length p^25 at +p = 2), 27 (loose count at p = 2, sharp count p >= 3), normalizer 5 (63 > 32). Tightness at p = 2: an across-cell +overshoot of 1/64 over the ideal off-sum (S-2)/S exceeds (S-2)/(S-1): 63*63 > 62*64. Bare-kernel example: theta = beta += 1/4, h = 1, g = 2 gives square gap 2 = 32/16 against rho h^2 = 5/4 = 20/16. Exact rationals p = 2..64, all-p +arguments where stated. Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as F +import hashlib +import itertools +import json +import math +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def main(): + for row in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"]: + need(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], row["path"]) + loga = (ROOT / "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md").read_text(encoding="utf-8") + need("`n_i,h=exp(-a[(rho*h+beta_i)^2-beta_(i+h)^2])`" in loga, "LOG-A entry law") + # split identity: (1-e)[a/(1-e) + (t-a)] - t = -e (t-a), polynomial of degree <= 2 per variable, 3x3x3 grid + vals = [F(1, 7), F(2, 5), F(3, 4)] + for a, t, e in itertools.product(vals, repeat=3): + need((1 - e) * (a / (1 - e) + (t - a)) - t == -e * (t - a), "split identity") + for p in range(2, 65): + S = 16 * p * p + g, eps = F(1, 8 * p * p), F(1, S) + off = (1 - g) / (1 - eps) + need(off == F(S - 2, S - 1) and 1 - off == F(1, S - 1), "ceiling: gap 1/(16p^2-1)") + need(1 + off < 2, "absolute sums below 2") + B = S - 1 + need(B * B <= p ** 12 and B < p ** 6, "endpoint 12, normalizer 6") + need(B < p ** 7, "normalizer 7 also works") + L = p ** 26 + need((2 * L - 1) * (p - 1) < p ** 28 and (2 * L + 1) * (p - 1) < p ** 28, "bandwidth/agreement 28") + # error at length p^26: B (1 - p^-24)^(p^26) <= B e^-(p^2) < p^6 e^-(p^2) + need(B < p ** 6, "series error") + if p >= 3: + need((2 * p ** 26 - 1) * (p - 1) > p ** 27, "27 fails (sharp count, p >= 3)") + need(63 * 63 > 2 ** 11, "endpoint 11 fails at p = 2") + need(63 > 2 ** 5, "normalizer 5 fails at p = 2") + need((2 * 2 ** 26 + 1) > 2 ** 27, "27 fails (loose count, p = 2)") + # length p^25 fails at p = 2 on this route: B (1-x)^L >= B exp(-xL - x^2 L) with x = 2^-24, L = 2^25 + x, L = F(1, 2 ** 24), 2 ** 25 + need(math.log(63) - float(x * L + x * x * L) > math.log(64) - 4, "length 25 fails at p = 2") + # all p >= 2: (16p^2-1)^2 <= p^12 and 16p^2-1 < p^6 (p^4 >= 16, room 1 at p = 2) + need(all((16 * p * p - 1) ** 2 <= p ** 12 for p in range(2, 1000)), "endpoint 12 sample") + need(16 * 16 < 3 ** 8, "p >= 3: (16p^2)^2 < p^12 since p^8 >= 3^8 > 256") + # tightness at p = 2 + Sx = 64 + need(F(Sx - 2, Sx) + F(1, 64) > F(Sx - 2, Sx - 1) and 63 * 63 == 3969 and 62 * 64 == 3968, "p = 2 tightness") + # bare-kernel example + theta, beta, h, gstep = F(1, 4), F(1, 4), 1, 2 + rho = 1 + theta + beta_next = beta + rho * h - gstep + gap = (rho * h + beta) ** 2 - beta_next ** 2 + need(beta_next == F(-1, 2) and gap == 2 and rho * h * h == F(5, 4) and gap * 16 == 32 and rho * 16 == 20, + "bare-kernel example: square gap 32/16 against 20/16") + print(json.dumps({"status": "PASS_EPS_HALO_EXPONENT_CHECK", "exact_p_range": [2, 64], + "exponents": {"spectral_endpoint": 12, "series_length": 26, "bandwidth": 28, + "agreement_distance": 28, "normalizer": 6}, + "fails_confirmed": ["11 at p=2", "25 at p=2", "27 (loose p=2, sharp p>=3)", "normalizer 5 at p=2"], + "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())