diff --git a/research/gaussian-column-cut/README.md b/research/gaussian-column-cut/README.md new file mode 100644 index 0000000000..30b2efc778 --- /dev/null +++ b/research/gaussian-column-cut/README.md @@ -0,0 +1,238 @@ +# The ideal column bound survives a g=2 step + +**Claim type:** a written lemma for the ideal narrow matrix `N`. **No new κ.** +This answers the ideal-matrix half of open question 1 in +[#4402](https://github.com/CrocSwap/integer-mult-bounds/pull/4402). It does not +bound the rounded reference `H`, and it does not edit the #4100 notes. + +#4402 proved, inside one constant-phase run, + +```text +||N-I||_1 <= exp(-2aθ) + exp(-2a(1-θ)) + 2 exp(-2a)/(1-exp(-4a)). +``` + +Its own control shows the run identity `β_{i+h} = β_i + θh` fails across a cut. +The same majorant nevertheless holds for every column once each step is only +`g ∈ {1, 2}`. + +## Question + +`LOG-A-PHASE-SCHUR-AUDIT.md` defines + +```text +n_{i,h} = exp(-a[(ρh + β_i)^2 - β_{i+h}^2]), ρ = 1+θ, β_i = ρ i - q_i, +``` + +with diagonal 1, each `β_i ∈ [-1/2, 1/2)`, and each step `g_i = q_i - q_{i-1}` +in `{1, 2}`. A cut in this model is a step `g = 2`, not a separate entry law. +Does #4402's column majorant still bound a column that meets such a step? + +## Lemma + +Under that entry law, every column satisfies + +```text +||N-I||_1 <= exp(-2aθ) + exp(-2a(1-θ)) + 2 exp(-2a)/(1-exp(-4a)). +``` + +The nearest sum is largest on a both-steps-1 column. A `g = 2` step makes the +nearest contribution smaller. Assume in addition that `p >= 2` is an integer, +`θ ∈ [1/(4p^2), 1/p^2]` and `4 log(16p) <= a <= 5 log(16p)`, where `log` is the +inverse of `exp` as in `GAUSSIAN.md`. Then the column gap is strictly larger +than `1/(8p^2)`. Zeroing positive off-diagonal entries, including a truncation +at bandwidth `< p`, does not increase the off-sum. An entrywise change of size +`ε` on the at most `2p-1` nonzeros keeps the gap above `1/(16p^2)` whenever +`2p ε <= 1/(16p^2)`. + +These `a` and `θ` inequalities are hypotheses. The note's statement that they +hold eventually is not re-proved. The historical rounding budget is not +identified with this `ε`. + +## Proof + +The recurrence is `β_j = β_{j-1} + 1 + θ - g_j`. Substitute it into the two +nearest formulas from the audit: + +```text +n_{j-1,+1} = exp(-a g_j (g_j + 2 β_j)), +n_{j+1,-1} = exp(-a g_{j+1} (g_{j+1} - 2 β_j)). +``` + +Since `θ <= 1/4 < 1/2`, the landing intervals are disjoint: + +| Incoming `g_j` | Outgoing `g_{j+1}` | `β_j` | +| --- | --- | --- | +| 2 | 1 | `[-1/2, -1/2+θ)` | +| 1 | 1 | `[-1/2+θ, 1/2-θ)` | +| 1 | 2 | `[1/2-θ, 1/2)` | + +On the middle interval write `t = 2|β|`. Then `t <= 1-2θ`, and the sum is +`exp(-a(1+t)) + exp(-a(1-t))`. For `0 <= t < m`, + +```text +(e^{at} + e^{-at}) - (e^{am} + e^{-am}) + = (e^{at} - e^{am}) (1 - e^{-a(t+m)}) < 0, +``` + +so the sum increases with `t`. Its maximum is the endpoint `m = 1-2θ`, where +the two factors are `2θ` and `2-2θ`: + +```text +exp(-2aθ) + exp(-2a(1-θ)). +``` + +On the incoming `g = 2` interval write `β = -1/2 + u` with `0 <= u < θ`. The +two factors become `2(1+2u)` and `2(1-u)`. Since `u >= 0` and `θ < 1`, +`1+2u > θ`, and since `u <= θ`, `1-u >= 1-θ`. Each term is therefore at most +the matching term of the middle endpoint, and the first is strictly smaller. +The outgoing `g = 2` interval `β = 1/2 - u` produces the same two factors. + +For a positive offset `h`, the same recurrence gives `ρh + β_{j-h} = β_j + s` +with `s = q_j - q_{j-h} >= h`. The square difference is `s(s + 2 β_j)`. Because +`β_j >= -1/2` and `s >= h >= 1`, + +```text +s(s + 2 β_j) >= s(s-1) >= h(h-1). +``` + +The negative offset is `s(s - 2 β_j)` with the column index's `β`, and +`β_j < 1/2` gives the same lower bound. Thus every `|h| = k >= 2` entry is at +most `exp(-a k(k-1))`. For `k >= 2`, + +```text +k(k-1) - (4k - 6) = (k-2)(k-3) >= 0, +``` + +so `exp(-a k(k-1)) <= exp(-2a) exp(-4a(k-2))`. One direction sums to at most +`exp(-2a)/(1-exp(-4a))`, and both directions to twice that. This is the tail +in #4402. It no longer needs `β_{i+h} = β_i + θh`. + +The pure-run exponent is not equal to the cut exponent. At `h = 1`, `s = 2` +and `β = 0` the cut exponent is 4 and the pure-run exponent is 1. The cut +entry is the smaller one. #4402's equality control remains in force. + +## The gap for every integer p >= 2 + +Let `x = 2 log(16p) / p^2` and `U = (16p)^{-8}`. The hypotheses give +`2aθ >= x`, `2aθ <= 5x` and `exp(-2a) <= U`, so + +```text +exp(-2a(1-θ)) <= U exp(5x), 4 exp(-2a) <= 4U. +``` + +Also `exp(-4a) <= U^2`. For `U^2 <= 1/2` the sharp tail is at most `4U`. At +`p = 2`, `U = 2^{-40}`, so this holds for every integer `p >= 2`. Therefore + +```text +off-sum <= exp(-x) + U (4 + exp(5x)). +``` + +Now `(16p)^4 <= 32^{p^2}`. Equality holds at `p = 2`. For `p >= 2`, +`(p+1)/p <= 3/2` and `32^{2p+1} = 32^5 · 32^{2(p-2)}`, while +`(3/2)^4 = 81/16 < 32^5`. The inequality is therefore strict for `p >= 3`, and +`x <= log(32)/2`. Hence `exp(5x) <= 4096 √2`. Since `17^2 = 289 > 288 = 2·12^2`, +`√2 < 17/12` and `4096 √2 < 17408/3`. The added 4 gives + +```text +4 + exp(5x) < 17420/3, off-sum < exp(-x) + (17420/3) U. +``` + +The series `1 + 1 + 1/2 + 1/6 = 8/3` and the positive next term give `e > 8/3`. +Then `(8/3)^4 - (8/3)^2 - 1 = 3439/81 > 0`. The derivative `4x^3 - 2x` is +positive for `x > 1`, so `e^4 - e^2 - 1 > 0`, which is `exp(-4) + exp(-2) < 1`. +In particular `exp(-2) < 9/64 < 1/2`. Also `1/k! <= 1/2^{k-1}` for `k >= 1`, +strictly at `k = 3`, so `e < 3 < 32` and `log(32) > 1`. Thus `x > 2/p^2`. + +From `e^y > 1 + y` for `y > 0`, `1 - exp(-x) > x/(1+x)`. The function +`t/(1+t)` is increasing, so `x/(1+x) > 2/(p^2+2)`. The slack is + +```text +2/(p^2+2) - 1/(8p^2) = (15p^2 - 2) / (8p^2 (p^2+2)). +``` + +For `p >= 2`, `p^2 + 2 <= 2p^2`, and the denominator is at most `16p^4`. The +polynomial + +```text +(15(p+1)^2 - 2)(p+1)^4 - (15p^2 - 2)p^4 + = 90p^5 + 225p^4 + 292p^3 + 213p^2 + 82p + 13 +``` + +has positive coefficients. Combined with the integer comparison +`17420 · 16 · 2^4 = 4459520 <= 3(15·4 - 2)(32)^8`, this yields + +```text +(17420/3) U <= (15p^2 - 2)/(16p^4) +``` + +for every integer `p >= 2`. The column gap is therefore strictly above +`1/(8p^2)`. + +## Truncation and a sufficient rounding budget + +Every off-diagonal entry is positive. Setting any of them to zero, including +every `|h| > W`, does not increase the off-sum. A positive diagonal alias is +not part of that off-sum; deleting it moves the diagonal toward the audit's +diagonal value 1. After those deletions the gap is still above `1/(8p^2)`. + +`GAUSSIAN.md` has bandwidth `< p`, so a column has at most `2(p-1)+1 = 2p-1` +nonzeros. If each changes by at most `ε` and `2p ε <= 1/(16p^2)`, the diagonal +falls by at most `ε` and the off-sum rises by at most `(2p-2)ε`. The gap loss +is strictly less than `1/(16p^2)`, and the gap stays above + +```text +1/(8p^2) - 1/(16p^2) = 1/(16p^2). +``` + +This is a sufficient budget. It is not a reading of the written precision, and +it is not `LOG-A`'s older `||H-N|| < 1/(16p)` estimate. + +## Not covered + +- Column sums of `A = diag(ahat) Ghat diag(ahat)^{-1}`. The audit gives + `log(a_i/a_j) = a(i-j)(β_i+β_j)` inside one cell. Conjugation by a + non-constant diagonal does not preserve column sums. Across cells the rounded + matrix uses the downward dyadic entries, which are not `n_{i,h}`. +- A step `g >= 3`. The audit assumes every step is in `{1, 2}`. +- `||N^{-1}||_1`. #4402 already turns a column gap of this shape into + `1/δ_col` inside a run. This package does not replay that inverse step and + does not claim it for `H`. +- The exponent replacements in #4406. They still wait on the rounded matrix. +- Any new κ. The selected record remains `23/10000`. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/gaussian-column-cut --check-only +python3.12 -B scripts/research_package.py --package research/gaussian-column-cut +``` + +The verifier is integer arithmetic only. Base `2a13eb1827784206202db90e5dc8327cf8a250db`, +priority revision 7, selection refresh κ = `23/10000`. + +Overlap on 2026-10-21, including open PRs and discussion #1166: #4402 is the +predecessor and stops at a constant-phase run. #4403 and #4406 treat the +`p^10` guards and the conditional halo exponents. #4435 is the broad-forward +turning-point asymptotic. No searched item states this `g ∈ {1, 2}` column +majorant. A search miss is not a novelty certificate. + +## Open next questions + +1. **What is the column off-sum of the rounded within-cell matrix?** + The callers invert `H`, whose within-cell block is + `diag(ahat) Ghat diag(ahat)^{-1}`. The ideal bound does not transfer through + that diagonal. The first step is to bound one column of + `Ghat_{j-k} ahat_j / ahat_k` on a single cell, using the pinned log-ratio + `a(i-j)(β_i+β_j)`, and then the downward entries used across a cell. The + blocker is that ratio: it changes column sums, and the across-cell rule is + not the ideal entry `n_{i,h}`. + +## Credit + +- The entry law and the row estimate are PR1673's, as quoted by #4100's + `LOG-A-PHASE-SCHUR-AUDIT.md` and `GAUSSIAN.md`. +- The in-run column majorant, and the question this package continues, are + Ryanson Jonathan's #4402. +- The gauge formula is the capped-gauge audit's. + +Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0. diff --git a/research/gaussian-column-cut/SOURCES.json b/research/gaussian-column-cut/SOURCES.json new file mode 100644 index 0000000000..c2826aa85e --- /dev/null +++ b/research/gaussian-column-cut/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/CAPPED-GAUGE-AUDIT.md", + "usage": "input", + "git_blob": "a2d1c5ae923db7649627dbf419434e36267e57c6", + "sha256": "1030a34922709ab8d3434a4c57a4a58934ae268c237fb598cb415697da411c9f" + }, + { + "path": "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md", + "usage": "input", + "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73", + "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + } + ] +} diff --git a/research/gaussian-column-cut/TASK.json b/research/gaussian-column-cut/TASK.json new file mode 100644 index 0000000000..9cd4b58531 --- /dev/null +++ b/research/gaussian-column-cut/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": "Prove the ideal narrow column off-sum across every legal step g in {1, 2}, and compare that gap with 1/(8p^2) under GAUSSIAN.md's stated a and theta inequalities.", + "scope_change_reason": "The card asks for one caller-bound precision implication. This package continues #4402's column gap from a constant-phase run to the ideal entry law at a g=2 step. It does not bound the rounded matrix the callers invert.", + "bottleneck_link": "The selected frontier is unchanged. A column gap of the rounded reference is what would let the halo exponents in #4406 move; the ideal matrix is the step before that transfer.", + "budget_minutes": 60, + "stop_rule": "Stop once the ideal column majorant and the uniform gap comparison are proved. Do not bound the gauge-conjugated matrix, do not edit the #4100 notes, and do not claim a new kappa.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/gaussian-column-cut", + "author": "James Reed", + "ai_assistance": "Substantial help from Cursor Grok 4.7 on the cut identities, the gap comparison and the package text.", + "open_questions": [ + { + "question": "What is the column off-sum of the rounded within-cell matrix diag(ahat) Ghat diag(ahat)^{-1}?", + "why_it_matters": "Callers invert that rounded reference. The ideal bound does not by itself move the halo exponents.", + "first_step": "Bound one column of Ghat_(j-k) ahat_j/ahat_k on a single cell from the pinned log-ratio a(i-j)(beta_i+beta_j), then the downward entries used across a cell.", + "blocked_by": "The ratio ahat_j/ahat_k changes column sums, and the across-cell rule is the downward dyadic entry rather than the ideal entry n_i,h." + } + ] +} diff --git a/research/gaussian-column-cut/VERIFY.json b/research/gaussian-column-cut/VERIFY.json new file mode 100644 index 0000000000..bca2288327 --- /dev/null +++ b/research/gaussian-column-cut/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/capped-phase-fusion/CAPPED-GAUGE-AUDIT.md", + "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md", + "research/unconditional-batched-crt/GAUSSIAN.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Cut identities, the shared majorant, and the gap comparison for every integer p >= 2." + } + ] +} diff --git a/research/gaussian-column-cut/verify.py b/research/gaussian-column-cut/verify.py new file mode 100644 index 0000000000..04024f8029 --- /dev/null +++ b/research/gaussian-column-cut/verify.py @@ -0,0 +1,252 @@ +#!/usr/bin/env python3 +"""Column off-sum of the ideal narrow Gaussian matrix at a g=2 step. + +Every comparison is an integer or rational identity. The exponential series +is used only through the partial sum of e and the remainder sign stated in +the README. This does not bound the gauge-conjugated matrix H. +""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "gaussian-column-cut" + + +def digest(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def add(left, right): + out = dict(left) + for key, coeff in right.items(): + out[key] = out.get(key, 0) + coeff + if out[key] == 0: + del out[key] + return out + + +def scale(poly, factor): + return {key: factor * coeff for key, coeff in poly.items() if factor * coeff} + + +def mul(left, right): + out = {} + for left_key, left_coeff in left.items(): + for right_key, right_coeff in right.items(): + key = tuple(a + b for a, b in zip(left_key, right_key)) + out[key] = out.get(key, 0) + left_coeff * right_coeff + return {key: coeff for key, coeff in out.items() if coeff} + + +def uni_add(left, right): + return add(left, right) + + +def uni_mul(left, right): + out = {} + for degree, coeff in left.items(): + for other, factor in right.items(): + key = degree + other + out[key] = out.get(key, 0) + coeff * factor + return {key: coeff for key, coeff in out.items() if coeff} + + +def pins_and_phrases() -> None: + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + for row in sources["files"]: + if row["usage"] == "input": + assert digest(ROOT / row["path"]) == row["sha256"], row["path"] + log_a = ( + ROOT / "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md" + ).read_text(encoding="utf-8") + gaussian = ( + ROOT / "research/unconditional-batched-crt/GAUSSIAN.md" + ).read_text(encoding="utf-8") + gauge = ( + ROOT / "research/capped-phase-fusion/CAPPED-GAUGE-AUDIT.md" + ).read_text(encoding="utf-8") + selected = json.loads( + (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8") + ) + assert "beta_i=rho*i-q_i" in log_a + assert "n_i,h=exp(-a[(rho*h+beta_i)^2-beta_(i+h)^2])" in log_a + assert "each in {1,2}" in log_a + assert "n_i,-1=exp(-a*g_i*(2rho-2beta_i-g_i))" in log_a + assert "n_i,+1=exp(-a*g_(i+1)*(2rho+2beta_i-g_(i+1)))" in log_a + assert "(rho*h+beta_i)^2-beta_(i+h)^2 >= h^2-|h|" in log_a + assert "||N-I||_infinity <= exp(-2a theta)+5 exp(-2a)`." in log_a + assert "nonzero periodic diagonal aliases" in log_a + assert "Use theta=t/s-1 in [1/(4p^2),1/p^2]" in gaussian + assert "Eventually 4log(16p)<=a<=5log(16p)." in gaussian + assert "||N-I||_infinity <= exp(-2a theta)+5exp(-2a)." in gaussian + assert "Thus its row gap exceeds 1/(8p^2) eventually." in gaussian + assert "W=O(sqrt(p)polylog(p))=1/(16p^2) and row norm<2." in gaussian + assert "does not assume that a row norm bounds a column norm." in gaussian + assert "log(a_i/a_j)=a(i-j)(beta_i+beta_j)" in gauge + assert "A=diag(ahat) Ghat diag(ahat)^-1" in gauge + assert selected["kappa"] == "23/10000" + + +def entry_algebra() -> None: + one = {(0, 0, 0): 1} + theta = {(1, 0, 0): 1} + beta = {(0, 1, 0): 1} + step = {(0, 0, 1): 1} + previous = add(add(add(beta, scale(one, -1)), scale(theta, -1)), step) + from_left = add( + scale(add(one, theta), 2), + add(scale(previous, 2), scale(step, -1)), + ) + assert from_left == add(step, scale(beta, 2)) + nxt = add(add(add(beta, one), theta), scale(step, -1)) + from_right = add( + scale(add(one, theta), 2), + add(scale(nxt, -2), scale(step, -1)), + ) + assert from_right == add(step, scale(beta, -2)) + bee = {(1, 0): 1} + ess = {(0, 1): 1} + square = add(mul(add(bee, ess), add(bee, ess)), scale(mul(bee, bee), -1)) + assert square == add(mul(ess, ess), scale(mul(ess, bee), 2)) + + +def step_dominates_the_pure_run_exponent() -> None: + # s(s+2β)-h(h+2β)=(s-h)(s+h+2β). At 2β=-1 the second factor is s+h-1. + hole = {(1, 0): 1} + pure = {(0, 1): 1} + beta_term = {(0, 0): 1} + gap = mul(add(hole, scale(pure, -1)), add(add(hole, pure), scale(beta_term, -1))) + expanded = add( + mul(add(hole, scale(pure, -1)), add(hole, pure)), + scale(add(hole, scale(pure, -1)), -1), + ) + assert gap == expanded + # A g=2 step is not the pure-run exponent. h=1, s=2, β=0: 4 against 1. + assert 2 * (2 + 2 * 0) == 4 + assert 1 * (1 + 2 * 0) == 1 + assert 4 > 1 + # At β=-1/2 the g=2 nearest exponent is 2, while the pure-run exponent is 0. + assert 2 * (2 - 1) == 2 + assert 1 * (1 - 1) == 0 + assert 2 > 0 + + +def regions_and_nearest_endpoints() -> None: + # θ<=1/4<1/2, so incoming g=2 and outgoing g=2 occupy disjoint beta intervals. + assert 2 * 1 < 4 + # β=-1/2+θ and both steps equal 1. Cleared of the denominator: + # 1+2β=2θ and 1-2β=2-2θ. + left_factor = uni_add(uni_add({0: 1}, {0: -1}), {1: 2}) + right_factor = uni_add(uni_add({0: 1}, {0: 1}), {1: -2}) + assert left_factor == {1: 2} + assert right_factor == {1: -2, 0: 2} + # The g=2 column at β=-1/2 has both nearest factors equal to 2. + assert 2 * (2 + (-1)) == 2 + assert 1 - (-1) == 2 + # At β=-1/2+θ the g=2 factor 2+4θ exceeds the both-steps-1 factor 2θ by 2+2θ. + excess = uni_add({1: 4, 0: 2}, scale({1: 2}, -1)) + assert excess == {1: 2, 0: 2} + assert all(coeff > 0 for coeff in excess.values()) + + +def side_columns_are_smaller() -> None: + # β=-1/2+u: factors 2(1+2u) and 2(1-u). u is the first variable, θ the second. + left = {(0, 0): 1, (1, 0): 2} + theta = {(0, 1): 1} + assert add(left, scale(theta, -1)) == {(0, 0): 1, (1, 0): 2, (0, 1): -1} + right_gap = add({(0, 1): 1}, scale({(1, 0): 1}, -1)) + assert right_gap == {(1, 0): -1, (0, 1): 1} + # θ<=1/4 makes the constant part 1-θ at least 3/4. + assert 4 - 1 == 3 + + +def tail_reduction() -> None: + # k(k-1)-(4k-6)=(k-2)(k-3), which is nonnegative for every integer k>=2. + quadratic = uni_add(uni_mul({1: 1}, {1: 1, 0: -1}), {1: -4, 0: 6}) + factored = uni_mul({1: 1, 0: -2}, {1: 1, 0: -3}) + assert quadratic == {2: 1, 1: -5, 0: 6} + assert factored == {2: 1, 1: -5, 0: 6} + # 2u/(1-u^2)<=4u/u = 4 once u^2<=1/2, so the sharp tail is at most 4u. + assert 2 * 2 == 4 + + +def exponential_bounds() -> None: + # Partial sum through 1/3! equals 8/3. The next term 1/24 is positive, so e>8/3. + assert 6 + 6 + 3 + 1 == 16 + assert 16 * 3 == 6 * 8 + assert (8 ** 4) - (8 ** 2) * (3 ** 2) - 3 ** 4 == 4096 - 64 * 9 - 81 + assert 4096 - 576 - 81 == 3439 + assert 3439 > 0 + # 1/(k+1) <= 1/2 for k>=1, so 1/k! <= 1/2^{k-1}, strictly at k=3. + assert 2 <= 1 + 1 + assert 1 * 4 < 6 + # Therefore e<3, so log(32)>1. + assert 32 > 3 + # sqrt(2)<17/12. + assert 17 * 17 > 2 * 12 * 12 + # 4096*sqrt(2) < 17408/3, and 4+17408/3=17420/3. + assert 4096 * 17 * 3 == 17408 * 12 + assert 4 * 3 + 17408 == 17420 + # (8/3)^2=64/9, so exp(-2)<9/64<1/2 once e>8/3. + assert 9 * 2 < 64 + + +def parameter_majorant() -> None: + # (16*2)^4 = 32^{2^2}. For p>=2 the inductive factor is strictly below 1. + assert (16 * 2) ** 4 == 32 ** 4 + # 3p - 2(p+1) = p-2, so (p+1)/p <= 3/2 for every integer p>=2. + assert uni_add({1: 3}, scale({1: 2, 0: 2}, -1)) == {1: 1, 0: -2} + # 2p+1-5 = 2(p-2), so 32^{2p+1} = 32^5 * 32^{2(p-2)}. + assert uni_add({1: 2, 0: 1}, {0: -5}) == {1: 2, 0: -4} + assert (2 + 1) ** 4 == 81 + assert 81 < 16 * 32 ** 5 + # 2*4*log = 8*log gives (16p)^{-8}; 2*5*log/p^2 = 5 * (2 log/p^2). + assert 2 * 4 == 8 + assert 2 * 5 == 10 + assert 10 == 5 * 2 + # Slack numerator 16p^2 - (p^2+2) = 15p^2-2. + assert 16 - 1 == 15 + assert 0 - 2 == -2 + # p^2+2 <= 2p^2 for p>=2, so the denominator 8p^2(p^2+2) <= 16p^4. + assert 2 <= 2 * 2 + assert 8 * 2 == 16 + growth = uni_mul({2: 15, 1: 30, 0: 13}, {4: 1, 3: 4, 2: 6, 1: 4, 0: 1}) + assert growth[6] == 15 + plain = {6: 15, 4: -2} + difference = uni_add(growth, scale(plain, -1)) + assert difference == {5: 90, 4: 225, 3: 292, 2: 213, 1: 82, 0: 13} + assert all(coeff > 0 for coeff in difference.values()) + # 17420*16*p^4 <= 3*(15p^2-2)*(16p)^8 at p=2, hence for every larger integer. + left = 17420 * 16 * 2 ** 4 + right = 3 * (15 * 2 * 2 - 2) * (16 * 2) ** 8 + assert left == 4459520 + assert left <= right + # U=(16p)^{-8}<=2^{-40}, so U^2<=2^{-80}<=1/2 and the sharp tail is <= 4U. + assert (16 * 2) ** 8 == 2 ** 40 + assert 2 ** 80 > 2 + # Bandwidth < p leaves at most 2p-1 nonzeros. Gap halves: 1/8-1/16=1/16. + assert 2 * (2 - 1) + 1 == 2 * 2 - 1 + assert 2 * 16 - 1 * 16 == 16 + assert 1 * 16 == 16 + + +def main() -> None: + pins_and_phrases() + entry_algebra() + step_dominates_the_pure_run_exponent() + regions_and_nearest_endpoints() + side_columns_are_smaller() + tail_reduction() + exponential_bounds() + parameter_majorant() + print("PASS_GAUSSIAN_COLUMN_CUT") + + +if __name__ == "__main__": + main()