From 4f02def8bd1268b2dcb3506a96e3b14dc22171f2 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Sun, 18 Oct 2026 23:58:05 +0530 Subject: [PATCH 1/2] Independent reproof of the arithmetic layer of PR3562's ordinary-rate theorem (no kappa) Step-by-step reproof of the arithmetic layer of PR3562 (jmbarrancoml, abb93be8) from its stated premises, conditional on its line-154 physical bound (P5): moment certificates under two exact engines (integer-root bisection; rational interval atanh/exp series; PR3562's stated methods, implemented independently), the C0 majorant (parametric Lemma B), the e>=2^20 selector fit, the composed 4283584 C V e^(1-a) bound and the Consequence arithmetic. Every audited arithmetic step (a)-(e) holds. Line 158 is stated without derivation. The bounds listed beside it on line 156 (n<=e^(1-c), w<=2e^c) do not imply it (exact witness, ratio 2^(1-c)); n<=e/w from the selector definition on line 117 does, so 4283584 holds as written. Deriving line 158 from the two line-156 bounds alone would give 8033584. Not audited: the physical composition behind line 154 (lines 141-154), history/preparation/reserve (84-104), binary transfer (172-174) and the space/restoration/ownership claims (20-25). Includes source binding to the selected bit supplier, a convention-explicit ceiling remark for the c(1-c) shape (sup b(1-b)), and seven frozen negative controls. Not a kappa, frontier change or multiplication theorem. Co-Authored-By: Claude Opus 5.5 --- .../PROOF.md | 314 ++++++++++++++ .../README.md | 211 +++++++++ .../SOURCES.json | 36 ++ .../TASK.json | 78 ++++ .../VERIFY.json | 24 ++ .../verify.py | 399 ++++++++++++++++++ 6 files changed, 1062 insertions(+) create mode 100644 research/pr3562-ordinary-coupling-reproof-audit/PROOF.md create mode 100644 research/pr3562-ordinary-coupling-reproof-audit/README.md create mode 100644 research/pr3562-ordinary-coupling-reproof-audit/SOURCES.json create mode 100644 research/pr3562-ordinary-coupling-reproof-audit/TASK.json create mode 100644 research/pr3562-ordinary-coupling-reproof-audit/VERIFY.json create mode 100644 research/pr3562-ordinary-coupling-reproof-audit/verify.py diff --git a/research/pr3562-ordinary-coupling-reproof-audit/PROOF.md b/research/pr3562-ordinary-coupling-reproof-audit/PROOF.md new file mode 100644 index 0000000000..af5d907408 --- /dev/null +++ b/research/pr3562-ordinary-coupling-reproof-audit/PROOF.md @@ -0,0 +1,314 @@ +# Independent reproof of the arithmetic layer of PR3562's ordinary-rate theorem + +Sagar Thakrar (`thakrarsagar`), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. + +**Object.** [PR3562](https://github.com/CrocSwap/integer-mult-bounds/pull/3562) +by Jose Manuel (`jmbarrancoml`), head `abb93be8b9ceca07a2b17f3a97db7bb6b074271d`, +file `research/retuned-ordinary-coupling/PROOF.md` (sha256 +`3e554832c38b4b801f55b20868679f3283bc90cd5a9d8ce1960f828ed2655f22`). Line +numbers below refer to that file. I wrote this reproof from that PROOF.md and +its stated premises only. I did not read PR3562's EVIDENCE.md, certificate or +verifier code. + +**Verdict.** + +- Every audited arithmetic step (a)-(e) holds from premises P1-P5 below. +- One exposition gap. Line 156 lists `n<=e^(1-c)`, `w<=2e^c` and the bound + `n^(1-c)w <= 2^c e^(1-a)` of line 158. Line 158 is stated without + derivation. The two bounds listed beside it do not imply it: alone they give + only `n^(1-c)w <= 2e^(1-a)` (exact witness below). +- The inequality `n <= e/w` follows from the selector definition + `n=floor((e-k)/w)` on line 117 of the same file, and it does imply line 158. + So the stated bound, and the constant `4283584`, hold exactly as written. +- Deriving line 158 from the two line-156 bounds alone would give the + coefficient `8033584`. The O-bound `O_q(V e^(1-a))` would be unchanged. + +**Scope.** This is an independent check of a scoped all-size arithmetic +implication, P1-P5 ⇒ (2) and the Consequence, under PR3562's retained +source/refinement and physical-cost premises. It does not admit those +premises. In particular it takes PR3562's line 154 as premise P5, although +PR3562 derives that line (lines 141-154) from physical claims audited nowhere +here. It does not reprove history, preparation and reserve (lines 84-104), the +binary transfer (lines 172-174), or the space, restoration and ownership claims +(lines 20-25). It is not a κ, not a frontier change and not a complete +multiplication theorem. + +## Premises used (all stated in PR3562's PROOF.md) + +- P1 (lines 36-41): m=64, W=28416, H={1:381024, 2:400416, 3:22752, + 4:26880, 5:29376, 6:17376, 7:26784, 42:288}, ε=10^-16, F=32·64²·ΣH_r=118606528512. +- P2 (lines 45-50): the C0 recurrence for normalized time T(n,w), with f=floor(n/64): + T(n,w) ≤ Cw for 0 1. + +**μ_(576/577).** It is enclosed by two exact engines. They use the same two +methods that PR3562 says it used (lines 64-72), implemented independently +without reading PR3562's code: + +- E1, integer-root bisection. For each r, find the integer z with + z^577·64^576 ≤ r^576·Q^577 < (z+1)^577·64^576, at Q=2^128 (PR3562: 2^160). Then + z/Q ≤ (r/64)^(576/577) < (z+1)/Q. +- E2, a rational interval series. It encloses ln 2, ln 3, ln 5 and ln 7 by + atanh(1/m) series for m=3,5,9,15, each with an explicit geometric tail. It then + forms L_r = ln(64/r) and encloses exp(t·L_r) by a Horner Taylor sum. All + terms are positive, so outward dyadic rounding at 2^-256 is monotone, and the + Lagrange tail is u^(K+1)/(K+1)!·1/(1-u/(K+2)). Finally + (r/64)^t = 1/exp(t·L_r). + +Both engines combine the eight radix terms and the fallback term with exact +nonnegative rational weights: + +| engine | enclosure of μ_(576/577) | width (printed by verify.py) | +|---|---|---| +| E1 | 0.999998938581682162866772413602788… | 9.358e-38 | +| E2 | 0.999998938581682162866772413602788… | 1.695e-77 | + +Both enclosures lie inside PR3562's 10^-30 enclosure, and +10^6(1-μ_(576/577)) = 1.0614183178… > 1 under both. The fallback term is +retained. Without it, μ_(576/577) = 0.999998938575113…, which is outside PR3562's +enclosure. So PR3562's stated enclosure is the fallback-inclusive moment, as +claimed. + +**Source binding.** The verifier binds P1 to main: + +- H and W match the selected bit supplier: the "nine" profile and live count + in `research/e8-bit-p111-tuned/tune/EXPECTED.json`, whose `bit_lower` equals the + selected `ASSEMBLY.json` value. +- εF/W matches the literal `118606528512 / (10000000000000000 * 28416)` in + `research/lean-bit-moment-discharge/lean/Selected.lean`. + +## (b) The C0 majorant (parametric) + +**Lemma B.** Let 0 1.2. The verifier also checks 2^D(e) ≤ e² for every + 2 ≤ e ≤ 2^20. As a side computation it prints the largest ratio + D(e)/floor(log2 e) there: 22/19, first attained at e = 941248. + The induction uses child rank r_max = 42; it needs 2log2(64/r_max) ≥ 1, + that is r_max ≤ 45. +2. *Stock exponent.* By P4, K(w) < q·q^4096·q^(4096(w-1)) = q^(4096w+1). So + stock < q^((4096w+1)D(e)) whenever D(e) ≥ 1. Hence + k ≤ (4096w+1)D(e) ≤ 4097w·2log2(e) = 8194 w log2(e) ≤ 8195 w log2(e). + If D(e)=0, then stock=1 and k=0. Since w=ceil(e^c) ≤ e^c+1 ≤ 2e^c, + k ≤ 16390 e^c log2(e) for e ≥ 2, as stated on line 123. +3. *2k 1/(1-c), so in particular for e ≥ 2^20. Thus + 2k/e ≤ 32780 g(e) ≤ 32780·20·2^(20c)/2^20. Also 20c < 20/512 = 5/128, and + 2^(5/128) < 17/16 because 17^128 > 32·16^128. So + 2k/e < 32780·20·(17/16)/2^20 = 696575/2^20 < 1. +4. *n ≥ 64.* From 2k (e/2)/(2e^c) = e^(1-c)/4. + Hence n=floor((e-k)/w) > e^(1-c)/4 - 1 ≥ 2^10/4 - 1 > 64, since c<1/2. + +So for e ≥ 2^20 neither elementary predicate fires, as stated on lines 133-135. +At e=2^20 itself: w=2, D=22 and k ≤ 180246. The worst case of k then gives +n ≥ 434165, an exact boundary check. + +## (d) The composed bound (2): the 2^c factor and the constant + +In the non-elementary branch, P3 gives n=floor((e-k)/w) with k ≥ 0. So + + n ≤ e/w. (N) + +Together with e^c ≤ w ≤ 2e^c and 1-a = 1-c+c²: + + n^(1-c) w ≤ (e/w)^(1-c) w = e^(1-c) w^c ≤ e^(1-c)(2e^c)^c = 2^c e^(1-a). (*) + +Also 2^c < 2^(1/512) < 17/16, because 17^512 > 2·16^512. This is +line 158's inequality. + +**The derivation gap (lines 156-158).** Line 156 lists n ≤ e^(1-c), w ≤ 2e^c and +the bound of line 158; line 158 is stated without derivation. Lines 160-161 bound +only k, w and 1, so n ≤ e^(1-c) is what bounds the 801n term. The two bounds listed +beside line 158 do not imply it: alone they give +n^(1-c)w ≤ e^((1-c)²)·2e^c = 2e^(1-a), not 2^c e^(1-a). + +*Witness.* For c=p/q, take e=2^q. The values n=e^(1-c)=2^(q-p) and +w=2e^c=2^(p+1) satisfy both line-156 bounds with equality. For them, +log2(n^(1-c)w) - log2(2^c e^(1-a)) = 1-c exactly. So the ratio is +2^(1-c) > 2^(511/512) > 17/16, which violates line 158's conclusion. These +values have nw = 2^(q+1) > e, so they violate (N). They also violate +w = ceil(e^c) = 2^p (line 18). (N) excludes the witness, and (N) follows from +line 117. So line 158 is true for the actual selector; what is missing is only +its derivation. + +**Constant.** The remaining terms of P5 are bounded as follows, for e ≥ 1 and +c < 1/512: + +- n ≤ e/w ≤ e^(1-c) ≤ e^(1-a); +- w ≤ 2e^c ≤ 2e^(1-a), since c ≤ 1-a ⟺ (1-c)² ≥ 0; +- 1 ≤ e^(1-a); +- k ≤ 16390 e^c log2(e) ≤ 32780 e^(1-a). This uses log2(x) ≤ 2x^s for x ≥ 1 and + s=(1-c)²: max_{x≥1} log2(x)/x^s = 1/(s·exp(1)·ln 2) < 2, because s·exp(1)·ln 2 > 1/2. + For e=1, k=0. + +Hence + + T_B(e)/V ≤ C e^(1-a) (801 + 4000000·17/16 + 32780 + 2 + 1) = 4283584 C e^(1-a). + +The identity 801 + 4250000 + 32780 + 2 + 1 = 4283584 is exact. Deriving line 158 +from the two line-156 bounds alone (factor 2) would give +801 + 8000000 + 32780 + 3 = 8033584. This derivation of (2) does not use +e ≥ 2^20, so it covers every e at which the non-elementary branch is taken. + +**Elementary branch and setup.** + +- For e < 2^20, a < c < 1/512 gives e^a < 2^(20/512) < 2. So C·V·e < 2C·V·e^(1-a) + fits (2). This reads the "elementary fallback coefficient" of line 142, used on + lines 165-166, as T_elem ≤ C·V·e; PR3562 does not write that form explicitly. +- For e ≥ 2^20, step (c) rules out the elementary branch. +- *Setup absorption* (1+log2 V)^4 ≤ 512V for V ≥ 1, by a different route from + PR3562's. Since ln 2 > 1/2, 1+log2 V ≤ 1+y with y = 2ln V. Then + (1+y)^4 exp(-y/2) is maximized at y=7, where it equals 8^4 exp(-7/2) < 4096/33 < 512. + The verifier certifies exp(7) > 33² with E2's exp bounds. + +## (e) Consequence arithmetic + +- The excess is exact: a - C_complex = 576/332929 - 1729033982646513517717/10^24 + = 354445191478901059996907/(332929·10^24) ≈ 1.0646e-6 > 0, as on line 181. +- E2 brackets the selected bit root inside (b_sel, b_sel+10^-24], with + b_sel = 0.001733427039589844234749. Hence 1/577 < b < 1/576. +- The ratio 576/577² exceeds C_complex, while 577/578² < C_complex. +- (j-1)/j² - j/(j+1)² = (j²-j-1)/(j²(j+1)²) > 0 for j ≥ 2, so (j-1)/j² is + decreasing on j ≥ 2. +- Together these give the restricted statement on lines 183-187: among couplings 1/j, + j ≥ 2, only j=577 passes both tests. + +C_complex is PR2979's primitive complex lower bound. Main's archived comparator +`research/rank7-coupled-586-588-carrier-fold/comparators/PR2979-CLAIM.json` +records `complex_lower` = 1729033982646513517717/10^24 and +κ = complex_lower - 10^-46 - 10^-70. So line 181 compares primitive with primitive. + +## Gap classification + +| step | status | consequence | +|---|---|---| +| (a) μ_1, μ_(576/577) | proved, two engines, inside the stated enclosure | none | +| (b) majorant (1) | proved (Lemma B, parametric) | none | +| (c) fit for e ≥ 2^20 | proved; 8195 is looser than the 8194 that P4 gives | none | +| (d) line 158 | exposition gap: stated without derivation; not implied by the bounds listed on line 156, implied by (N) from line 117 | 4283584 stands; deriving from the line-156 bounds alone gives 8033584, same O-bound | +| (d) elementary branch | holds; reads the elementary cost as C·V·e (implicit in PR3562) | none | +| (e) consequence | exact | none | + +For the consumers ([PR3576](https://github.com/CrocSwap/integer-mult-bounds/pull/3576), +`kumagi`; [PR3690](https://github.com/CrocSwap/integer-mult-bounds/pull/3690), `zxv`), +the audited arithmetic implication holds, including the inherited 4283584. It is +conditional on P5 and PR3562's other retained premises. This narrows, and does not +lift, PR3576's stated limit that the all-size PR3562 theorem is not independently +reproved. + +Steps (b)-(d) are parametric. At PR3690's c=1/576 with M=10^6, the (c)-(d) +arithmetic gives the same 4283584 and a = 575/331776. This assumes PR3690 keeps the +same selector and stock definitions (D with child rank 42, K(w)), the same P5 +composition, A=200 and the same P2 form for R437. PR3690 reports its own two-engine +moment enclosure; I did not recheck it or bind its R437 histogram. Under the +selected histogram, μ_(575/576) > 1, because 1/576 > b. + +## Ceiling remark (proof shape, not a barrier) + +This shape needs μ_(1-c) < 1, that is c < b, where b is the fallback-inclusive +root. The function c(1-c) is increasing on (0,1/2). So on the selected bit program +the shape's exponent has supremum b(1-b) = 0.001730422270288263023337…, not attained. +E2 places the root in (b_sel, b_sel+10^-24], where b_sel is the selected +bit_saving. E1 independently brackets it in (10/5769, 9/5192). verify.py certifies +that the fallback-free root lies above b_sel + 10^-24 (decimal cross-checks in the +review passes put it about 2.0·10^-12 higher), so the selected value is the +fallback-inclusive root. + +**Like-for-like comparisons.** PR2979, PR3633, PR3642 and PR3653 each state their +endpoint as κ = X - 10^-46 - 10^-70, with X a primitive complex lower bound (the +modern outer). So the like-for-like comparison is a or b(1-b) against X, primitive +with primitive. Under the retained transfer x ↦ x/(1+x), both sides move by the same +increasing map and no order changes. I do not use the mixed comparison of a/(1+a) +against a modern-outer κ, which this loop's sibling PR3700 withdrew. + +| endpoint X | a - X, a = 576/332929 | b(1-b) - X | +|---|---|---| +| PR2979 | +1.0646e-6 | +1.3883e-6 | +| PR3633 | +2.246e-9 | +3.259e-7 | +| PR3642 | -2.958e-7 | +2.788e-8 | +| PR3653 | -3.203e-7 | +3.371e-9 | + +The reciprocal coupling clears PR2979 and PR3633 but not PR3642 or PR3653. A +non-reciprocal c can still clear PR3653, inside a window of width about 3.4e-9 +below b. One E2-only example: c' = b_sel - 10^-9 gives c'(1-c') - X_3653 = +2.374e-9. +It needs M = 305992814, so the coefficient is 2601006087/2 ≈ 1.3e9. This is a remark +about the shape's reach, not a claimed endpoint. Which primitive binds is decided by +the complex side; this audit does not change it. + +On a different supplier, pending PR3690 (R437, c=1/576) reports a = 575/331776. +verify.py prints 575/331776 - X for all four endpoints; the smallest is +2.678e-6 +(PR3653). So this ceiling matters only if R437 is not admitted. R437's moments are +not checked here. + +## Not covered + +- PR3562's retained premises: P5 and its physical composition (lines 141-154), and + the PR2753/PR2809/PR2899/PR2808 inventory, history and wrapper arguments. +- History, preparation and reserve (lines 84-104) and the bit-wrapper transfer + (lines 172-174). +- The O_q(V)+F_q space bound, borrowed-input restoration and ownership claims + (lines 20-25). +- PR3562's code, EVIDENCE.md and production factory. +- PR3576's T74 binding, and PR3690's R437 source binding and moments. diff --git a/research/pr3562-ordinary-coupling-reproof-audit/README.md b/research/pr3562-ordinary-coupling-reproof-audit/README.md new file mode 100644 index 0000000000..722aec5b35 --- /dev/null +++ b/research/pr3562-ordinary-coupling-reproof-audit/README.md @@ -0,0 +1,211 @@ +# Independent reproof of the arithmetic layer of PR3562's ordinary-rate theorem (no κ) + +**Result.** I reproved the arithmetic layer of the all-size ordinary-rate theorem in +[PR3562](https://github.com/CrocSwap/integer-mult-bounds/pull/3562) (Jose Manuel, +`jmbarrancoml`, head `abb93be8b9ceca07a2b17f3a97db7bb6b074271d`) from its stated +premises. Every audited arithmetic step holds: + +- (a) the two moment certificates; +- (b) the C0 majorant; +- (c) the e ≥ 2^20 selector fit; +- (d) the composed bound `T_B(e) <= 4283584 C V e^(1-a)` with `a = 576/332929`; +- (e) the Consequence arithmetic. + +The audit is conditional on PR3562's line-154 physical bound, called P5 here: +`T_B(e)/V <= C(801n + 4000000 n^(1-c) w + k + w + 1)`. P5 is PR3562's own derivation +step (lines 141-154), which I take as a premise. Its coefficients are one line of +arithmetic: two reversed C0 calls, each on padded volume below 2V, times majorant (1), +plus the wrapper bill. That gives 801 = 2·2·200 + 1 and 4000000 = 2·2·10^6. The physical +claims behind that line are not audited here (see Inherited assumptions). + +I found one **exposition gap** and no mathematical gap. Line 156 lists `n <= e^(1-c)`, +`w <= 2e^c` and the bound `n^(1-c) w <= 2^c e^(1-a)` of line 158. Line 158 is stated +without derivation, and the two bounds listed beside it do not imply it. An exact +witness exceeds it by the ratio 2^(1-c). The inequality `n <= e/w`, which follows from +the selector definition `n = floor((e-k)/w)` on line 117, does imply it. So line 158 +and `4283584` hold as written. Deriving line 158 from the two line-156 bounds alone +would give only a factor of 2 and the coefficient `8033584`, with the same O-bound. + +For the consumers [PR3576](https://github.com/CrocSwap/integer-mult-bounds/pull/3576) +(Hiroki KUMAZAKI, `kumagi`) and [PR3690](https://github.com/CrocSwap/integer-mult-bounds/pull/3690) +(`zxv`): the arithmetic layer they inherit holds, including 4283584, conditional on P5 +and PR3562's other retained premises. This narrows, and does not lift, PR3576's stated +limit that the all-size PR3562 theorem is not independently reproved. Still unaudited +are lines 141-154 (the physical composition behind P5), lines 84-104 (history, +preparation and reserve), lines 172-174 (binary transfer) and lines 20-25 (space +bound, borrowed-input restoration and ownership). PR3690's R437 moments are not +checked here. + +**Scope.** This is an independent check of a scoped all-size arithmetic implication, +P1-P5 ⇒ (2) and the Consequence. It assumes PR3562's retained source/refinement and +physical-cost premises and does not admit them. It is not a κ, not a frontier change +and not a complete multiplication theorem. + +## What is checked, and how + +[PROOF.md](PROOF.md) has the written reproof, the gap classification and the ceiling +remark. [verify.py](verify.py) is stdlib-only, uses exact `Fraction` arithmetic, takes +about 5 s and stays under 40 MB RSS. + +- **Two exact engines** for the moments μ_t = (Σ_r H_r (r/64)^t + εF(1/64)^t)/W. + Both use the same two methods PR3562 says it used (lines 64-72), but I implemented + them independently without reading PR3562's code: + - E1, integer-root bisection: z^q·64^p ≤ r^p·Q^q < (z+1)^q·64^p, at Q = 2^128 + (PR3562 uses 2^160); + - E2, a rational interval series: atanh-based logarithms and a Horner exp with a + Lagrange tail, using outward dyadic rounding. + + μ_1 = 2874298095721977/2890625000000000 < 199/200. Both engines enclose μ_(576/577) + as 0.999998938581682162866772413602788… (the verifier prints widths 9.358e-38 for E1 + and 1.695e-77 for E2). Both enclosures lie inside PR3562's stated 10^-30 enclosure, + and 10^6(1-μ) = 1.0614 > 1. +- **Source binding to main.** + - H and W are the selected bit supplier's "nine" profile and live count in + `research/e8-bit-p111-tuned/tune/EXPECTED.json`. Its `bit_lower` equals the selected + `ASSEMBLY.json` endpoint. + - εF/W is the literal in `research/lean-bit-moment-discharge/lean/Selected.lean`. + - The selected certificate hash is checked through `certificates/selected-result.json`. + - E2 shows that the selected `bit_saving` 0.001733427039589844234749 is the + fallback-inclusive root truncated to 24 digits. The fallback-free root lies about + 2.0e-12 higher; that figure comes from decimal cross-checks in the review passes, + and verify.py certifies only that it lies above b_sel + 10^-24. E1 brackets the root + in (10/5769, 9/5192). +- **Steps (b)-(d) parametric** in rational c ∈ (17/10000, 1/512). Lemma B covers any + histogram whose moments satisfy A(1-μ_1) ≥ 1 and M(1-μ_t) ≥ 1. At c = 1/576 with + M = 10^6 (PR3690's choice), the (c)-(d) arithmetic also gives 4283584. This holds + provided PR3690 keeps the same selector and stock definitions (D with child rank 42, + K), the same P5 composition and A = 200. +- **Line-158 witness.** At e = 2^q with c = p/q, the values n = e^(1-c) and w = 2e^c + satisfy both line-156 bounds with equality. They exceed line 158's bound by exactly + 2^(1-c) > 17/16. They also violate n ≤ e/w and w = ceil(e^c) (line 18), so the + selector excludes them. The verifier checks this exponent arithmetic. The + classification as an exposition gap rests on the written argument in PROOF.md. + +## Reproduce + +From the repository root, on base `20ecf2891d80b5acf18d980b2164fb44ea7faa90`: + +```sh +python3 -B research/pr3562-ordinary-coupling-reproof-audit/verify.py +``` + +Expected last line: + +```text +PASS_PR3562_REPROOF_AUDIT: audited arithmetic steps (a)-(e) hold from P1-P5; line-156 bounds alone give factor 2, n <= e/w from line 117 gives 2^c; coefficient 4283584 justified +``` + +To also check PR3562's exact bytes and literals, run: + +```sh +git fetch origin pull/3562/head +git show abb93be8b9ceca07a2b17f3a97db7bb6b074271d:research/retuned-ordinary-coupling/PROOF.md > /tmp/pr3562-PROOF.md +python3 -B research/pr3562-ordinary-coupling-reproof-audit/verify.py --pr3562-proof /tmp/pr3562-PROOF.md +``` + +The expected PROOF.md sha256 is `3e554832c38b4b801f55b20868679f3283bc90cd5a9d8ce1960f828ed2655f22`. +That file is not vendored, because the package pin format accepts only same-path head pins. + +**Negative controls.** These seven run through the same `audit()` function and must +each be rejected; the verifier fails if any is accepted: + +| control | rejected at | +|---|---| +| c = 9/5192, just above b | (a) μ not below 1 | +| c = 10/5769 with M = 10^6 | (a)/(b) M too small | +| H_7 + 1 | source binding | +| fallback term dropped | (a) outside PR3562's enclosure | +| reciprocal j = 576 | (e) | +| reciprocal j = 578 | (e) | +| factor 2 instead of 2^c | (d) 8033584 ≠ 4283584 | + +The "fallback dropped" control fails only against PR3562's stated enclosure. At +c = 1/577 the fallback-free moment would still satisfy 10^6(1-μ) > 1. The need for the +fallback term comes from the G(f) term in Lemma B's written proof, not from this control. + +I froze the code before the single control sweep (verify.py sha256 recorded in VERIFY.json). + +## Ceiling remark (proof shape only) + +The c(1-c) shape needs μ_(1-c) < 1, which means c < b. So on the selected bit program +its exponent has supremum b(1-b) = 0.0017304222702882630233…, which is not attained. + +PR2979, PR3633, PR3642 and PR3653 state κ = X − 10^-46 − 10^-70 under the modern outer, +so I compare against their primitive complex lower bounds X. This is primitive against +primitive. It avoids the mixed a/(1+a)-versus-modern-κ comparison that the sibling PR3700 +withdrew. + +- The reciprocal a = 576/332929 exceeds X for PR2979 (+1.0646e-6) and PR3633 (+2.246e-9). +- It falls short of X for PR3642 (−2.958e-7) and PR3653 (−3.203e-7). +- The supremum b(1-b) exceeds PR3653's X by 3.371e-9, so only a narrow window of + non-reciprocal c just below b clears PR3653 (example in PROOF.md). +- On a different supplier, pending PR3690 (R437, c = 1/576) reports a = 575/331776. That + exceeds every X here, by at least +2.678e-6 (PR3653). So this ceiling matters only if + R437 is not admitted. R437's moments are not checked here. + +These are statements about the proof shape, not a claimed endpoint. + +## Inherited assumptions and unresolved obligations + +- P5 is assumed, not audited. It rests on these physical claims (PR3562 lines 141-154): + - there are exactly two reversed C0 calls; + - each call's padded volume is below 2V; + - each call costs its padded volume times the normalized time T at the same n; + - the wrapper bill CV(n+k+w+1) is complete. + Also assumed: the retained PR2753/PR2809/PR2899/PR2808 inventory, history and + wrapper arguments. +- Not audited: history, preparation and reserve (lines 84-104), the bit-wrapper + transfer to binary width E (lines 172-174), and the O_q(V)+F_q space bound with its + borrowed-input restoration and ownership claims (lines 20-25). +- The elementary branch is read as costing at most C·V·e. PR3562 names the "elementary + fallback coefficient" on line 142 and uses it on lines 165-166, but does not write + that form explicitly. +- PR3562's code, EVIDENCE.md and factory are not reviewed. They were deliberately not + read, to keep this reproof independent. +- Not re-audited: PR3576's T74 step, and PR3690's R437 source binding and moments. + +## Open next questions + +The structured form (question, why_it_matters, first_step, blocked_by) is in +[TASK.json](TASK.json). + +1. **Derive line 158 in PR3562?** Citing `n <= e/w` (line 117) at lines 156-158 makes + the written derivation match the stated bound. This is the author's call. First + step: a one-line edit to PR3562 PROOF.md. +2. **Audit the physical inputs behind P5.** Its arithmetic is checked here. The + remaining trust lies in four claims: exactly two calls, padded volume below 2V per + call, cost scaling with padded volume at the same n, and a complete wrapper bill, + plus the elementary cost ≤ C·V·e and setup absorbed into C. First step: trace them in + PR2899/PR2808's wrapper bill. +3. **Decoupled width exponent.** With w = ceil(e^γ) and γ < c, the shape's saving + becomes c(1-γ), not c(1-c). The retained PR2753 history estimates need + γ ≥ 17/10000. Does a decoupled γ raise the reach to about b(1 − 17/10000)? First + step: redo (d) with separate γ and recheck lines 86-97. +4. **Recheck PR3690's R437 moments at c = 1/576.** PR3690 reports its own two-engine + enclosure. Still open: an independent recheck with this package's engines, and + binding of its R437 histogram to source. Blocked by: not reading PR3690's pipeline + in this audit. + +## Credit and provenance + +- Object: PR3562 by Jose Manuel (`jmbarrancoml`), head `abb93be8b9ceca07a2b17f3a97db7bb6b074271d`. + It builds on David Arias's PR2753 (`DavidAriasC`), Jose Manuel's PR2809 and PR2899, + and Nick Petalas's PR2808 (`petalas`), as credited there. +- Consumers named, not re-audited: + - PR3576, Hiroki KUMAZAKI (`kumagi`), head `1630afea0fc1083717b5b2799b8de7a819a6ea02`; + - PR3690, `zxv`, head `03c141ef1fd372cf42951488767537e55675c072`. +- Endpoints cited: + - PR2979, `mdumitrean`, merged archive, head `be191346391661f4d35fc0d1508d0a6029572576`; + - PR3633, Pierre-Loic Doulcet (`hexapode`), head `2969dce9739c4043330ddf76f395ca0dd3a90baa`; + - PR3642, `roger-sato`, head `6568db75adbb61437190545f6fef1534c70e91e5`; + - PR3653, `rohanarun`, head `607a09ff441c79b215a8127a81f4cc70021d0d9b`. +- Convention note: PR3700 (this account's sibling loop, head `aa0bd9fbc8700506b1fafcc55bca9bd32aced7d9`). +- Selected bit supplier and moment literal: `research/e8-bit-p111-tuned` and + `research/lean-bit-moment-discharge` on main, credited in their own packages. + +The verifier and proof were reviewed by four independent AI review passes in the same +loop: reproducibility, adversarial mathematics, provenance and referee. This is not +human review, and none is claimed. Source pins are in [SOURCES.json](SOURCES.json). + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. diff --git a/research/pr3562-ordinary-coupling-reproof-audit/SOURCES.json b/research/pr3562-ordinary-coupling-reproof-audit/SOURCES.json new file mode 100644 index 0000000000..83d2c32575 --- /dev/null +++ b/research/pr3562-ordinary-coupling-reproof-audit/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + { + "path": "research/lean-bit-moment-discharge/lean/Selected.lean", + "usage": "input", + "git_blob": "129c0b14ec5510fa587c9cf365481333c3da2d8f", + "sha256": "1d63b79d222e3518c90a9018ee8116397361ec34bd3cba85a921bc3850a8cf45" + } + ] +} diff --git a/research/pr3562-ordinary-coupling-reproof-audit/TASK.json b/research/pr3562-ordinary-coupling-reproof-audit/TASK.json new file mode 100644 index 0000000000..5c0b850ca1 --- /dev/null +++ b/research/pr3562-ordinary-coupling-reproof-audit/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.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 the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "refined", + "actual_scope": "Prove or falsify, step by step from its stated premises, the arithmetic layer of PR3562's all-size ordinary-rate theorem (head abb93be8b9ceca07a2b17f3a97db7bb6b074271d, research/retuned-ordinary-coupling/PROOF.md): moment certificates, C0 majorant, e>=2^20 selector fit, the composed 4283584 C V e^(1-a) bound with a=576/332929, and the Consequence arithmetic, conditional on its line-154 physical bound (P5); classify any gap and state the reach of the c(1-c) proof shape like for like. Not covered: the physical composition behind line 154 (lines 141-154), history/preparation/reserve (84-104), binary transfer (172-174), space/restoration/ownership (20-25).", + "scope_change_reason": "The card asks for one exact all-size implication proved or falsified; this instantiates it on the specific open theorem that two consumers (PR3576, PR3690) depend on and that had no independent check.", + "bottleneck_link": "The ordinary-rate theorem is an all-size transfer obligation consumed by PR3576 and PR3690; an independent reproof of its arithmetic layer (with its constant) narrows what those consumers still inherit unchecked to the physical premises. Side output: the exact reach of the c(1-c) shape on the selected bit program.", + "budget_minutes": 60, + "stop_rule": "Stop when every audited step is proved or a failing step is pinned with an exact witness; if (d) is only a constant gap, report the justified or corrected coefficient and do not chase other premises.", + "outcome": "completed", + "evidence": "verify.py (stdlib, exact): two moment engines (integer-root bisection; rational interval atanh/exp series; same methods as PR3562 states, implemented independently) agree inside PR3562's 10^-30 enclosure; source binding to the selected bit supplier and Selected.lean fallback literal; P5 coefficient composition 801 = 2*2*200+1; parametric (c)-(d) arithmetic; line-158 witness; selected bit_saving shown to be the fallback-inclusive root; seven frozen negative controls rejected. PROOF.md gives the written reproof. Result: every audited arithmetic step (a)-(e) holds from P1-P5. Line 158 is stated without derivation; the bounds listed beside it on line 156 (n<=e^(1-c), w<=2e^c) do not imply it (exact witness, ratio 2^(1-c)), while n<=e/w from line 117 does, so 4283584 holds as written; deriving line 158 from the two line-156 bounds alone would give 8033584.", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for the reproof, verifier and text; reviewed by four independent AI review passes in the same loop (reproducibility, adversarial mathematics, provenance, referee), not by a human.", + "open_questions": [ + { + "question": "Should PR3562 derive line 158 from n<=e/w (line 117) at lines 156-158?", + "why_it_matters": "Consumers quote the composed constant; the fix makes the written derivation match the stated bound verbatim.", + "first_step": "One-line edit to PR3562 PROOF.md line 156.", + "blocked_by": "Author's decision." + }, + { + "question": "Are the physical inputs behind PR3562's line-154 bound (P5) correct: exactly two reversed C0 calls, padded volume below 2V per call, cost equal to padded volume times T at the same n, a complete wrapper bill CV(n+k+w+1), elementary cost <= C*V*e and setup absorbed into C?", + "why_it_matters": "The arithmetic from these inputs to 801 and 4000000 (2*2*200+1, 2*2*10^6) and on to 4283584 is checked here; the theorem's remaining trust lies in these physical inputs.", + "first_step": "Trace the wrapper bill and padding in PR2899/PR2808.", + "blocked_by": "none" + }, + { + "question": "Does a decoupled width exponent gamma (w=ceil(e^gamma), gamma= e^(17/10000)." + }, + { + "question": "Does an independent recheck with this package's two engines confirm PR3690's reported R437 moments (mu_1<199/200 and mu_(575/576)<1-10^-6), with its R437 histogram bound to source?", + "why_it_matters": "PR3690 reports its own two-engine enclosure; with an independent recheck, steps (b)-(d) here cover its c=1/576 template, provided PR3690 keeps the same D (child rank 42), K, P5 composition, A=200 and P2 form.", + "first_step": "Bind the R437 histogram and run the two engines of this package.", + "blocked_by": "Out of this audit's scope (PR3690 pipeline not read)." + } + ] +} diff --git a/research/pr3562-ordinary-coupling-reproof-audit/VERIFY.json b/research/pr3562-ordinary-coupling-reproof-audit/VERIFY.json new file mode 100644 index 0000000000..945f2a403a --- /dev/null +++ b/research/pr3562-ordinary-coupling-reproof-audit/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "research/lean-bit-moment-discharge/lean/Selected.lean" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Two exact moment engines inside PR3562's enclosure; source binding to the selected bit supplier; P5 coefficient composition; parametric (c)-(d) arithmetic; line-158 witness; fallback-inclusive root binding; seven negative controls rejected through audit(). Frozen verify.py sha256 e91884740bd07b208d6b735f5c46b6b024f3e857be9ba1f0a239eadbcbca7e15" + } + ] +} diff --git a/research/pr3562-ordinary-coupling-reproof-audit/verify.py b/research/pr3562-ordinary-coupling-reproof-audit/verify.py new file mode 100644 index 0000000000..b8ee411a16 --- /dev/null +++ b/research/pr3562-ordinary-coupling-reproof-audit/verify.py @@ -0,0 +1,399 @@ +#!/usr/bin/env python3 +"""Independent exact audit of the arithmetic layer of PR3562's ordinary-rate theorem. + +Two exact engines (E1 integer-root bisection, E2 rational interval log/exp +series), source binding to the selected bit supplier on main, the arithmetic +of PROOF.md steps (a)-(e) from premises P1-P5, the line-158 witness and a frozen control +sweep. Stdlib only; no floating-point value is accepted as evidence. + +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +import argparse +import hashlib +import json +import sys +from functools import lru_cache +from fractions import Fraction as Fr +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + +# Literals under audit: PR3562 head abb93be8b9ceca07a2b17f3a97db7bb6b074271d, +# research/retuned-ordinary-coupling/PROOF.md (sha256 below; --pr3562-proof checks the bytes). +PR3562_HEAD = "abb93be8b9ceca07a2b17f3a97db7bb6b074271d" +PR3562_PROOF_SHA256 = "3e554832c38b4b801f55b20868679f3283bc90cd5a9d8ce1960f828ed2655f22" +HIST = {1: 381024, 2: 400416, 3: 22752, 4: 26880, 5: 29376, 6: 17376, 7: 26784, 42: 288} +CLAIM = { + "hist": HIST, "W": 28416, "eps": Fr(1, 10**16), "F": 118606528512, + "c": Fr(1, 577), "A": 200, "M": 10**6, + "enclosure": (Fr(999998938581682162866772413602, 10**30), Fr(999998938581682162866772413603, 10**30)), + "fallback": True, "two_power": "2^c", "coeff": 4283584, "j": 577, + "C_complex": Fr(1729033982646513517717, 10**24), "excess": 354445191478901059996907, +} +# Endpoints X of the pending complex claims; each PR states kappa = X - 10^-46 - 10^-70 +# (modern outer), so X is a primitive complex lower bound and compares like for like with a. +ENDPOINTS = { + "PR2979 (merged archive, mdumitrean)": Fr(1729033982646513517717, 10**24), + "PR3633 (hexapode)": Fr(1730096363528623534230, 10**24), + "PR3642 (roger-sato)": Fr(1730394391813963415120, 10**24), + "PR3653 (rohanarun)": Fr(1730418899766071163804, 10**24), +} +E1_BRACKET = (Fr(10, 5769), Fr(9, 5192)) # best rationals below/above b with denominator <= 6000 + + +class AuditFailure(Exception): + pass + + +def need(ok, msg): + if not ok: + raise AuditFailure(msg) + + +# ---------------- E1: integer-root bisection ---------------- +@lru_cache(maxsize=None) +def e1_pow(r, t): + """Enclose (r/64)^t, t=p/q, by [z/Q,(z+1)/Q], Q=2^bits, with z^q 64^p <= r^p Q^q < (z+1)^q 64^p.""" + p, q = t.numerator, t.denominator + need(0 < r < 64 and 0 < t <= 1 and q <= 6000, "E1 needs 0 1: + mid = (lo + hi) >> 1 + if mid**q * den <= rhs: + lo = mid + else: + hi = mid + need(lo**q * den <= rhs < hi**q * den, "E1 invariant") + return Fr(lo, Q), Fr(hi, Q) + + +# ---------------- E2: rational interval log/exp series ---------------- +P = 256 # dyadic outward-rounding precision (bits) + + +def rdn(x): + return Fr((x.numerator << P) // x.denominator, 1 << P) + + +def rup(x): + return Fr(-((-x.numerator << P) // x.denominator), 1 << P) + + +def atanh_inv(m, terms=140): + """Enclose atanh(1/m)=sum z^(2k+1)/(2k+1), z=1/m; tail <= z^(2K+1)/((2K+1)(1-z^2)).""" + z2, t, s = Fr(1, m * m), Fr(1, m), Fr(0) + for k in range(terms): + s += t / (2 * k + 1) + t *= z2 + return s, s + t / ((2 * terms + 1) * (1 - z2)) + + +def _iadd(*xs): + return sum(x[0] for x in xs), sum(x[1] for x in xs) + + +def _iscale(k, x): + return (k * x[0], k * x[1]) if k >= 0 else (k * x[1], k * x[0]) + + +def ln_table(): + a3, a5, a9, a15 = (atanh_inv(m) for m in (3, 5, 9, 15)) + ln2 = _iscale(2, a3) + ln3 = _iadd(ln2, _iscale(2, a5)) # 3/2 -> atanh(1/5) + ln5 = _iadd(_iscale(2, ln2), _iscale(2, a9)) # 5/4 -> atanh(1/9) + ln7 = _iadd(_iscale(3, ln2), _iscale(-2, a15)) # 7/8 -> -atanh(1/15) + ln = {1: (Fr(0), Fr(0)), 2: ln2, 3: ln3, 4: _iscale(2, ln2), 5: ln5, + 6: _iadd(ln2, ln3), 7: ln7, 42: _iadd(ln2, ln3, ln7)} + # L_r = ln(64/r) = 6 ln2 - ln r > 0 + return {r: _iadd(_iscale(6, ln2), _iscale(-1, v)) for r, v in ln.items()} + + +LN64 = None + + +def exp_bounds(u, terms=120): + """For rational u>=0 return (lo, hi) with lo <= exp(u) <= hi (Horner, outward rounding, Lagrange tail).""" + need(u >= 0 and terms + 2 > u, "exp_bounds domain") + ul, uh = rdn(u), rup(u) + sl = sh = Fr(1) + for k in range(terms, 0, -1): + sl = rdn(1 + ul * sl / k) + sh = rup(1 + uh * sh / k) + tail = Fr(1) + for k in range(1, terms + 2): + tail *= uh / k + tail = rup(tail / (1 - uh / (terms + 2))) + return sl, sh + tail + + +@lru_cache(maxsize=None) +def e2_pow(r, t): + """Enclose (r/64)^t = exp(-t ln(64/r)) for rational t in (0,1].""" + global LN64 + if LN64 is None: + LN64 = ln_table() + lo_L, hi_L = LN64[r] + return 1 / exp_bounds(t * hi_L)[1], 1 / exp_bounds(t * lo_L)[0] + + +def moment(params, t, engine): + """Enclose mu_t = (sum_r H_r (r/64)^t + eps F (1/64)^t)/W.""" + W, lo, hi = params["W"], Fr(0), Fr(0) + terms = [(h, r) for r, h in params["hist"].items()] + if params["fallback"]: + terms.append((params["eps"] * params["F"], 1)) + for weight, r in terms: + a, b = engine(r, t) + lo += weight * a + hi += weight * b + return lo / W, hi / W + + +def mu1(params): + v = sum(Fr(h * r, 64) for r, h in params["hist"].items()) + if params["fallback"]: + v += params["eps"] * params["F"] / 64 + return v / params["W"] + + +# ---------------- source binding ---------------- +def sha(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def bind_sources(params): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for row in sources["files"]: + if row.get("usage") == "input": + need(sha(ROOT / row["path"]) == row["sha256"], "source pin mismatch: " + row["path"]) + record = json.loads((ROOT / "certificates/selected-result.json").read_text()) + need(sha(ROOT / record["certificate"]) == record["certificate_sha256"], "selected certificate hash") + assembly = json.loads((ROOT / record["certificate"]).read_text()) + nine = json.loads((ROOT / "research/e8-bit-p111-tuned/tune/EXPECTED.json").read_text())["nine"] + need(nine["bit_lower"] == assembly["bit_lower"], "supplier/assembly bit endpoint differ") + supplier = {int(k): v for k, v in nine["profile"].items()} + need(params["hist"] == supplier, "histogram differs from the selected bit supplier") + need(params["W"] == nine["bit"]["live"], "W differs from the selected bit supplier") + need(params["F"] == 32 * 64**2 * sum(params["hist"].values()), "F != 32*64^2*sum H") + lean = (ROOT / "research/lean-bit-moment-discharge/lean/Selected.lean").read_text() + need("%d / (%d * %d)" % (params["F"], 1 / params["eps"], params["W"]) in lean, + "fallback weight eps*F/W is not the main-side Selected.lean literal") + return Fr(assembly["bit_lower"]) + + +# ---------------- the audit ---------------- +@lru_cache(maxsize=None) +def selector_D(N): + D = [0] * (N + 1) + for e in range(64, N + 1): + D[e] = 1 + D[42 * (e >> 6)] + return tuple(D) + + +def depth_ratio_max(N): + """Side computation: max of D(e)/floor(log2 e) over 2 <= e <= N, as (ratio, first e attaining it).""" + D, best, arg = selector_D(N), Fr(0), None + for e in range(2, N + 1): + if D[e] * best.denominator > best.numerator * (e.bit_length() - 1): + best, arg = Fr(D[e], e.bit_length() - 1), e + return best, arg + + +@lru_cache(maxsize=None) +def depth_bound_ok(N): + D = selector_D(N) + return all(2**D[e] <= e * e for e in range(2, N + 1)) # D(e) <= 2 log2 e + + +def fit_and_composition(c, M, two_power="2^c", claimed=None): + """Steps (c)-(d) for rational c in (17/10000, 1/512) and majorant coefficient M (histogram-free).""" + need(Fr(17, 10000) < c < Fr(1, 512), "c outside (17/10000, 1/512)") + # (c) selector fit for e >= 2^20 (analytic proof in PROOF.md; exact boundary arithmetic here) + need(17**128 > 32 * 16**128, "(c) 2^(5/128) < 17/16") + need(20 * c < Fr(5, 128), "(c) 20c < 5/128") + need(2 * 8195 * 2 == 32780 and 32780 * 20 * 17 == 696575 * 16 and 696575 < 2**20, "(c) 2k/e boundary") + D = selector_D(2**20) + need(depth_bound_ok(2**20), "(c) D(e) <= 2 log2 e fails") + e0 = 2**20 + need(c.denominator <= 10**30, "c must be an explicit rational") + w0 = 2 # ceil(e0^c): 1 < 2^(20c) < 2^(5/128) < 2 for 0 < c < 1/512 + k0 = (4096 * w0 + 1) * D[e0] # k <= (4096 w + 1) D(e) from |GL_64|= 64, "(c) fit predicates at e = 2^20") + need(Fr(e0, 4 * w0) - 1 > 64, "(c) e^(1-c)/4 - 1 > 64 at e = 2^20") + # (d) composition: coefficient, the 2^c factor and the line-156 gap witness + p, q = c.numerator, c.denominator + need(2 * 16**512 < 17**512, "(d) 2^c < 2^(1/512) < 17/16") + if LN64 is None: + e2_pow(1, Fr(1)) + ln2_lo = LN64[1][0] / 6 + # log2 x <= 2 x^s for x >= 1, s=(1-c)^2: max of log2(x)/x^s is 1/(s e ln2), so need s*e*ln2 >= 1/2 + need((1 - c)**2 * exp_bounds(Fr(1))[0] * ln2_lo >= Fr(1, 2), "(d) log2 e <= 2 e^((1-c)^2)") + # setup absorption (1+log2 V)^4 <= 512 V: with y=2 ln V, (1+y)^4 e^(-y/2) <= 8^4 e^(-7/2) < 4096/33 + need(exp_bounds(Fr(7))[0] > 33**2 and Fr(4096, 33) <= 512, "(d) setup absorption") + factor = Fr(17, 16) if two_power == "2^c" else Fr(2) + coeff = 801 + 4 * M * factor + 2 * 8195 * 2 + 2 + 1 + if claimed is not None: + need(coeff == claimed, "(d) coefficient %s != claimed %s" % (coeff, claimed)) + a = c * (1 - c) + # premise-extremal witness at e=2^q: n=e^(1-c)=2^(q-p), w=2e^c=2^(p+1); exponents of 2: + lhs = (q - p) * (1 - c) + p + 1 # log2(n^(1-c) w) + rhs = c + q * (1 - a) # log2(2^c e^(1-a)) + need(lhs - rhs == 1 - c, "(d) witness identity") + need(2**511 * 16**512 > 17**512, "(d) witness ratio 2^(1-c) > 2^(511/512) > 17/16") + need((q - p) + (p + 1) > q, "(d) witness violates n <= e/w (excluded by n=floor((e-k)/w))") + return {"a": a, "coeff": coeff, "coeff_cited_premises_only": 801 + 4 * M * 2 + 32780 + 3} + + +def audit(params, full=True): + out = {} + bit_lower = bind_sources(params) + c, A, M = params["c"], params["A"], params["M"] + t = 1 - c + need(Fr(17, 10000) < c < Fr(1, 512), "c outside (17/10000, 1/512)") + # P5 composition: two C0 calls x padded volume < 2V x majorant (A, M), plus wrapper bill (n+k+w+1) + need(2 * 2 * A + 1 == 801, "P5: 801 != 2*2*A + 1") + + # (a) moment certificates, two engines + m1 = mu1(params) + need(A * (1 - m1) > 1, "(a) A(1-mu_1) <= 1") + encs = {"E1": moment(params, t, e1_pow), "E2": moment(params, t, e2_pow)} + for name, (lo, hi) in encs.items(): + need(lo <= hi, name + " empty") + need(hi < 1, "(a) %s: mu_(1-c) not certified below 1" % name) + need(M * (1 - hi) > 1, "(a)/(b) %s: M(1-mu_(1-c)) <= 1, majorant coefficient too small" % name) + if params.get("enclosure"): + L, U = params["enclosure"] + need(L <= lo and hi <= U, "(a) %s enclosure not inside PR3562's stated enclosure" % name) + out["mu_1"] = m1 + out["mu_t"] = encs + + out.update(fit_and_composition(c, M, params["two_power"], params["coeff"])) + a = out["a"] + + # (e) consequence arithmetic and reciprocal restriction + C = params["C_complex"] + need(a - C == Fr(params["excess"], 332929 * 10**24), "(e) stated excess") + need(a > C, "(e) a <= C_complex") + j = params["j"] + need(Fr(1, j) < bit_lower and Fr(j - 1, j * j) > C, "(e) reciprocal 1/%d fails" % j) + out["reciprocal"] = {jj: (Fr(1, jj) < bit_lower, Fr(jj - 1, jj * jj) > C) for jj in (576, 577, 578)} + + if not full: + return out + # root binding and ceiling: E2 at the selected endpoint, E1 on a small-denominator bracket + blo, bhi = bit_lower, bit_lower + Fr(1, 10**24) + need(moment(params, 1 - blo, e2_pow)[1] < 1 < moment(params, 1 - bhi, e2_pow)[0], + "root: selected bit_saving does not bracket the fallback-inclusive root") + nofb = dict(params, fallback=False) + need(moment(nofb, 1 - bhi, e2_pow)[1] < 1, "root: fallback-free root not separated") + lo1, hi1 = E1_BRACKET + need(moment(params, 1 - lo1, e1_pow)[1] < 1 < moment(params, 1 - hi1, e1_pow)[0], "root: E1 bracket") + need(lo1 < blo and bhi < hi1, "root: E1 bracket does not contain the E2 bracket") + need(Fr(1, 577) < blo and bhi < Fr(1, 576), "root: 1/577 < b < 1/576") + out["root"] = (blo, bhi) + # informational (E2 only): one non-reciprocal c' inside the window where c'(1-c') exceeds PR3653's X + cw = blo - Fr(1, 10**9) + mw = moment(params, 1 - cw, e2_pow)[1] + Mw = int(1 / (1 - mw)) + 1 + need(mw < 1 and Mw * (1 - mw) > 1, "window example") + out["window"] = (cw, cw * (1 - cw), Mw, fit_and_composition(cw, Mw)["coeff"]) + out["ceiling"] = (blo * (1 - blo), bhi * (1 - bhi)) + return out + + +def controls(): + base = dict(CLAIM) + altered = dict(HIST) + altered[7] += 1 + return { + "c just above b (c = 9/5192 = b + 9.0e-9)": dict(base, c=E1_BRACKET[1], enclosure=None), + "M = 10^6 too small (c = 10/5769 = b - 2.4e-8)": dict(base, c=E1_BRACKET[0], enclosure=None), + "altered histogram (H_7 + 1)": dict(base, hist=altered), + "fallback dropped": dict(base, fallback=False), + "reciprocal j = 576": dict(base, j=576), + "reciprocal j = 578": dict(base, j=578), + "factor 2 instead of 2^c": dict(base, two_power="2"), + } + + +def check_pr3562_bytes(path): + data = Path(path).read_bytes() + need(hashlib.sha256(data).hexdigest() == PR3562_PROOF_SHA256, "PR3562 PROOF.md sha256") + text = data.decode() + for lit in ("{1:381024,2:400416,3:22752,4:26880,", "5:29376,6:17376,7:26784,42:288}", + "W=28416", "epsilon=10^-16", "F=32*64^2*sum H_r=118606528512", + "999998938581682162866772413602", "999998938581682162866772413603", + "c=1/577, w=ceil(e^c), a=c(1-c)=576/332929", "T(n,w)<=200C n+1000000C n^(576/577)w.", + "k<=8195w log2(e)<=16390e^c log2(e).", "4283584 C V e^(1-a)", + "I use n<=e^(1-c), w<=2e^c and", "n^(1-c)w<=2^c e^(1-c+c^2)<(17/16)e^(1-a).", + "C_complex=1729033982646513517717/10^24", "354445191478901059996907/(332929*10^24)>0."): + need(lit in text, "PR3562 literal not found: " + lit) + + +def dec(x, digits=28): + s = "-" if x < 0 else "" + x = abs(x) + i = x.numerator * 10**digits // x.denominator + return s + str(i // 10**digits) + "." + str(i % 10**digits).zfill(digits) + + +def main(): + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("--pr3562-proof", help="optional path to PR3562's PROOF.md at head " + PR3562_HEAD) + args = ap.parse_args() + if args.pr3562_proof: + check_pr3562_bytes(args.pr3562_proof) + print("PR3562 PROOF.md bytes and audited literals: match") + r = audit(CLAIM) + (l1, h1), (l2, h2) = r["mu_t"]["E1"], r["mu_t"]["E2"] + print("(a) mu_1 =", r["mu_1"], "<", Fr(199, 200)) + print("(a) mu_(576/577) E1 in [%s, %s], width %.3e" % (dec(l1, 33), dec(h1, 33), h1 - l1)) + print("(a) mu_(576/577) E2 in [%s, %s], width %.3e" % (dec(l2, 33), dec(h2, 33), h2 - l2)) + print("(a) both inside PR3562's 10^-30 enclosure and below 999999/10^6") + print("(b) 200(1-mu_1) > 1 and 10^6(1-mu_(576/577)) > 1 under both engines") + print("(c) 17^128 > 32*16^128; 2k/e <= 696575/2^20 < 1; 2^D(e) <= e^2 on [2, 2^20]; fit holds at e = 2^20") + rmax, emax = depth_ratio_max(2**20) + print("(c) side computation: max D(e)/floor(log2 e) on [2, 2^20] =", rmax, "first at e =", emax) + print("(d) P5 = 2 calls x 2V x (200n + 10^6 n^(1-c) w) + (n+k+w+1): 801 = 2*2*200+1, 4000000 = 2*2*10^6") + print("(d) 2^c < 17/16; log2 e <= 2e^((1-c)^2); (1+log2 V)^4 <= 512V; line-158 witness: the line-156 bounds alone allow n^(1-c)w = 2^(1-c) * 2^c e^(1-a)") + print("(d) coefficient 801 + 4250000 + 32780 + 2 + 1 = %d (uses n <= e/w from line 117);" % CLAIM["coeff"], + "the line-156 bounds n<=e^(1-c), w<=2e^c alone give factor 2: coefficient", r["coeff_cited_premises_only"]) + print("(e) a - C_complex = %s; reciprocal (1/jC): %s" % (dec(r["a"] - CLAIM["C_complex"]), r["reciprocal"])) + tpl = fit_and_composition(Fr(1, 576), 10**6) + print("(c)-(d) parametric template at c = 1/576, M = 10^6 (PR3690's c; assumes the same D, K, P5 composition and A = 200; R437 moments not checked here): coefficient", + tpl["coeff"], "a =", tpl["a"]) + blo, bhi = r["root"] + print("root: fallback-inclusive root in (%s, %s] (selected bit_saving + 10^-24); E1 bracket (10/5769, 9/5192)" % (dec(blo, 24), dec(bhi, 24))) + cl, ch = r["ceiling"] + print("ceiling b(1-b) in [%s, %s]" % (dec(cl, 24), dec(ch, 24))) + for name, X in ENDPOINTS.items(): + print(" %s X=%s: a-X=%s, b(1-b)-X in [%s, %s], 575/331776-X=%s" % ( + name, dec(X, 24), dec(r["a"] - X, 24), dec(cl - X, 24), dec(ch - X, 24), dec(tpl["a"] - X, 24))) + cw, aw, Mw, kw = r["window"] + print("window (E2 only, informational): c' = b_sel - 10^-9 gives c'(1-c') - X(PR3653) = %s with M = %d, coefficient %s" + % (dec(aw - ENDPOINTS["PR3653 (rohanarun)"], 24), Mw, kw)) + failures = 0 + for name, params in controls().items(): + try: + audit(params) + except AuditFailure as exc: + print("control rejected as required:", name, "->", exc) + continue + failures += 1 + print("CONTROL ACCEPTED (bad):", name) + need(failures == 0, "%d control(s) accepted" % failures) + print("PASS_PR3562_REPROOF_AUDIT: audited arithmetic steps (a)-(e) hold from P1-P5; line-156 bounds alone give factor 2, " + "n <= e/w from line 117 gives 2^c; coefficient 4283584 justified") + + +if __name__ == "__main__": + try: + main() + except AuditFailure as exc: + print("FAIL:", exc) + sys.exit(1) From 946d03dd6b9cc794190876fe3f0f89b0ebc01c59 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Mon, 19 Oct 2026 00:11:49 +0530 Subject: [PATCH 2/2] PR3562 reproof audit: round-2 review text fixes - Scope "no mathematical gap" to the audited steps (a)-(e). - Add a sharper line-158 witness that also keeps w = ceil(e^c) (e=2^20, w=2, n=1023683; ratio about 1.95, exactly > 17/16), with a one-line reproducing command in PROOF.md; only n <= e/w excludes it. - Re-source the fallback-free root offset (about 2.01e-12) as independent decimal bisections outside verify.py, not certified by the verifier. - Split the consumer paragraph: PR3576 inherits tau = 1-a = 332353/332929 and (2) with 4283584; PR3690 inherits only the c=1/576 template, R437 moments unchecked. - Define P1-P4 (and P6) in the README; note the E2 Lagrange tail is a by-construction soundness term no control tests. - Provenance: seven AI review passes over two rounds in the same loop. verify.py is unchanged (sha256 e9188474...); verifier output is identical. Co-Authored-By: Claude Opus 5.5 --- .../PROOF.md | 39 +++++++---- .../README.md | 64 ++++++++++++------- .../TASK.json | 2 +- 3 files changed, 71 insertions(+), 34 deletions(-) diff --git a/research/pr3562-ordinary-coupling-reproof-audit/PROOF.md b/research/pr3562-ordinary-coupling-reproof-audit/PROOF.md index af5d907408..02296979e2 100644 --- a/research/pr3562-ordinary-coupling-reproof-audit/PROOF.md +++ b/research/pr3562-ordinary-coupling-reproof-audit/PROOF.md @@ -13,7 +13,8 @@ verifier code. **Verdict.** -- Every audited arithmetic step (a)-(e) holds from premises P1-P5 below. +- Every audited arithmetic step (a)-(e) holds from premises P1-P5 below, with + c fixed by P6. - One exposition gap. Line 156 lists `n<=e^(1-c)`, `w<=2e^c` and the bound `n^(1-c)w <= 2^c e^(1-a)` of line 158. Line 158 is stated without derivation. The two bounds listed beside it do not imply it: alone they give @@ -190,7 +191,21 @@ log2(n^(1-c)w) - log2(2^c e^(1-a)) = 1-c exactly. So the ratio is 2^(1-c) > 2^(511/512) > 17/16, which violates line 158's conclusion. These values have nw = 2^(q+1) > e, so they violate (N). They also violate w = ceil(e^c) = 2^p (line 18). (N) excludes the witness, and (N) follows from -line 117. So line 158 is true for the actual selector; what is missing is only +line 117. + +*Sharper witness, respecting line 18.* Take e=2^20, c=1/577, w=2 and n=1023683. +Then 1 < e^c < 2, so w = ceil(e^c) ≤ 2e^c, and n = floor(e^(1-c)) because +n^577 ≤ 2^11520 < (n+1)^577. Raising to the power 332929 = 577², the exact integer +comparison n^(576·577)·2^332929·16^332929 > 17^332929·2^577·2^(20·332353) shows +n^(1-c)w > (17/16)·2^c·e^(1-a); the ratio to 2^c e^(1-a) is about 1.9502. These +values satisfy both line-156 bounds and line 18 and violate only (N), since +n > e/w = 524288. So among the stated constraints, (N) is what closes the gap. This +check is not part of verify.py; it was run separately (and in one AI review pass), +and this one line reproduces it: + + python3 -c "n=1023683; print(n**577<=2**11520<(n+1)**577, n**(576*577)*2**332929*16**332929 > 17**332929*2**577*2**(20*332353), 2*n>2**20)" + +which prints `True True True`. So line 158 is true for the actual selector; what is missing is only its derivation. **Constant.** The remaining terms of P5 are bounded as follows, for e ≥ 1 and @@ -251,12 +266,13 @@ records `complex_lower` = 1729033982646513517717/10^24 and | (d) elementary branch | holds; reads the elementary cost as C·V·e (implicit in PR3562) | none | | (e) consequence | exact | none | -For the consumers ([PR3576](https://github.com/CrocSwap/integer-mult-bounds/pull/3576), -`kumagi`; [PR3690](https://github.com/CrocSwap/integer-mult-bounds/pull/3690), `zxv`), -the audited arithmetic implication holds, including the inherited 4283584. It is -conditional on P5 and PR3562's other retained premises. This narrows, and does not -lift, PR3576's stated limit that the all-size PR3562 theorem is not independently -reproved. +[PR3576](https://github.com/CrocSwap/integer-mult-bounds/pull/3576) (`kumagi`) +substitutes PR3562's exponent τ = 1-a = 332353/332929 into T74. The audited layer it +inherits, including (2) with the constant 4283584, holds from P1-P5, conditional on P5 +and PR3562's other retained premises. This narrows, and does not lift, PR3576's stated +limit that the all-size PR3562 theorem is not independently reproved. +[PR3690](https://github.com/CrocSwap/integer-mult-bounds/pull/3690) (`zxv`) inherits +only the parametric template below; its step (a) on R437 is not checked here. Steps (b)-(d) are parametric. At PR3690's c=1/576 with M=10^6, the (c)-(d) arithmetic gives the same 4283584 and a = 575/331776. This assumes PR3690 keeps the @@ -272,9 +288,10 @@ root. The function c(1-c) is increasing on (0,1/2). So on the selected bit progr the shape's exponent has supremum b(1-b) = 0.001730422270288263023337…, not attained. E2 places the root in (b_sel, b_sel+10^-24], where b_sel is the selected bit_saving. E1 independently brackets it in (10/5769, 9/5192). verify.py certifies -that the fallback-free root lies above b_sel + 10^-24 (decimal cross-checks in the -review passes put it about 2.0·10^-12 higher), so the selected value is the -fallback-inclusive root. +that the fallback-free root lies above b_sel + 10^-24, so the selected value is the +fallback-inclusive root. Independent 60-80 digit decimal bisections outside verify.py +put the fallback-free root about 2.01·10^-12 higher; the verifier does not certify +that figure. **Like-for-like comparisons.** PR2979, PR3633, PR3642 and PR3653 each state their endpoint as κ = X - 10^-46 - 10^-70, with X a primitive complex lower bound (the diff --git a/research/pr3562-ordinary-coupling-reproof-audit/README.md b/research/pr3562-ordinary-coupling-reproof-audit/README.md index 722aec5b35..40f5658b1d 100644 --- a/research/pr3562-ordinary-coupling-reproof-audit/README.md +++ b/research/pr3562-ordinary-coupling-reproof-audit/README.md @@ -18,26 +18,38 @@ arithmetic: two reversed C0 calls, each on padded volume below 2V, times majoran plus the wrapper bill. That gives 801 = 2·2·200 + 1 and 4000000 = 2·2·10^6. The physical claims behind that line are not audited here (see Inherited assumptions). -I found one **exposition gap** and no mathematical gap. Line 156 lists `n <= e^(1-c)`, -`w <= 2e^c` and the bound `n^(1-c) w <= 2^c e^(1-a)` of line 158. Line 158 is stated -without derivation, and the two bounds listed beside it do not imply it. An exact -witness exceeds it by the ratio 2^(1-c). The inequality `n <= e/w`, which follows from -the selector definition `n = floor((e-k)/w)` on line 117, does imply it. So line 158 +I found one **exposition gap** and no mathematical gap in the audited steps (a)-(e). +Line 156 lists `n <= e^(1-c)`, `w <= 2e^c` and the bound `n^(1-c) w <= 2^c e^(1-a)` of +line 158. Line 158 is stated without derivation, and the two bounds listed beside it do +not imply it. An exact witness exceeds it by the ratio 2^(1-c). A second witness that +also keeps the selector's w = ceil(e^c) exceeds it by about 1.95 (exactly certified as +more than 17/16). The inequality `n <= e/w`, which follows from the selector definition +`n = floor((e-k)/w)` on line 117, does imply it. So line 158 and `4283584` hold as written. Deriving line 158 from the two line-156 bounds alone would give only a factor of 2 and the coefficient `8033584`, with the same O-bound. -For the consumers [PR3576](https://github.com/CrocSwap/integer-mult-bounds/pull/3576) -(Hiroki KUMAZAKI, `kumagi`) and [PR3690](https://github.com/CrocSwap/integer-mult-bounds/pull/3690) -(`zxv`): the arithmetic layer they inherit holds, including 4283584, conditional on P5 -and PR3562's other retained premises. This narrows, and does not lift, PR3576's stated -limit that the all-size PR3562 theorem is not independently reproved. Still unaudited +The two consumers inherit different parts: + +- [PR3576](https://github.com/CrocSwap/integer-mult-bounds/pull/3576) (Hiroki KUMAZAKI, + `kumagi`) substitutes PR3562's exponent τ = 1-a = 332353/332929 into T74. The audited + layer it inherits, including (2) with the constant 4283584, holds from P1-P5. This + narrows, and does not lift, PR3576's stated limit that the all-size PR3562 theorem is + not independently reproved. +- [PR3690](https://github.com/CrocSwap/integer-mult-bounds/pull/3690) (`zxv`) runs the + template at c = 1/576 on the R437 histogram. Steps (b)-(d) cover it only if it keeps + the same D, K, P5 composition and A = 200. Its R437 moments (step (a)) are not checked + here. + +Both remain conditional on P5 and PR3562's other retained premises. Still unaudited are lines 141-154 (the physical composition behind P5), lines 84-104 (history, preparation and reserve), lines 172-174 (binary transfer) and lines 20-25 (space -bound, borrowed-input restoration and ownership). PR3690's R437 moments are not -checked here. +bound, borrowed-input restoration and ownership). **Scope.** This is an independent check of a scoped all-size arithmetic implication, -P1-P5 ⇒ (2) and the Consequence. It assumes PR3562's retained source/refinement and +P1-P5 ⇒ (2) and the Consequence. P1-P4 are PR3562's histogram and fallback weight +(lines 36-41), the C0 recurrence (lines 45-50), the selector definitions (lines 108-118) +and the retained bounds (lines 120-121); c = 1/577 is fixed by line 18 (P6). PROOF.md +states them in full. It assumes PR3562's retained source/refinement and physical-cost premises and does not admit them. It is not a κ, not a frontier change and not a complete multiplication theorem. @@ -53,7 +65,9 @@ about 5 s and stays under 40 MB RSS. - E1, integer-root bisection: z^q·64^p ≤ r^p·Q^q < (z+1)^q·64^p, at Q = 2^128 (PR3562 uses 2^160); - E2, a rational interval series: atanh-based logarithms and a Horner exp with a - Lagrange tail, using outward dyadic rounding. + Lagrange tail, using outward dyadic rounding. The tail is a soundness term by + construction: it lies far below the printed resolution, so no output or control + tests it. μ_1 = 2874298095721977/2890625000000000 < 199/200. Both engines enclose μ_(576/577) as 0.999998938581682162866772413602788… (the verifier prints widths 9.358e-38 for E1 @@ -66,10 +80,10 @@ about 5 s and stays under 40 MB RSS. - εF/W is the literal in `research/lean-bit-moment-discharge/lean/Selected.lean`. - The selected certificate hash is checked through `certificates/selected-result.json`. - E2 shows that the selected `bit_saving` 0.001733427039589844234749 is the - fallback-inclusive root truncated to 24 digits. The fallback-free root lies about - 2.0e-12 higher; that figure comes from decimal cross-checks in the review passes, - and verify.py certifies only that it lies above b_sel + 10^-24. E1 brackets the root - in (10/5769, 9/5192). + fallback-inclusive root truncated to 24 digits. verify.py certifies only that the + fallback-free root lies above b_sel + 10^-24. Independent 60-80 digit decimal + bisections outside verify.py put it about 2.01e-12 higher; the verifier does not + certify that figure. E1 brackets the root in (10/5769, 9/5192). - **Steps (b)-(d) parametric** in rational c ∈ (17/10000, 1/512). Lemma B covers any histogram whose moments satisfy A(1-μ_1) ≥ 1 and M(1-μ_t) ≥ 1. At c = 1/576 with M = 10^6 (PR3690's choice), the (c)-(d) arithmetic also gives 4283584. This holds @@ -78,7 +92,12 @@ about 5 s and stays under 40 MB RSS. - **Line-158 witness.** At e = 2^q with c = p/q, the values n = e^(1-c) and w = 2e^c satisfy both line-156 bounds with equality. They exceed line 158's bound by exactly 2^(1-c) > 17/16. They also violate n ≤ e/w and w = ceil(e^c) (line 18), so the - selector excludes them. The verifier checks this exponent arithmetic. The + selector excludes them. A sharper witness keeps the selector's w: at e = 2^20, + c = 1/577, take w = 2 = ceil(e^c) and n = 1023683 = floor(e^(1-c)). It satisfies + both line-156 bounds and line 18, yet exceeds line 158 by a ratio of about 1.95; only + n ≤ e/w = 524288 excludes it (a one-line exact check is given in PROOF.md; verify.py + does not run it). The + verifier checks the first witness's exponent arithmetic. The classification as an exposition gap rests on the written argument in PROOF.md. ## Reproduce @@ -203,9 +222,10 @@ The structured form (question, why_it_matters, first_step, blocked_by) is in - Selected bit supplier and moment literal: `research/e8-bit-p111-tuned` and `research/lean-bit-moment-discharge` on main, credited in their own packages. -The verifier and proof were reviewed by four independent AI review passes in the same -loop: reproducibility, adversarial mathematics, provenance and referee. This is not -human review, and none is claimed. Source pins are in [SOURCES.json](SOURCES.json). +The verifier and proof were reviewed by seven AI review passes over two rounds in the +same loop (round 1: reproducibility, adversarial mathematics, provenance, referee; +round 2: reproducibility, adversarial mathematics, referee). This is not human review, +and none is claimed. Source pins are in [SOURCES.json](SOURCES.json). Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Apache-2.0. diff --git a/research/pr3562-ordinary-coupling-reproof-audit/TASK.json b/research/pr3562-ordinary-coupling-reproof-audit/TASK.json index 5c0b850ca1..1476d5afcc 100644 --- a/research/pr3562-ordinary-coupling-reproof-audit/TASK.json +++ b/research/pr3562-ordinary-coupling-reproof-audit/TASK.json @@ -48,7 +48,7 @@ "outcome": "completed", "evidence": "verify.py (stdlib, exact): two moment engines (integer-root bisection; rational interval atanh/exp series; same methods as PR3562 states, implemented independently) agree inside PR3562's 10^-30 enclosure; source binding to the selected bit supplier and Selected.lean fallback literal; P5 coefficient composition 801 = 2*2*200+1; parametric (c)-(d) arithmetic; line-158 witness; selected bit_saving shown to be the fallback-inclusive root; seven frozen negative controls rejected. PROOF.md gives the written reproof. Result: every audited arithmetic step (a)-(e) holds from P1-P5. Line 158 is stated without derivation; the bounds listed beside it on line 156 (n<=e^(1-c), w<=2e^c) do not imply it (exact witness, ratio 2^(1-c)), while n<=e/w from line 117 does, so 4283584 holds as written; deriving line 158 from the two line-156 bounds alone would give 8033584.", "author": "Sagar Thakrar (thakrarsagar)", - "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for the reproof, verifier and text; reviewed by four independent AI review passes in the same loop (reproducibility, adversarial mathematics, provenance, referee), not by a human.", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for the reproof, verifier and text; reviewed by seven AI review passes over two rounds in the same loop (round 1: reproducibility, adversarial mathematics, provenance, referee; round 2: reproducibility, adversarial mathematics, referee), not by a human.", "open_questions": [ { "question": "Should PR3562 derive line 158 from n<=e/w (line 117) at lines 156-158?",