10.2 Named external/source trust atoms
The current public theorem has 93 named external/source atoms. These nodes intentionally omit : each is an explicit citation boundary, not a repository proof of the reported computation.
Trust tier: EF-U. This is a named paper source plus complete reproducible external FLINT/Arb verification retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/2512.15709v1; ../../../ext/ch25_certificates/scripts/verify_a7_boundary.py; ../../../ext/ch25_certificates/certificates/a7_boundary.json.
Source: chirre-helfgott-2025, Lemma A.7, pp. 42–43 [source-shaped].
Trust tier: EF-U. This is a named external computation reported in paper retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/2512.15709v1.
Source: chirre-helfgott-2025, Lemma 9.2, pp. 35–36 [source-shaped].
Trust tier: EF-U. This is a named multiplicity-preserving zero enumeration/enclosure handoff plus ordinary-kernel reciprocal certificate and independent LMFDB/Platt fold retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/2512.15709v1; https://www.lmfdb.org/knowledge/show/rcs.source.zeros.zeta; ../../../ext/ch25_certificates/scripts/verify_flint_head.py; ../../../ext/ch25_certificates/certificates/ch25_prop77_flint.json; ../../../ext/ch25_certificates/scripts/verify_lmfdb_head.py; ../../../ext/ch25_certificates/certificates/ch25_prop77_lmfdb.json.
Source: chirre-helfgott-2025, Proposition 7.7, pp. 25–27 [adapted]
Source: chirre-helfgott-2025, Lemma A.7, pp. 42–43 [derived]
Source: lmfdb-zeta-zero-data, source, completeness, and rigor knowledge pages [local-reproduction]
Source: flint-acb-dirichlet-3-6, Riemann zeta function zeros documentation and FLINT 3.6.0 acb_dirichlet source [local-reproduction].
Trust tier: EF-U. This is a named computer-assisted paper theorem retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/2004.09765v1; https://doi.org/10.1112/blms.12460.
Trust tier: EF-U. This is a named external computation reported in paper retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1501.05438v2.
Source: helfgott-ternary-2015, Proposition 12.2.4, pp. 236–242 [source-shaped].
Trust tier: EF-U. This is a named computer-assisted paper theorem retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1305.3062v2.
Trust tier: EF-U. This is a named bounded external verifier contract; sampled locally; corrected V2 full-capable conditional bridge, no retained full run retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://doi.org/10.7169/facm/1229618741; ../../../scripts/cdem_squarefree_heads_segmented.py; ../../../MathExtras/NumberTheory/Analysis/HurstGPUProverBridge.lean.
Source: cohen-dress-el-marraki-2007, Lemma 1, p. 55, and Theorems 3 and 3 bis [local-reproduction].
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; completed fail-safe audit of the bounded Abel scan retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://doi.org/10.7169/facm/1229618741; ../../../MathExtras/NumberTheory/Analysis/CohenDressElMarrakiCompCertBridge.lean; ../../../../leancompcert/LeanCompCert/Ports/CDEMAbelProductionAuditCertificate.lean; ../../../../leancompcert/bench/results/cdem_abel_audit_5e9.json.
Source: cohen-dress-el-marraki-2007, Lemma 4, p. 59, and Theorem 5 bis, p. 62 [local-reproduction].
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; completed twelve-cell production observation retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../../../../leancompcert/LeanCompCert/Ports/CDEMAbelProductionCertificate.lean; ../../../../leancompcert/bench/results/cdem_abel.md.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; completed production marking-budget computation retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../../../../leancompcert/LeanCompCert/Ports/CDEMAbelMarkBudgetProductionCertificate.lean; ../../../audits/compcert/cdem_abel_mark_budget/cdem_abel_mark_budget.stamp.json.
Trust tier: EF-U. This is a named finite computation reported in primary and secondary sources; V2 full-capable conditional bridge, no retained full run retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1610.08551v2; https://arxiv.org/abs/2208.06141v4; ../../../MathExtras/NumberTheory/Analysis/HurstGPUProverBridge.lean.
Source: hurst-2018, Section 6.1, pp. 1020–1022 [background]
Source: lee-leong-2024, Corollary 1.3, equation 4; Section 5.3 [source-shaped].
Trust tier: EF-U. This is a named external verified-zero computation reported in paper retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1305.3087v1; https://arxiv.org/abs/1305.2897v4.
Source: helfgott-major-2013, Section 4.6, pp. 56–59 [derived]
Source: platt-2013, Theorem 7.1, p. 14 [exact].
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; opening squared-residue campaign completed and proved through the paper proposition retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../../../MathExtras/NumberTheory/Reductions/CrossMultipliedSweepReduction.lean; ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlattAuditCertificate.lean; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlattAuditTrace.lean; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlattAuditFold.lean; ../../../../leancompcert/bench/results/array_seg_folds.md.
Source: helfgott-minor-2013, sentence following equation 2.11, p. 8 [source-shaped].
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; opening fail-safe audit completed with zero retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../../../../leancompcert/bench/results/array_seg_folds.md; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlattAuditCertificate.lean; ../../../MathExtras/NumberTheory/Reductions/ArraySegMobiusPlattPaperBridge.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; exact opening low-carry observation completed retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../../../../leancompcert/bench/results/array_seg_folds.md; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlattAuditCertificate.lean; ../../../ext/tg_native_certificates/TGNativeCertificates/ArraySegMobiusPlattSound.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; exact opening high-carry observation completed retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../../../../leancompcert/bench/results/array_seg_folds.md; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlattAuditCertificate.lean; ../../../ext/tg_native_certificates/TGNativeCertificates/ArraySegMobiusPlattSound.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; tail squared-residue campaign completed and proved through the paper proposition retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlattAuditCertificate.lean; ../../../../leancompcert/bench/results/array_seg_folds.md; ../../../MathExtras/NumberTheory/Reductions/ArraySegMobiusPlattPaperBridge.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; tail fail-safe audit completed with zero retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../../../../leancompcert/bench/results/array_seg_folds.md; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlattAuditCertificate.lean; ../../../ext/tg_native_certificates/TGNativeCertificates/ArraySegMobiusPlattSound.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; full root-table prime count completed retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../../../../leancompcert/bench/results/platt_prime_counts.md; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlattFiniteEvidence.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; crossing-prefix prime count completed retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../../../../leancompcert/bench/results/platt_prime_counts.md; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlattFiniteEvidence.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; opening weighted marking budget completed retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../../../../leancompcert/bench/results/platt_prime_counts.md; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlattFiniteEvidence.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; tail weighted marking budget completed retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../../../../leancompcert/bench/results/platt_prime_counts.md; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlattFiniteEvidence.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; current retained production C passed under CompCert and gcc retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Helfgott/Section413G2SmallCompCertCert.lean.
Trust tier: EF-U. This is a named paper source plus foundation-only typed 29-execution semantic route; physical evidence pending retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/2408.05969v2; ../verify_ramare_2013_seams.py; ../extract_ramare_r2_certificate.py; ../ramare_zuniga_2024_lemma_6_2_full21e9.json.
Source: ramare-zuniga-alterman-2024, equation 19 and Lemma 6.2, p. 10 [exact].
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/tg_native_certificates/TGNativeCertificates/Ramare/MStar140MCompCertCert.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with flag 0 and a one-cell rejecting control retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/Section413G1Head10000Certificate.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with flag 0 and a one-cell rejecting control retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/Section413G2Head10000Certificate.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; runtime comparison of all 199,998 source-derived event words against the paper bound retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/Section413Window99999Certificate.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract for the runtime arithmetic precursor; the paper-predicate instructions remain incomplete retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/tg_native_certificates/TGNativeCertificates/Ramare/Combined100MRuntimeCert.lean.
Trust tier: PF-U. This is a named explicit pending source-to-program correspondence and omitted-paper-check obligation; not an execution result retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/tg_native_certificates/TGNativeCertificates/Ramare/Combined100MCert.lean; ../../../docs/RAMARE_COMBINED100M_EMITTER_WORKLIST.md.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract for the full 168-factor upward-rounded fixed-point product; production execution and one-unit rejecting control completed retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Helfgott/Section413Lemma42G2LargeMixedProducts.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract for the full 168-factor weak-H upward-rounded fixed-point product; production execution and one-unit rejecting control completed retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Helfgott/Section413Lemma42G2LargeMixedProductsWeakHHeadCompiled.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract for the verified normalized Q40 sum of 222 Simpson nodes and two exact error terms retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Helfgott/WACor49Eta2ExpMomentCertEnclosure.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract for all 512 independently certified Q32 leaf-word comparisons retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Helfgott/WAProp48QuadraticLogL2CompCert.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract for a verified normalized Q40 sum of all 50 weighted nodes retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Helfgott/WAProp48LogMomentChunk/Window750.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Helfgott/Section413Lemma42G2WeakHeadCompCertCert.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; completed 1092-window observation campaign retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlatt211Certificate.lean; ../../../../leancompcert/bench/results/manifests/platt211_1e12.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; completed 1092-window fail-safe audit retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlatt211Certificate.lean; ../../../../leancompcert/bench/results/platt211_audit_1e12.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; completed root cursor batch retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlatt211RootCertificate.lean; ../../../../leancompcert/bench/results/platt211_root_1e12.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; completed guarded root batch retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlatt211RootCertificate.lean; ../../../../leancompcert/bench/results/platt211_root_1e12.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; completed weighted marking-budget batch retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlatt211MarkBudgetCertificate.lean; ../../../../leancompcert/bench/results/platt211_mark_budget_1e12.md.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; exact prefix accumulator observation retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlatt211Prefix100Certificate.lean; ../../../../leancompcert/bench/results/platt211_prefix100.md.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; complete 100-prefix observation batch retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: https://arxiv.org/abs/1205.5252v4; ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/ArraySegMobiusPlatt211Prefix100Certificate.lean; ../../../../leancompcert/bench/results/platt211_prefix100.md.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/analytic_nt/AnalyticNT/Chebyshev/PsiFixedCompCertCerts.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/analytic_nt/AnalyticNT/Chebyshev/PsiFixedCompCertCerts.lean.
Trust tier: EF-U. This is a named conditional attested CompCert execution admission retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../../../ext/attested_compcert_bridge/AttestedCompCert/RunFromReceipt.lean; ../../../../attested-compute/SparkInterval/Execution/CompCertRunReceipt.lean; ../../../Math/Problems/TernaryGoldbach/Certs/SingularSeriesDeficitProdTwoMillionCert.lean; ../../../ext/analytic_nt/AnalyticNT/LargeSieve/UFoldUIv7ThreeAttested.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Certs/LiouvilleEllSweepCompCertCert.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/rs62_certificates/Rs62Certificates/RS62MertensFirstCompCert.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/tg_native_certificates/TGNativeCertificates/CDEMMertensCert0.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/tg_native_certificates/TGNativeCertificates/CDEMMertensCert1.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/tg_native_certificates/TGNativeCertificates/CDEMMertensCert2.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/tg_native_certificates/TGNativeCertificates/CDEMMertensCert3.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/tg_native_certificates/TGNativeCertificates/CDEMMertensCert4.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/tg_native_certificates/TGNativeCertificates/CDEMMertensCert5.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/tg_native_certificates/TGNativeCertificates/CDEMMertensCert6.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/tg_native_certificates/TGNativeCertificates/CDEMMertensCert7.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../ext/tg_native_certificates/TGNativeCertificates/WeightedMoment217CompCert.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Vinogradov/SingularSeriesC17CompCertCert.lean.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../MathExtras/NumberTheory/Analysis/A7BoundaryCompCertCert.lean; ../../../bench/results/manifests/a7_boundary_compcert_shards.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62AnchorPrefixCertificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_anchor_campaign_5.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62AnchorCertificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_anchor_campaign_5.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62AnchorCertificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_anchor_campaign_5.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62AnchorCertificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_anchor_campaign_5.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62Loop314Certificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_loop314_campaign_2.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62Loop314Certificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_loop314_campaign_2.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62Loop314Certificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_loop314_config_campaign_2.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62Loop314Certificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_loop314_config_campaign_2.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62Loop314Certificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_loop314_config_campaign_2.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62Loop314Certificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_loop314_config_campaign_2.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62Loop410Certificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_loop410_campaign_2.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62Loop410Certificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_loop410_campaign_2.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62Loop410Certificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_loop410_campaign_2.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62Loop410Certificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_loop410_campaign_2.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62Loop410Certificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_loop410_campaign_2.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62Loop410Certificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_loop410_campaign_2.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62CheckpointConfigCertificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_checkpoint_config_120.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62CheckpointConfigCertificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_checkpoint_config_120.json.
Trust tier: EF-U. This is a named exact external CompCert-artifact run contract; production execution completed with exit 0 retained as a Lean trust atom. Its expanded Lean proposition, the source proposition, exact symbol/range map, weakening derivation, artifact status, and human audit checklist are together in the self-contained comparison card.
Primary locators: ../compcert_campaigns.json; ../../../../leancompcert/LeanCompCert/Ports/RS62CheckpointCertificate.lean; ../../../../leancompcert/bench/results/manifests/rs62_checkpoint_campaign_120.json.
The next generated catalog is broader than the theorem’s trust boundary. It records every work in the public bibliography, including independently formalized methods and background-only references. Its relationship field is therefore essential: a source tag is not, by itself, an axiom or dependency.