Formal proof: closed-form stf(b) via Lean 4 + Mathlib

[djdarcy]

Summary

Track the formal proof work toward a closed-form expression for stf(b) (Sum of Triangular Factors) in Lean 4 + Mathlib. This decomposes the journey from algebraic foundations through to a single-formula closed form.

Background

stf(b) computes the sum of digit-row values in a triangular arrangement for base b. For b = 10: stf(10) = 9 + 78 + 456 + 123 = 666. The goal is to prove a general closed-form expression for stf(b) for any triangular base.

The algebraic form rowValue'(b, z) and the telescoping identity reduce stf to three simpler quantities (boundary term, correction sum, boundary sum), each of which needs its own closed form.

Completed

• Phase 3B: rowValue_eq_rowValue' — bridge algorithmic to algebraic rowValue (v0.7.16)
• Phase 3C: Decomposition, stf bridge, recursive relation (v0.7.20)
  • rowValue'_split — decompose into constant-coeff geometric + linearly-weighted power sum
  • stf' / stf_eq_stf' — algebraic stf definition and bridge
  • rowValue'_succ_add — recursive relation (additive form)
  • geom_sum_mul_add_one, power_sum_reverse — geometric sum helpers
• Step 4: power_sum_closed — Mathlib geometric series closed form (ed56eac)
• Phase 3D: Telescoping identity (uncommitted)
  • rowValue'_zero, rowValue'_one — boundary lemmas
  • rowValue'_sum_index_shift — index shift for rv' sums
  • sum_rowValue'_succ_eq — summed recursive relation
  • stf'_telescope — stf'(b) + C + b·rv'(b,r) = b·stf'(b) + B

Remaining

• Closed form for B (boundary sum): Σ (b - tri(z) + z) = r·b - (r-1)·r·(r-2)/6
  • Python-verified. Uses standard sum identities. Difficulty: Low
• Arithmetic-geometric sum: Σ i·b^i identity — the mathematical bottleneck
  • Standard identity: (b-1)² · Σ i·b^i = polynomial in b, n
  • Provable by induction but involves (b-1)² divisibility
  • Difficulty: Medium-High
• Closed form for C (correction sum): Σ (z+1)·G(z+1) via arithmetic-geometric sum
  • Depends on the Σ i·b^i identity above
  • Difficulty: Medium (once arithmetic-geometric is done)
• Closed form for rv'(b,r): weighted power sum Σ i·b^(r-1-i) for last row
  • For triangular bases b = tri(r), digits are [0, 1, ..., r-1]
  • Also depends on Σ i·b^i identity
  • Difficulty: Medium
• Per-row closed form (Level A): rowValue'(b,z) = N(b,z) / (2·(b-1)²)
  • N is a known polynomial from sympy analysis
  • Requires divisibility proof 2·(b-1)² | N(b,z) in Nat (or cast to ℤ)
  • Difficulty: High
• Full stf closed form (Level B): stf(b) = F(b) as single expression
  • Combine all of the above
  • Difficulty: High

Key Insight

The telescoping theorem reduces stf(b) to three quantities B, C, rv'(b,r). All three ultimately depend on the arithmetic-geometric sum Σ i·b^i. This is the single bottleneck — once proven, the remaining closed forms follow.

Approaches Under Consideration

1. Stay in Nat: Prove multiplicative forms avoiding division (e.g., (b-1)·stf'(b) = ...)
2. Cast to ℤ via zify: Use push_cast + ring + induction for polynomial identities
3. Semi-closed form: Accept telescoping as a structural result without full simplification

Analysis

See 2026-02-08__10-00-17__dev-workflow_phase3d-closed-form-stf-pathway.md for detailed pathway analysis.
See 2026-02-08__12-13-07__full-postmortem_phase3d-telescoping-stf-and-remaining-roadmap.md for Phase 3D postmortem.