FailureOfComposition

This is the maintained repository for the Lean formalization and LaTeX source of Pointwise provable equality and the failure of composition.

• Palomar Registry: PALOMAR-2026-10-01-000013, version 1
• Paper on arXiv (math.LO): DOI 10.48550/arXiv.2609.25556
• Lean development and verification guide
• Manuscript version 37: source, PDF, and provenance and build instructions
• Mathematical statements and Lean signatures
• Manuscript-to-Lean coverage map
• Palomar interface and local verification history
• Codex setup in WSL2 and first toolchain-port task

The development proves the failure of induced composition on pointwise provability classes, the Pi-one completeness characterization, the classification of the generated composition congruence, and the weak-totality and range obstructions. The coverage map states the exact program-index scope. Version 37 revises the exposition and related work while preserving the mathematical statements, proofs, and theorem numbering. Palomar Registry version 1 records the manuscript and corresponding Lean development together at commit fb32a19c4883baad83b286d4594cfbc6b1d2ad5c. Later manuscript and documentation revisions on main do not change that immutable registered snapshot.

Paper

Read the current manuscript (PDF) | arXiv DOI

Repository layout and history

The mathematical development and its verifier are in Lean/. The two declared libraries are FailureOfComposition and the 31 pinned CategoricalRiceShapiro evaluator modules it uses. The default build target is FailureOfComposition. The Lake package name remains CategoricalRiceShapiro to preserve the dependency manifest; it does not identify the repository where development is maintained.

Verification

The Lean 4.35.0-rc2 port at d2100df passed the independent WSL rerun on 2026-09-25. With that toolchain and the pinned dependencies installed under this checkout's Lean/.lake/packages, run from this directory:

bash scripts/verify-failure-composition.sh --check-environment
bash scripts/verify-failure-composition.sh

The environment check invokes no Lake command. Full verification builds the library and runs the style, theorem, dependency, and kernel checks. The evaluator style cleanup extends warnings-as-errors checks to all 31 evaluator sources. The cleanup passed its full WSL verification; see the validation record. CRS_LAKE_PACKAGES may supply an existing package mapping. The scripts validate the dependency pins and do not fetch new checkouts.

For a source checkout on /mnt/c, use the persistent Linux mirror described in scripts/README.md. Choose a fresh mirror, such as ~/src/FailureOfCompositionStandalone: the existing ~/src/FailureOfComposition mirror belongs to the original repository's checkout. Mirror ownership is tied to its source directory.

Licensing and Palomar

The Lean formalization and supporting code use the existing Apache-2.0 license. The author retains copyright in the manuscript, which was submitted under arXiv's perpetual, non-exclusive distribution license; that grant is not a general public reuse license. See the manuscript notes.

Palomar's service verification of all nine selected declarations passed on October 1, 2026. Its automated editorial review identified no blocking problems, and version 1 was registered that day. The registry entry records the exact source revision, selected declarations, verification evidence, and automated review. The verification run is also public.

The earlier local Comparator and official-verifier runs remain documented in the local verification history and Nine checkpoint status. Those records identify their own tested revisions and are distinct from the subsequent Palomar service verification and registration.