Ternary Goldbach in Lean 4

A Lean 4 formalization of the ternary (weak) Goldbach theorem: every odd integer at least seven is a sum of three primes.

theorem Math.Problems.TernaryGoldbach.ternary_goldbach :
    ∀ n : ℕ, Odd n → 7 ≤ n → IsThreePrimeSum n

Proof map: the reviewed interactive Ternary Goldbach Blueprint and its dependency graph are prepared for the public-release site. The same compiled files are checked in under blueprint/web/; Pages remains disabled during private review.

Historical context

The modern Goldbach problems trace back to the 1742 correspondence between Christian Goldbach and Leonhard Euler. Goldbach's literal wording used an eighteenth-century convention under which 1 could be counted as prime, so it was not quite the statement written above. In modern language, the ternary or weak Goldbach theorem says that every odd integer greater than 5 is a sum of three primes. It is called weak because the still-open binary Goldbach conjecture would imply it.

Hardy and Littlewood's 1923 paper (archival record and scan) proved the ternary statement for sufficiently large odd integers, conditionally on the generalized Riemann hypothesis. Vinogradov removed that assumption in 1937, again for sufficiently large integers, but without a practical bound that settled every case; the original 1937 publication is listed in the public bibliography. In 2013, Harald Andrés Helfgott completed the proof: his analytic argument covers odd integers from 10^27 onward, while a finite verification with David J. Platt reaches beyond 8.875·10^30. The overlapping ranges give the theorem for every odd integer greater than 5.

Current formalization status

As of 2026-08-29, the public Lean theorem is complete and its dependency cone is sorry-free. A fresh source build and #print axioms found no sorryAx and no native_decide atom. The fast capstone has 105 unique atoms: Lean's 3 ordinary foundations, 93 named external/source atoms, and 9 explicit HeavyCertificateStub.* placeholders for repository-owned kernel proofs that fast mode skips. The full capstone builds those nine proofs and has 96 atoms: the same 3 foundations and 93 named atoms, with no stubs.

The registry covers 104 LeanCompCert-shaped run declarations (90 in the capstone) across 79 campaigns. The readiness audit finds all 104 runnable, already run, and receipt-bound; 86 have fully certified receipts, 103 have a proved mathematical denotation, 10 enter Lean as receipt-derived theorems, and 94 still enter through standalone run axioms. Exactly one declaration, the Ramaré 100-million runtime arithmetic precursor, does not yet execute its live paper predicate end to end. The historical emission-time constant carrier is retired and absent from the live closure. The machine-readable coverage map is in compcert_campaigns.json, and the complete measurement index is capstone_compcert_runs.md. The remaining source-level replacement audit has ten bounded literature/external-source inputs. All 93 exact capstone atoms have one self-contained comparison card in problems/ternary-goldbach/citations/. Those ten literature inputs are not yet all replaceable merely by paying for a Phala run. The strict replacement audit currently reports 0 receipt-ready and 10 proof-incomplete routes: several integer programs still need concrete schedule/readiness composition, while the zeta, Dirichlet-L, and Arb-boundary routes still need formal interval evaluators or complete transcripts. A route counts as receipt-ready only when a concrete Lean ReceiptReadyProgram (or sharded ReceiptReadyCampaign) fixes the exact proposition, proved program semantics, guarded drivers, emitted bytes, digests, coverage/seams, and future receipt specifications. The strict audit asks Lean to verify both that the package's indexed proposition is definitionally the cited declaration's exact type and that the package has no non-foundation axioms. See REMAINING_COMPCERT_COST.md and tools/audit_tg_citation_replaceability.py --require-receipt-ready.

