v1.1.2 — exposition revision

v1.1.2 — exposition revision

This patch release revises the English, JCTA, arXiv, and Simplified-Chinese
exposition for “The exact saturated 6- and 7-Sperner numbers”. The complete
Lean 4 formalization and certificate payload are unchanged.

Principal verified results

• the eventual saturated 6-Sperner number is 30;
• the eventual saturated 7-Sperner number is 55;
• the explicit 55-member construction has small/large split 28/27;
• the analogous complete seven-core layered template class has minimum 56.

The revision makes the abstract more selective, gives the introduction a more
natural mathematical narrative, and shortens repeated verification and scope
qualifications. It also streamlines the Supplement headings. It changes no
mathematical statement, Lean theorem, certificate, or computational result.

The archive README distinguishes mathematical proofs, computed discovery
results, and Lean-formalized statements. Run verify-integrity.sh first,
then verify-core.sh; use verify-drat.sh for the archived DRAT certificates.
Each core replay retains the full transcript and per-step logs and writes
machine-readable steps.ndjson and result.json summaries containing the
commands, exit codes, Lake warning count, final theorem types, and expected
axiom boundary.

The preceding v1.1.1 package preserves the same complete proof and
certificate payload. The underlying v1.1.0 package passed all eight core
replay steps, including the Lean, construction, saved-result, and P0054 test
checks. This exposition patch changes no proof file or executable result and
passes its regenerated integrity manifest and PDF metadata checks. Its nine
CNF/DRAT pairs contain 18 verified files. The release asset and checksum
sidecar are published together at GitHub release v1.1.2 and archived on
Zenodo under DOI
10.5281/zenodo.21770438. All preceding releases remain immutable.

v1.1.1 — professional manuscript typography refresh

v1.1.1 — professional manuscript typography refresh

This patch release synchronizes professionally typeset English, JCTA, arXiv,
and Simplified-Chinese manuscript variants for “The exact saturated 6- and
7-Sperner numbers” with the unchanged complete Lean 4 formalization and
certificate payload.

Principal verified results

• the eventual saturated 6-Sperner number is 30;
• the eventual saturated 7-Sperner number is 55;
• the explicit 55-member construction has small/large split 28/27;
• the analogous complete seven-core layered template class has minimum 56.

The revision improves PDF metadata and bookmarks, adopts portable Chinese
fonts, standardizes tables and title typography, and repairs the JCTA abstract
column layout. It changes no mathematical statement, Lean theorem,
certificate, or computational result.

The archive README distinguishes mathematical proofs, computed discovery
results, and Lean-formalized statements. Run verify-integrity.sh first,
then verify-core.sh; use verify-drat.sh for the archived DRAT certificates.
Each core replay retains the full transcript and per-step logs and writes
machine-readable steps.ndjson and result.json summaries containing the
commands, exit codes, Lake warning count, final theorem types, and expected
axiom boundary.

The preceding v1.1.0 package passed all eight core replay steps, including
the Lean, construction, saved-result, and P0054 test checks. This typography
patch changes no proof file or executable result and passes its regenerated
integrity manifest and PDF metadata checks. Its nine CNF/DRAT pairs contain 18
verified files. The release asset and checksum sidecar are published together
at GitHub release v1.1.1 and archived on Zenodo under DOI
10.5281/zenodo.21769438. The preceding v1.1.0 release remains immutable.

v1.1.0

v1.1.0 — revised manuscript and complete formalization artifacts

This release synchronizes the revised manuscript and Supplement for “The exact
saturated 6- and 7-Sperner numbers” with the complete Lean 4 formalization. It
also contains the exact-search programs, construction verifiers, certificate
generators, CNF instances, DRAT proofs, verification scripts, manifests,
checksums, tests, and locked dependency metadata.

Principal verified results

• the eventual saturated 6-Sperner number is 30;
• the eventual saturated 7-Sperner number is 55;
• the explicit 55-member construction has small/large split 28/27;
• the analogous complete seven-core layered template class has minimum 56.

The revision clarifies that the named Lean declarations are the primary proof
objects for the largest finite classifications, adds a worked arbitrary-finite
five-row-kernel interface, and repairs the manuscript/Supplement crosswalk.

The archive README distinguishes mathematical proofs, computed discovery
results, and Lean-formalized statements. Run verify-integrity.sh first,
then verify-core.sh; use verify-drat.sh for the archived DRAT certificates.
Each core replay retains the full transcript and per-step logs and writes
machine-readable steps.ndjson and result.json summaries containing the
commands, exit codes, Lake warning count, final theorem types, and expected
axiom boundary.

The release directory passes its integrity check. The authoritative core
script passes the Lean, construction, saved-result, and P0054 test replays,
including a controlled failure-path test. The release asset and checksum are
attached together and mirrored unchanged on Zenodo under DOI
10.5281/zenodo.21730916.

v1.0.0 — reproducibility artifacts

v1.0.0 — reproducibility artifacts

This release supports the manuscript “The exact saturated 6- and 7-Sperner
numbers”. It contains the Lean 4 formalization, exact-search programs,
construction verifiers, certificate generators, CNF instances, DRAT proofs,
verification scripts, manifests, checksums, tests, and locked dependency
metadata.

Principal verified results

• the eventual saturated 6-Sperner number is 30;
• the eventual saturated 7-Sperner number is 55;
• the explicit 55-member construction has small/large split 28/27;
• the analogous complete seven-core layered template class has minimum 56.

The archive README distinguishes mathematical proofs, computed discovery
results, and Lean-formalized statements. Run verify-integrity.sh first,
then verify-core.sh; use verify-drat.sh for the archived DRAT certificates.

The release asset and checksum must be attached together. The matching
Zenodo record has reserved DOI
10.5281/zenodo.21679078.