lean-canny
A Lean formalization of the theorem that the
Existential Theory of the Reals (ETR) is in PSPACE,
or stated in terms of complexity-theory classes: ∃ℝ ⊆ PSPACE,
and native PSPACE bounds for semialgebraic point and whole-space connectivity.
This theorem is from John Canny's 1988 technical report
Some Algebraic and Geometric Computations in PSPACE
(stored in this repo as canny-tr.pdf), published as a
STOC ’88 paper (pp. 460–467).
The main results in
ETR/CoercivePSPACE.lean are:
LeanCanny.ETR.etr_mem_PSPACE : LeanCanny.ETR.language ∈ LeanCanny.PSPACE
LeanCanny.ETR.existsReal_subset_PSPACE : LeanCanny.ExistsReal ⊆ LeanCanny.PSPACE
These are unconditional theorems for the project's encoded ETR language and Complexitylib's machine-based PSPACE class. The coefficient algorithms, metadata preparation, recursive evaluation, and final sign decisions are constructed internally. The development uses Lean 4.36.0-rc1 with pinned Mathlib, CSLib, and Complexitylib dependencies.
This establishes the report's ETR and connectivity PSPACE upper bounds for the encoded problems below. Explicit roadmap output and motion-planning interfaces are separate from these language-membership results. The proof uses a coercive one-parameter sampling construction; it does not formalize every intermediate construction in the report verbatim.
The formalization also identifies a gap in Canny's coordinate-recovery argument: three collinear solutions can produce a cubic GCD where the construction requires a linear one, regardless of the projection coefficients. The completed PSPACE proof avoids this failed step.
For independently readable, checked statements of all three PSPACE bounds, see
Abstract.lean. A reader can inspect its definitions
and theorem statements to assess the claimed result; Lean verifies the proofs
through AbstractBridge.lean and the development.
All public definitions are local to the abstract or use background libraries.
A declaration-driven command generates the local flat token encoding using
Complexitylib encoders; its PSPACE transfer is checked
in AbstractEncodingBridge.lean.
ETR proof outline
- Compile ETR to one integer equation. The binary grammar, normalization, and equation compiler have native polynomial-time certificates. Correctness covers every bitstring; malformed formulas are rejected. Degree, arity, encoded length, and coefficient-mass bounds are derived from the input.
- Construct bounded critical samples. For the compiled polynomial q,
minimize
q² + s * Σ Xᵢ^(2D+2)as positive s tends to zero. Its gradient has finite fibers for every nonzero s. Bounded integer coordinate annihilants give a source-size root radius, so satisfiability is equivalent to eventual bounded critical samples with the required residual and penalty bounds. - Compute annihilants and primitive coordinates. A fixed full Macaulay block determinant supplies nonzero coordinate annihilants. Native modular readers feed actual integer degree/GCD/direction preparation. A uniform recursive symbolic evaluator computes the prepared primitive parameter; indexed pair readers and ordered matrix products compute its rational coordinates. All child computation costs and malformed metadata cases are included in the space certificates.
- Decide eventual signs. Even denominator clearing preserves the sample
equations and inequalities. Native readers compute the resulting integer
bivariate queries without storing their expanded coefficients. The
infinitesimal root/sign decision procedure decides four sign patterns in
PSPACE. Their union is exactly ETR; closure under polynomial-time reductions
gives
ExistsReal ⊆ PSPACE.
Selected entry points:
| Stage | Modules |
|---|---|
| Encoding and compilation | Grammar, EquationCompilerFP, Complexity |
| Bounded sample semantics | CoerciveSourceSampling, CoerciveRootRadius |
| Actual annihilator and query coefficients | CoerciveNativeOriginalResidue, CoerciveQueryCoefficient |
| Native preparation and symbolic parameter | CoerciveIntegerPreparation, CoerciveTableCorrectness, CoerciveParameterCoefficient |
| Coordinates and cleared queries | CoerciveCoordinatePairReaders, CoerciveClearedQueryCoefficient |
| Final decision | CoerciveInfinitesimalSemantics, CoercivePSPACE |
SpaceFunction wraps
Complexitylib's ComputableInPolySpace.
SpaceDecider carries membership in
its native PSPACE class. Polynomial-time reductions and all FP controls also
use Complexitylib directly. Space composition charges the original readers;
no free coefficient oracle or execution-time bound on a space-bounded child
is assumed.
Alternative constructions
The default LeanCanny library and import LeanCanny contain the completed
ETR and connectivity proofs through the formal abstract. The optional
LeanCannyAlternatives library is available through
import LeanCanny.Alternatives; it also imports
the completed result. All source modules retain their existing paths.
The repository also develops Canny's compact tube and generic projection constructions, projective elimination, finite-root sign feasibility, and nonsingular tube sampling. These are independently proved ingredients and alternative samplers. The tube route's effective epsilon/delta/direction and retained-level choices are unresolved; the completed ETR theorem uses the coercive route and does not depend on those choices.
Further work includes relating this encoding to other ETR presentations,
proving the NP lower inclusion, and constructing explicit roadmaps and
motion-planning interfaces. The alternative library remains checked by the full
verification commands below.
See RESEARCH.md for prior work,
proof details, and the unused tube route's precise gaps.
Connectivity
The separate LeanCannyConnectivity target (import LeanCanny.Connectivity)
proves both original connectivity languages are in native PSPACE:
LeanCanny.Connectivity.pointLanguage_mem_PSPACE :
LeanCanny.Connectivity.pointLanguage ∈ LeanCanny.PSPACE
LeanCanny.Connectivity.connectedLanguage_mem_PSPACE :
LeanCanny.Connectivity.connectedLanguage ∈ LeanCanny.PSPACE
The closed statements are in
NativeConnectivityPSPACE.lean.
Inputs contain a unary dimension and arbitrary Boolean combinations of integer
polynomial sign conditions. Point inputs describe singleton endpoints by formulas,
allowing irrational algebraic points. Whole-space connectivity means
IsPreconnected, accepting the empty set. Malformed, ill-scoped, inconsistent
and nonunique endpoint inputs are rejected. Neither theorem takes a geometric
model, component oracle, edge evaluator or radius bound as a premise.
The construction checks both original component labels, the actual radial grid and every interval cut on one complete sampler tuple. The original frontier edge is exactly projected-sample equality or oriented guarded joint feasibility. Endpoint formulas select existing samples after adding tautologies that preserve the space. Native finite graph scans finish both decision procedures. See the connectivity proof outline and correctness pitfalls for the construction and the failed shortcuts it must avoid. Detailed construction notes and the historical checkpoint ledger are separate.
Attribution and report integrity
The Sturm–Tarski proof adaptation and its changes are documented in
STURM_SOURCES.md.
The report PDF canny-tr.pdf is from the
Berkeley Technical Reports archive.
The downloaded file has 936,246 bytes and SHA-256
7606d41dea23ac1160562a759c196267906d8aec0f754cd4998fdd14fcd185f8.
The report retains its original rights; the source-code license does not apply
to it.
Build and verification
Install elan, then run:
lake update
lake exe cache get
lake build
lean-toolchain and lake-manifest.json
record the versions used. The default entry point is LeanCanny.lean.
lake build checks the formal abstract and its completed proofs. To build the
retained alternative constructions, run lake build LeanCannyAlternatives;
their entry point is Alternatives.lean.
Build the connectivity extension with lake build LeanCannyConnectivity.
Import the formal abstract with import LeanCanny.Abstract, or build it with
lake build --wfail LeanCanny.Abstract. It is also included in the default build.
Dependencies are pinned to Complexitylib revision 393e2b13 and Lean
v4.36.0-rc2, with matching CSLib and Mathlib revisions. The Lake package is
complexitylib, from its canonical cslib-community/complexitylib repository.
The build targets above require only their transitive dependency imports;
they do not build Complexitylib's full library or result collection.
For stricter verification:
lake build LeanCanny LeanCannyAlternatives LeanCannyConnectivity --wfail --iofail
lake env lean scripts/CheckCoreImports.lean
lake env lean scripts/CheckAxioms.lean
lake env lean scripts/CheckAbstract.lean
lake env lean scripts/CheckAbstractEncoding.lean
lake env lean scripts/CheckGrammar.lean
lake env lean scripts/CheckSpaceFoundation.lean
lake env lean scripts/CheckPolyTimeFoundation.lean
lake env lean scripts/CheckConnectivity.lean
lake env lean scripts/CheckJointFrontier.lean
lake env lean scripts/CheckConnectivityPSPACE.lean
lake env lean scripts/CheckImplicitStratumSampler.lean
lake env lean scripts/CheckEffectiveBallConnections.lean
lake env lean scripts/CheckProviderAtomic.lean
lake env lean scripts/CheckProviderSemantics.lean
lake env lean scripts/CheckProviderRecursive.lean
lake env lean scripts/CheckAlgebraicArcs.lean
lake env lean scripts/CheckAffineShiftArcs.lean
lake env lean scripts/CheckIntegerGridValues.lean
lake env lean scripts/CheckIntegerGridArcs.lean
lake env lean scripts/CheckFiniteFiberSlabs.lean
lake env lean scripts/CheckBinaryValueReaders.lean
lake env lean scripts/CheckGridValueReaders.lean
lake env lean scripts/CheckEndpointMidpoints.lean
lake env lean scripts/CheckAffineShiftReaders.lean
lake env lean scripts/CheckActualHeightReaders.lean
lake env lean scripts/CheckRoadmapBridges.lean
lake env lean scripts/CheckRoadmapChains.lean
lake env lean scripts/CheckRoadmapEncoding.lean
lake env lean scripts/CheckRoadmapInternal.lean
lake env lean scripts/CheckRoadmapLevels.lean
lake env lean scripts/CheckRoadmapNativeGraph.lean
lake env lean scripts/CheckRoadmapOccurrences.lean
lake env lean scripts/CheckRoadmapOrigins.lean
The core import check keeps the ETR endpoint independent of the optional tube
route. The formal abstract also imports connectivity and its shared algebra.
The axiom and space audits include all three library targets. The axiom audit checks
declarations in the LeanCanny namespace, local Nat
codec extensions, and their transitive dependencies, allowing only Lean's
standard propext, Classical.choice, and Quot.sound axioms. The foundation
checks enforce the native Complexitylib time and space interfaces and reject
legacy machine dependencies. CheckAbstract also follows public definitions
and statement dependencies to reject hidden implementation references.