GAMUT

Research record — Published from the project repository. Each record states its own date, scope and evidence status.

Research records: Trust & validation

Proof trust and release validation

Trusted foundations

  • Lean: leanprover/lean4:v4.19.0, compiler commit 6caaee842e94.
  • Mathlib: c44e0c8ee63ca166450922a373c7409c5d26b00b (v4.19.0).
  • All nine package repositories are locked by resolved git SHA in lake-manifest.json. Mutable upstream inputRev labels do not replace those pins. Verification consumes this lockfile without lake update.
  • Only propext, Classical.choice, and Quot.sound may occur in transitive axiom dependencies. This is not a claim of absolute axiom-freedom.
  • The audit rejects any other axiom, including sorryAx or native-evaluation admission, every locally authored axiom, and unsafe required or source-ranged declarations.

audit.lean.in uses Lean’s collectAxioms on all 256 required exports and the complete module-origin cohort: every declaration whose imported defining module has prefix GAMUT, including private, generated and out-of-namespace declarations. It does not merely match declaration names. Lean 4.19 also emits unsafe compiler auxiliaries for safe definitions. declRangeExt distinguishes ordinary source declarations from those auxiliaries: required exports and source-ranged unsafe declarations are rejected, while unsafe compiler auxiliaries without source ranges are inspected, counted, and excluded as runtime artifacts. These include axiom stubs for compiled stages, which are not mathematical axioms usable by kernel-safe proofs. Every safe declaration still receives the full transitive axiom scan, regardless of visibility or namespace. This metadata check is not a general defense against custom elaborators deliberately hiding unsafe declarations; kernel checking and transitive proof dependencies are the mathematical trust boundary. The audit tool is outside the proof-library cohort. Unused mathlib declarations outside the imported proof dependencies are not part of the authored release.

proof-manifest.json contains F01–F10 metadata and the §8 regression mapping; PROOFS.md is its checked rendering. The independent required-exports.txt retains the reviewed acceptance inventory. Deleting a manifest export fails even if documentation is regenerated. Missing declarations are checked before dependency inspection. The checker itself remains reviewable verification infrastructure, not a proved Lean program.

Census certificate and exact computation

Census12Certificate.lean supplies a candidate list of 224 natural-number masks. Its provenance is the exhaustive minimum-over-24-affine-images algorithm on masks 0..4095, implemented in that same file; numericMaskCertificate12_exact kernel-checks equality of the candidate with the complete exhaustive filter using decide +kernel. Trust does not depend on how candidate numerals were initially suggested. Census12Counts.lean checks the exact cardinality distribution. The mask representation, decoding/encoding inverses, action interpretation, minimality, class equivalence, and quotient correspondence are proved in Census12Masks.lean and Census12.lean. Thus the count is attached to the mathematical T/I quotient, not merely an expected number.

There are 224 classes including empty and 223 nonempty classes; cardinalities 0 through 12 have counts [1,1,6,12,29,38,50,38,29,12,6,1,1]. The audited theorems certify these facts without external data, floating-point equality, native_decide, or a custom mathematical axiom. General complex Fourier identities use symbolic proofs; exact finite regressions use ordinary kernel-checked reduction.

Validation record — 13 September 2026

The release verification command is python3 verify.py from formal/. It builds modules sequentially before the full library target to avoid overlapping expensive jobs on private 8GB GitHub runners. CI uses precisely that command. No remote CI execution is claimed.

The full command passed on committed proof/infrastructure snapshot 7e698d5 in 152.605 seconds, with maximum child resident set 5,183,717,376 bytes (4.83 GiB) on Darwin arm64. Measurement used a fresh Python parent and resource.getrusage(RUSAGE_CHILDREN).ru_maxrss (Darwin byte units): maximum child-process RSS, not a sum of simultaneous process RSS. All thirteen project modules and the root were freshly rebuilt; the audit inspected 883 origin declarations, axiom-checked 404 safe declarations and separately counted 479 unsafe compiler artifacts. All four rejection tests passed for their intended diagnostics. Linux CI resource usage may differ; no remote run is claimed. The clean environment uses fresh clones of all nine locked dependency repositories, no development symlinks, and the official precompiled mathlib cache. Project .lake/build is deleted before the full command. This is a clean project proof rebuild with cached dependencies, not a rebuild of all of mathlib from source.

The negative checks invoke the actual release audit (including a source-ranged authored unsafe definition): an out-of-namespace custom axiom and its private dependent theorem are compiled into temporary imported module GAMUT.AuditFixture; the audit must reject its module-origin cohort. Separate checks remove a manifest row and request a nonexistent Lean declaration. Acceptance requires the specific diagnostic for each intended failure, not merely any nonzero exit. Fixture files and imports do not persist.

Source correspondence and limitations

The current discrete sources were remediated at 8bd538b; durable anchors and corrections are in PROOFS.md and the R01–R15 ledger. Baseline specification fingerprints refer to historical 725ceb2, not the remediated source. Later proofs do not change the source’s domains or conventions. The AMS source and currently served AMS PDF were compared during source remediation; the served PDF SHA-256 is 08da1e38ffc140a6361ec3c932cd9280300b56ee674c9a19d556848b2851fa7a.

Source-remediation validation ran 312 RMCP tests and built all 22 site pages; the manuscripts were compiled and their pages rendered/inspected. RMCP changes were docstrings only, with AST comparison confirming unchanged behavior. These are software/source cross-checks, not Lean proofs. This release integration changes proof infrastructure and Markdown status only, so it does not repeat unaffected manuscript/site builds. Existing minor PDF layout/destination warnings and the explicitly superseded technical-survey revision remain recorded in the remediation ledger.

F01–F10 do not establish the repaired paper’s differential/symplectic derivations, all of introductory Theorems A–E, historical taxonomy/attribution, runtime correctness, corpus detection reliability or musical utility. Those questions remain separate. Independent release and whole-branch review is a subsequent gate; this validation record does not claim that review has already run.