There is now an exact generated target for completing that migration. PhalaEvidence.lean defines the 70 empirical fields in the fresh parameterized-capstone closure; TGPhalaEvidence pairs them with the 40 existing TGFiniteCertificates fields. The deliberately opt-in PhalaEvidenceBoundary.lean re-derives the capstone over this bundle. Fresh axiom prints of ternary_goldbach_of_evidence and ternary_goldbach_of_phala_evidence contain only propext, Classical.choice, and Quot.sound. This proves that populating the exact bundle through typed receipt routes is sufficient; it does not claim that all 110 fields are populated today. The generated exact-field ledger phala_evidence_routes.json currently verifies ten fields as ordinary foundation-only Lean theorems, 25 receipt-ready fields (10 with retained receipts attached), and reports 75 fields as proof-incomplete. Its independent denotation-only audit checks 83 exact foundation-only semantic packages without importing packed receipt artifacts. Those packages bring the union of Lean proofs, receipt-ready packages, and semantic packages to all 110 fields. Atom23 (the Ramaré--Zúñiga Lemma 6.2 dense sweep) now has a foundation-only semantic declaration from its typed physical receipt proposition to the exact source claim. This completes its denotation layer, not its physical evidence. The proved finite post-mark scanner campaign specializes to the actual dense configurations: one 998-cell scanner for the first head, and two scanner shards for the 143,999-cell second head split at index 72,000, with the last interval clamped to the live length. These are foundation-only conditional cover and causal assembly theorems, not completed executions. The mark-only producer and its accepted physical endpoint are also proved. The campaign has five literal gates: two mark-prefix producer/audit gates and three product-plane scanner gates. The formerly residual pointwise CompletedCellSemanticFacts obligations—RootTruncatedFactorization and cell.lsum < 2^29 for every completed cell; serialized-carry replay soundness and final physical composition are also proved. Atom23 is still proof_incomplete because its physical receipt is absent. The retained full dense receipt did not preserve the intermediate product plane and is not evidence for these stages. The typed receipt proposition contains 29 positive/audit CompCert executions across the corrected runtime, both physical heads, and both carry replays. None has been run on Phala for this route, no launcher proof is attached, and no cost is claimed. The future dense-carry payload is the exact u64-le-v1 layout zero-workspace || producer-physical-planes || serialized-carry-triples || scheduler-witness-triples; its manifest binds every component and rejects nonzero workspace bytes. This payload contract is not itself a launcher proof or a receipt-ready route. The ten attached receipts are four uFold bounds, gFold, g1215, both dyadic cE bounds, the two-million-prime deficit product, and the Section 4.1.3 small-G2 certificate. The fifteen run-pending packages are the C17 sieve check, two fixed-psi checks, the Liouville ell sweep, the RS62 Mertens-first check, eight CDEM/Mertens shards, the weighted-moment check, and the weak-G2-head check. Their static packages use only Lean's foundational trio; their exact field proofs add only MathExtras.Attestation.execution_of_certifiedReceipt. Run scripts/check_tg_phala_evidence_boundary.py for the cheap drift check and add --full for the memory-capped proof-cone audit. Regenerate and verify the route ledger with python3 tools/generate_tg_phala_route_ledger.py and python3 tools/audit_tg_phala_route_ledger.py. During denotation-first work, use python3 tools/audit_tg_phala_route_ledger.py --denotations-only; this avoids rebuilding or importing receipt payload modules. --require-no-denotation-gaps is the strict completion gate: it is now green because every computation field has a foundation-only semantic, Lean, or ready route, independently of whether any Phala receipt has been purchased. Reusable conditional AProgramClaimCampaign packages underlie the completed semantic routes for CH25 psi, Hurst, and CDEM. Proposition 12.2.4 now also has an exact indexed signature-to-source campaign plus Prop1224CanonicalDeploymentMetadata.lean, which supplies compact, receipt-free finite generator coordinates. Production metadata, artifact binding, and the actual independently sharded Phala runs remain to be supplied. The predicate audit identifies the live Ramaré precursor as the single program that does not implement its claimed mathematical predicate. See the strict audit commands in STATUS.md.

The established external atoms also have conditional, source-shaped import theorems from the separate gpu_prover/SparkInterval package. A single review file, GPUProverRegisteredBridgeAudit.lean, prints the trust closure of every replacement; scripts/check_tg_registered_bridges.py verifies the exact registered source propositions and restricts those bridges to the foundational trio plus accepted_run_certificate_sound. This is a route for deliberately admitting reviewed receipts, not a silent replacement of the named source atoms in the public capstone.

