← Session 18 — Lean tier (ii): finite-height proof + certified base points
thinking (45 chars)
Session 012 complete. Summarize for the user.
Session 012 complete — option (a) executed per the notes' split. Summary:
## Tier (ii) step 1: DONE — `lambda_pos_finite_height` proved modulo `SfBoundProp`
The finite-height Li theorem is now machine-proved in Lean from exactly five named hypotheses:
| Hypothesis | Class |
|---|---|
| `SfBoundProp`: ∀ n ∈ [10⁵, N₁], \|S_f n\| ≤ B(n) | ⭐ the single named analytic obligation |
| `RHUpTo (3×10¹²)` | computational perimeter (Platt–Trudgian) |
| `LiVerifiedUpTo (5×10⁵)` | computational perimeter |
| `hbase`, `hbase2` | two elementary margin evaluations |
**Axiom audit: `[propext, Classical.choice, Quot.sound]` — no `sorryAx`.** LiSkeleton.lean is now sorry-free.
Three design catches worth knowing:
1. **The true Trudgian majorant fails the convexity hypothesis** — ψ[F+S_b] crosses *positive* on [5.47, ~16] (caught by hand-computation before instantiation; it would have falsified `hψ`). Fixed by the FAlt swap: drop the negative-weight term, cost ≈ 0.9√n = 256 against margin 15 764.
2. **Derivative base point eliminated** in favor of a secant two-point argument — both remaining numeric obligations are plain function evaluations (cheapest possible discharge).
3. Convex + two points doesn't give positivity *between* the points (convex functions can dip) — regime split moved to n = 10⁵.
## Triage + perimeter decision (D-062, the notes' step 2)
Inside `SfBoundProp`: kernel bounds / R-bound / zero-avoidance = Mathlib-tractable; the rectangle-contour residue machinery = the main formalization lift (thin in Mathlib); **Trudgian 2014 N(T)/S(T) → declared trusted perimeter** (same footing as Platt–Trudgian — published infrastructure; formalizing it is Backlund–Rosser-class with zero insight gained). Paper appendix updated to declare exactly this (compiles clean, 12 pp).
## Deferred (clean sub-stage boundary)
Step 2 — discharging `hbase`/`hbase2` by rational interval bounds: the full plan is pre-verified at dps 40 in D-062 §5 (certified margin(8×10⁴) > 9 960, margin(10⁵) − margin(8×10⁴) > 2.2×10⁴; tightest link log π ≤ 1.1448 at 0.007%). Est. ~400–600 lines of interval grind.
**Commits:** `741d2c5`, `f39499a`, `d4c6ba0`. Session protocol run: journal-012, STATE.md (NEXT ACTION set), D-061/NGUYEN.md updated (including the missing session-011 log entry), research.db registered.
raw content_json (database row)
[{"type":"thinking","thinking":"Session 012 complete. Summarize for the user.","signature":""},{"type":"text","text":"Session 012 complete — option (a) executed per the notes' split. Summary:\n\n## Tier (ii) step 1: DONE — `lambda_pos_finite_height` proved modulo `SfBoundProp`\n\nThe finite-height Li theorem is now machine-proved in Lean from exactly five named hypotheses:\n\n| Hypothesis | Class |\n|---|---|\n| `SfBoundProp`: ∀ n ∈ [10⁵, N₁], \\|S_f n\\| ≤ B(n) | ⭐ the single named analytic obligation |\n| `RHUpTo (3×10¹²)` | computational perimeter (Platt–Trudgian) |\n| `LiVerifiedUpTo (5×10⁵)` | computational perimeter |\n| `hbase`, `hbase2` | two elementary margin evaluations |\n\n**Axiom audit: `[propext, Classical.choice, Quot.sound]` — no `sorryAx`.** LiSkeleton.lean is now sorry-free.\n\nThree design catches worth knowing:\n1. **The true Trudgian majorant fails the convexity hypothesis** — ψ[F+S_b] crosses *positive* on [5.47, ~16] (caught by hand-computation before instantiation; it would have falsified `hψ`). Fixed by the FAlt swap: drop the negative-weight term, cost ≈ 0.9√n = 256 against margin 15 764.\n2. **Derivative base point eliminated** in favor of a secant two-point argument — both remaining numeric obligations are plain function evaluations (cheapest possible discharge).\n3. Convex + two points doesn't give positivity *between* the points (convex functions can dip) — regime split moved to n = 10⁵.\n\n## Triage + perimeter decision (D-062, the notes' step 2)\n\nInside `SfBoundProp`: kernel bounds / R-bound / zero-avoidance = Mathlib-tractable; the rectangle-contour residue machinery = the main formalization lift (thin in Mathlib); **Trudgian 2014 N(T)/S(T) → declared trusted perimeter** (same footing as Platt–Trudgian — published infrastructure; formalizing it is Backlund–Rosser-class with zero insight gained). Paper appendix updated to declare exactly this (compiles clean, 12 pp).\n\n## Deferred (clean sub-stage boundary)\n\nStep 2 — discharging `hbase`/`hbase2` by rational interval bounds: the full plan is pre-verified at dps 40 in D-062 §5 (certified margin(8×10⁴) > 9 960, margin(10⁵) − margin(8×10⁴) > 2.2×10⁴; tightest link log π ≤ 1.1448 at 0.007%). Est. ~400–600 lines of interval grind.\n\n**Commits:** `741d2c5`, `f39499a`, `d4c6ba0`. Session protocol run: journal-012, STATE.md (NEXT ACTION set), D-061/NGUYEN.md updated (including the missing session-011 log entry), research.db registered."}]