ComputationalPathsLean

A Lean 4 book companion repository for computational paths: explicit, trace-carrying witnesses of equality built on top of Lean's Eq.

At the core, a path records both an equality proof and its rewrite trace:

structure Path {A : Type u} (a b : A) where
  steps : List (Step A)
  proof : a = b

This library develops:

• the computational-path rewrite system (Step, Rw, RwEq, normalization),
• genuine loop quotients (PathRwQuot) together with separate synthetic winding-expression presentations (including circle and torus case studies),
• weak higher-groupoid structure (OmegaGroupoid),
• and a broad collection of mathematical modules under ComputationalPaths/.

Palomar associativity certificate

The standalone Palomar boundary proves termination, canonical normalization, global confluence, and semantic completeness for proof-relevant associativity rewriting on Mathlib free magmas. It also constructs and separates the two directed routes around Mac Lane's pentagon. The eight selected declarations are stated in Challenge.lean, proved in Solution.lean, and explained in ASSOCIATIVITY_COHERENCE_CERTIFICATE.md.

Run the complete local audit with:

scripts/check-palomar-associativity.sh

The pinned Comparator/NanoDa replay runs in the Palomar Readiness workflow. Submissions use the current Palomar submission form.

Higher-coherence extension

AssocHigher.allParallel connects all parallel signed associativity traces using explicit pentagon, interchange, naturality and structural higher cells. evalHigherRwEq interprets these witnesses in the existing computational-path tower. See the higher-coherence scope and verification note for the proof architecture, comparison with existing work, and limitations. This extension is separate from the original eight-declaration Comparator boundary; it has not been externally submitted or independently replayed by that Comparator.

lake build ComputationalPaths.Path.OmegaGroupoid.AssocHigherBridge
lake env lean scripts/AssocHigherAudit.lean

Certified finite-torus preimages

The library includes a certificate-driven solver for preimages of loop classes under continuous maps between finite tori induced by rectangular integer matrices. The topology-independent core checks finite integer data and returns one of three distinct outcomes: an invalid certificate, a concrete solution with the complete affine kernel lattice, or an explicit divisibility row that proves nonexistence. The torus bridge proves that the same answer is correct for the actual quotient fundamental groups and winding classifier.

The optional SymPy producer is untrusted: Lean rechecks every certificate, literal answer, kernel projection, and obstruction used by the checked-in fixtures. The producer is not a verified Smith-normal-form implementation and no complexity bound is claimed.

python3 -m pip install -r scripts/requirements-torus-preimage.txt
scripts/check-torus-preimage.sh
python3 scripts/torus-preimage-certificate.py \
  examples/torus-preimage-coupled.json --verify

See the scope and verification note. The underlying winding and integer linear algebra are classical; the note makes no publication, priority, or independent-review claim for this research prototype.

Project scope

Representative results and modules include:

• ComputationalPaths/Path/CompPath/CircleStep.lean (synthetic circle winding-expression quotient ≃ ℤ)
• ComputationalPaths/Path/CompPath/TorusStep.lean (synthetic product winding quotient ≃ ℤ × ℤ)
• ComputationalPaths/Path/CompPath/KleinBottle.lean (π₁(K) ≃ ℤ ⋊ ℤ via loop-expression quotients)
• ComputationalPaths/Path/OmegaGroupoid.lean (weak ω-groupoid-style hierarchy)
• ComputationalPaths/Path/Rewrite/Step.lean (primitive rewrite-step relation)
• ComputationalPaths/Path/TypeTheory/MetadataJ.lean (metadata-fiber classification for based elimination, factorizing motives, and the computational-trace obstruction)
• ComputationalPaths/Path/TypeTheory/MetadataRepair.lean (universal setoid repair, projection/kernel and PathRwQuot/K criteria, raw-vs-RwEq traces, and genuine-vs-synthetic circle/torus no-bridge theorems)
• ComputationalPaths/Path/Algebra/CertifiedIntegerMatrixPreimage.lean (validated integer-matrix certificates, complete affine solution sets, and explicit obstructions)
• ComputationalPaths/Path/Topology/CertifiedTorusPreimage.lean (transport of the certified solver to actual finite-torus loop homotopy classes)

The current Circle is a one-constructor Lean type and Torus is its product. Their genuine PathRwQuot loop fibers are therefore contractible. The noncontractible ℤ and ℤ × ℤ results belong to explicitly synthetic expression quotients; the library proves that no SimpleEquiv can bridge those quotients to the current genuine loop fibers.

More strongly, PathRwQuot A a b ≃ PLift (a = b) for every carrier A (ComputationalPaths/Path/TypeTheory/QuotientPathInduction.lean): the rewrite quotient is ambient equality, so it supports unrestricted based path induction precisely because it retains no computational-path information. See ERRATA.md for the corrections this implies for earlier public descriptions of the library, including the arXiv preprint.

Beyond Path/, the repository also includes broad companion developments such as arithmetic, geometric, motivic, topos-theoretic, and representation-theoretic modules.

Repository structure overview

Top-level layout:

ComputationalPathsLean/
├── ComputationalPaths.lean           # Root import hub
├── Main.lean                         # CLI entry (prints libraryVersion)
├── lakefile.lean                     # Lake package configuration
├── lake-manifest.json                # Lake dependency manifest
├── lean-toolchain                    # Pinned Lean toolchain
├── Challenge.lean                    # Palomar statement boundary
├── Solution.lean                     # Palomar checked proofs
├── comparator.json                   # Selected declaration contract
├── formalization.yaml                # Provenance and scope metadata
├── ComputationalPaths/
│   ├── Basic.lean                    # Core exports + libraryVersion
│   ├── Path/                         # Computational paths core ecosystem
│   │   ├── Basic/                    # Path/Step core definitions
│   │   ├── Rewrite/                  # Step, Rw, RwEq, normalization, tactics
│   │   ├── Homotopy/                 # Loop spaces, π₁, πₙ, fibrations, etc.
│   │   ├── CompPath/                 # Circle/Torus/Sphere/Pushout constructions
│   │   ├── OmegaGroupoid/            # Higher coherence and derived omega-groupoid APIs
│   │   ├── Algebra/                  # Algebraic constructions over paths
│   │   ├── Topology/                 # Topological applications
│   │   ├── Category/                 # Category-theoretic path developments
│   │   └── Logic/                    # Logic/type-theoretic path modules
│   ├── Arithmetic/
│   ├── Birational/
│   ├── Chromatic/
│   ├── Cobordism/
│   ├── Condensed/
│   ├── Crystalline/
│   ├── Etale/
│   ├── Floer/
│   ├── Hodge/
│   ├── KacMoody/
│   ├── Langlands/
│   ├── Motivic/
│   ├── OperadicAlgebra/
│   ├── Perfectoid/
│   ├── Prismatic/
│   ├── Quantum/
│   ├── SymplecticDuality/
│   ├── Topos/
│   ├── Tropical/
│   └── VertexAlgebra/
├── docs/
│   ├── ARCHITECTURE.md               # Canonical architecture overview
│   ├── axioms.md                     # Canonical axiom/typeclass inventory
│   └── archive/                      # Historical audits and run outputs
├── paper/                            # Paper/book source material
└── scripts/
    └── legacy/                       # Archived maintenance scripts

Getting started

Prerequisites

• elan (Lean toolchain manager)
• git

This project is pinned to:

• Lean v4.33.0 (lean-toolchain)
• Mathlib v4.33.0 (lakefile.lean)

Build

# Clone
git clone https://github.com/Arthur742Ramos/ComputationalPathsLean.git
cd ComputationalPathsLean

# Build all modules
lake build

Optional (faster first build when available):

lake exe cache get

Run executable

lake exe computational_paths

Build specific modules

lake build ComputationalPaths.Path.CompPath.CircleStep
lake build ComputationalPaths.Path.CompPath.TorusStep
lake build ComputationalPaths.Path.CompPath.KleinBottleStep
lake build ComputationalPaths.Path.OmegaGroupoid
lake build ComputationalPaths.Path.TypeTheory.MetadataJ
lake build ComputationalPaths.Path.TypeTheory.MetadataRepair

Metadata-J paper and companion

The focused theory paper is paper/adequacy/main.tex. It develops diagnosis and universal setoid repair for equality metadata, the projection/kernel classification, the exact PathRwQuot/local-K criterion, and the genuine-versus-synthetic circle/torus audit.

The stable Lean names for the headline chain are based_identity_total_space_contractible, unrestricted_based_elimination_iff_contractible, and metadata_fiber_criterion.

The earlier raw, scope-indexed de Bruijn calculus is preserved independently at paper/adequacy/companion/main.tex; it is not folded into the theory article. See paper/README.md for the manuscript build matrix and the external BSLstyle.cls/BSLbibstyle.bst prerequisites of the separate legacy paper/main.tex source. Build the manuscripts separately:

cd paper/adequacy
latexmk -pdf -interaction=nonstopmode -halt-on-error main.tex

cd companion
latexmk -pdf -interaction=nonstopmode -halt-on-error main.tex

Useful maintenance checks

# Find placeholders
rg "sorry" --glob "*.lean" ComputationalPaths

# Find custom axiom declarations
rg "^axiom " --glob "*.lean" ComputationalPaths

CI status

GitHub Actions workflow: Lean Action CI

• Workflow file: .github/workflows/lean_action_ci.yml
• Triggers: pushes to main, pull requests, manual dispatch
• Runner: ubuntu-latest
• Main step: leanprover/lean-action@v1 with Mathlib cache enabled

Use the badge at the top of this README to check live build status.

Contributing

• Keep proofs sorry-free and avoid new global axioms.
• Prefer Path/RwEq-based reasoning for equality developments.
• Run lake build before opening a PR.
• Keep canonical documentation under docs/; move historical audits or generated run logs to docs/archive/ rather than leaving them in the repository root.

License

MIT License — see LICENSE.

References

• de Queiroz, de Oliveira & Ramos, Propositional equality, identity types, and direct computational paths (SAJL, 2016)
• Ramos, de Queiroz & de Oliveira, On the Identity Type as the Type of Computational Paths (IGPL, 2017)
• de Veras, Ramos, de Queiroz & de Oliveira, On the Calculation of Fundamental Groups in HoTT by Means of Computational Paths (arXiv:1804.01413)
• Lumsdaine, Weak ω-categories from intensional type theory (TLCA, 2009)
• van den Berg & Garner, Types are weak ω-groupoids (PLMS, 2011)