Session 012 — 2026-08-20 — Lean tier (ii) step 1: assembly modulo SfBoundProp

Directive

session-012-notes.txt (read at session start per the session-011 user directive): pick option (a) Lean tier (ii), but SPLIT it first — assembly-first with the finite-part bound as a named hypothesis, then triage. User confirmed option (a) at session start.

What happened

Step 1: assembly-first (COMPLETE, two commits)

Read LiSkeleton.lean (tier-(i) state) + D-037/D-056/D-057 for the exact assembly chain: λ_n = S_∞ − S_f + 1 (BL Thm 2) ⟹ λ_n ≥ S(n) − B(n) + 1 = margin(n), convexity + base point ⟹ margin > 0 on the range, finite verification below.

Key design decisions (all in D-062):

Sf := SInfty n + 1 − (liCoeff n).re — BL Thm 2 holds by construction; the D-036 contour argument proves identity + bound in one stroke, so no separate BL formalization is needed downstream.
FAlt majorant swap — discovered during design: the true Trudgian F + S_b has ψ > 0 on [5.47, ~16] (negative-weight −(log 2πe/2π)T term against the negative-ψ T-block), which would FALSIFY the marginTilde_convex hypothesis hψ for the explicit majorant. Dropped the negative-weight term: FAlt ≥ F + S_b pointwise, all four blocks provably ψ < 0 (D-057 rows #1/#3/#4), margin cost ≈ 0.9√n = 256 at n = 8×10⁴ vs margin 15 764 — negligible. (Caught by hand-computing ψF+S_b = −0.0006 — barely negative — before attempting the Lean instantiation.)
Two-point base (secant) instead of the derivative base point: pos_of_convex_of_two_points (ConvexOn.slope_mono_adjacent) — the remaining numeric obligations are two PLAIN evaluations of the explicit margin function, no deriv machinery. Caveat found: convex + two points does NOT give positivity between the points (convex can dip), so the regime split moved to n = 10⁵ (second point), with finite verification covering below.
Refactor: margin regularity ContDiff ℝ 2 F → ContDiffOn (Ioi 1) (FAlt log-singularities at 0, 1); chain_rule_sqrt_shift_on generalized to c ≤ 1; unused hmaj dropped from marginTilde_convex.

Result: lambda_pos_finite_height PROVED from 5 named hypotheses (hRH perimeter, hfinite perimeter, hbase, hbase2, hSf : SfBoundProp). PrintAxioms = [propext, Classical.choice, Quot.sound] — NO sorryAx. LiSkeleton.lean is now sorry-free; sorryAx remains only on the 4 valley statements + R003 skeleton (tiers iii/iv) by design.

Commits: 741d2c5 (step 1), f39499a (two-point variant).

Step 2 design: triage + perimeter decision (COMPLETE, D-062)

Decomposed SfBoundProp into layers L0–L7 with tractability verdicts:

Mathlib-tractable: kernel bounds, R-bound (mod N(T)), zero-avoidance.
Main lift: L0 rectangle-contour/residue machinery (thin in Mathlib).
DECISION (declared, per the notes' instruction to decide deliberately): Trudgian 2014 explicit N(T)/S(T) → INSIDE the trusted perimeter, same footing as Platt–Trudgian. Rationale: published refereed infrastructure; formalizing it is Backlund–Rosser-class (larger than everything done so far) with zero insight into R-004's actual content. Paper appendix updated to declare exactly this.
M₀ → computational perimeter after E-023b (acb certificate).

Step 2 prep: base-point discharge plan VALIDATED (D-062 §5)

Full rational-interval bound chain pre-verified at dps 40: log 80000 ∈ [11.263, 11.3], log 100000 ≥ 11.5, log T ≤ 5.7/5.8, log log ≤ 1.75/1.77, log 285 ≥ 5.6, log π ∈ [1.14, 1.1448] (upper link 0.007% — tightest), e⁴ ∈ [54.5978, 54.6015], IIMaj ≤ 4.56(s+1)·2. Certified outcome: margin(8×10⁴) ∈ [9 960·slack, 63 989], margin(10⁵) ≥ 86 220 — hbase and hbase2 both comfortably provable (~400–600 lines of interval grind along block_range_bounds/iimaj_bracket_bound patterns).

Paper

draft.tex Formal verification appendix: new paragraph (tier (ii) assembly form, five named hypotheses, Trudgian perimeter declaration, FAlt note) + remaining-tiers paragraph updated (ii → ii′ inside SfBoundProp). MiKTeX compile clean, 12 pp. Audit note (D-060 §5 rule): the edited lines are exactly the new/updated paragraphs; claims match the Lean state verbatim (hypothesis list, axiom profile).

Files

research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean (+~470 lines: FAlt/Bn/Sf/SfBoundProp defs, marginTilde_eq_sub, ψ-blocks #1/#3/#4, contDiffOn_FAlt, FAlt_psi_neg, pos_of_convex_of_base/two_points, lambda_pos_finite_height; refactor of margin regularity)
research/lean/NguyenRH1/PrintAxioms.lean (new declarations added)
research/derivations/D-062-SfBound-triage.md (NEW)
D-061 §5 update (session-012 status)
research/paper/draft.tex (Formal verification appendix)
research/journal/session-012.md (this file)

State at stop

Tier (ii) step 1 COMPLETE and committed. Next: tier (ii) step 2 — discharge hbase/hbase2 per the D-062 §5 plan (validated), then the long pole: SfBoundProp layers L0–L3 (contour formalization), with L4 perimeter decided. Optional hygiene: E-023b (M₀ acb certificate).

Continuation (same day): mathematician's review notes + tier (ii) STEP 2 COMPLETE

Read session-012-end-notes.txt (mathematician's comment; user directive: use good advice). Directives extracted:

Discharge hbase/hbase2 next (cheap, pre-verified) — DONE (below).
Reconcile the margin-number trail (16 020 → 15 764 → certified bound) in the main text with a footnote — DONE (draft.tex Step 4 footnote + numerics bullet + Step 5 overlap factor 5 at the 10⁵ split).
Hold the paper's formal-status paragraph until the discharge lands — it landed; paragraph finalized at THREE hypotheses.
Tier ii′ (rectangle-contour interior of SfBoundProp) = POST- PUBLICATION work; don't let it delay Paper A. Part-2 objections (Theorem 3's tempered-FT bookkeeping + o(eᵃ) in its statement, L3/L4, authorship policy) standing, unchanged — no action this session.

Tier (ii) step 2: base points DISCHARGED (commit fc2e55e)

New file NguyenRH1/LiBasePoints.lean (~560 lines, clean compile):

Machinery: exp_le_inv_sub_sixteen (exp x ≤ (1−x/16)⁻¹⁶ from Real.add_one_le_exp), exp_one_pow_le/ge (d9 rational powers), exp_eleven/five/four (Real.exp_nat_mul), certified log bounds (log 80000 ∈ [11.263, 11.3], log 100000 ≥ 11.5, log π ∈ [1.14, 1.15]), sqrt bounds (sqrt_le_left/le_sqrt).
sInftyLower_eq' (γ cancels at point level, ring) + three evaluated bounds; Bn evaluations (three: two-sided at 8×10⁴, upper at 10⁵) with full mul_le_mul chains through FAlt/Ĉ₀/Ĥ/bracket/e⁴/IIMaj.
marginTilde_FAlt_80000_pos (≥ 8001; true 15 764), marginTilde_FAlt_80000_lt_100000 (65 001 < 85 501), lambda_pos_finite_height_verified: R-004 modulo SfBoundProp + perimeter ONLY. PrintAxioms: 3 standard axioms, no sorryAx.
Lean caught a real 3×10⁻⁶ rounding slip (110.34987 → 110.3498) — methodology working as intended.
LiSkeleton gained public IIMaj_le_two_mul / IIMaj_nonneg (psiTilde is private there; the base-point file consumes the public wrappers).

Paper (reconciled, compile clean 12 pp)

§3.1 Step 4: main-text number now 15 764 (the Lean-consumed FAlt majorant value) + footnote with the full trail (16 020 E-028 → 15 764 FAlt → ≥ 8 001 certified interval bound) + secant argument.
Step 5: overlap factor 5 at the 10⁵ split (6.25× at N₀ = 8×10⁴ retained).
Numerics bullet: 16 020 annotated with the 15 764 cross-reference.
Formal verification appendix: headline now THREE named hypotheses (lambda_pos_finite_height_verified); the margin evaluations declared discharged in LiBasePoints.lean.

Docs

D-062 §5 EXECUTED note (executed targets vs plan; the rounding swap log π ≤ 1.15 for 1.1448; 1/(2π) ≤ 1/6 for 0.1592; the 110.3498 slip). STATE.md + NGUYEN.md + db updated; session-012-end-notes.txt archived.

State at stop (final)

Tier (ii) steps 1+2 COMPLETE. R-004 is machine-verified modulo one named analytic hypothesis (SfBoundProp) + the declared computational perimeter — the mathematician's "headline claim" moment reached. Paper A's formal-verification story is complete pending publication split. Remaining: tier ii′ (SfBoundProp layers L0–L3 contour formalization — post-publication per the review), tiers iii/iv skeletons, optional E-023b. Paper-B (★) workstream stays separate.