Historical native manifests, replay facades, and classification files remain useful migration records, but they do not describe the current live trust boundary. Do not infer current trust from them or from a grep for axiom; use a fresh capstone #print axioms and the two exact coverage audits.

Finite claims that were previously evaluated with native_decide are now ordinary-kernel certificates or explicit LeanCompCert routes. The latter do not pretend that an OS exit is a kernel proof: the run remains one named admission axiom, while the program refinement and the implication from its denotation to the exact mathematical proposition are proved in Lean. This makes the computational trust boundary explicit and independently benchmarkable.

There are no unbounded analytic residual axioms in the public theorem's dependency cone. The named public external atoms cover bounded verified-zero ranges, finite tables and computations, and the finite ternary-Goldbach verification. The extension library retains one dormant, proof-corrected Helfgott Theorem 3.1 opposite-sign source atom; it is documented in the Blueprint but does not enter ternary_goldbach. Some external computations do not have enough raw data for a local replay; their cards say so explicitly.

Three CH25 computations now have complete, locally replayable external artifacts in ext/ch25_certificates/: the low-height and boundary inputs to Lemma A.7 and the Proposition 7.7 zeta-zero head through 20,000. The boundary input and the shared Proposition 7.7 zero enumeration remain named trust atoms because their FLINT/Arb semantics run outside Lean's ordinary kernel. The low-height claim is a Lean theorem derived from that same enumeration, so it is no longer a separate atom. Proposition 7.7 is checked two ways—an independent FLINT count/isolation/fold and an exact fold of the official LMFDB/Platt files. LMFDB's public archive stops at height 30,610,046,000, so it does not replace the distinct Platt--Trudgian RH verification through about 3·10^12.

Thus “complete” means complete under this finite and computational trust boundary, not a claim that every external computation has been reconstructed inside Lean. The vendored dependency tree also contains unrelated unfinished upstream declarations; build warnings from those declarations do not enter ternary_goldbach. The theorem's fresh axiom print is the authority.

Phala TDX receipt status (2026-08-31)

The Phala machinery is operational, and the retained evidence has been re-audited rather than trusted from cached verifier logs. There are 135 receipts across 13 deployments. Every deployment's app identity, enclave public key, and quote-bound compose hash is now in the closed Lean review table, after the offline verifier passed its current evidence with no skipped checks. The readiness audit also requires the receipt result and the quote-bound run statement to refer to the same deployment and to the exact locally stamped binary.

This does not mean that every receipt has already replaced a Lean run axiom. At the run-declaration level, all 104 registered admissions are ready, have run, and have a receipt bound to their exact binary; 86 are full-scale certificates and 18 are only shard-scale evidence. In the public capstone the corresponding figures are 75 full certificates out of 90 run declarations, with 15 still requiring a full run. deficitProduct_compcert_run and uIv7Three_compcert_run have been converted from standalone per-run axioms to theorems through returns_of_certifiedReceipt, which is itself derived from the single typed execution_of_certifiedReceipt admission. The other receipts are strong, checked external evidence for their existing run axioms, but are not yet causal Lean premises.

The reusable artifact bottleneck is now closed. A ReceiptReadyProgram accepts a direct kernel proof of the emitted-C digest for small artifacts; the bridge also exposes structured emitter chunks and ChunkedEmissionCertificate for large ones, where consecutive UTF-8 windows are checked against one packed byte source and bounded SHA-256 states are recomputed by the kernel. Its GuardedMain premise pins the exact ABI-mangled, fail-closed driver: exit status zero is accepted only when the emitted function returns the ProgramClaim's accepting value. The retained 8,101-byte ufold_uiv7_cert_3 artifact exercises this path end to end. Remaining standalone run axioms need artifact-specific generated witnesses, but no new infrastructure and no new Phala run when a suitable full receipt already exists.

