Unconditional 0.6727556 simple-critical-line proportion: six-translate Montgomery–Taylor penalty with a kernel-checked 5D certificate (+ Union and LineDecimal topics) - #17
Open
mdumitrean wants to merge 20 commits into
Conversation
… 5D certificate Adds the sextuple penalty/packing/transfer/ledger chain, the audited 56-piece macro envelope and 871 scalar certificates, and the concrete five-dimensional affine certificate replayed in the kernel (2969 subtree chunk modules, generic split-step assembly). Exports Certificate.sextuple_affine, zetaSextupleLedgerInterface, thmD₀_sextuple, thmD₀_sextuple_6727556 and cumulative variants; all on [propext, Classical.choice, Quot.sound]. Root now imports ThmD.Sextuple.LineDecimal.
Adds comparator topic Sextuple (four trusted statements at 0.672755620655 / 0.6727556, dyadic and cumulative; Solution delegates to Zeta23.ThmD.Sextuple), PrintAxioms file, README/AUDIT amendments. Removes the dead packedLeafLayoutCheck from Macro/TreeReader and fixes linter warnings in Sextuple/LineDecimal. Clean from-scratch rebuild of the certificate chain: exit 0, 4397 s wall; all declarations on the standard three axioms.
…ld logs Vendors the provenance material for the sextuple certificate into the repository: exact envelope and serialized tree data, the deterministic generators and verifiers (paths made repository-relative), the five independent audit reports, the clean rebuild / axiom / comparator logs, and a README with regeneration commands. AUDIT.md and README.md now reference these in-tree paths.
Brings in upstream's Mathlib-only challenge modules, single 17-statement base set, minimized ChallengeDeps, and formalization.yaml. The fork topics Union, LineDecimal, and Sextuple are ported to the new convention (definition layer inlined, import Mathlib only); N0/Nsimple move to ChallengeDeps/Union.lean. Build: 12,073 jobs, 35 deliberate challenge sorrys, all audited declarations on the standard axioms.
…/4000) via kernel-checked 5D certificate Zeta23.ThmD.Sextuple.A1275: Certificate.sextuple_affine (51/4000 <= E6(g) + B6*span g) by decide +kernel replay of an exact rational branch-and-bound certificate (272-model catalog = 56 stable + 216 Lean-checked refinement cells, 1,383 scalar seam certificates, 385,967-node dyadic tree with 192,984 leaves in 8,953 chunk modules and 90 assembly parts), the exact comparator 6727837118/10^10 < (6 B_MT - 10 pi B6)/(6 - 51/4000), and the unconditional dyadic and cumulative endpoints thmD0_sextuple(_cumulative)(_6727837118). Shared layers: Macro/StableCatalog (stable table extracted from ScalarData), Macro/TreeFormat, Macro/ParametricAdapter (audited leaf checker for arbitrary exact A, B, cutoff, table/scalar counts). Words stored two levels deep for cheap kernel lookups; A1275/FlatEquivalence proves the replayed streams equal the audited flat packed streams. Comparator topic SextupleA1275 (four statements). All audited declarations depend only on propext, Classical.choice, Quot.sound.
…, manifests, audits, build driver, and build logs Provenance for the A = 51/4000 certificate: exact serialized tree and refinement catalog with manifests and independent exact replays, the exact-rational generators and verifiers, the frozen source manifests, the independent data/plan, foundation, source-freeze, closure, scalar and assembly audits, the two-level word generator with its decode verifier, the assembly-statement regenerator, the batched memory-shaped Lake chunk driver, SHA256SUMS, and the logs of the foundation, chunk (8,953/8,953, 10,552 s wall), assembly, baseline-rebuild, root, comparator and axiom-audit builds; STATE.md and README amended; audit tools now cover A1275.
Feat/a1275 sextuple 6727837118
…7/20000) via kernel-checked 5D certificate Zeta23.ThmD.Sextuple.A1285: Certificate.sextuple_affine (257/20000 <= E6(g) + B6*span g) by decide +kernel replay of an exact rational branch-and-bound certificate over the shared 272-model catalog (3,365 scalar seam certificates, 1,771,973-node dyadic tree with 885,987 leaves in 30,153 chunk modules and 302 assembly parts), the exact comparator 6727949489/10^10 < (6 B_MT - 10 pi B6)/(6 - 257/20000), and the unconditional dyadic and cumulative endpoints thmD0_sextuple(_cumulative)(_6727949489). Every module of the target is emitted by certificates/sextuple/tools/gen_sextuple_target_lean.py from the canonical streams (two-level word literals, two-level scalar table, box-free split steps, decide +kernel scalar checks); the generator reproduces the committed A1275 artifacts. Comparator topic SextupleA1285. All audited declarations depend only on propext, Classical.choice, Quot.sound.
…r evidence, tools, and build logs Provenance for the A = 257/20000 certificate: the exact serialized tree and its independent exact replay (PASS), the generation report, the packed-words decode verification, frontier evidence (A = 0.0128 closes; A = 0.0129 does not close within 6,000,000 nodes), SHA256SUMS, the namespace-parameterised chunk driver and packed-words verifier, audit tools covering A1285, and the logs of the foundation, chunk (30,153/30,153, 48,654 s wall / 420,042 s CPU), assembly, root, comparator and axiom-audit builds; STATE.md and README amended.
…9/10000) over a 666-model catalog Zeta23.ThmD.Sextuple.A1290: Certificate.sextuple_affine (129/10000 <= E6(g) + B6*span g) by decide +kernel replay of an exact rational branch-and-bound certificate (4,299 scalar seam certificates, 3,550,925-node dyadic tree with 1,775,463 leaves in 56,924 chunk modules and 570 assembly parts), the exact comparator 6728005676/10^10 < (6 B_MT - 10 pi B6)/(6 - 129/10000), and the unconditional dyadic and cumulative endpoints thmD0_sextuple(_cumulative)(_6728005676). A1290/RefinementData2 adds 394 Lean-checked one-dimensional pieces (narrow wells on stable piece 36; 1/64-width constant barriers over barrier piece 43 and [59,60] with the constants Lean's own kernelRange certifies) and A1290/Catalog assembles the 666-entry table; without them A = 0.0129 is not certifiable. Generator gains --limit/--catalog-* parameters. Comparator topic SextupleA1290. All audited declarations depend only on propext, Classical.choice, Quot.sound.
…erators, interval replica, frontier analysis, logs Provenance for the A = 129/10000 certificate: the exact serialized tree and its independent exact replay (PASS), the catalog v2/v3 JSON and generator with the exact Fraction replica of Lean's RatInterval/TrigInterval/KernelInterval (reproduces committed pieces bit-for-bit), the v2/v3 branch-and-bound and verifier wrappers, the ceiling maps (true-kernel ceiling A* <= 0.0129938, B-scan), frontier evidence (A = 0.01293 closes externally with replay PASS; 0.01295 node cap; 0.01298 depth limit), SHA256SUMS, audit-tool coverage, and the logs of the catalog, foundation, chunk (56,924/56,924, 114,916 s wall / 996,422 s CPU), assembly, root, comparator and axiom-audit builds; STATE.md and README amended.
Author
|
Pushed three further kernel-checked refinements of the sextuple certificate on top of this PR's head (branch
All audited declarations depend only on
|
…eat/a1275-sextuple-6727837118 Adopt the upstream restructure: the project moves into zeta23/, the former comparator/ directory is dissolved into the Palomar template positions (Challenge/<Topic>.lean, Solution/<Topic>.lean, comparator-<topic>.json with "definition_names": [], scripts/PrintAxioms/<Topic>.lean), the root gains the monorepo README, .gitignore and CI workflows, and the seven Zeta23/LinAlg headers take the upstream authorship sentence. This fork's six topics (Union, LineDecimal, Sextuple, SextupleA1275, SextupleA1285, SextupleA1290), the Zeta23/ThmD/Sextuple development with its A1275/A1285/A1290 certificate chains, and certificates/sextuple/ are carried into zeta23/ with no change to statement, definition or proof bytes; their configurations and path mentions are rewritten to the template layout (README.md, AUDIT.md, formalization.yaml, tools). The root README and formalization.yaml of the old layout are replaced by the upstream ones; the old comparator/README.md rows are folded into zeta23/README.md. Module resolution and the Mathlib-only challenge modules are checked in the new layout; the full rebuild required by the LinAlg header edits is recorded in a follow-up revision note.
Author
|
Merged upstream One caveat for the repository's CI: the three certificate chains total ≈100k |
…Alg modules; 85/85 print-axioms standard; audits clean)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR raises the unconditional simple-and-on-the-critical-line proportion from the Montgomery–Taylor endpoint 2 − 1/c₁* = 0.672500703679… to
liminf N₀ˢ(T,2T)/N(T,2T) ≥ (6·B_MT − 10π·B₆)/(6 − A₆) = 0.672755620656…, with A₆ = 1/80, B₆ = 1094977/5000000000,
in dyadic and cumulative windows (Zeta23.ThmD.Sextuple.thmD₀_sextuple, _cumulative), with fixed-coefficient corollaries at 0.6727556 and 0.672755620655. The gain is small (+0.000255) but unconditional and fully formal.
Mathematics. Six translates of the Montgomery–Taylor kernel give a positive spectral penalty that the base argument previously discarded; the penalty is transferred through an exact finite Gram identity, packed into 5/6-span blocks, and fed into the zero-count ledger. The only numerical input is the five-dimensional affine inequality A₆ ≤ E₆(g) + B₆·Σg over all nonnegative gap vectors (Certificate.sextuple_affine).
Proof of the certificate. Exact rational branch-and-bound, replayed in the Lean kernel with decide +kernel: an audited 56-piece one-dimensional kernel envelope (analytic soundness proved via derivative enclosures), 871 exact scalar seam certificates, and a 99,507-node dyadic tree (49,754 leaves) split over 2,969 subtree modules and assembled by one generic split lemma. The soundness layer (AffineTree.lean) is stated for arbitrary input streams, so no decoder or generator is trusted; no floating point, native_decide, ofReduceBool, or external result enters the proof.
Comparator. New Mathlib-only topic Sextuple (four statements, config-sextuple.json), plus the Union (simple-or-on-line inclusion–exclusion) and certified-decimal LineDecimal topics, all ported to the current inlined-definition-layer convention. All 35 sorrys are the deliberate challenge ones; every audited declaration (77) reports [propext, Classical.choice, Quot.sound] (plus the two documented PairCeiling exceptions). Generators, canonical certificate data, five independent audit reports, and build logs are in certificates/sextuple/.
Cost. Clean rebuild of the certificate chain: 73 min wall / 7.8 CPU-h at ten builders (LEAN_NUM_THREADS=10; each builder ~8 GB). Comparator runs for the three topics are still to be done; the nanoda replay of the Sextuple solution will be long (it re-evaluates the whole certificate).