D-057 — Repair 4.5b: margin convexity, proved (symbolic building-block table)
Date: 2026-08-19 | Session: 009 | Task: 4.5b Status: complete. Support computation E-029 (ALL CHECKS PASS). Repairs D-054 F4 (D-037's "every component concave" assertion).
1. Setup
margin(n) = S(n) − B(n) + 1 with S(n) = ½n log n + C₁ᴸn − 4, S″(n) = 1/(2n), and B(n) the D-036/D-056 assembly (T = √n + 1): B = 2N(T) + 4T[(2/3)C₀(T) + A log(T+2) + B₀] + 40M₀ + 2(e⁴+1)[7H(T) + 3.3] + I_I + 1, C₀ honest (D-036 §0 erratum), H = 3C₀² + A log(T+2) + B₀, A = 10.5, B₀ = 48 (D-056).
Step 1 (closed-form majorant). Replace C₀ by its proved closed-form bound (D-056 §2): C₀(t) ≤ Ĉ₀(t) := 0.433 log(t+2) + 0.886 log log(t+2) + 2.9. Write B̃(n) for the resulting bound: B̃(n) ≥ B(n), so margiñ(n) := S(n) − B̃(n) + 1 ≤ margin(n). It suffices to prove margiñ convex on n ≥ 20 (then margiñ(N₀) > 0 ∧ margiñ′(N₀) > 0 ⟹ margin(n) ≥ margiñ(n) > 0 for all n ∈ [N₀, N₁]).
Step 2 (chain rule). With T(n) = √n + 1: d²/dn² φ(T(n)) = [φ″(T) − φ′(T)/(T−1)] / (4n) =: ψφ/(4n). So each component of B̃ is concave in n iff its ψ(T) < 0 (T ≥ T₀ := √20 + 1 = 5.4721…).
2. The building-block table
B̃ is a positive combination of the blocks below (constants and the I_I term handled separately). For each: the exact ψ and the sign argument for T ≥ T₀. (L1 := log(T+2) ≥ 2.011, L2 := log log(T+2) ≥ 0.6983 on the range; both increasing.)
| # | φ(T) | ψ(T) = φ″ − φ′/(T−1) | sign |
|---|---|---|---|
| 1 | T log T | 1/T − (log T + 1)/(T−1) | < 0 ⟺ (T−1) < T(log T + 1) ⟺ −1 < T log T ✓ |
| 2 | T | −1/(T−1) | < 0 ✓ |
| 3 | log T | −1/T² − 1/(T(T−1)) | < 0 ✓ |
| 4 | log log T | −(log T + 1)/(T log T)² − 1/(T log T (T−1)) | < 0 ✓ |
| 5 | T·L1 | (T+4)/(T+2)² − L1/(T−1) − T/((T+2)(T−1)) | < 0: L1 ≥ 2 gives ψ ≤ [(T+4)(T−1) − (3T+4)(T+2)]/((T+2)²(T−1)) and (T+4)(T−1) − (3T+4)(T+2) = −2T² − 7T − 12 < 0 ✓ |
| 6 | T·L2 | [T(L1−1)+4L1]/((T+2)L1)² − L2/(T−1) − T/((T+2)L1(T−1)) | < 0: suffices 2 ≤ L1·L2·(T+2) (chain: LHS < L1(T+2)², RHS > T(T+2)L1 + L2(T+2)²L1²; divide L1(T+2): condition (T+2) ≤ T + L2(T+2)L1); at T₀: 2.011·0.6983·7.4721 = 10.49 ≥ 2, increasing ✓ |
| 7 | L1² | 2(1−L1)/(T+2)² − 2L1/((T+2)(T−1)) | < 0 (L1 > 1) ✓ |
| 8 | L1·L2 | [1/L1 − L2 − 1]/(T+2)² − (L2+1)/((T+2)(T−1)) | < 0 (1/L1 ≤ 0.498 < 1 + L2) ✓ |
| 9 | L2² | 2[1 − L2(L1+1)]/((T+2)L1)² − 2L2/((T+2)L1(T−1)) | < 0 (L2(L1+1) ≥ 2.1 > 1) ✓ |
| 10 | L1 | −1/(T+2)² − 1/((T+2)(T−1)) | < 0 ✓ |
| 11 | L2 | −(L1+1)/((T+2)L1)² − 1/((T+2)L1(T−1)) | < 0 ✓ |
(Component expansion: 2F(T) → #1, #2 (mod constants); 2S_b(T) → #3,
4; 4T·(2/3)Ĉ₀ → #5, #6, #2; 4T·A·L1 → #5; 4T·B₀ → #2; 6(e⁴+1)Ĉ₀²
→ #7, #8, #9, #10, #11; 14(e⁴+1)A·L1 → #10. All weights positive.)
3. The I_I term
B̃₄(n) = 2(√n+1)·(e^{√n/2}+1)·0.57·2^{−(2√n−2)} — not concave, so bounded directly: |B̃₄″(n)| ≤ B̃₄(n)·[c²/(4n) + c/(2n^{3/2})·…] with c = 2 log 2 − ½ = 0.8863; at n = 20: B̃₄ = 0.525, |B̃₄″| ≤ 0.011 < 1/(2·20) = 0.025, and |B̃₄″| decays ~e^{−0.886√n}·poly while 1/(2n) decays polynomially, so margiñ″(n) ≥ 1/(2n) − |B̃₄″(n)| > 0 for all n ≥ 20. E-029 verifies max_{n ∈ [20, 10⁴]} 2n·|B̃₄″| < 1 on a dense grid (actual max 0.189 at n = 20) and the asymptotic domination beyond.
4. Assembly and conclusion
margiñ″(n) = 1/(2n) − Σᵢ wᵢψᵢ(T(n))/(4n) − B̃₄″(n) ≥ 1/(2n) − |B̃₄″(n)| > 0 for all n ≥ 20, since every wᵢ > 0 and ψᵢ < 0 (table). E-029 (ALL CHECKS PASS): sympy-derived ψᵢ match the hand forms (rel dev ≤ 1e-15 / abs ≤ 1e-12), all ψᵢ < 0 on [T₀, 3.1×10¹²]; margiñ convex on [20, 4×10⁵] (exact 2nd differences > 0); margiñ crossover N₀̃ = 75 621; **at the adopted N₀ = 80 000: margiñ(8×10⁴) = 16 020 > 0 and margiñ′(8×10⁴) = 3.7
0**; max_{[20,10⁴]} 2n|B̃₄″| = 0.189 < 1 (and the e^{−0.886√n} decay vs 1/(2n) covers n > 10⁴). Hence margin(n) ≥ margiñ(n) > 0 for ALL n ∈ [N₀, N₁]. ∎
P6 is now analytic (D-037 inventory): convexity PROVED (this file); contiguity N₀ < 5×10⁵ vs Misguich–Voros coverage unchanged.
5. Caveats
- The proof is for the margiñ majorant; the substitution Ĉ₀ ≥ C₀ is the D-056 closed-form bound (proved there).
- E-029 provides the symbolic-expression check (sympy table matches the hand-derived ψᵢ to machine precision) and the grid verifications; the sign arguments of §2–3 are hand-provable as written.
6. Lean formalization note (session 011): 11 conditions → 8 blocks
The Lean proof of marginTilde_convex (NguyenRH1, session 011) diverges
from this file's presentation by design:
- This file's table has 11 rows. Rows #1–#4 (T log T, T, log T, log log T) exist to expand the Trudgian N(T)/S(T) majorants F and S_b into elementary pieces. The Lean theorem is parameterized over F (the majorant and its ψ-condition hψ are hypotheses, discharged elsewhere for the explicit Trudgian majorant), so those rows never appear: the 2F(T) term is handled atomically via hψ.
- The remaining rows collapse to 8 block types: id (#2), T·L1 (#5), T·L2 (#6), L1² (#7), L1·L2 (#8), L2² (#9), L1 (#10), L2 (#11) — exactly the blocks generated by the closed-form Ĉ₀/Ĥ terms.
- B̃₄ (the I_I term) is not concave, so it is excluded from the ψ-machinery and bounded directly: IIMaj is rewritten as ψ̃(s) = 4.56(s+1)(e^{−as}+e^{−bs}) and the analytic factor-monotone bound ψ̃″(s) − ψ̃′(s)/s ≤ 1.316 < 2 (iimaj_bracket_bound) replaces this file's §3 grid-plus-decay argument (E-029's measured max 2n·|B̃₄″| = 0.189 — the measured-to-traced conversion also highlighted in draft.tex's Formal verification appendix).