Almost-linear modular composition

English | 简体中文

This repository accompanies our paper Almost-Linear Modular Composition over Arbitrary Commutative Rings. It contains the manuscript (PDF), LaTeX source, and our Lean formalization of the algorithm's correctness and ring-operation bound.

Authors: Yang Zhou and Mingsheng Wang.

We construct a division-free arithmetic circuit for g(a) mod f, where f is monic of degree n and a, g have degree below n. The same circuit works over every commutative ring with identity, including the zero ring. Its ring-operation count is n · 2^{O(√log n)}, including all preprocessing.

The correspondence between our paper and Lean declarations is described in docs/FORMALIZATION.md.

Main theorems

AlmostLinear/MainTheorem.lean provides two entry points:

• exists_modularCompositionCircuit_with_cost: for each n ≥ 2, one circuit computes modular composition over every commutative ring and satisfies an explicit cost bound with logarithmic factors.
• exists_modularCompositionFamily_with_asymptotic_cost: the same circuit family has cost O(n · 2^{(2√2+ε)√(log₂ n)}) for every ε > 0.

The counts refer to arithmetic gates in the circuit syntax. Some definitions are noncomputable; the formalized gate bounds do not give bounds on Lean execution or circuit-generation time. Integer-constant resource bounds are proved separately in OptimizedCompositionBits.lean.

Build

Install elan, Python 3, and Git. The project pins Lean 4.32.0 and mathlib revision 81a5d257c8e410db227a6665ed08f64fea08e997.

Place the two repositories next to each other:

parent/
├── almost-linear-modular-composition-lean/
└── division-free-arithmetic-lean/

The arithmetic dependency revision is recorded in docs/ARITHMETIC_DEPENDENCY.json. From the modular-composition repository, run:

lake exe cache get
python3 scripts/check.py

The check verifies manuscript checksums, builds all modules in both libraries, checks the arithmetic usage example, and audits transitive axiom dependencies. The permitted axioms are propext, Classical.choice, and Quot.sound.

The Lake dependency uses the sibling directory. CI checks out the recorded arithmetic commit from division-free-arithmetic-lean under the same GitHub owner. To use another owner or repository name, set the repository variable DIVISION_FREE_REPOSITORY to owner/repository.

Manuscript

The paper directory contains the current manuscript, its bibliography, and an optional SageMath check of finite instances. To create a minimal arXiv source archive and verify that it compiles independently, install pdfLaTeX with the standard packages used in paper/main.tex, then run:

python3 scripts/package_paper.py --check

The archive is written to dist/arxiv-source.zip. It contains only main.tex, references.bib, and main.bbl.

Organization

Path	Contents
AlmostLinear.lean	Imports every library module
AlmostLinear/	Algorithm, correctness proofs, and cost bounds
docs/FORMALIZATION.md	Theorem mapping and representation details
paper/	Manuscript, PDF, bibliography, and finite-instance checks
scripts/	Build checks, axiom audit, and manuscript packaging