An Explicit Collar Recursion for Type-013 Benzel Tilings

This repository contains the manuscript and complete kernel-only Lean 4 formalization resolving Propp's Problem 4 on type-013 benzel tilings.

Main result

Every valid (a,b)-benzel with nonpositive Conway--Lagarias invariant admits a tiling by left stones and all three orientations of bones, with no right stones. The proof constructs a universal collar around a translated B(a-3,b-3) and iterates it to a bone-only Kim--Propp base or one of three explicit small bases.

The strengthened publication endpoint also proves that the constructed tiling's left-stone bases are exactly

p_t = (1-d^2-2L+3t, L+d(d-1)/2-3t),  0 <= t < L,

where d=a-b and L=(a+b-3d^2)/6. These bases are distinct and their cardinality is L.

Formal verification

The literal publication endpoints are:

• BenzelProblem4Kernel.publication_problem4;
• BenzelProblem4Kernel.publication_problem4_with_spine.

They use the manuscript's exact axial-cell carrier, benzel inequalities, left stone, three bone orientations, and unique-cover tiling predicate. The axiom audit reports only propext, Classical.choice, and Quot.sound, with no project axiom, sorry, or admit.

Run the kernel-only check from the repository root:

powershell -NoProfile -ExecutionPolicy Bypass -File scripts\verify_kernel.ps1

Run the complete manuscript, symbolic, finite-regression, spine, and kernel suite with:

powershell -NoProfile -ExecutionPolicy Bypass -File scripts\verify_all.ps1

Repository contents

• paper/benzel_problem4.pdf: rendered manuscript;
• paper/benzel_problem4.tex, paper/references.bib, and paper/figures/collar_b99.tex: manuscript source;
• lean4/BenzelProblem4Kernel/: literal Lean development;
• lean4/PUBLICATION_MANIFEST.json: byte-complete formal source manifest;
• FORMALIZATION_CORRESPONDENCE.md: manuscript-to-Lean theorem map;
• KERNEL_STATUS.md: exact publication boundary;
• scripts/: kernel verification, paper build, and independent regression checks;
• REPRODUCIBILITY.md: pinned environment and cache restoration procedure.

Prebuilt Lean cache

The v1.0.0 GitHub Release contains a source-bound archive of project-owned compiled Lean outputs and a member-level SHA-256 manifest. It excludes Mathlib and all other third-party dependency caches. The Release assets are re-downloaded and restore-tested before the cache is treated as recoverable.

Software archive Concept DOI: 10.5281/zenodo.22306076.

Licensing

See LICENSE.md. Lean sources, verification scripts, and repository documentation are Apache-2.0; manuscript source and PDF are CC BY 4.0.