A Type II Square-Discriminant Framework for Sums of Three Cubes

This repository contains the Lean 4 formalisation support and documentation for version 4 of the paper A Type II Square-Discriminant Framework for Sums of Three Cubes. The project studies the equation x³ + y³ + z³ = k, where k is an integer with k ≠ ±4 mod 9. The paper does not claim an unconditional proof of Heath-Brown’s three-cubes conjecture. Its purpose is to isolate and formalise a Type II square-discriminant mechanism, prove the algebraic and medium-determinant components of that mechanism, and reduce the remaining obstruction to an explicit analytic endpoint. The starting point is the substitution d = x + y,u = x − y,z = −Z, which transforms the equation into d³ + 3du² − 4Z³ = 4k. For d ≠ 0 this yields a divisor-square criterion together with a quadratic discriminant square condition. The Type II framework studies moduli of the form d = pb, where p ≍ A is prime and b ≍ B = A^(1+η). The medium determinant range is controlled using: • determinant identities,• local root-lattice decomposition,• a no-short-vector argument,• lattice-strip geometry,• square-sieve estimates,• large-gcd decomposition,• vertical-range extraction. The far determinant range is progressively reduced through: • first-level same-p compatibility,• shifted-square structure,• overlap reductions,• bounded-quotient identities,• fixed-determinant reductions,• an off-diagonal sextic resultant collapse. The final obstruction is isolated as a sparse divisor trace / reciprocal near-spacing endpoint associated to R(h) = h⁶ + 27k². The endpoint takes the form of sparse divisor-Kloosterman sums in the no-long-variable regime D > Y. The repository includes a detailed endpoint audit explaining why several standard closure strategies fail in this range, including: • Bombieri–Vinogradov transfer,• direct completion,• bilinear/trilinear averaging,• reciprocity-based reductions. The Lean development formalises the exact algebraic and combinatorial infrastructure of the framework, including: • divisor-square reduction,• mod 3 lift,• determinant divisibility identities,• quadratic-discriminant algebra,• large-gcd reductions,• vertical extraction,• cubic norm identities,• shifted-square identities,• bounded-quotient algebra,• off-diagonal sextic collapse,• endpoint reduction bookkeeping,• sparse reciprocal endpoint structure. The analytic estimates themselves are not formalised in Lean and the final sparse endpoint estimate remains open. Repository contents include: • Lean 4 source files,• LaTeX source of the paper,• compiled PDF documentation,• Lean-to-paper correspondence notes,• repository overview documentation. This repository represents the final v4 reduction-and-endpoint-isolation form of the project.