Current task: —

← Session 35 — ii′-6-R: Lagarias 6.1 right-tail re-proof (E-032/D-073)

#2217 assistant 2026-08-26 12:22:06.623 UTC · 1656→9377 tok open ⤢
thinking (21478 chars)
As suspected — the three Bn evaluation proofs fail at their final linarith (lines 390, 479, 623): - Line 390 (Bn_FAlt_80000_le's final `linarith [hFAlt, hterm2, hterm4, hII]`): the new Bn has the dog-leg share, and the old proof lacks the DogLegRight bound — linarith fails. - Line 479 (Bn_FAlt_80000_ge's final linarith). - Line 623 (Bn_FAlt_100000_le's final linarith). So I need to patch the three Bn evaluation proofs with DogLegRight bounds. The cleanest: add a certified bound on DogLegRight at each point (8e4 and 10⁵): DogLegRight(n) = ((√n+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj(n)/4. - At 8e4: ((283.84)/2)·(e^{5/2}+1)/2 + 8.38 + IIMaj(8e4)/4. (√80000 ≤ 283, so √80000+1 ≤ 284: (284/2)·(e^{5/2}+1)/2 = 142·(e^{5/2}+1)/2 = 71·(e^{5/2}+1) ≤ 71·13.19 = 936.49. +8.38 = 944.87. +IIMaj/4 ≤ 2590.08/4·... hmm — the old hII bounds IIMaj ≤ 2590.08 (the coarse 4.56·284·2 form): IIMaj/4 ≤ 647.52. So DogLegRight(8e4) ≤ 936.49+8.38+647.52 = 1592.39. And 2·DogLegRight ≤ 3184.78. Hmm wait — the dog-leg part of the new Bn's horizontal share is 2·DogLegRight ≤ 3184.78 — vs the old share's 2(e⁴+1)·3.3 = 2·55.6015·3.3 = 367.0. So the new Bn(8e4) ≤ old-Bn-bound (327,058) − 367 + 3,184.78 = 329,876 — EXCEEDS the old certified 329,000!!! Need to re-certify ≤ 330,000 (or tighter). Let me recompute carefully with the old proof's term structure: - The old Bn_FAlt_80000_le proof: hFAlt : FAlt T ≤ 273.82; hterm2 : 4·284·112.9637 (the I_III bracket); hterm4 : 2·(54.6015+1)·(7·251.46+3.3) (the OLD horizontal); hII : IIMaj ≤ 2590.08. The old Bn ≤ 4·273.82 + 4·284·112.9637 + 40·1.3352 + 2·55.6015·(7·251.46+3.3) + 2590.08 + 1 = 1095.28 + 128,410.755 + 53.408 + 2·55.6015·1763.52 + 2590.08 + 1 = 1095.28+128,410.755+53.408+196,117.3+2590.08+1 = 328,250.8?? — the old comment says "certified ≈ 327 058, true 322 309" and the bound is ≤ 329,000. Hmm — my hand-arithmetic is off; whatever — the KEY: the old proof's final linarith: Bn ≤ 4·hFAlt + 4·284·112.9637 + 40·1.3352 + hterm4 + hII + 1 ≤ 329,000 — with hterm4 = 2·55.6015·(7·251.46+3.3). - The new Bn's horizontal share: 2(e⁴+1)·7Ĥ(T) + 2·DogLegRight — with Ĥ ≤ 251.46 (old hH): 2(e⁴+1)·7·251.46 = 2·55.6015·1760.22 = 195,846. And 2·DogLegRight ≤ 2·1592.39 = 3,184.78. So the new horizontal total ≤ 195,846+3,184.78 = 199,030.78. Hmm — but the old hterm4 covered 2(e⁴+1)(7·251.46+3.3) = 2·55.6015·1763.52 = 196,117.4?? — 2·55.6015 = 111.203; ×1763.52 = 196,117.4. And the new: 111.203·1760.22 = 195,745.9 + 3,184.78 = 198,930.7. Difference: +2,813.3. - So the new Bn(8e4) ≈ old certified (327,058) + 2,813 ≈ 329,871. New certified bound: ≤ 330,000. Wait — but E-034's Bn_DL(8e4) = 324,912.99 — MUCH less than 329,871. The difference: E-034's Bn_DL uses T = √n+1 with the EXACT Ĥ/etc. values, while the old certified proof's coarse bounds (hlogT ≤ 5.7, hH ≤ 251.46, etc.) are LOOSE (they certify the OLD Bn's terms loosely). The new certified bound will be correspondingly loose. E-034's exact 324,913 vs the certified ~329,871 — the certified bound has the same looseness as the old one (which certified 327,058 vs true 322,309 — ~2.4% loose). So the new certified target: ≤ 330,000 (comfortable) or ≤ 331,000 for extra comfort. For Bn_FAlt_80000_ge (the LOWER bound ≥ 274,000): the new Bn's dog-leg share only ADDS (positive terms), so Bn_new ≥ Bn_old-ish? — NO — the new Bn's horizontal share CHANGED: 2(e⁴+1)·7Ĥ + 2·DogLegRight vs old 2(e⁴+1)(7Ĥ+3.3) — the new share is BIGGER (adds 2·DogLegRight ~3,184 but removes 2(e⁴+1)·3.3 ~367): net +2,817. So Bn_new ≥ Bn_old + 2,817 ≥ 274,000 + ... — the lower bound proof bounds the big terms from BELOW (hterm2 lower + hterm4 lower + others ≥ 0) — the dog-leg share is POSITIVE (2·DogLegRight ≥ 0 ✓) so the lower bound EASILY survives: Bn_new ≥ [the old proof's lower terms] + 2·DogLegRight ≥ old-lower + 0 ≥ 274,000 ✓ — the old lower proof should STILL work if I add `0 ≤ 2·DogLegRight` (positivity). Actually the old lower proof's final linarith: Bn ≥ 4·hFAlt0 + hterm2-lo + hterm4-lo + hII-0 + 40·1.3352 + 1 ≥ 274,000 — with the new Bn's form having the dog-leg share — linarith needs 2·DogLegRight ≥ 0 to absorb ✓ — add `have hDLnn : (0:ℝ) ≤ DogLegRight 80000 := by unfold DogLegRight; positivity` and include in the linarith. Hmm wait — actually the new Bn's horizontal share is 2(e⁴+1)·7Ĥ + 2·DogLegRight — the old hterm4-lo bounds 2(e⁴+1)(7Ĥ+3.3) ≥ ... — the new share's 2(e⁴+1)·7Ĥ part is ≤ the old (no 3.3) — the lower bound on the new share = (lower on 2(e⁴+1)·7Ĥ) + (lower on 2·DogLegRight = 0). The old hterm4-lo proves a lower bound on 2(e⁴+1)(7Ĥ+3.3) — which is LARGER than 2(e⁴+1)·7Ĥ — so hterm4-lo's lower bound on the OLD share does NOT lower-bound the new share's 2(e⁴+1)·7Ĥ part (the new part is SMALLER). Hmm — the old hterm4-lo : 2·(54.5978+1)·(7·191.85+3.3) ≤ 2(e⁴+1)(7Ĥ+3.3) — the new part 2(e⁴+1)·7Ĥ ≤ 2(e⁴+1)(7Ĥ+3.3) — so the old lower bound OVERCOUNTS for the new part: 2(e⁴+1)·7Ĥ ≥ 2(e⁴+1)·7·(Ĥ-lo − 3.3·...)·... hmm — the cleanest: recompute the lower bound for the new form: 2(e⁴+1)·7Ĥ ≥ 2·(54.5978+1)·7·191.85 (the old hHlo's 191.85, without the +3.3): = 111.1956·1342.95 = 149,355. And 2·DogLegRight ≥ 0. So new Bn ≥ 4·hFAlt0 + hterm2-lo + (2(e⁴+1)·7·191.85-lo) + 0 + 40·1.3352 + hII0 + 1 — the old proof's lower total was ≥ 274,000 with the OLD hterm4-lo (2·55.5978·(7·191.85+3.3) = 111.1956·1346.25 = 149,722). The new hterm4-lo (without 3.3): 111.1956·1342.95 = 149,355 — smaller by 367. And the dog-leg adds 0 (lower). So new lower total ≈ 274,000 − 367 + 0 ≈ 273,633 — hmm — that's BELOW 274,000!! The old certified lower was exactly 274,000 — with the 3.3 removed, the new lower total is ~273,633 < 274,000 — so the certified lower bound needs to drop to ≤ 273,000 or re-certify at 273,000. Hmm wait — but the margin uses margin(8e4) ≤ sInfty_up − Bn_lo + 1 for hbase2 — with Bn_lo = 273,000: margin(8e4) ≤ 339,000 − 273,000 + 1 = 66,001 — and margin(10⁵) ≥ 432,500 − Bn_up + 1. With Bn_up(10⁵) needing re-certification too (the same +2,817 issue: old ≤ 350,000 → new ≈ 352,800): margin(10⁵) ≥ 432,500 − 352,800 + 1 = 79,701. Then hbase2: margin(8e4) ≤ 66,001 < 79,701 ✓ still works!! And hbase: margin(8e4) ≥ 336,000 − Bn_up(8e4) + 1 = 336,000 − 330,000 + 1 = 6,001 > 0 ✓ works! Wait — but hold on: I should double check the E-034 margins: E-034's margin_DL at 8e4 = 13,160 and at 10⁵ = 88,911. My certified bounds give margin(8e4) ∈ [6,001, 66,001] and margin(10⁵) ≥ 79,701 — the hbase (0 < margin(8e4)) ✓ and hbase2 (66,001 < 79,701 ✓) — both work but MUCH coarser than E-034's true values (13,160 / 88,911). The certified bounds should target closer to E-034's: Bn_up(8e4) ≤ 325,000 (E-034's 324,913 + slack ~200 for the certified looseness): margin(8e4) ≥ 336,000−325,000+1 = 11,001; Bn_lo(8e4) ≥ 322,000: margin(8e4) ≤ 339,000−322,000+1 = 17,001; Bn_up(10⁵) ≤ 345,000 (E-034 344,838): margin(10⁵) ≥ 432,500−345,000+1 = 87,501. hbase2: 17,001 < 87,501 ✓✓ — those match the session-038 certified form (8,001/82,501) closely and are much better. Hmm — but E-034's Bn_DL uses the EXACT arithmetic (C_zeta3 = 0.5 charged as 0.5; e^{5/2}+1 charged 13.19; etc.) — the certified LiBasePoints bounds use the d9-certified logs and the coarse IIMaj (4.56(√n+1)·2 ≈ 2590) — the certified Bn_up will be looser than E-034's by the IIMaj-coarse and the log looseness. E-034's 324,913 vs old-certified-true 322,309 — the difference is the dog-leg share (+2,813) minus nothing: 322,309+2,813 = 325,122 — hmm — E-034's Bn_DL(8e4) = 324,913 < 325,122?! — because E-034's dog-leg charge uses VLeftBound with C_zeta3 = 0.5: VLeftBound(8e4) = ((√n+1)/2)·13.19·0.5 = 142·6.595 = 936.49 ✓ matches my 936.49 ✓. And IIMaj/4 with the exact form (not the coarse 4.56·284·2): E-034's IIMaj(n) = 2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)} = tiny (~1e-105) — E-034's IIMaj/4 ≈ 0!! — while my certified bound uses the COARSE IIMaj ≤ 2590.08 (IIMaj_le_two_mul) → IIMaj/4 ≤ 647.52. So E-034's DogLegRight ≈ 936.49+8.38+0 = 944.87, mine (coarse) ≈ 936.49+8.38+647.52 = 1,592.39 — difference 647.5 (the coarse IIMaj/4). And the I_I's IIMaj: E-034's I_I ≈ 0, mine coarse ≈ 2590. Total IIMaj: E-034 ~0, mine ~3,237. So my certified Bn_up(8e4) ≈ E-034's 324,913 + 3,237 ≈ 328,150?? — no wait — E-034's Bn_DL ALREADY uses IIMaj(n) for the I_I piece (with the exact ~0 value) and VRightBound = IIMaj/4 (~0). My certified version charges the COARSE IIMaj (2590) for I_I and coarse IIMaj/4 (647.5) for the dog-leg — total IIMaj-ish 3,237.5 vs E-034's ~0. So certified Bn_up(8e4) ≈ E-034's 324,913 + 3,237 ≈ 328,150. Hmm — that's ABOVE my 325,000 target. Let me use 330,000 (comfortable). Ugh — actually wait. The OLD certified proof (session 012, updated session 038) certified Bn ≤ 329,000 with the coarse IIMaj 2590.08 — the old true Bn (session-038 form) ≈ 322,309 (E-023/E-030's exact) — the old certified 329,000 has slack 6,691 over true. The NEW Bn's true ≈ 325,122 (old true + 2,813). So new certified target with the same slack: ≤ 335,000 (325,122 + ~9,900 slack for the log looseness) — or keep it tighter: the old proof's STRUCTURE gave 329,000 from the loose bounds; the new structure with the same loose bounds gives ~329,000 − 367 (3.3 removed) + 3,184.78 (dog-leg) ≈ 331,818. So certify ≤ 332,000 (small slack) or 333,000 (comfortable). Let me just patch the three proofs minimally: for the upper bounds (le), add a certified DogLegRight upper bound and bump the target; for the lower bound (ge), subtract the 3.3 from the hterm4-lo and add DogLegRight ≥ 0, lowering the target appropriately (or keep the 3.3 in the lower form for simplicity: the old hterm4-lo's form (7·191.85+3.3) — the new share's constant part — hmm, the new share is 2(e⁴+1)·7Ĥ + 2·DogLegRight: its LOWER bound: 2(e⁴+1)·7·Ĥ-lo + 0 = 2·55.5978·7·191.85 = 149,355 — and the old proof's total-lower was 274,000 with 149,722 for hterm4-lo: new total-lower = 274,000 − 367 = 273,633 — hmm — but the OTHER pieces' lower bounds are unchanged ✓ so the new total-lower ≈ 273,633. Certify ≥ 273,000 (slack 633) ✓. Hmm wait, actually — for the ge (lower) bound I can keep it SIMPLE: the new share's 2(e⁴+1)·7Ĥ ≥ the old hterm4-lo's form MINUS the 3.3-part: 2(e⁴+1)·7Ĥ ≥ 2·55.5978·(7·191.85) = 149,355 ✓ — and 2·DogLegRight ≥ 0 ✓. New total-lower = 4·hFAlt0 + hterm2-lo + hterm4'-lo (149,355) + hII0 + 40·1.3352 + 1 = old-total − 367 = 273,633 ✓ certify ≥ 273,000 ✓. For the two le (upper) bounds: add DogLegRight ≤ 1,593 (at 8e4: 936.49+8.38+647.52 = 1,592.39 → 1,593; at 10⁵: (√10⁵+1)/2·13.19/2·... = 317.23/2·... hmm: (√100000+1)/2 = 158.6: 158.6·(e^{5/2}+1)/2 = 158.6·6.591 = 1,045.4; +8.38 = 1,053.78; +IIMaj/4 ≤ 2900.16/4 = 725.04: DogLegRight(10⁵) ≤ 1,778.82 → 1,779) and bump the targets: new share at 8e4 = old-share-minus-3.3 + 2·DogLegRight: hterm4-new = 2·55.6015·(7·251.46) + 2·1593 = 195,845.9 + 3,186 = 199,031.9 — and the old proof's total was ≤ 329,000 with hterm4 = 196,117.4: new total = 329,000 − 196,117.4 + 199,031.9 = 331,914.5 — certify ≤ 332,000. At 10⁵: hterm4-new = 2·55.6015·(7·255.05) + 2·1779 = 198,471.7 + 3,558 = 202,029.7; old total ≤ 350,000 with hterm4 = 198,838.5: new = 350,000 − 198,838.5 + 202,029.7 = 353,191.2 — certify ≤ 354,000. Hmm wait — let me recompute the old hterm4 values from the file. The old Bn_FAlt_80000_le's hterm4: `2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 80000 + 1) + 3.3) ≤ 2 * (54.6015 + 1) * (7 * 251.46 + 3.3)` — so the old proof's horizontal share bound is 2·55.6015·(7·251.46+3.3) = 2·55.6015·1763.52 = 196,117.4 (matches my estimate ✓). And the old Bn_FAlt_100000_le's hterm4: `2 * (54.6015 + 1) * (7 * 255.05 + 3.3)` = 2·55.6015·1788.65 = 198,838.7 ✓. And the new horizontal shares: - 8e4: 2(e⁴+1)·7Ĥ + 2·DogLegRight ≤ 2·55.6015·7·251.46 + 2·1593 = 2·55.6015·1760.22 + 3,186 = 195,845.9 + 3,186 = 199,031.9. - 10⁵: 2·55.6015·7·255.05 + 2·1779 = 2·55.6015·1785.35 + 3,558 = 198,471.6 + 3,558 = 202,029.6. New certified upper bounds: - Bn(8e4) ≤ 4·273.82 + 4·284·112.9637 + 53.408 + 199,031.9 + 2590.08 + 1 = 1095.28 + 128,410.76 + 53.41 + 199,031.9 + 2590.08 + 1 = 331,181.4?? — hmm — wait, the old proof's final linarith used hterm2 = 4·284·112.9637 = 128,410.76 — and the total was ≤ 329,000 — so old total = 1095.28 + 128,410.76 + 53.41 + 196,117.4 + 2590.08 + 1 = 328,267.9 → ≤ 329,000 (slack 732). New total = 328,267.9 − 196,117.4 + 199,031.9 = 331,182.4 → certify ≤ 332,000 (slack 818). - Bn(10⁵) ≤ 4·311.45 + 4·318·114.0656 + 53.41 + 202,029.6 + 2900.16 + 1 = 1245.8 + 145,091.33 + 53.41 + 202,029.6 + 2900.16 + 1 = 351,521.3 → ≤ 352,000 (slack 479) — or 353,000 (slack 1,479 — more comfortable; the old had 350,000 with slack ~3,080 vs true ~330,900 — wait the old certified was 350,000 vs "certified ≈ 346 920; true ≈ 330 900" — slack 3,080 vs certified, 19,100 vs true. New true ≈ 333,700. Certify ≤ 353,000 (slack 1,479 vs the loose-certified 351,521).) Hmm — let me double-check E-034's Bn_DL values: 324,913 (8e4) and 344,838 (10⁵). My new certified upper bounds 332,000/352,000 have slack ~7,000 over E-034's exact — fine (the old certified had similar looseness). Actually — wait. Let me reconsider: E-034's Bn_DL(8e4) = 324,913 uses the EXACT IIMaj (~1e-105) and exact IIMaj/4 (~0), while my certified uses the coarse IIMaj_le_two_mul (2590.08 at 8e4, 2900.16 at 10⁵). The coarse-vs-exact IIMaj difference is 2590+647 = 3,237 at 8e4 and 2900+725 = 3,625 at 10⁵. So my certified Bn_up(8e4) ≈ E-034's 324,913 + 3,237 + (the old-certified-vs-true looseness ~4,750) ≈ 332,900?? — hmm — the old certified 329,000 vs old true 322,309 — slack 6,691 (includes the IIMaj-coarse 2,590 + log looseness ~4,100). So new certified ≈ E-034's 324,913 + 6,691 + (dog-leg-vs-old-3.3 difference: +2,817·... — wait — E-034's Bn_DL already INCLUDES the dog-leg share with its exact IIMaj/4 (~0) — my certified's DogLegRight includes the coarse IIMaj/4 (647.52) — so my certified Bn_up(8e4) ≈ E-034's 324,913 + (log looseness ~4,100) + (IIMaj-coarse on I_I: 2,590) + (IIMaj-coarse on dog-leg: 647.52) ≈ 332,250. Certify ≤ 333,000. And 10⁵: E-034's 344,838 + ~4,600 + 2,900 + 725 ≈ 353,063. Certify ≤ 354,000. Hmm — these are getting close to the margins: margin(8e4) ≥ 336,000 − 333,000 + 1 = 3,001 > 0 ✓ (E-034's true margin is 13,160 — my certified lower is much coarser but positive ✓). hbase2: margin(8e4) ≤ 339,000 − 273,000 + 1 = 66,001 < margin(10⁵) ≥ 432,500 − 354,000 + 1 = 78,501 ✓ (66,001 < 78,501 ✓ works). Hmm — 3,001 is a bit thin. Let me tighten the upper bound on the IIMaj-coarse for the dog-leg: the DogLegRight's IIMaj/4 — I could use the TRUE IIMaj's tiny value via a better bound than IIMaj_le_two_mul... — the old proof's hII uses IIMaj_le_two_mul (the coarsest 4.56(√n+1)·2). There's no tighter certified IIMaj bound in the codebase (the psiTilde decay analysis gives IIMaj ≤ 4.56(√n+1)(e^{−a√n}+e^{−b√n}) — the TRUE tiny value — but no certified lemma bounds it below 4.56(√n+1)·2·e^{−a√n}·... hmm — actually IIMaj_le_two_mul is the ONLY IIMaj upper bound — and it gives 9.12(√n+1). The true IIMaj at 8e4 is ~4.56·283.84·(e^{−0.8863·282.84}+e^{−1.3863·282.84}) = 4.56·283.84·(e^{−250.7}+e^{−392.2}) ≈ 4.56·283.84·e^{−250.7} ≈ 1294.8·2.4e-109 ≈ 3e-106 — ASTRONOMICALLY smaller than 2,590!! The coarse bound loses 10^109×!! So the certified Bn_up could be MUCH tighter with a finer IIMaj bound. But the old proof uses the coarse form and it works (the margin is robust). For the dog-leg Bn, the coarse form still works (margins stay positive). Let me not over-engineer: certify with the coarse IIMaj form at ≤ 333,000/≤ 354,000, margins 3,001/78,501 — hbase ✓ (3,001 > 0) hbase2 ✓ (66,001 < 78,501). But 3,001 is thin-ish — let me instead use a slightly better IIMaj/4 bound in the dog-leg share to fatten the margin: actually — the E-034 margins (13,160/88,911) are the TRUE ones; the certified base points just need to WORK. 3,001 works but is uncomfortably close to 0 for a "certified" claim. Let me instead target the E-034-matching form more carefully: Actually — the cleanest: bound DogLegRight with the EXACT IIMaj/4 form (not the coarse): DogLegRight's IIMaj/4 needs an IIMaj bound — the only one is IIMaj_le_two_mul (coarse). Alternatively, use a NEW tighter IIMaj bound: IIMaj(n) ≤ 4.56·(√n+1)·2·e^{−(√n)/2}?? — psiTilde(s) = 4.56(s+1)(e^{−as}+e^{−bs}) ≤ 4.56(s+1)·2·e^{−as} (both exp ≤ e^{−as} since a ≤ b): IIMaj n = psiTilde(√n) ≤ 4.56(√n+1)·2·e^{−0.8863√n} — a certified version via the existing machinery? — there's no such lemma, but IIMaj_le_two_mul exists. For the base points, the old proof's coarse form is the established pattern — let me keep it and just fatten by using 333,000/354,000 with margins 3,001/78,501 — hmm — 3,001 is fine actually (it's a certified positive lower bound; the true margin is 13,160). Hmm — wait, actually, let me reconsider: is the tightness of hbase (0 < margin) critical? pos_of_convex_of_two_points needs hbase : 0 < marginTilde FAlt 80000 and hbase2 : marginTilde FAlt 80000 < marginTilde FAlt 100000. 3,001 > 0 ✓ and 66,001 < 78,501 ✓ — both work. The margin's certified positivity at 8e4 is 3,001 — that's the certified claim, true is 13,160. Acceptable. BUT — actually, I realize I should double-check my arithmetic for the new Bn at 8e4 vs 333,000. Let me recompute with the old proof's exact term values: Old proof's pieces at 8e4 (from the file): - hFAlt : FAlt(√80000+1) ≤ 273.82 → 4·273.82 = 1,095.28 - hterm2 : 4·284·112.9637 = 4·284 = 1,136; ×112.9637 = 128,330.76?? — 1,136·112.9637 = 128,330.76 (I said 128,410 earlier — recompute: 284·112.9637 = 32,081.69; ×4 = 128,326.77. Hmm — 284·112.9637: 284·112 = 31,808; 284·0.9637 = 273.69; total 32,081.69; ×4 = 128,326.77.) - 40·1.3352 = 53.408 - hterm4 : 2·55.6015·(7·251.46+3.3) = 2·55.6015·1763.52 = 111.203·1763.52 = 196,120.6?? — 111.203·1763.52: 111.203·1760 = 195,717.3; 111.203·3.52 = 391.4; total 196,108.7. Hmm — 7·251.46 = 1,760.22; +3.3 = 1,763.52 ✓; ×111.203 = 196,108.7. - hII : IIMaj ≤ 2590.08 - +1 Old total: 1,095.28 + 128,326.77 + 53.41 + 196,108.7 + 2590.08 + 1 = 328,175.24 → the old proof certified ≤ 329,000 (slack 825) — and the file's comment says "certified ≈ 327 058" — close enough (my hand-arithmetic ~1,100 off; whatever). New pieces: - hterm4-new : 2(e⁴+1)·7·251.46 + 2·DogLegRight = 111.203·1760.22 + 2·DogLegRight = 195,754.3 + 2·DogLegRight. DogLegRight(8e4) ≤ (284/2)·(e^{5/2}+1)/2 + 8.38 + 2590.08/4 = 142·(e^{5/2}+1)/2 + 8.38 + 647.52 = 71·(e^{5/2}+1)·... = 71·13.19·... — hmm: (284/2)·(e^{5/2}+1)/2 = 142·(13.1825+1)/2?? — no: (e^{5/2}+1)/2 = (12.1825+1)/2 = 13.1825/2 = 6.59125 — the (e^{5/2}+1)/2 factor is 6.59125?? — WAIT: (e^{5/2}+1)/2 = 6.591 — and ((√n+1)/2)·(e^{5/2}+1)/2 = 142·6.59125 = 935.96. +8.38 = 944.34. +647.52 = 1,591.86. → 2·DogLegRight = 3,183.72. So hterm4-new = 195,754.3 + 3,183.72 = 198,938.0. - e^{5/2}+1's certified bound: E-034's E52P1 = 13.19 ≥ e^{5/2}+1 = 13.182494 — the certified 13.19 has slack 0.0075 ✓. For the certified DogLegRight I should use the certified e^{5/2}+1 ≤ 13.19 — the old file has exp bounds (exp_le_inv_sub_sixteen for e^{0.263} etc. — need e^{5/2} = e²·e^{0.5}: e² ≤ 7.3891, e^{0.5} ≤ 1.6488: e^{5/2} ≤ 12.1852 → e^{5/2}+1 ≤ 13.1852 — hmm — tighter than 13.19 ✓ use 13.19 or 13.186). Let me use e^{5/2}+1 ≤ 13.186 (e²·e^{0.5} ≤ 7.3891·1.6488 = 12.18517 → +1 = 13.18517 → 13.186). Then (284/2)·13.186/2 = 142·6.593 = 936.2; +8.38 = 944.58; +647.52 = 1,592.1 → 2·DogLegRight ≤ 3,184.2. New total at 8e4: 1,095.28 + 128,326.77 + 53.41 + 198,938.0 + 2590.08 + 1 = 331,004.5 → certify ≤ 332,000 (slack ~995). At 10⁵: - hFAlt : FAlt(√100000+1) ≤ 311.45 → 4·311.45 = 1,245.8 - hterm2 : 4·318·114.0656 = 1,272·114.0656 = 145,091.5?? — 318·114.0656 = 36,272.86; ×4 = 145,091.4. - 40·1.3352 = 53.41 - hterm4-new : 2·55.6015·7·255.05 + 2·DogLegRight = 111.203·1785.35 + 2·DogLegRight = 198,510.7 + 2·DogLegRight. DogLegRight(10⁵) ≤ (318/2)·13.186/2 + 8.38 + 2900.16/4 = 159·6.593 + 8.38 + 725.04 = 1,048.3 + 8.38 + 725.04 = 1,781.7 → 2·DogLegRight = 3,563.4. hterm4-new = 198,510.7 + 3,563.4 = 202,074.1. - hII : IIMaj ≤ 2900.16 - +1 New total at 10⁵: 1,245.8 + 145,091.4 + 53.41 + 202,074.1 + 2900.16 + 1 = 351,365.9 → certify ≤ 352,000 (slack ~634). Margins: margin(8e4) ≥ 336,000 − 332,000 + 1 = 4,001 ✓ (better than 3,001); margin(10⁵) ≥ 432,500 − 352,000 + 1 = 80,501 ✓. hbase2: margin(8e4) ≤ 339,000 − Bn_lo(8e4) + 1 — Bn_lo(8e4) with the 3.3 removed: old ge's form: 2(e⁴+1)·7·191.85 + 0 = 149,355 — new ge total = old-total − 367: the old proof's final linarith gave ≥ 274,000 — with the 3.3 part removed: 274,000 − 2·55.5978·3.3·... hmm — the old hterm4-lo was 2·55.5978·(7·191.85+3.3) = 111.1956·1346.25 = 149,722.8?? — 7·191.85 = 1,342.95; +3.3 = 1,346.25; ×111.1956 = 149,723.5. New hterm4-lo : 2(e⁴+1)·7·191.85 = 111.1956·1342.95 = 149,356.7. Difference: −366.8. So new ge total = 274,000 − 366.8 = 273,633.2 → certify ≥ 273,000 (slack 633). margin(8e4) ≤ 339,000 − 273,000 + 1 = 66,001 < 80,501 ✓✓ hbase2 ✓. And hbase: margin(8e4) ≥ 4,001 > 0 ✓. These certified bounds work. Now — the cleanest implementation: patch the three Bn evaluation proofs to add the DogLegRight term with its certified bound and adjust the targets. Let me look at the exact structure of the three proofs' final linarith calls to patch minimally. Actually — a cleaner minimal patch: bound `2·DogLegRight n ≤ [constant]` and add it to the existing linarith lists, adjusting the hterm4 to remove the 3.3. Let me look at the exact final blocks of the three proofs (lines ~378-390, ~470-479, ~615-623).
The three Bn evaluation proofs need DogLegRight bounds. Checking their final assembly blocks.
tool: Read ok
input
{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean",
  "offset": 370,
  "limit": 115
}
result 2026-08-26 12:22:06Z → 2026-08-26 12:22:06Z
{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean",
    "content": "      10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 := by\n    linarith [hZ2nn, hlogT2nn]\n  -- IIMaj \u2264 2590.08\n  have hII : IIMaj 80000 \u2264 (2590.08 : \u211d) := by\n    refine le_trans (IIMaj_le_two_mul 80000 (by norm_num)) ?_\n    have h3 : (4.56 : \u211d) * (Real.sqrt 80000 + 1) \u2264 4.56 * 284 :=\n      mul_le_mul_of_nonneg_left (by linarith [sqrt80000_le]) (by norm_num)\n    linarith [h3]\n  -- assemble\n  simp only [Bn]\n  have hterm2 : 4 * (Real.sqrt 80000 + 1) * ((2 / 3) * Z2hat (Real.sqrt 80000 + 1) +\n      10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48) \u2264 4 * 284 * 112.9637 := by\n    apply mul_le_mul _ hbr hbrnn (by norm_num)\n    exact mul_le_mul_of_nonneg_left hT (by norm_num)\n  have hterm4 : 2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 80000 + 1) + 3.3) \u2264\n      2 * (54.6015 + 1) * (7 * 251.46 + 3.3) := by\n    apply mul_le_mul _ _ (by linarith [hHnn]) (by norm_num)\n    \u00b7 apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : \u211d) \u2264 2)\n      linarith [he4]\n    \u00b7 linarith [hH]\n  linarith [hFAlt, hterm2, hterm4, hII]\n\n/-- [PROVED session 012] Bn FAlt(8\u00d710\u2074) \u2265 274000 (certified \u2248 274 668;\ntrue 322 309 \u2014 the lower side only needs the two big terms). -/\ntheorem Bn_FAlt_80000_ge : (274000 : \u211d) \u2264 Bn FAlt 80000 := by\n  have hTge : (283 : \u211d) \u2264 Real.sqrt 80000 + 1 := by\n    have h := sqrt80000_ge\n    linarith\n  have hTpos : (0 : \u211d) < Real.sqrt 80000 + 1 := by linarith\n  -- log (T+2) \u2265 5.6 (T+2 \u2265 285 \u2265 e\u2075\u00b7\u2076 = e\u2075\u00b7e\u2070\u00b7\u2076, 148.414\u00b71.8433 = 273.571)\n  have h5up : Real.exp 5 \u2264 (148.414 : \u211d) := by\n    rw [exp_five]\n    exact le_trans (exp_one_pow_le 5) (by norm_num)\n  have h06up : Real.exp 0.6 \u2264 (1.8433 : \u211d) :=\n    le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n  have h56 : Real.exp 5.6 = Real.exp 5 * Real.exp 0.6 := by\n    rw [show (5.6 : \u211d) = 5 + 0.6 by norm_num, Real.exp_add]\n  have h56small : Real.exp 5.6 \u2264 (285 : \u211d) := by\n    rw [h56]\n    exact le_trans (mul_le_mul h5up h06up (Real.exp_pos _).le (by norm_num))\n      (by norm_num)\n  have hlogT2ge : (5.6 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1 + 2) := by\n    have hbig : (285 : \u211d) \u2264 Real.sqrt 80000 + 1 + 2 := by linarith\n    have h1 : (5.6 : \u211d) \u2264 Real.log 285 := by\n      have h := Real.log_le_log (Real.exp_pos _) h56small\n      rwa [Real.log_exp] at h\n    exact le_trans h1 (Real.log_le_log (by norm_num : (0 : \u211d) < 285) hbig)\n  -- log log (T+2) \u2265 0 (log (T+2) \u2265 5.6 \u2265 1)\n  have hloglogT2nn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) :=\n    Real.log_nonneg (by linarith)\n  -- log T \u2265 0 and log log T \u2265 0 (T \u2265 283 \u2265 e)\n  have hlogTnn : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) :=\n    Real.log_nonneg (by linarith)\n  have hlogTge1 : (1 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) := by\n    have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 :=\n      le_trans Real.exp_one_lt_d9.le (by linarith)\n    have h := Real.log_le_log (Real.exp_pos 1) he\n    rwa [Real.log_exp] at h\n  have hloglogTnn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1)) :=\n    Real.log_nonneg hlogTge1\n  -- FAlt T \u2265 0 (every term nonneg)\n  have hFAlt0 : (0 : \u211d) \u2264 FAlt (Real.sqrt 80000 + 1) := by\n    unfold FAlt\n    have hpi : (0 : \u211d) < Real.pi := Real.pi_pos\n    have hp1 : (0 : \u211d) \u2264 (1 / (2 * Real.pi)) * ((Real.sqrt 80000 + 1) *\n        Real.log (Real.sqrt 80000 + 1)) :=\n      mul_nonneg (by positivity) (mul_nonneg hTpos.le hlogTnn)\n    have hp2 : (0 : \u211d) \u2264 0.137 * Real.log (Real.sqrt 80000 + 1) :=\n      mul_nonneg (by norm_num) hlogTnn\n    have hp3 : (0 : \u211d) \u2264 0.443 * Real.log (Real.log (Real.sqrt 80000 + 1)) :=\n      mul_nonneg (by norm_num) hloglogTnn\n    linarith [hp1, hp2, hp3]\n  -- \u0108\u2080 T \u2265 5.3248\n  have hC0lo : (5.3248 : \u211d) \u2264 C0hat (Real.sqrt 80000 + 1) := by\n    unfold C0hat\n    linarith [hlogT2ge, hloglogT2nn]\n  -- H\u0302 T \u2265 191.85\n  have hHlo : (191.85 : \u211d) \u2264 Hhat (Real.sqrt 80000 + 1) := by\n    unfold Hhat\n    have hsq : (5.3248 : \u211d) ^ 2 \u2264 C0hat (Real.sqrt 80000 + 1) ^ 2 :=\n      pow_le_pow_left\u2080 (by norm_num) hC0lo 2\n    linarith [hsq, hlogT2ge]\n  -- e\u2074 \u2265 54.5978\n  have he4 : (54.5978 : \u211d) \u2264 Real.exp 4 := by\n    rw [exp_four]\n    exact le_trans (by norm_num) (exp_one_pow_ge 4)\n  -- assemble\n  simp only [Bn]\n  -- Z\u2082 T \u2265 6.06 (0.6\u00b75.6 + 0 + 2.7; log log \u2265 0; the corrected count, D-071)\n  have hZ2lo : (6.06 : \u211d) \u2264 Z2hat (Real.sqrt 80000 + 1) := by\n    unfold Z2hat\n    linarith [hlogT2ge, hloglogT2nn]\n  have hbrlo : (110.84 : \u211d) \u2264 (2 / 3 : \u211d) * Z2hat (Real.sqrt 80000 + 1) +\n      10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 := by\n    have h1 := mul_le_mul_of_nonneg_left hZ2lo (by norm_num : (0 : \u211d) \u2264 2 / 3)\n    have h2 := mul_le_mul_of_nonneg_left hlogT2ge (by norm_num : (0 : \u211d) \u2264 10.5)\n    linarith [h1, h2]\n  have hterm2 : (4 * 283 * 110.84 : \u211d) \u2264 4 * (Real.sqrt 80000 + 1) *\n      ((2 / 3) * Z2hat (Real.sqrt 80000 + 1) +\n        10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48) := by\n    apply mul_le_mul _ hbrlo (by norm_num) (by positivity)\n    exact mul_le_mul_of_nonneg_left hTge (by norm_num)\n  have hterm4 : (2 * (54.5978 + 1) * (7 * 191.85 + 3.3) : \u211d) \u2264\n      2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 80000 + 1) + 3.3) := by\n    apply mul_le_mul _ _ (by norm_num) (by positivity)\n    \u00b7 apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : \u211d) \u2264 2)\n      linarith [he4]\n    \u00b7 linarith [hHlo]\n  have hII : (0 : \u211d) \u2264 IIMaj 80000 := IIMaj_nonneg 80000\n  linarith [hFAlt0, hterm2, hterm4, hII]\n\n/-- [PROVED session 012] Bn FAlt(10\u2075) \u2264 347000 (certified \u2248 346 920;\ntrue \u2248 330 900). -/\ntheorem Bn_FAlt_100000_le : Bn FAlt 100000 \u2264 (350000 : \u211d) := by\n  have hT : Real.sqrt 100000 + 1 \u2264 318 := by",
    "numLines": 115,
    "startLine": 370,
    "totalLines": 665
  }
}
raw content_json (database row) 
[{"type":"thinking","thinking":"As suspected — the three Bn evaluation proofs fail at their final linarith (lines 390, 479, 623):\n- Line 390 (Bn_FAlt_80000_le's final `linarith [hFAlt, hterm2, hterm4, hII]`): the new Bn has the dog-leg share, and the old proof lacks the DogLegRight bound — linarith fails.\n- Line 479 (Bn_FAlt_80000_ge's final linarith).\n- Line 623 (Bn_FAlt_100000_le's final linarith).\n\nSo I need to patch the three Bn evaluation proofs with DogLegRight bounds. The cleanest: add a certified bound on DogLegRight at each point (8e4 and 10⁵):\n\nDogLegRight(n) = ((√n+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj(n)/4.\n- At 8e4: ((283.84)/2)·(e^{5/2}+1)/2 + 8.38 + IIMaj(8e4)/4. (√80000 ≤ 283, so √80000+1 ≤ 284: (284/2)·(e^{5/2}+1)/2 = 142·(e^{5/2}+1)/2 = 71·(e^{5/2}+1) ≤ 71·13.19 = 936.49. +8.38 = 944.87. +IIMaj/4 ≤ 2590.08/4·... hmm — the old hII bounds IIMaj ≤ 2590.08 (the coarse 4.56·284·2 form): IIMaj/4 ≤ 647.52. So DogLegRight(8e4) ≤ 936.49+8.38+647.52 = 1592.39. And 2·DogLegRight ≤ 3184.78.\n  Hmm wait — the dog-leg part of the new Bn's horizontal share is 2·DogLegRight ≤ 3184.78 — vs the old share's 2(e⁴+1)·3.3 = 2·55.6015·3.3 = 367.0. So the new Bn(8e4) ≤ old-Bn-bound (327,058) − 367 + 3,184.78 = 329,876 — EXCEEDS the old certified 329,000!!! Need to re-certify ≤ 330,000 (or tighter).\n\nLet me recompute carefully with the old proof's term structure:\n- The old Bn_FAlt_80000_le proof: hFAlt : FAlt T ≤ 273.82; hterm2 : 4·284·112.9637 (the I_III bracket); hterm4 : 2·(54.6015+1)·(7·251.46+3.3) (the OLD horizontal); hII : IIMaj ≤ 2590.08. The old Bn ≤ 4·273.82 + 4·284·112.9637 + 40·1.3352 + 2·55.6015·(7·251.46+3.3) + 2590.08 + 1 = 1095.28 + 128,410.755 + 53.408 + 2·55.6015·1763.52 + 2590.08 + 1 = 1095.28+128,410.755+53.408+196,117.3+2590.08+1 = 328,250.8?? — the old comment says \"certified ≈ 327 058, true 322 309\" and the bound is ≤ 329,000. Hmm — my hand-arithmetic is off; whatever — the KEY: the old proof's final linarith: Bn ≤ 4·hFAlt + 4·284·112.9637 + 40·1.3352 + hterm4 + hII + 1 ≤ 329,000 — with hterm4 = 2·55.6015·(7·251.46+3.3).\n- The new Bn's horizontal share: 2(e⁴+1)·7Ĥ(T) + 2·DogLegRight — with Ĥ ≤ 251.46 (old hH): 2(e⁴+1)·7·251.46 = 2·55.6015·1760.22 = 195,846. And 2·DogLegRight ≤ 2·1592.39 = 3,184.78. So the new horizontal total ≤ 195,846+3,184.78 = 199,030.78. Hmm — but the old hterm4 covered 2(e⁴+1)(7·251.46+3.3) = 2·55.6015·1763.52 = 196,117.4?? — 2·55.6015 = 111.203; ×1763.52 = 196,117.4. And the new: 111.203·1760.22 = 195,745.9 + 3,184.78 = 198,930.7. Difference: +2,813.3.\n- So the new Bn(8e4) ≈ old certified (327,058) + 2,813 ≈ 329,871. New certified bound: ≤ 330,000.\n\nWait — but E-034's Bn_DL(8e4) = 324,912.99 — MUCH less than 329,871. The difference: E-034's Bn_DL uses T = √n+1 with the EXACT Ĥ/etc. values, while the old certified proof's coarse bounds (hlogT ≤ 5.7, hH ≤ 251.46, etc.) are LOOSE (they certify the OLD Bn's terms loosely). The new certified bound will be correspondingly loose. E-034's exact 324,913 vs the certified ~329,871 — the certified bound has the same looseness as the old one (which certified 327,058 vs true 322,309 — ~2.4% loose). So the new certified target: ≤ 330,000 (comfortable) or ≤ 331,000 for extra comfort.\n\nFor Bn_FAlt_80000_ge (the LOWER bound ≥ 274,000): the new Bn's dog-leg share only ADDS (positive terms), so Bn_new ≥ Bn_old-ish? — NO — the new Bn's horizontal share CHANGED: 2(e⁴+1)·7Ĥ + 2·DogLegRight vs old 2(e⁴+1)(7Ĥ+3.3) — the new share is BIGGER (adds 2·DogLegRight ~3,184 but removes 2(e⁴+1)·3.3 ~367): net +2,817. So Bn_new ≥ Bn_old + 2,817 ≥ 274,000 + ... — the lower bound proof bounds the big terms from BELOW (hterm2 lower + hterm4 lower + others ≥ 0) — the dog-leg share is POSITIVE (2·DogLegRight ≥ 0 ✓) so the lower bound EASILY survives: Bn_new ≥ [the old proof's lower terms] + 2·DogLegRight ≥ old-lower + 0 ≥ 274,000 ✓ — the old lower proof should STILL work if I add `0 ≤ 2·DogLegRight` (positivity). Actually the old lower proof's final linarith: Bn ≥ 4·hFAlt0 + hterm2-lo + hterm4-lo + hII-0 + 40·1.3352 + 1 ≥ 274,000 — with the new Bn's form having the dog-leg share — linarith needs 2·DogLegRight ≥ 0 to absorb ✓ — add `have hDLnn : (0:ℝ) ≤ DogLegRight 80000 := by unfold DogLegRight; positivity` and include in the linarith.\n\nHmm wait — actually the new Bn's horizontal share is 2(e⁴+1)·7Ĥ + 2·DogLegRight — the old hterm4-lo bounds 2(e⁴+1)(7Ĥ+3.3) ≥ ... — the new share's 2(e⁴+1)·7Ĥ part is ≤ the old (no 3.3) — the lower bound on the new share = (lower on 2(e⁴+1)·7Ĥ) + (lower on 2·DogLegRight = 0). The old hterm4-lo proves a lower bound on 2(e⁴+1)(7Ĥ+3.3) — which is LARGER than 2(e⁴+1)·7Ĥ — so hterm4-lo's lower bound on the OLD share does NOT lower-bound the new share's 2(e⁴+1)·7Ĥ part (the new part is SMALLER). Hmm — the old hterm4-lo : 2·(54.5978+1)·(7·191.85+3.3) ≤ 2(e⁴+1)(7Ĥ+3.3) — the new part 2(e⁴+1)·7Ĥ ≤ 2(e⁴+1)(7Ĥ+3.3) — so the old lower bound OVERCOUNTS for the new part: 2(e⁴+1)·7Ĥ ≥ 2(e⁴+1)·7·(Ĥ-lo − 3.3·...)·... hmm — the cleanest: recompute the lower bound for the new form: 2(e⁴+1)·7Ĥ ≥ 2·(54.5978+1)·7·191.85 (the old hHlo's 191.85, without the +3.3): = 111.1956·1342.95 = 149,355. And 2·DogLegRight ≥ 0. So new Bn ≥ 4·hFAlt0 + hterm2-lo + (2(e⁴+1)·7·191.85-lo) + 0 + 40·1.3352 + hII0 + 1 — the old proof's lower total was ≥ 274,000 with the OLD hterm4-lo (2·55.5978·(7·191.85+3.3) = 111.1956·1346.25 = 149,722). The new hterm4-lo (without 3.3): 111.1956·1342.95 = 149,355 — smaller by 367. And the dog-leg adds 0 (lower). So new lower total ≈ 274,000 − 367 + 0 ≈ 273,633 — hmm — that's BELOW 274,000!! The old certified lower was exactly 274,000 — with the 3.3 removed, the new lower total is ~273,633 < 274,000 — so the certified lower bound needs to drop to ≤ 273,000 or re-certify at 273,000.\n\nHmm wait — but the margin uses margin(8e4) ≤ sInfty_up − Bn_lo + 1 for hbase2 — with Bn_lo = 273,000: margin(8e4) ≤ 339,000 − 273,000 + 1 = 66,001 — and margin(10⁵) ≥ 432,500 − Bn_up + 1. With Bn_up(10⁵) needing re-certification too (the same +2,817 issue: old ≤ 350,000 → new ≈ 352,800): margin(10⁵) ≥ 432,500 − 352,800 + 1 = 79,701. Then hbase2: margin(8e4) ≤ 66,001 < 79,701 ✓ still works!! And hbase: margin(8e4) ≥ 336,000 − Bn_up(8e4) + 1 = 336,000 − 330,000 + 1 = 6,001 > 0 ✓ works!\n\nWait — but hold on: I should double check the E-034 margins: E-034's margin_DL at 8e4 = 13,160 and at 10⁵ = 88,911. My certified bounds give margin(8e4) ∈ [6,001, 66,001] and margin(10⁵) ≥ 79,701 — the hbase (0 < margin(8e4)) ✓ and hbase2 (66,001 < 79,701 ✓) — both work but MUCH coarser than E-034's true values (13,160 / 88,911). The certified bounds should target closer to E-034's: Bn_up(8e4) ≤ 325,000 (E-034's 324,913 + slack ~200 for the certified looseness): margin(8e4) ≥ 336,000−325,000+1 = 11,001; Bn_lo(8e4) ≥ 322,000: margin(8e4) ≤ 339,000−322,000+1 = 17,001; Bn_up(10⁵) ≤ 345,000 (E-034 344,838): margin(10⁵) ≥ 432,500−345,000+1 = 87,501. hbase2: 17,001 < 87,501 ✓✓ — those match the session-038 certified form (8,001/82,501) closely and are much better.\n\nHmm — but E-034's Bn_DL uses the EXACT arithmetic (C_zeta3 = 0.5 charged as 0.5; e^{5/2}+1 charged 13.19; etc.) — the certified LiBasePoints bounds use the d9-certified logs and the coarse IIMaj (4.56(√n+1)·2 ≈ 2590) — the certified Bn_up will be looser than E-034's by the IIMaj-coarse and the log looseness. E-034's 324,913 vs old-certified-true 322,309 — the difference is the dog-leg share (+2,813) minus nothing: 322,309+2,813 = 325,122 — hmm — E-034's Bn_DL(8e4) = 324,913 < 325,122?! — because E-034's dog-leg charge uses VLeftBound with C_zeta3 = 0.5: VLeftBound(8e4) = ((√n+1)/2)·13.19·0.5 = 142·6.595 = 936.49 ✓ matches my 936.49 ✓. And IIMaj/4 with the exact form (not the coarse 4.56·284·2): E-034's IIMaj(n) = 2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)} = tiny (~1e-105) — E-034's IIMaj/4 ≈ 0!! — while my certified bound uses the COARSE IIMaj ≤ 2590.08 (IIMaj_le_two_mul) → IIMaj/4 ≤ 647.52. So E-034's DogLegRight ≈ 936.49+8.38+0 = 944.87, mine (coarse) ≈ 936.49+8.38+647.52 = 1,592.39 — difference 647.5 (the coarse IIMaj/4). And the I_I's IIMaj: E-034's I_I ≈ 0, mine coarse ≈ 2590. Total IIMaj: E-034 ~0, mine ~3,237. So my certified Bn_up(8e4) ≈ E-034's 324,913 + 3,237 ≈ 328,150?? — no wait — E-034's Bn_DL ALREADY uses IIMaj(n) for the I_I piece (with the exact ~0 value) and VRightBound = IIMaj/4 (~0). My certified version charges the COARSE IIMaj (2590) for I_I and coarse IIMaj/4 (647.5) for the dog-leg — total IIMaj-ish 3,237.5 vs E-034's ~0. So certified Bn_up(8e4) ≈ E-034's 324,913 + 3,237 ≈ 328,150. Hmm — that's ABOVE my 325,000 target. Let me use 330,000 (comfortable).\n\nUgh — actually wait. The OLD certified proof (session 012, updated session 038) certified Bn ≤ 329,000 with the coarse IIMaj 2590.08 — the old true Bn (session-038 form) ≈ 322,309 (E-023/E-030's exact) — the old certified 329,000 has slack 6,691 over true. The NEW Bn's true ≈ 325,122 (old true + 2,813). So new certified target with the same slack: ≤ 335,000 (325,122 + ~9,900 slack for the log looseness) — or keep it tighter: the old proof's STRUCTURE gave 329,000 from the loose bounds; the new structure with the same loose bounds gives ~329,000 − 367 (3.3 removed) + 3,184.78 (dog-leg) ≈ 331,818. So certify ≤ 332,000 (small slack) or 333,000 (comfortable).\n\nLet me just patch the three proofs minimally: for the upper bounds (le), add a certified DogLegRight upper bound and bump the target; for the lower bound (ge), subtract the 3.3 from the hterm4-lo and add DogLegRight ≥ 0, lowering the target appropriately (or keep the 3.3 in the lower form for simplicity: the old hterm4-lo's form (7·191.85+3.3) — the new share's constant part — hmm, the new share is 2(e⁴+1)·7Ĥ + 2·DogLegRight: its LOWER bound: 2(e⁴+1)·7·Ĥ-lo + 0 = 2·55.5978·7·191.85 = 149,355 — and the old proof's total-lower was 274,000 with 149,722 for hterm4-lo: new total-lower = 274,000 − 367 = 273,633 — hmm — but the OTHER pieces' lower bounds are unchanged ✓ so the new total-lower ≈ 273,633. Certify ≥ 273,000 (slack 633) ✓.\n\nHmm wait, actually — for the ge (lower) bound I can keep it SIMPLE: the new share's 2(e⁴+1)·7Ĥ ≥ the old hterm4-lo's form MINUS the 3.3-part: 2(e⁴+1)·7Ĥ ≥ 2·55.5978·(7·191.85) = 149,355 ✓ — and 2·DogLegRight ≥ 0 ✓. New total-lower = 4·hFAlt0 + hterm2-lo + hterm4'-lo (149,355) + hII0 + 40·1.3352 + 1 = old-total − 367 = 273,633 ✓ certify ≥ 273,000 ✓.\n\nFor the two le (upper) bounds: add DogLegRight ≤ 1,593 (at 8e4: 936.49+8.38+647.52 = 1,592.39 → 1,593; at 10⁵: (√10⁵+1)/2·13.19/2·... = 317.23/2·... hmm: (√100000+1)/2 = 158.6: 158.6·(e^{5/2}+1)/2 = 158.6·6.591 = 1,045.4; +8.38 = 1,053.78; +IIMaj/4 ≤ 2900.16/4 = 725.04: DogLegRight(10⁵) ≤ 1,778.82 → 1,779) and bump the targets: new share at 8e4 = old-share-minus-3.3 + 2·DogLegRight: hterm4-new = 2·55.6015·(7·251.46) + 2·1593 = 195,845.9 + 3,186 = 199,031.9 — and the old proof's total was ≤ 329,000 with hterm4 = 196,117.4: new total = 329,000 − 196,117.4 + 199,031.9 = 331,914.5 — certify ≤ 332,000. At 10⁵: hterm4-new = 2·55.6015·(7·255.05) + 2·1779 = 198,471.7 + 3,558 = 202,029.7; old total ≤ 350,000 with hterm4 = 198,838.5: new = 350,000 − 198,838.5 + 202,029.7 = 353,191.2 — certify ≤ 354,000.\n\nHmm wait — let me recompute the old hterm4 values from the file. The old Bn_FAlt_80000_le's hterm4: `2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 80000 + 1) + 3.3) ≤ 2 * (54.6015 + 1) * (7 * 251.46 + 3.3)` — so the old proof's horizontal share bound is 2·55.6015·(7·251.46+3.3) = 2·55.6015·1763.52 = 196,117.4 (matches my estimate ✓). And the old Bn_FAlt_100000_le's hterm4: `2 * (54.6015 + 1) * (7 * 255.05 + 3.3)` = 2·55.6015·1788.65 = 198,838.7 ✓.\n\nAnd the new horizontal shares:\n- 8e4: 2(e⁴+1)·7Ĥ + 2·DogLegRight ≤ 2·55.6015·7·251.46 + 2·1593 = 2·55.6015·1760.22 + 3,186 = 195,845.9 + 3,186 = 199,031.9.\n- 10⁵: 2·55.6015·7·255.05 + 2·1779 = 2·55.6015·1785.35 + 3,558 = 198,471.6 + 3,558 = 202,029.6.\n\nNew certified upper bounds:\n- Bn(8e4) ≤ 4·273.82 + 4·284·112.9637 + 53.408 + 199,031.9 + 2590.08 + 1 = 1095.28 + 128,410.76 + 53.41 + 199,031.9 + 2590.08 + 1 = 331,181.4?? — hmm — wait, the old proof's final linarith used hterm2 = 4·284·112.9637 = 128,410.76 — and the total was ≤ 329,000 — so old total = 1095.28 + 128,410.76 + 53.41 + 196,117.4 + 2590.08 + 1 = 328,267.9 → ≤ 329,000 (slack 732). New total = 328,267.9 − 196,117.4 + 199,031.9 = 331,182.4 → certify ≤ 332,000 (slack 818).\n- Bn(10⁵) ≤ 4·311.45 + 4·318·114.0656 + 53.41 + 202,029.6 + 2900.16 + 1 = 1245.8 + 145,091.33 + 53.41 + 202,029.6 + 2900.16 + 1 = 351,521.3 → ≤ 352,000 (slack 479) — or 353,000 (slack 1,479 — more comfortable; the old had 350,000 with slack ~3,080 vs true ~330,900 — wait the old certified was 350,000 vs \"certified ≈ 346 920; true ≈ 330 900\" — slack 3,080 vs certified, 19,100 vs true. New true ≈ 333,700. Certify ≤ 353,000 (slack 1,479 vs the loose-certified 351,521).)\n\nHmm — let me double-check E-034's Bn_DL values: 324,913 (8e4) and 344,838 (10⁵). My new certified upper bounds 332,000/352,000 have slack ~7,000 over E-034's exact — fine (the old certified had similar looseness).\n\nActually — wait. Let me reconsider: E-034's Bn_DL(8e4) = 324,913 uses the EXACT IIMaj (~1e-105) and exact IIMaj/4 (~0), while my certified uses the coarse IIMaj_le_two_mul (2590.08 at 8e4, 2900.16 at 10⁵). The coarse-vs-exact IIMaj difference is 2590+647 = 3,237 at 8e4 and 2900+725 = 3,625 at 10⁵. So my certified Bn_up(8e4) ≈ E-034's 324,913 + 3,237 + (the old-certified-vs-true looseness ~4,750) ≈ 332,900?? — hmm — the old certified 329,000 vs old true 322,309 — slack 6,691 (includes the IIMaj-coarse 2,590 + log looseness ~4,100). So new certified ≈ E-034's 324,913 + 6,691 + (dog-leg-vs-old-3.3 difference: +2,817·... — wait — E-034's Bn_DL already INCLUDES the dog-leg share with its exact IIMaj/4 (~0) — my certified's DogLegRight includes the coarse IIMaj/4 (647.52) — so my certified Bn_up(8e4) ≈ E-034's 324,913 + (log looseness ~4,100) + (IIMaj-coarse on I_I: 2,590) + (IIMaj-coarse on dog-leg: 647.52) ≈ 332,250. Certify ≤ 333,000.\n\nAnd 10⁵: E-034's 344,838 + ~4,600 + 2,900 + 725 ≈ 353,063. Certify ≤ 354,000.\n\nHmm — these are getting close to the margins: margin(8e4) ≥ 336,000 − 333,000 + 1 = 3,001 > 0 ✓ (E-034's true margin is 13,160 — my certified lower is much coarser but positive ✓). hbase2: margin(8e4) ≤ 339,000 − 273,000 + 1 = 66,001 < margin(10⁵) ≥ 432,500 − 354,000 + 1 = 78,501 ✓ (66,001 < 78,501 ✓ works).\n\nHmm — 3,001 is a bit thin. Let me tighten the upper bound on the IIMaj-coarse for the dog-leg: the DogLegRight's IIMaj/4 — I could use the TRUE IIMaj's tiny value via a better bound than IIMaj_le_two_mul... — the old proof's hII uses IIMaj_le_two_mul (the coarsest 4.56(√n+1)·2). There's no tighter certified IIMaj bound in the codebase (the psiTilde decay analysis gives IIMaj ≤ 4.56(√n+1)(e^{−a√n}+e^{−b√n}) — the TRUE tiny value — but no certified lemma bounds it below 4.56(√n+1)·2·e^{−a√n}·... hmm — actually IIMaj_le_two_mul is the ONLY IIMaj upper bound — and it gives 9.12(√n+1). The true IIMaj at 8e4 is ~4.56·283.84·(e^{−0.8863·282.84}+e^{−1.3863·282.84}) = 4.56·283.84·(e^{−250.7}+e^{−392.2}) ≈ 4.56·283.84·e^{−250.7} ≈ 1294.8·2.4e-109 ≈ 3e-106 — ASTRONOMICALLY smaller than 2,590!! The coarse bound loses 10^109×!!\n\nSo the certified Bn_up could be MUCH tighter with a finer IIMaj bound. But the old proof uses the coarse form and it works (the margin is robust). For the dog-leg Bn, the coarse form still works (margins stay positive). Let me not over-engineer: certify with the coarse IIMaj form at ≤ 333,000/≤ 354,000, margins 3,001/78,501 — hbase ✓ (3,001 > 0) hbase2 ✓ (66,001 < 78,501). But 3,001 is thin-ish — let me instead use a slightly better IIMaj/4 bound in the dog-leg share to fatten the margin: actually — the E-034 margins (13,160/88,911) are the TRUE ones; the certified base points just need to WORK. 3,001 works but is uncomfortably close to 0 for a \"certified\" claim. Let me instead target the E-034-matching form more carefully:\n\nActually — the cleanest: bound DogLegRight with the EXACT IIMaj/4 form (not the coarse): DogLegRight's IIMaj/4 needs an IIMaj bound — the only one is IIMaj_le_two_mul (coarse). Alternatively, use a NEW tighter IIMaj bound: IIMaj(n) ≤ 4.56·(√n+1)·2·e^{−(√n)/2}?? — psiTilde(s) = 4.56(s+1)(e^{−as}+e^{−bs}) ≤ 4.56(s+1)·2·e^{−as} (both exp ≤ e^{−as} since a ≤ b): IIMaj n = psiTilde(√n) ≤ 4.56(√n+1)·2·e^{−0.8863√n} — a certified version via the existing machinery? — there's no such lemma, but IIMaj_le_two_mul exists. For the base points, the old proof's coarse form is the established pattern — let me keep it and just fatten by using 333,000/354,000 with margins 3,001/78,501 — hmm — 3,001 is fine actually (it's a certified positive lower bound; the true margin is 13,160).\n\nHmm — wait, actually, let me reconsider: is the tightness of hbase (0 < margin) critical? pos_of_convex_of_two_points needs hbase : 0 < marginTilde FAlt 80000 and hbase2 : marginTilde FAlt 80000 < marginTilde FAlt 100000. 3,001 > 0 ✓ and 66,001 < 78,501 ✓ — both work. The margin's certified positivity at 8e4 is 3,001 — that's the certified claim, true is 13,160. Acceptable.\n\nBUT — actually, I realize I should double-check my arithmetic for the new Bn at 8e4 vs 333,000. Let me recompute with the old proof's exact term values:\n\nOld proof's pieces at 8e4 (from the file):\n- hFAlt : FAlt(√80000+1) ≤ 273.82 → 4·273.82 = 1,095.28\n- hterm2 : 4·284·112.9637 = 4·284 = 1,136; ×112.9637 = 128,330.76?? — 1,136·112.9637 = 128,330.76 (I said 128,410 earlier — recompute: 284·112.9637 = 32,081.69; ×4 = 128,326.77. Hmm — 284·112.9637: 284·112 = 31,808; 284·0.9637 = 273.69; total 32,081.69; ×4 = 128,326.77.)\n- 40·1.3352 = 53.408\n- hterm4 : 2·55.6015·(7·251.46+3.3) = 2·55.6015·1763.52 = 111.203·1763.52 = 196,120.6?? — 111.203·1763.52: 111.203·1760 = 195,717.3; 111.203·3.52 = 391.4; total 196,108.7. Hmm — 7·251.46 = 1,760.22; +3.3 = 1,763.52 ✓; ×111.203 = 196,108.7.\n- hII : IIMaj ≤ 2590.08\n- +1\nOld total: 1,095.28 + 128,326.77 + 53.41 + 196,108.7 + 2590.08 + 1 = 328,175.24 → the old proof certified ≤ 329,000 (slack 825) — and the file's comment says \"certified ≈ 327 058\" — close enough (my hand-arithmetic ~1,100 off; whatever).\n\nNew pieces:\n- hterm4-new : 2(e⁴+1)·7·251.46 + 2·DogLegRight = 111.203·1760.22 + 2·DogLegRight = 195,754.3 + 2·DogLegRight. DogLegRight(8e4) ≤ (284/2)·(e^{5/2}+1)/2 + 8.38 + 2590.08/4 = 142·(e^{5/2}+1)/2 + 8.38 + 647.52 = 71·(e^{5/2}+1)·... = 71·13.19·... — hmm: (284/2)·(e^{5/2}+1)/2 = 142·(13.1825+1)/2?? — no: (e^{5/2}+1)/2 = (12.1825+1)/2 = 13.1825/2 = 6.59125 — the (e^{5/2}+1)/2 factor is 6.59125?? — WAIT: (e^{5/2}+1)/2 = 6.591 — and ((√n+1)/2)·(e^{5/2}+1)/2 = 142·6.59125 = 935.96. +8.38 = 944.34. +647.52 = 1,591.86. → 2·DogLegRight = 3,183.72. So hterm4-new = 195,754.3 + 3,183.72 = 198,938.0.\n- e^{5/2}+1's certified bound: E-034's E52P1 = 13.19 ≥ e^{5/2}+1 = 13.182494 — the certified 13.19 has slack 0.0075 ✓. For the certified DogLegRight I should use the certified e^{5/2}+1 ≤ 13.19 — the old file has exp bounds (exp_le_inv_sub_sixteen for e^{0.263} etc. — need e^{5/2} = e²·e^{0.5}: e² ≤ 7.3891, e^{0.5} ≤ 1.6488: e^{5/2} ≤ 12.1852 → e^{5/2}+1 ≤ 13.1852 — hmm — tighter than 13.19 ✓ use 13.19 or 13.186). Let me use e^{5/2}+1 ≤ 13.186 (e²·e^{0.5} ≤ 7.3891·1.6488 = 12.18517 → +1 = 13.18517 → 13.186). Then (284/2)·13.186/2 = 142·6.593 = 936.2; +8.38 = 944.58; +647.52 = 1,592.1 → 2·DogLegRight ≤ 3,184.2.\n\nNew total at 8e4: 1,095.28 + 128,326.77 + 53.41 + 198,938.0 + 2590.08 + 1 = 331,004.5 → certify ≤ 332,000 (slack ~995).\n\nAt 10⁵:\n- hFAlt : FAlt(√100000+1) ≤ 311.45 → 4·311.45 = 1,245.8\n- hterm2 : 4·318·114.0656 = 1,272·114.0656 = 145,091.5?? — 318·114.0656 = 36,272.86; ×4 = 145,091.4.\n- 40·1.3352 = 53.41\n- hterm4-new : 2·55.6015·7·255.05 + 2·DogLegRight = 111.203·1785.35 + 2·DogLegRight = 198,510.7 + 2·DogLegRight. DogLegRight(10⁵) ≤ (318/2)·13.186/2 + 8.38 + 2900.16/4 = 159·6.593 + 8.38 + 725.04 = 1,048.3 + 8.38 + 725.04 = 1,781.7 → 2·DogLegRight = 3,563.4. hterm4-new = 198,510.7 + 3,563.4 = 202,074.1.\n- hII : IIMaj ≤ 2900.16\n- +1\nNew total at 10⁵: 1,245.8 + 145,091.4 + 53.41 + 202,074.1 + 2900.16 + 1 = 351,365.9 → certify ≤ 352,000 (slack ~634).\n\nMargins: margin(8e4) ≥ 336,000 − 332,000 + 1 = 4,001 ✓ (better than 3,001); margin(10⁵) ≥ 432,500 − 352,000 + 1 = 80,501 ✓. hbase2: margin(8e4) ≤ 339,000 − Bn_lo(8e4) + 1 — Bn_lo(8e4) with the 3.3 removed: old ge's form: 2(e⁴+1)·7·191.85 + 0 = 149,355 — new ge total = old-total − 367: the old proof's final linarith gave ≥ 274,000 — with the 3.3 part removed: 274,000 − 2·55.5978·3.3·... hmm — the old hterm4-lo was 2·55.5978·(7·191.85+3.3) = 111.1956·1346.25 = 149,722.8?? — 7·191.85 = 1,342.95; +3.3 = 1,346.25; ×111.1956 = 149,723.5. New hterm4-lo : 2(e⁴+1)·7·191.85 = 111.1956·1342.95 = 149,356.7. Difference: −366.8. So new ge total = 274,000 − 366.8 = 273,633.2 → certify ≥ 273,000 (slack 633).\n\nmargin(8e4) ≤ 339,000 − 273,000 + 1 = 66,001 < 80,501 ✓✓ hbase2 ✓.\n\nAnd hbase: margin(8e4) ≥ 4,001 > 0 ✓.\n\nThese certified bounds work. Now — the cleanest implementation: patch the three Bn evaluation proofs to add the DogLegRight term with its certified bound and adjust the targets. Let me look at the exact structure of the three proofs' final linarith calls to patch minimally.\n\nActually — a cleaner minimal patch: bound `2·DogLegRight n ≤ [constant]` and add it to the existing linarith lists, adjusting the hterm4 to remove the 3.3. Let me look at the exact final blocks of the three proofs (lines ~378-390, ~470-479, ~615-623).","signature":""},{"type":"text","text":"The three Bn evaluation proofs need DogLegRight bounds. Checking their final assembly blocks."},{"type":"tool_use","id":"Read_623","name":"Read","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean","offset":370,"limit":115},"extra_content":null}]