← Session 36 — ii′-6-DL dog-leg + side bounds; Paper A review
**Review fully actioned.** All six items addressed, with the factual vulnerability verified against the source texts rather than patched cosmetically. Master @ `973edbb` (+ the Lean commit `79c96f2`).
## Point-by-point disposition
1. **Step 5 / Misguich–Voros** — confirmed the vulnerability is *real*, not just stylistic: Voros 2020 verifies a **deformed sequence Λ_n** (G. Misguich, *private communication* 2017), not the ordinary λ_n. The citation was **retracted** everywhere. Replacement found *in Voros's own text*: **Johansson 2015 § 4.2** (Numer. Algor. 69:253–270) — a published, rigorous interval-arithmetic computation of the ordinary λ₀…λ₁₀₀₀₀₀, all positive (λ₁₀₀₀₀₀ certified to ~2900 digits). The Lean perimeter `LiVerifiedUpTo` was reduced `(5·10⁵) → (10⁵)` to match the checkable evidence — the assembly's hfinite branch uses exactly n < 10⁵, so nothing else changes; rebuild green, audit re-run clean.
2. **Theorem vs trust boundary** — both Theorem environments now assume (i) RH verified to T₀ (Platt–Trudgian) **and** (ii) λ_n > 0 for n ≤ 10⁵ (Step 5). Appendix B gained the instantiation list mapping each hypothesis to its cited source (Platt–Trudgian also discharges `NoLowZeros`; Trudgian 2014 the three counting Props; E-023 `MZeroProp`).
3. **"Exactly eight" — you were right, it's SEVEN** (2 + 5; the analytic list itself names five). Fixed in the paper, Lean docstrings, NGUYEN.md, STATE.md, R-004. Per your advice, Appendix B now prints the **actual final Lean signature verbatim** (tt-quote, unicode via math) and counts from it.
4. **Novelty toned down** — "first" → "we have found no previous explicit assembly"; "maximal content" → the narrow Voros form (eventual positivity of all large λ_n ⟹ RH ⟹ no infinite positive tail short of RH). During the citation check I also found **Oesterlé 2000's unpublished precursor** (prop. 2: RH-to-T₀ ⟹ λ_n ≥ 0 for n ≤ T₀², cited in Voros 2020) — now explicitly acknowledged with a new bib entry, alongside Lagarias's published weaker window.
5. **F-D promoted to its own §3.1** ("Repair of the right-horizontal estimate") with your exact framing: the geometric-decrease conclusion following (6.12) *is not implied by the displayed bounds* when T ≍ √n (ratio e/2 > 1) — a proof gap, not a theorem-false claim — plus the displayed H_low = H_high − V_right + V_left deformation and the safe high-tail contraction. The Step-2 footnote now carries only F-A/F-B/F-E.
6. **Appendix B** — now includes the verbatim signature and your dependency-chain display (partial fractions → S_f = Res₁ → rectangle identity → four side bounds → `sfBoundProp` → `lambda_pos_finite_height_closed`). **Section 2 compressed** to one paragraph. **Revision date** → 2026-08-26.
**Verified:** pdflatex+bibtex clean, **11 pp**, zero undefined refs; both new bib entries resolve; cover-letter.md and referee-list.md corrected to Johansson; `draft.tex` (frozen), paperB.tex, and your correspondence package untouched. Archive: R-004, D-037 erratum addendum, NGUYEN.md, STATE.md, journal-042, db registration — all committed.
Ready for your read-through of the revised `paperA.pdf`.
raw content_json (database row)
[{"type":"text","text":"**Review fully actioned.** All six items addressed, with the factual vulnerability verified against the source texts rather than patched cosmetically. Master @ `973edbb` (+ the Lean commit `79c96f2`).\n\n## Point-by-point disposition\n\n1. **Step 5 / Misguich–Voros** — confirmed the vulnerability is *real*, not just stylistic: Voros 2020 verifies a **deformed sequence Λ_n** (G. Misguich, *private communication* 2017), not the ordinary λ_n. The citation was **retracted** everywhere. Replacement found *in Voros's own text*: **Johansson 2015 § 4.2** (Numer. Algor. 69:253–270) — a published, rigorous interval-arithmetic computation of the ordinary λ₀…λ₁₀₀₀₀₀, all positive (λ₁₀₀₀₀₀ certified to ~2900 digits). The Lean perimeter `LiVerifiedUpTo` was reduced `(5·10⁵) → (10⁵)` to match the checkable evidence — the assembly's hfinite branch uses exactly n < 10⁵, so nothing else changes; rebuild green, audit re-run clean.\n\n2. **Theorem vs trust boundary** — both Theorem environments now assume (i) RH verified to T₀ (Platt–Trudgian) **and** (ii) λ_n > 0 for n ≤ 10⁵ (Step 5). Appendix B gained the instantiation list mapping each hypothesis to its cited source (Platt–Trudgian also discharges `NoLowZeros`; Trudgian 2014 the three counting Props; E-023 `MZeroProp`).\n\n3. **\"Exactly eight\" — you were right, it's SEVEN** (2 + 5; the analytic list itself names five). Fixed in the paper, Lean docstrings, NGUYEN.md, STATE.md, R-004. Per your advice, Appendix B now prints the **actual final Lean signature verbatim** (tt-quote, unicode via math) and counts from it.\n\n4. **Novelty toned down** — \"first\" → \"we have found no previous explicit assembly\"; \"maximal content\" → the narrow Voros form (eventual positivity of all large λ_n ⟹ RH ⟹ no infinite positive tail short of RH). During the citation check I also found **Oesterlé 2000's unpublished precursor** (prop. 2: RH-to-T₀ ⟹ λ_n ≥ 0 for n ≤ T₀², cited in Voros 2020) — now explicitly acknowledged with a new bib entry, alongside Lagarias's published weaker window.\n\n5. **F-D promoted to its own §3.1** (\"Repair of the right-horizontal estimate\") with your exact framing: the geometric-decrease conclusion following (6.12) *is not implied by the displayed bounds* when T ≍ √n (ratio e/2 > 1) — a proof gap, not a theorem-false claim — plus the displayed H_low = H_high − V_right + V_left deformation and the safe high-tail contraction. The Step-2 footnote now carries only F-A/F-B/F-E.\n\n6. **Appendix B** — now includes the verbatim signature and your dependency-chain display (partial fractions → S_f = Res₁ → rectangle identity → four side bounds → `sfBoundProp` → `lambda_pos_finite_height_closed`). **Section 2 compressed** to one paragraph. **Revision date** → 2026-08-26.\n\n**Verified:** pdflatex+bibtex clean, **11 pp**, zero undefined refs; both new bib entries resolve; cover-letter.md and referee-list.md corrected to Johansson; `draft.tex` (frozen), paperB.tex, and your correspondence package untouched. Archive: R-004, D-037 erratum addendum, NGUYEN.md, STATE.md, journal-042, db registration — all committed.\n\nReady for your read-through of the revised `paperA.pdf`."}]