diff --git a/research/narrow-row-half-gap/README.md b/research/narrow-row-half-gap/README.md new file mode 100644 index 0000000000..eb659ee46b --- /dev/null +++ b/research/narrow-row-half-gap/README.md @@ -0,0 +1,210 @@ +# The narrow row keeps half its certified gap + +**Claim type:** one quantified implication for the #4100 narrow reference row. +**No new κ.** The selected conditional value stays `60403/20000000 = 0.00302015`. + +`vendor/FINE-PRIME.md` says that deleting diagonal aliases preserves a +polynomial gap, and that exponentially accurate band truncation and rounding +preserve half of it. `GAUSSIAN.md` concludes that the rounded reference `H` +has diagonal 1, row gap at least `1/(16p^2)` and row norm below 2. The +coverage map still lists an explicit form of that half-gap sentence as open. +This note supplies the budget the sentence does not write down. + +## Statement + +Fix an integer `p ≥ 1`. Write `log` for the natural logarithm, as required by +the comparison `5 exp(-2a) ≤ 5/(16p)^8` in LOG-A §1 when `a ≥ 4 log(16p)`. +Let `a ≥ 4 log(16p)` and `θ ≥ 1/(4p^2)`, and set + +```text +S = exp(-2 a θ) + 5 exp(-2 a), γ = 1 - S. +``` + +The parameter minimum is the worst case: both terms of `S` fall as `a` or `θ` +grows. At that minimum, + +```text +γ ≥ 1/(8p^2). +``` + +Let a real row have nonnegative diagonal `d` and off-diagonal absolute sum +`Off`, with + +```text +Off + |d - 1| ≤ S. +``` + +Form the reference row as follows. + +1. **Alias removal.** Replace the diagonal by 1 and leave the off-diagonal + entries unchanged. +2. **Band truncation.** Replace any set of off-diagonal entries by 0. +3. **Rounding.** Add a real perturbation whose off-diagonal absolute row sum + is at most `τ`, then set the diagonal back to 1. + +The resulting diagonal is 1 and the row gap is at least `γ - τ`. In +particular, every + +```text +τ ≤ 1/(16p^2) +``` + +leaves row gap at least `1/(16p^2)` and absolute row sum strictly below 2. +Alias removal and truncation spend none of the certificate `γ`. Only rounding +spends it, and the published half is exactly this uniform budget. + +A sufficient per-entry rule is: at most `2p` off-diagonal entries change, and +each absolute value grows by at most `2^{-5p}`. At `p = 1` the total equals +`1/(16p^2)`. For every `p ≥ 1`, `(1 + 1/p)^3 ≤ 8 ≤ 32`, so the same comparison +persists at `p + 1`. The same count with `2^{-4p}` fails at `p = 1`. This does +not identify #4100's unnamed precision constant with 5. + +Any defect at most `p^M 2^{-c p}`, for integers `c ≥ 1` and `M ≥ 0`, is inside +the budget once `2^{c p} / p^{M+2}` is at least 16 and increasing. For `c = 1` +the checker records a sufficient such `p` for every `M ≤ 8`: 11, 16, 22, 29, +35, 42, 49, 57 and 64. FINE-PRIME's eventual row-norm bound +`poly(p) 2^{-(C-o(1))p}` therefore meets `τ ≤ 1/(16p^2)` for every fixed +`C > 0` and all large `p`. The implicit degree and the finite cutoff are not +extracted here. + +## Proof + +**Ideal certificate.** Let `x = 2 a θ`. The minimum is +`x ≥ 2 log(16p) / p^2`. The series remainder gives `exp(2) < 8`, so +`log(16p) > 2`. Thus the minimum `x` is greater than 1 at `p = 1` and at +`p = 2`. +The same series gives `exp(1) > 8/3`, hence `1 - exp(-1) > 5/8`. For these two +values of `p`, + +```text +γ ≥ 5/8 - 5 (16p)^{-8} ≥ 1/(8p^2). +``` + +For the Taylor step, `f(x) = 1 - x + x^2/2 - exp(-x)` satisfies `f(0) = f'(0) = 0` +and `f''(x) = 1 - exp(-x) ≥ 0` for `x ≥ 0`. Thus `f` and `f'` stay nonnegative, +`exp(-x) ≤ 1 - x + x^2/2`, and + +```text +1 - exp(-x) ≥ x(1 - x/2) ≥ x/2 for 0 ≤ x ≤ 1. +``` + +The partial sum of `exp(9/2)` through degree 5 exceeds 48, so the minimum `x` +is at most 1 at `p = 3`. The partial sum of `exp(7/2)` through degree 2 exceeds +2, and `(p+1)/p ≤ 4/3 < 2` for `p ≥ 3`, so `exp(p + 1/2) ≥ (p+1)/p`. Therefore +`16p ≤ exp(p^2/2)` persists for every integer `p ≥ 3`, and the worst-case `x` +stays at most 1. There + +```text +1 - exp(-x) ≥ x/2 ≥ log(16p)/p^2 ≥ 2/p^2, +γ ≥ 2/p^2 - 5 (16p)^{-8}. +``` + +Clearing the positive denominator is the integer comparison +`15 · 2^{32} ≥ 40`, which is exactly `2/p^2 - 5/(16p)^8 ≥ 1/(8p^2)` at `p = 1` +and is stronger for `p > 1`. + +**Three operations.** From `Off + |d - 1| ≤ S` and `d ≥ 0`: + +- if `d ≥ 1`, then `Off ≤ S - (d - 1)` and `1 - Off ≥ 1 - S`; +- if `0 ≤ d < 1`, then `Off ≤ S - (1 - d)` and `1 - Off ≥ 2 - S - d ≥ 1 - S`. + +Zeroing an off-diagonal entry cannot increase an absolute sum, whatever its +sign. A perturbation of off-diagonal absolute row sum `τ` increases that sum +by at most `τ`, by the triangle inequality. Resetting the diagonal to 1 +discards only the diagonal part of the perturbation. The gap is therefore at +least `γ - τ`. + +The budget is sharp relative to the certificate, whether or not the Gaussian +tail meets it. A row with `d = 1` and `Off = 1 - 1/(8p^2)`, and with truncation +removing nothing, is allowed by `γ ≥ 1/(8p^2)`. A defect of exactly `1/(16p^2)` +then leaves gap exactly `1/(16p^2)`, and a defect of `1/(8p^2)` leaves gap 0. +Alias mass or a deleted tail makes the final gap strictly larger, so those two +operations cannot be what forces the factor one half. The Gaussian value of +`S` may be strictly smaller than `1 - 1/(8p^2)`; that extra slack is not used. + +**Row norm and principal sections.** Diagonal 1 and off-sum at most +`1 - 1/(16p^2)` give absolute row sum `2 - 1/(16p^2) < 2`. A principal +subrow keeps a subset of the off-diagonal entries, so its absolute off-sum +is no larger and its gap is no smaller. + +**What the factor one half is not.** It is half of the published certificate +`1/(8p^2)`, not necessarily half of the true `γ`. The `x/2` branch is at least +`2/p^2` before the tiny tail, sixteen times `1/(8p^2)`. Extra slack is real +and unused. Charging each of `2p - 1` band entries with mass `1/(16p)`, the +old margin copied once per entry, produces a row change larger than +`1/(8p^2)` for every `p ≥ 2`. The budget has to be a total row sum. + +## What this does not prove + +LOG-A §3 already shows that one elimination step on a strictly row-diagonally +dominant matrix does not decrease the minimum absolute row gap. The identity +does not use the numerical size of the gap, so it applies to a matrix whose +gap is `1/(16p^2)`. This package does not re-prove that identity, and it does +not rerun the Gaussian circuit. + +The column statement in `research/gaussian-gauge-column` is a different +mechanism: a relative weight error inside one cell, with the explicit warning +that a row-sum bound does not replace it. #4402 and #4437 bound ideal column +sums. #4481 keeps a Schur margin of `1/(10p^2)` once that larger gap is +already known. None of those is the alias, truncation and rounding budget for +the row. + +The Neumann bound `‖H^{-1}‖_∞ ≤ 1/δ` applies after this lemma with +`δ = 1/(16p^2)`, because `H = I - E` with `‖E‖_∞ ≤ 1 - δ`. The `p^{10}` norm, +the chirp origin, across-cell columns and the unnamed setup constant remain +open. This is not an admission of #4100 and not a change to the selected +frontier. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 -B scripts/research_package.py --package research/narrow-row-half-gap --check-only +python3 -B scripts/research_package.py --package research/narrow-row-half-gap +``` + +`verify.py` pins the five source sentences, checks the series comparisons, the +uniform integer certificate, the three operations for `p = 1..200`, the `C = 5` +and `C = 4` entry rules, the polynomial thresholds, and the singular control. +It does not evaluate a Gaussian matrix and does not replay #4100. + +## Task and overlap + +- Card `uniform-transfer-audit`, scope refined to this one precision sentence. +- Base: canonical main `fbc9ea0249746acca4f504d4fda2b84e0e36cf0d`, priority + revision 7. #4100 remains pinned by the family record at + `337d04939571a637aeab54a0f58f54fde811663a`. +- The coverage map's still-open column, after dropping merged closures + including #4356, #4371, #4373, #4376 and #4377, puts this sentence at the + ninth remaining obligation. #4217 open question 1 and #4371 open question 2 + ask for the same explicit budget. +- #4438 records that its column gauge is not a row argument. This package is + that missing row argument. + +## Open next questions + +1. Does the stored narrow band have at most `2p` off-diagonal entries in every + row, and does the note's rounding meet absolute error `2^{-5p}`? The total + budget above is proved either way. The first step is the definition of `W` + in `GAUSSIAN.md` together with one rounding mode for a kernel entry. It is + blocked until that mode is pinned; the name `C` in the setup formula is not + yet a number. +2. Which chirp origin does the interior caller use? The coverage map lists + this beside the half-gap sentence, and #4304 shows that a centred chirp can + push one `p = 19` entry above 1. The first step is to name the origin in + the interior kernel and compare that one entry. This row budget does not + choose the origin. + +## Credit + +The ideal bound `‖N-I‖_∞ ≤ exp(-2aθ) + 5 exp(-2a)` is LOG-A §1 from PR1673. +PR1786, and #4100's byte-identical `vendor/FINE-PRIME.md`, state the half-gap +sentence. The `1/(8p^2)` certificate for every `p ≥ 1` is the merged +`pr1786-fine-prime-transfer-audit`. #4217 asked the question. #4438 +(James Reed) separated the within-cell column gauge from any row-sum charge. +#4402, #4437 and #4481 are the neighbouring column and Schur results cited +above and not reused as a row proof. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +No independent human or formal-kernel review is claimed. diff --git a/research/narrow-row-half-gap/SOURCES.json b/research/narrow-row-half-gap/SOURCES.json new file mode 100644 index 0000000000..7f9552dc79 --- /dev/null +++ b/research/narrow-row-half-gap/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "docs/research/pr4100-audit-coverage-map.md", + "usage": "input", + "git_blob": "8bcf878042c15f9f45652664999058b38c944030", + "sha256": "b9b45dbc288d5da63a8d0cb31cbaca83e7ff200f692dc481ff5b9a2616569203" + }, + { + "path": "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md", + "usage": "input", + "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73", + "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272" + }, + { + "path": "research/gaussian-gauge-column/README.md", + "usage": "input", + "git_blob": "7926f38cfcb0bbf0a47517ed5aa40e7f5a80dc5e", + "sha256": "82101b0310ea5f7b1c273a11fd1cd72185f025a158023379d976e747cb329c9b" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + }, + { + "path": "research/unconditional-batched-crt/vendor/FINE-PRIME.md", + "usage": "input", + "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3", + "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce" + } + ] +} diff --git a/research/narrow-row-half-gap/TASK.json b/research/narrow-row-half-gap/TASK.json new file mode 100644 index 0000000000..acad26c31c --- /dev/null +++ b/research/narrow-row-half-gap/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "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": "Does alias removal, band truncation and a row-sum rounding defect of 1/(16p^2) leave the #4100 narrow reference row a gap of at least 1/(16p^2)?", + "scope_change_reason": "The card asks for one quantified #4100 implication at its caller. This package takes only the narrow-row half-gap sentence that FINE-PRIME.md asserts in one line and that the coverage map still lists as open after the ideal 1/(8p^2) certificate. It does not audit CRT repair, the free-algebra lift, the column gauge or the chirp origin.", + "bottleneck_link": "#4100 proposes an unconditional exponent above the selected kappa. GAUSSIAN.md's inverse bounds use row gap delta >= 1/(16p^2). The half-gap sentence is the step from the proved ideal certificate 1/(8p^2) to that rounded gap. A missing budget there blocks treating the proposed inverse norm as proved. This audit does not change the selected frontier.", + "budget_minutes": 60, + "stop_rule": "Stop after the ideal certificate, the three row operations and the explicit rounding budget. Do not identify the unnamed setup constant, execute the Gaussian circuit, or choose the chirp origin.", + "outcome": "completed", + "evidence": "verify.py pins the five source sentences and checks the series comparisons, the uniform integer certificate, the three operations for every p from 1 through 200, the C=5 and C=4 entry rules, the polynomial thresholds through degree 8, and the singular control.", + "author": "unpaidmoon", + "ai_assistance": "Cursor Grok 4.7", + "open_questions": [ + { + "question": "Does the stored narrow band have at most 2p off-diagonal entries per row, and does #4100's rounding meet absolute error 2^{-5p}?", + "why_it_matters": "The total row-sum budget tau <= 1/(16p^2) is proved. The per-entry rule is only a sufficient special case, and the note's unnamed C is not shown to be at least 5.", + "first_step": "Pin the definition of W in GAUSSIAN.md and one rounding mode for a kernel entry, then compare 2 W eta with 1/(16p^2).", + "blocked_by": "The pinned sentences name W only as O(sqrt(p) polylog(p)) and do not fix the rounding mode." + }, + { + "question": "Which chirp origin does the interior caller use?", + "why_it_matters": "The coverage map lists this beside the half-gap sentence. A centred chirp can push one p=19 shifted-kernel entry above 1, so the row budget does not choose the matrix.", + "first_step": "Name the origin in the interior kernel and compare that one p=19 entry with the centred witness.", + "blocked_by": "The origin is a different hypothesis from the rounding budget." + } + ] +} diff --git a/research/narrow-row-half-gap/VERIFY.json b/research/narrow-row-half-gap/VERIFY.json new file mode 100644 index 0000000000..6531ffd189 --- /dev/null +++ b/research/narrow-row-half-gap/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "docs/research/pr4100-audit-coverage-map.md", + "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md", + "research/gaussian-gauge-column/README.md", + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/vendor/FINE-PRIME.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source-sentence pins, ideal-gap series comparisons, three row operations for p=1..200, C=5 and C=4 entry rules, polynomial thresholds, and the singular control." + } + ] +} diff --git a/research/narrow-row-half-gap/verify.py b/research/narrow-row-half-gap/verify.py new file mode 100644 index 0000000000..56daac7007 --- /dev/null +++ b/research/narrow-row-half-gap/verify.py @@ -0,0 +1,203 @@ +#!/usr/bin/env python3 +"""Explicit half-gap budget for #4100's narrow reference row. + +The checker uses only the standard library. It pins the one-sentence claim, +proves the ideal certificate 1-S >= 1/(8p^2) by exact comparisons, and checks +that alias removal and band truncation preserve that certificate while a +rounding defect of 1/(16p^2) leaves a row gap of 1/(16p^2). +""" + +from fractions import Fraction +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +FINE = ROOT / "research/unconditional-batched-crt/vendor/FINE-PRIME.md" +GAUSSIAN = ROOT / "research/unconditional-batched-crt/GAUSSIAN.md" +LOGA = ROOT / "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md" +COVERAGE = ROOT / "docs/research/pr4100-audit-coverage-map.md" +COLUMN = ROOT / "research/gaussian-gauge-column/README.md" + +HALF_SENTENCE = ( + "Omitting the exponentially small nonzero diagonal aliases and setting the\n" + "diagonal exactly to one preserves a polynomial gap. Exponentially accurate\n" + "band truncation and coefficient rounding preserve half of it." +) +GAUSSIAN_CLAIM = ( + "round at sufficiently high fixed precision so the reference H has diagonal1,\n" + "row gap delta>=1/(16p^2) and row norm<2." +) + + +def series(y, n): + """Partial sum of exp(y) through degree n, as an exact rational.""" + total = Fraction(0) + term = Fraction(1) + for k in range(n + 1): + total += term + term *= y / (k + 1) + return total + + +def exp2_upper(): + """exp(2) < sum_{k=0}^{8} 2^k/k! + 2^9/9! * 10/8 < 8.""" + total = series(Fraction(2), 8) + # Next term is 2^9/9!, and later terms shrink by at most 2/10. + remainder = Fraction(2) ** 9 / series_factorial(9) * Fraction(10, 8) + return total + remainder + + +def series_factorial(n): + value = 1 + for k in range(2, n + 1): + value *= k + return value + + +def ideal_certificate(): + """1 - exp(-2a theta) - 5 exp(-2a) >= 1/(8p^2) at the parameter minimum.""" + # exp(2) < 8, so ln(8) > 2 and ln(16p) > 2 for every integer p >= 1. + if not exp2_upper() < 8: + raise AssertionError(exp2_upper()) + # exp(1) > 8/3, so 1 - exp(-1) > 5/8. + if not series(Fraction(1), 6) > Fraction(8, 3): + raise AssertionError(series(Fraction(1), 6)) + # exp(7/2) > 2, used for the inductive step p -> p+1. + if not series(Fraction(7, 2), 2) > 2: + raise AssertionError(series(Fraction(7, 2), 2)) + # exp(9/2) > 48, so the worst-case x is at most 1 at p = 3. + if not series(Fraction(9, 2), 5) > 48: + raise AssertionError(series(Fraction(9, 2), 5)) + + # p = 1, 2: worst-case x >= 1, so 1-exp(-x) > 5/8. + for p in (1, 2): + tail = Fraction(5, (16 * p) ** 8) + if not Fraction(5, 8) - tail >= Fraction(1, 8 * p * p): + raise AssertionError((p, Fraction(5, 8) - tail)) + + # Every p >= 1: 2/p^2 - 5/(16p)^8 >= 1/(8p^2), the x <= 1 branch. + # 15 * 2^32 >= 40 is the cleared denominator at p = 1, and p^6 only helps. + if not 15 * (1 << 32) >= 40: + raise AssertionError("uniform polynomial comparison") + + +def gap_lower(off, diagonal=1): + return diagonal - off + + +def operations_preserve(p): + """Worst case and a strict improvement, for one integer p.""" + gamma = Fraction(1, 8 * p * p) + budget = Fraction(1, 16 * p * p) + # Certified row: Off + |d - 1| <= 1 - gamma, d >= 0. + # Tight case d = 1, Off = 1 - gamma, nothing truncated. + off = 1 - gamma + final_off = off + budget + if gap_lower(final_off) < budget: + raise AssertionError((p, gap_lower(final_off))) + if gap_lower(final_off) != gamma - budget: + raise AssertionError("tight rounding should spend exactly the budget") + # Row norm is 1 + off-sum < 2. + if not 1 + final_off < 2: + raise AssertionError((p, 1 + final_off)) + # Positive alias mass and a deleted tail both increase the gap. + alias = Fraction(1, 100 * p * p) + removed = Fraction(1, 100 * p * p) + improved = off - alias - removed + budget + if not gap_lower(improved) > budget: + raise AssertionError((p, gap_lower(improved))) + # Spending the whole certificate leaves gap 0. One extra unit makes it negative. + if gap_lower(off + gamma) != 0: + raise AssertionError("full certificate is sharp") + if not gap_lower(off + gamma + Fraction(1, p * p)) < 0: + raise AssertionError("control past the certificate should fail") + + +def per_entry_budget(): + """At most 2p entries, each moved by at most 2^{-5p}, meet the row budget. + + At p=1 the two sides are equal. For p>=1, (1+1/p)^3 <= 8 <= 32, so + 32(p+1)^3 <= 2^5 * 32 p^3. The inequality therefore persists for every + larger integer once it holds at p=1. + """ + if 32 * 1 ** 3 != 2 ** 5: + raise AssertionError("C=5 should meet p=1 with equality") + if (1 + 1) ** 3 > 32: + raise AssertionError("inductive factor") + if 32 * 1 ** 3 <= 2 ** (4 * 1): + raise AssertionError("C=4 must fail at p=1") + # The rejected per-entry copy of the old 1/(16p) margin. + for p in range(2, 21): + band = 2 * p - 1 + if not Fraction(band, 16 * p) > Fraction(1, 8 * p * p): + raise AssertionError(("coarse row charge", p)) + + +def polynomial_threshold(c, degree): + """Smallest p such that p^degree / 2^{c p} <= 1/(16 p^2) from there on.""" + power = degree + 2 + for p in range(1, 10000): + holds = 16 * p ** power <= 2 ** (c * p) + increases = (1 << c) * p ** power >= (p + 1) ** power + if holds and increases: + return p + raise AssertionError((c, degree)) + + +def polynomial_thresholds(): + expected = {0: 11, 1: 16, 2: 22, 3: 29, 4: 35, 5: 42, 6: 49, 7: 57, 8: 64} + for degree, want in expected.items(): + got = polynomial_threshold(1, degree) + if got != want: + raise AssertionError((degree, got, want)) + if polynomial_threshold(5, 3) != 1: + raise AssertionError("Cp bits with C=5 and degree 3 should hold at p=1") + + +def principal_and_neumann(): + """A principal subrow keeps the gap. A singular control has gap 0.""" + full = [Fraction(1), Fraction(1, 5), Fraction(1, 5), Fraction(1, 5)] + # Drop the last off-diagonal entry. + sub_off = sum(full[1:3]) + full_off = sum(full[1:]) + if not gap_lower(sub_off) > gap_lower(full_off): + raise AssertionError("principal deletion should widen the gap") + # [[1,1],[1,1]] has off-sum 1 and determinant 0. + if gap_lower(Fraction(1)) != 0: + raise AssertionError("gap 0 control") + if 1 * 1 - 1 * 1 != 0: + raise AssertionError("singular control") + + +def pin_sources(): + fine = FINE.read_text(encoding="utf-8") + gaussian = GAUSSIAN.read_text(encoding="utf-8") + loga = LOGA.read_text(encoding="utf-8") + coverage = COVERAGE.read_text(encoding="utf-8") + column = COLUMN.read_text(encoding="utf-8") + if HALF_SENTENCE not in fine: + raise SystemExit("FINE-PRIME half-gap sentence not found") + if "1/(16p^2)" in HALF_SENTENCE: + raise SystemExit("the one sentence must stay unquantified") + if GAUSSIAN_CLAIM not in gaussian: + raise SystemExit("GAUSSIAN.md conclusion not found") + if "`5exp(-2a)<=5/(16p)^8<1/(8p)`." not in loga: + raise SystemExit("LOG-A natural-log comparison not found") + if "alias removal, band truncation and rounding keep half the gap" not in coverage: + raise SystemExit("coverage-map obligation not found") + if "A row-sum bound does not replace this argument." not in column: + raise SystemExit("column package does not record the row separation") + + +def main(): + pin_sources() + ideal_certificate() + for p in range(1, 201): + operations_preserve(p) + per_entry_budget() + polynomial_thresholds() + principal_and_neumann() + print("PASS_NARROW_ROW_HALF_GAP") + + +if __name__ == "__main__": + main()