← Session 31 — ii′-5f: tight R-bound 10.5/48 (piece 3 + pinch)
**ii′-5f is COMPLETE** — session 036 closed out cleanly.
## What was accomplished
**The tight R-bound is now Lean-proved modulo only the declared perimeter.**
```
logDeriv_riemannZeta_sub_nearZeros_le_tight (hZC) (hZC2) (hNLZ) :
‖logDeriv ζ s − Σ_{ρ near} m_ρ/(s−ρ)‖ ≤ 10.5·log(t+2) + 48
```
**5f-iii** (this phase, ~550 lines):
- **Pinch lemma** `pinch_tight_R`: 11.6318·log L − 4.6484·L ≤ 0.397094 for L ≥ log 12 — concave tangent at the certified critical point 2.5024 (f′ antitone on Ici(log 12), FTC in both directions, f(2.5024) ≤ −0.96231 certified via log 2.5024 ≤ 0.9173). Supporting bounds: log 12 = 4 log 2 − log(4/3) ≥ 2.4848 (new 4-term `neg_log_one_sub_le_four` machine), log 12 ≤ 2.5024, log 3 ≤ 1.0987.
- **C0hat L/LL conversion**: C0hat(t+1) ≤ 0.433(L+1/12) + 0.886(LL+0.03354) + 2.9.
- **Capstone**: the six-piece assembly into `Rexpr_decomp`'s norm chain — piece 1 dirichletC2 ≤ 1, piece 2 honest two-unit near count, piece 3 far_series_le, pieces 4/5 (0.045 each), piece 6 (6/t ≤ 0.6) — fold 5.8516L + 11.6318LL + 47.6029 ≤ 10.5L + 48 via the pinch (margin ≈ 1.36).
**Audits**: session036/036b — 33 declarations, 3 standard axioms only; full build green (8762 jobs).
**Archive closed** (§8.4): journal-036, STATE.md (new NEXT ACTION: **ii′-3b, the contour moments**), NGUYEN.md checklist (ii′-5f → ✅) + session log, research.db (session 036 + D-070).
## Session summary (all of session 036)
Piece 3 (~2700 lines: certified numerics, farW/S₃, six tail bricks, C0hat bridges, zeroMult_conj, farG + norm reduction, main bucket machine, two tail machines) + 5f-iii. Key banked gotcha for future sessions: `a * b / c` parses as `(a·b)/c` — write `c * (b / d)` with explicit parens when using `mul_left`-coefficient proofs, or isDefEq explodes.
Remaining map: **ii′-3b** (contour moments σ_k = −g^{(k−1)}(0)/(k−1)! — the R-bound now exists to drive the moment estimates) → ii′-3c (crux Sf = Res₁) → ii′-6 (L0 assembly; D-069 Finding 2's H(T) repair lives there) → ii′-7 (closure: `sfBoundProp`, the 3-perimeter-hypothesis final theorem, paper Appendix B).
raw content_json (database row)
[{"type":"text","text":"**ii′-5f is COMPLETE** — session 036 closed out cleanly.\n\n## What was accomplished\n\n**The tight R-bound is now Lean-proved modulo only the declared perimeter.**\n\n```\nlogDeriv_riemannZeta_sub_nearZeros_le_tight (hZC) (hZC2) (hNLZ) :\n ‖logDeriv ζ s − Σ_{ρ near} m_ρ/(s−ρ)‖ ≤ 10.5·log(t+2) + 48\n```\n\n**5f-iii** (this phase, ~550 lines):\n- **Pinch lemma** `pinch_tight_R`: 11.6318·log L − 4.6484·L ≤ 0.397094 for L ≥ log 12 — concave tangent at the certified critical point 2.5024 (f′ antitone on Ici(log 12), FTC in both directions, f(2.5024) ≤ −0.96231 certified via log 2.5024 ≤ 0.9173). Supporting bounds: log 12 = 4 log 2 − log(4/3) ≥ 2.4848 (new 4-term `neg_log_one_sub_le_four` machine), log 12 ≤ 2.5024, log 3 ≤ 1.0987.\n- **C0hat L/LL conversion**: C0hat(t+1) ≤ 0.433(L+1/12) + 0.886(LL+0.03354) + 2.9.\n- **Capstone**: the six-piece assembly into `Rexpr_decomp`'s norm chain — piece 1 dirichletC2 ≤ 1, piece 2 honest two-unit near count, piece 3 far_series_le, pieces 4/5 (0.045 each), piece 6 (6/t ≤ 0.6) — fold 5.8516L + 11.6318LL + 47.6029 ≤ 10.5L + 48 via the pinch (margin ≈ 1.36).\n\n**Audits**: session036/036b — 33 declarations, 3 standard axioms only; full build green (8762 jobs).\n\n**Archive closed** (§8.4): journal-036, STATE.md (new NEXT ACTION: **ii′-3b, the contour moments**), NGUYEN.md checklist (ii′-5f → ✅) + session log, research.db (session 036 + D-070).\n\n## Session summary (all of session 036)\n\nPiece 3 (~2700 lines: certified numerics, farW/S₃, six tail bricks, C0hat bridges, zeroMult_conj, farG + norm reduction, main bucket machine, two tail machines) + 5f-iii. Key banked gotcha for future sessions: `a * b / c` parses as `(a·b)/c` — write `c * (b / d)` with explicit parens when using `mul_left`-coefficient proofs, or isDefEq explodes.\n\nRemaining map: **ii′-3b** (contour moments σ_k = −g^{(k−1)}(0)/(k−1)! — the R-bound now exists to drive the moment estimates) → ii′-3c (crux Sf = Res₁) → ii′-6 (L0 assembly; D-069 Finding 2's H(T) repair lives there) → ii′-7 (closure: `sfBoundProp`, the 3-perimeter-hypothesis final theorem, paper Appendix B)."}]