For the restricted rolled scalar and one-flat-uint64_t-array subset used by the production emitters, the pinned LeanCompCert revision also supplies an exact C-to-Clight gate. CompCert's clightgen imports the emitted C, and Coq proves equality of the complete Clight.function—signature, locals, temporaries, types, every expression and statement, loop, and return—to the function covered by the generic big-step semantics theorem. The bounded gate also checks that the imported translation unit has exactly the expected function, with no extra user-defined functions or global variables. It checks the actual first and second R2 artifacts without executing their long loops. This is an exact whole-function and restricted translation-unit result; cross-kernel artifact generation, the CompCert backend-to-assembly composition, linking, platform ABI, executable binding, and the attested physical run remain separate explicit boundaries.

Array programs use the same one-axiom route. The foundation-only MathExtras.Attestation.arrayReturnsClaim turns a legacy array Returns proposition into an AProgramClaim via CompCert's proved denotation theorem; ProgramClaimCampaign and ArrayRunClaimCampaign package exact sharded signature-to-theorem semantics independently of emitted C, and their toReceiptReady conversions add only the later byte/spec layer; tools/attest/generate_array_attested_module.py generates the exact emitted-C and signed-receipt wrapper without replaying the numerical loop in Lean.

python3 tools/attest/audit_phala_readiness.py --by-axiom
python3 tools/attest/test_audit_phala_readiness.py

Informal/formal Blueprint

The focused Ternary Goldbach Blueprint links a curated informal proof narrative to 65 formal nodes with LeanArchitect. It follows the conditional threshold split, Fourier extraction, major arcs, repaired minor arcs, prime-power tail, production providers, and final theorem. It also links historical native-certificate families and citation atoms to their migration inventories and cards. The live 59-atom inventory supersedes those counts. Its source_map.json additionally records every primary/background work in the public bibliography, the exact revision or edition inspected, claim pinpoints, and whether each link is exact, source-shaped, derived, weakened, adapted, a local reproduction, an erratum, methodological, or background-only. "Inspected" here means the cited theorem/equation and its surrounding hypotheses were checked; it does not claim a cover-to-cover reading of every work.

One of those nodes records a dormant external analytic source atom; it is not part of the public theorem's dependency cone. Each node displays an explicit badge: definition/contract, base trio, historical native evaluation, external finite computation, external analytic source, or a combination. This is important because LeanArchitect's generated leanok marker excludes sorryAx, but does not by itself mean that a proposition is proved or that a theorem uses only Lean's base trio. A fresh theorem #print axioms remains authoritative. The Blueprint also explains how Lean 4.32 turns a successful native evaluation into a generated axiom; that discussion now documents the retired route.

lake build TernaryGoldbachBlueprint
lake build TernaryGoldbachBlueprint:blueprint \
  TernaryGoldbachBlueprint:blueprintJson
python3 scripts/tg_blueprint.py --require-json --require-tex --verify-tiers

# Render the reviewed static site with LeanBlueprint 0.0.20.
python3 scripts/build_blueprint_site.py
python3 scripts/check_blueprint_site.py

The target is non-default, so it does not enter the production theorem or the ordinary Math MathExtras build. The checked-in site is rendered with pinned LeanBlueprint tooling and a pinned MathJax asset. Its Lean links use a bundled declaration-to-source resolver, so they remain useful without shipping a second, very large doc-gen tree. A guarded, least-privilege Pages workflow is present, but it is inert unless the repository is public, the branch is main, Pages is enabled, and the repository variable PUBLISH_PAGES is explicitly set to true.

Built on prior work

This project is a formalization built on an existing mathematical achievement, together with supporting Lean infrastructure; it is not an independent replacement for that achievement. The central mathematical credit belongs to Harald Andrés Helfgott: the specific explicit major-arc/minor-arc estimates, smoothing choices, large-sieve refinements, and finite handoff formalized here are built on his proof of ternary Goldbach. The final finite range also relies on the computation by Helfgott and David J. Platt. Many further analytic and computational sources are credited in REFERENCES.md, with the exact remaining external propositions documented by individual citation cards.

The Lean development is also built on:

