Universal Residual Seeds
Deformation forests, transport categories, and conditional system completion
Paper X · Komorebi P.
| Read | Pages |
|---|---|
| Traditional manuscript | 92 |
| Visual guide | 33 |
| Lean and evidence guide | 37 |
| Delivered total | 162 |
Open START_HERE.html for the reading index. Keep the three PDFs together for their twenty relative companion links. Thirty atlas pages occur intentionally in both the manuscript and visual guide; the total is not a count of independent additions. The original historical paper has 41 pages separately.
This distribution freezes accepted release 1.0.0 of October 20, checkpoint P10-REBASE-001. Every selected baseline file retains its exact bytes; original root documentation and manifest are retained in the dated before/ directory.
Exact mathematical boundary
The amended 20/20 source contract is conditional. The terminal
PaperX.ConditionalOccupiedSystemCompletion.conditional_occupied_system_completion
has two independent existential outputs: a transported target family and a
recovered summand inside a supplied carrier. Identifying those outputs requires
another comparison. Actual source members, transport/profile closure, carrier
and constituent presentations, and local comparison data remain inputs.
The arithmetic separator is literally over GQ. Zero multiplicities are allowed;
nonzero occupancy requires a separate premise.
Classical Inputs 3.1 and 4.1 are outside the twenty-row reading concordance. The later stronger 19/20 residual-system attempt remains unpromoted. Universal occupancy, natural finite seed rank, unknown carriers, unrestricted compatible systems and general arithmetic local attachment remain open or outside the accepted contract. Name/type/axiom checking is not machine-certified equivalence with every prose claim. The bounded critical-source review does not claim an all-twenty proof audit.
Accepted production and evidence
The October 20 closeout records two fresh pinned builds of all 122 selected production/support modules, including a relocated source replay. All 392 generated artifacts match byte for byte and all 122 sources match preserved origins. No inherited project proof objects seeded those builds. External Lean/Mathlib objects were reused; dependencies were not rebuilt cold. The 97-module terminal closure is a subset of the 122.
The complete owning-module audit records 2,846 constants: 2,127 theorems, 648
definitions, 25 constructors, 23 inductives and 23 recursors. It includes 444
private names; all 122 owners are nonempty. All 45 explicit name/kind/owner
contracts resolve and their complete elaborated types are retained. Transitive
axioms are exactly Classical.choice, Quot.sound and propext. Sources and all
392 artifacts were pinned before and after the accepted audit. These are
accepted compiler/audit records authenticated for this freeze, not new runs.
The 64 unit methods, 18 compiler fixtures, supplemental private/generated cases, three live target rejections and four portability mutations are separate tooling evidence, not production theorem counts. Earlier 4 GB auditor failures, interrupted/partial records and tooling integration failures remain dated history. The unchanged full 122-owner auditor succeeded serially at a 6 GB cap.
The selected recovered October 10 source archive has SHA-256
29e504f3508d54e72bd891bdd77c8df8ded52448b9f5aa161c1ebae1716ce58d.
The October 16–17 packages remain unrecovered; their reported 122-module/39-test
run is unauthenticated and is not substituted into this lineage.
Written, finite and historical evidence
All 16 main proof bodies, 20 numbered records and four complete printed production modules (1,117 lines) remain unchanged. The source-integrity inventory covers 6,170 inherited evidence files across its four documented directories. Separately, the compact store restores 3,079 unique exact leaf payloads at 13,730 occurrences; it does not reconstruct original compressed nested ZIP streams.
The accepted current seven-gate science record includes 28 original pytest cases, 13 reader-regression methods including 3,123 canonical residue towers, 263 positive visual assertions and 14 rejected false controls. All 179 numerical model fields and the complete stored model JSON agree. Six additional exact suites—precision, summands, families, logarithms, quadratic packets and local quadratic data—have separate domains, bounds, seeds and exclusions. Their counts are not combined into a theorem total. Sixteen figure pairs were regenerated without an independent byte/pixel-equivalence claim. The 255 old source/object pairs are saved-hash checks, separate from the two accepted compiler builds.
The current scientific manifest pins 6,188 consumed inputs. Older selected- October-10 metadata bindings are historical and do not certify unchanged current root documentation. They remain unchanged with their accepted scope.
The original 41-page historical PDF, editable source, 23-entry bibliography and 14 vector figures were recovered. Current references restore those 23 keys with source-specific identity checks, the Kisin page correction to 511–528, and explicit access limits. This does not authenticate every cited theorem or application.
Verify and reproduce
Extract this single ZIP, enter its root and run:
python3 -B verify_release.py --strict
The unchanged Python standard-library checker verifies exact regular-file membership, safe canonical paths, sizes and SHA-256. Its accepted 21-control receipt pins the exact checker/harness; those controls are not rerun here. The checksum list excludes itself and the root manifest; the manifest additionally authenticates that list. Integrity is not compiler, scientific or proof replay.
Read BUILD_AND_VERIFY.md and the preserved original README for scoped reproduction commands. Use a separate working copy and external outputs. Tools, TeX/fonts and the pinned 2.9 GB runtime/cache remain external. Lean 4.34.0-rc2 and its executable adapter, Mathlib and nine dependency identities remain precisely pinned in the production records.
The three current PDFs retain their accepted bytes. The accepted isolated clean rebuild matched page counts, ordered page text, 86.4-dpi rendered pixels and bytes after normalizing only generated trailer IDs. Raw PDF byte identity was false for all three. That PDF rebuild is recorded acceptance evidence; no TeX/PDF build was rerun for this freeze. The 392-artifact production identity is a different, byte-exact comparison and must not be conflated with normalized PDF equality.
- Accepted closeout
- Production replay
- Declaration audit
- Freeze record and progress ledger
- Dated freeze audits and baseline preservation map
Open use
Original software and machine-readable material retain MIT terms; original writing, figures and editable writing sources retain CC BY 4.0. Code listings also permit MIT. Full grants, PDF sidecars and third-party exceptions are retained. See LICENSE.md, LICENSE_STATUS.json and LICENSES/, including Apache 2.0 support terms and authenticated font notice supplements. No PDF or font bytes were changed.
Frozen 21 October 2026, America/Chicago; checks retain actual UTC timestamps. No new Lean, declaration-auditor, finite/scientific suite, controls, generator, TeX/PDF build, external theorem audit or whole-paper proof audit is claimed. Next sequential distribution freeze: Paper XI.