This record archives the research package associated with the manuscript “A Formalization-Oriented Finite-Ledger Framework for Spectral Dispersion in Chen-Type Additive Prime Problems”. The package contains three files: Main manuscript.A research manuscript developing a formalization-oriented finite-ledger framework for spectral dispersion in Chen-type additive prime problems. The manuscript studies the signed Type II bilinear structures arising in Goldbach and fixed-even-difference prime-pair orientations, isolates the premature-positivity form of the parity barrier, and constructs a finite product-modulus route through Bezout reciprocity, Fourier--Kloosterman completion, Heath--Brown terminal opening, effective-conductor reduction, aggregated spectral coefficients, primitive collision ledgers, and routed analytic closure. Verification supplement.A supplementary guide providing a compressed proof map, the critical theorem chain, the finite signed-dispersion ledger, the analytic dependency ledger, the Lean repository guide, the imported-boundary ledger, and the final logical chain. The supplement is intended to make the proof architecture, dependency structure, theorem-boundary interfaces, and verification route easier to inspect alongside the main manuscript. Lean proof-architecture archive.A Lean 4 repository archive recording the finite and elementary proof architecture associated with the manuscript. The archive covers finite reindexings, Bezout and Fourier identities, Kloosterman-sum normalizations, folded Parseval ledgers, rational threshold arithmetic, local-factor positivity, dependency closure, and the logical deductions from the final affine lower bound to the stated additive-prime consequences. The archive should be read as a proof-architecture and interface formalization aid. It records finite identities, deterministic implications, theorem-boundary interfaces, and verification scaffolding associated with the manuscript. It does not claim to formalize from first principles the full analytic number theory inputs such as the Kuznetsov trace formula, the spectral large sieve, Kim--Sarnak exceptional-spectrum bounds, Bettin--Chandee type trilinear estimates, Barban--Davenport--Halberstam/Bombieri--Vinogradov inputs, Topacogullari’s additive-divisor theorem, or the classical linear-sieve density formula. Together, these materials are intended to support reproducibility, mathematical inspection, referee review, and long-term citation of the manuscript, the verification supplement, and the accompanying Lean-style proof-architecture materials.
Juan Moreno Borrallo (Thu,) studied this question.