• PrimeNumberTheoremAnd, whose citation title is Prime Number Theorem and More. It is a collaborative formalization organized by Alex Kontorovich and Terence Tao, with work by many additional contributors. This repository vendors a modified fork and preserves its upstream CITATION.cff, file-level notices, license, and VENDOR_PROVENANCE.md.
• Mathlib and the wider Lean community, which provide the foundational algebra, analysis, measure theory, number theory, tactics, and build ecosystem on which essentially all of this code rests.
• LeanCert and the other pinned direct or transitive packages recorded in lake-manifest.json, including PrimeCert, LeanArchitect, checkdecls, Aesop, Batteries, Qq, and ProofWidgets. Some are build or transitive dependencies rather than members of the final theorem cone; the manifest is the exact resolved package record.

See THIRD_PARTY_NOTICES.md for the dependency and adaptation notices. Project-code authorship does not supersede the mathematical or software credit above.

AI-assisted development process

Early in the project, we developed a custom AI-agent pipeline under scripts/ to decompose proof goals, maintain a dependency DAG, dispatch multiple agents and models, manage parallel attempts, and run Lean checks on proposed changes. The pipeline made it possible to explore a very large proof surface, but its autonomous runs also hallucinated frequently. They invented lemmas or source support, reported progress that did not survive a fresh build, and sometimes proposed vacuous or mathematically unsatisfiable residual statements. Those failures are why this repository treats source rebuilds, satisfiability checks, and fresh #print axioms output as mandatory.

As the formalization matured, most proof development, debugging, and review was done interactively with Anthropic's Claude Code and OpenAI's Codex, under Gershon Bialer's direction. We also experimented with Google's Gemini, but used it much less extensively. AI systems helped search for proof routes, write Lean, refactor modules, and audit dependencies; none of their prose or claimed results is trusted merely because a model produced it. A contribution entered the proof only after the relevant Lean source compiled and its actual theorem dependencies passed the project's trust checks.

Build time and auditing

The repository pins Lean, Mathlib, and its other dependencies. Building the Math and MathExtras targets is computationally substantial because it compiles thousands of finite-certificate leaves and several large analytic modules.

On the development machine (20 logical ARM CPUs and 119 GiB RAM), the 2026-08-06 memory-capped Math MathExtras integration build completed all 21,020 jobs successfully. Its changed Section 4.1.3 consumer cone was rebuilt with two workers, a 14 GiB hard cgroup limit, and swap disabled; the cgroup peak was 14,020,857,856 bytes. The graph and cache state change as certificates are split or migrated, so older job counts and wall times in planning documents are historical measurements, not current promises. A fresh clone or empty dependency cache can take hours; an incremental build usually touches a much smaller cone.

Do not run an aggregate build with bare lake build on a memory-constrained host. A Lean 4.32.1 rebuild on 2026-08-05 launched 20 certificate workers, exhausted the 119 GiB development machine plus swap, and triggered the global OOM killer. tools/safe_lake_build.sh is the supported aggregate-build entry point: it limits both Lake concurrency and the whole build's cgroup memory, and rejects a second concurrent build in the same checkout. Use TG_JOBS=1 for a known heavy certificate target.

The historical tg_native_certificates package still contains useful ordinary-kernel certificates and migration records, but its former expensive native leaves are no longer live native_decide dependencies of the capstone. Production compiled-code timings and controls now live in the LeanCompCert benchmark index linked above.

For work on the outer theorem interface without replaying the three hour-scale production folds, an explicitly axiomatized development target is available:

TG_COMPUTE_PROFILE=axiomatized python3 scripts/tg_build_profile.py

This builds a distinct Axiomatized.ternary_goldbach declaration whose two development assumptions are visible in #print axioms; it is not the public theorem and is never accepted by release audits. The cache-safe profile design, the remaining clean-build proof cone, human-readable computation contracts, and full/fast migration status are in BUILD_PROFILES.md.

tools/safe_lake_build.sh Math MathExtras

printf '%s\n' \
  'import Math.Problems.TernaryGoldbach.Statement' \
  '#print axioms Math.Problems.TernaryGoldbach.ternary_goldbach' \
  > /tmp/Check.lean
systemd-run --user --scope --quiet \
  -p MemoryHigh=20G -p MemoryMax=22G -p MemorySwapMax=0 \
  lake env lean /tmp/Check.lean | tee /tmp/Check.out

scripts/check_tg_citation_cards.py --from-file /tmp/Check.out
python3 tools/audit_tg_compcert_coverage.py --from-file /tmp/Check.out
scripts/check_authorship.py

⚠ Two build modes — the axiom count depends on which one you ran

lake build is the fast mode. It skips about 38 CPU-hours of ordinary-kernel interval certificates — nine Appendix A / A.5 adaptiveUpper bands — and discharges those leaves from named axioms in the HeavyCertificateStub namespace instead. Those proofs are in this repository, unchanged; the fast build simply declines to run them.

tools/safe_lake_build.sh Math MathExtras      # FAST: capstone carries 9 stubs
TG_MEM_HIGH=20G TG_MEM_MAX=22G TG_SWAP_MAX=0 TG_JOBS=1 \
  tools/safe_lake_build.sh HeavyCertificates # FULL: kernel certificates, 0 stubs

This exact full-build profile completed all 21,957 jobs from source on 2026-08-09 in about 2 h 23 min. The cgroup peak was 13,100,158,976 bytes (12.20 GiB), with zero swap and zero high, max, or OOM events. The single-worker setting is intentional: concurrent high-memory elaboration units, rather than any one unit exceeding 22 GiB, caused the earlier host failure.

The full mode produces HeavyCertificates.ternary_goldbach_fullBuild, the same proposition as ternary_goldbach (checked by rfl) with every stub discharged, and fails to build if any stub survives. tools/capstone_axioms.py prints which mode a tree is in before it prints any count, and --require-full refuses to report a fast-mode number as if it were the strong one. The complete statement of what each mode establishes is docs/BUILD_MODES.md. A release audit must quote the FULL mode.

The checked-in Structural CI workflow runs repository-policy, attribution, profile-isolation, unit, Blueprint-source freshness, reference-consistency, and compiled-site checks on an ordinary GitHub runner. It deliberately does not claim to replay the proof: the full release gate above needs the documented high-memory, hour-scale certificate build. A green structural-CI check is therefore not a substitute for the recorded full build and fresh axiom query.

The theorem trust print is the source of truth. The citation checker separates Lean's base trio and fast-build heavy stubs, reports any generated native_decide atoms (currently zero), and requires exact agreement between the remaining 59 names and citations/inventory.json. The authorship checker enforces project notices while preserving the explicitly classified vendored-fork exceptions.

Potentially reusable extension packages

To support the proof, this project developed the structure and proof glue for thirteen Lake packages under ext/ instead of burying every helper inside the ternary-Goldbach theorem. Each has its own dependency surface, public import, and independent build target, with separate tests where applicable. No ext/ directory is a vendored repository; individually noticed imported data and adapted artifacts retain their own licenses. This organization also makes the more general components candidates for reuse or eventual upstreaming without importing the full proof. The claim is deliberately “potentially reusable”: several packages also contain Helfgott-specific specializations.

Package	Scope and possible reuse
analytic_nt	Explicit analytic-number-theory infrastructure: Vaughan's identity, Type-I/Type-II bilinear estimates, large-sieve and mean-value tools, Diophantine approximation, and dyadic/product-cutoff machinery. It mixes reusable infrastructure with Helfgott-, Chirre–Helfgott-, Ramaré-, and Rosser–Schoenfeld-specific modules and finite/source interfaces.
ch25_certificates	Reproducible Chirre–Helfgott finite-computation artifacts and ordinary-kernel replays for the Lemma A.7 boundary transcript and Proposition 7.7 reciprocal-zero fold. The remaining zeta-evaluation and zero-enumeration semantics are kept as explicit external boundaries.
complex_compute	Tactics for reducing explicit complex re, im, norm, argument, logarithm, and exponential expressions to real arithmetic.
effective_asymptotics	Taylor bounds with explicit remainders, effective limits with moduli, derivative-certified monotonicity, and global bounds assembled from finite enclosures and analytic tails.
interval_arith	The verified_interval tactic, rational interval arithmetic, transcendental enclosures, bisection, derivative bounds, and certified Simpson/oscillatory-integration machinery.
kernel_certificates	Standalone ordinary-kernel certificate infrastructure for chunked finite arithmetic, prime-factor witness rows, exact prime-product traces, and outward-rounded Mertens-product transport.
quadrature_engine	Reusable multi-segment quadrature and pointwise-comparison certificates built over interval_arith, plus a small Helfgott-specific specialization.
saddle_point	A generic core for contour algebra and deformation, effective Laplace and steepest-descent bounds, and typed certificate/strategy interfaces, plus Helfgott-specific parabolic-cylinder specializations.
parabolic_cylinder	A verified raw integral, Weber equation, natural-domain Mellin identity, and reusable convolution/Gaussian helpers. Its historical continuation, V, Olver, and imaginary-axis interfaces are explicitly quarantined because their contracts do not match the cited formulas.
helfgott_certificates	Problem-specific finite certificates for Helfgott's minor-arc constants, isolated so they compile and cache independently.
rs62_certificates	Sharded numerical leaves for Rosser–Schoenfeld estimates and related explicit-prime bounds; the contracts are source-specific, while the certificate organization is reusable.
ternary_certificates	The heaviest closed native_decide leaves for the final theorem, split into parallel shards so analytic edits do not repeatedly rebuild them.
tg_native_certificates	Pure-Lean replacements for external and in-project finite sweeps. It combines LeanCert tables and checked Horner polynomial enclosures, ordinary-kernel rational/interval proofs, theorem-level reductions, and named LeanCompCert carriers for large production folds; its porting ledger records which Python/C++ audits are not yet practical Lean certificates.

The certificate packages are primarily an engineering and trust-boundary separation rather than general-purpose mathematics. Their independent caches are also a major reason warm incremental builds are much faster than the first source build.

Repository layout

Path	Purpose
Math/Problems/TernaryGoldbach/	Public theorem and circle-method assembly.
MathExtras/	Supporting analysis and explicit number theory.
ext/	Separately buildable, potentially reusable analysis/tactic packages and isolated heavy certificates.
forks/PrimeNumberTheoremAnd/	Vendored and locally modified upstream dependency; attribution is preserved.
blueprint/	Curated informal proof, LeanArchitect metadata, rendering sources, source-reference map, and reviewed compiled web Blueprint.
problems/ternary-goldbach/citations/	One expanded human-comparison card per named external/source atom.
docs/songs/	Complete chronological archive of the generally daily, AI-generated Suno-ready session songs from the project's final month-plus.
scripts/	Reproducibility and trust-audit tools.

Source papers are not distributed with the repository. See REFERENCES.md for primary public locators and the individual comparison cards for exact statement and range mappings.

Documentation

• STATUS.md — verified theorem and trust status.
• CITATIONS.md — historical citation audit.
• DISCHARGE_MAP.md — historical analytic-retirement map.
• ARCHITECTURE.md — package and proof architecture.
• BUILD_PROFILES.md — full and axiomatized builds, human-readable slow-computation boundaries, and cache safety.
• Computation-provider pattern — the Contract/Core/Sound/Full/Assumed layering and its current family map.
• MAJOR_RESULTS.md — generated exact trust tiers for curated major theorems, including base-trio results.
• Ternary Goldbach Blueprint — informal proof architecture linked to live Lean declarations and explicit trust boundaries; the reviewed compiled site is stored beside its sources.
• CONTRIBUTING.md — contribution and soundness rules.
• PUBLIC_RELEASE_CHECKLIST.md — preparation of a new, history-free public snapshot. The current private development repository and its existing history are not publication candidates.
• Songbook — the generally daily, AI-generated musical record of the final formalization sessions.

Authorship and license

Project-owned code is by Gershon Bialer and is licensed under Apache License 2.0. Vendored and adapted sources retain their own attribution; see AUTHORS.md, THIRD_PARTY_NOTICES.md, and LICENSE.