Lean 4 formalization of fixed-point constructions in monoidal closed, locally presentable categories, with connections to computability theory and categorical dimension.
42 files. 0 sorry. 0 custom axioms.
In any monoidal closed, locally finitely presentable category where the tensor product preserves finite presentability, the internal hom endofunctor has a fixed point that is unique up to isomorphism.
The proof combines Adamek's initial algebra theorem, Lambek's lemma, Adamek-Rosicky Theorem 2.23, and the LFP route (accessibility at aleph_0).
The fixed point L with Lambek iso [A, L] ≅ L is a reflexive object: it
encodes its own function space. From this structure:
- Self-application (
selfApp : A ⊗ L --> L): decode an element of L as a function via the Lambek inverse, then evaluate. - Categorical Y combinator (
omega f): for every endomorphismf : L --> L, the fixed-point equation holds:This is the morphism-level Kleene recursion theorem — every transformation of the carrier has a semantic fixed point.A ◁ omega(f) >> selfApp = selfApp >> f
The reflexive fixed point L ≅ [A, L] is a closed container: L contains its own transformation space, and the Lambek iso is the container boundary — applying the generator doesn't escape L. From containerization alone:
- Identity loop:
selfApp = reflexiveUncurry(𝟙)(evaluation is identity unfolded),omega(𝟙) = reflexiveCurry(selfApp)(the quine is evaluation folded). Identity modulation — fold/unfold via the Lambek iso — is the computational core. - Lambda calculus model: When the carrier L ≅ A (reflexive domain equation),
the reflexive object is a model of the untyped lambda calculus:
app(selfApp),abs(reflexiveCurry), β-reduction, η-expansion. The untyped lambda calculus is Turing-complete, so the reflexive fixed point supports universal computation without ℕ-enumeration. - Fixed points of all transformations:
omega(f) = abs(app ≫ f)satisfies the fixed-point equationL ◁ omega(f) ≫ app = app ≫ fpurely in lambda model terms.
A three-layer architecture connecting the categorical Y combinator to classical computability:
- Layer 1 (ReflexiveObject): categorical data — iso, selfApp, omega
- Layer 2 (SelfIndexedComputation): D indexes its own function space. The Lambek iso IS the naming function, CCC curry IS s-m-n, omega IS Kleene. No external enumeration needed.
- Layer 3 (KleeneDerivation): the N-bridge. A
ComputabilityStructuretypeclass adds enumerative data (countable programs, partial recursive evaluation). Kleene's recursion theorem is then derived from the generalCompModeltheory.
The Adamek chain is an N-indexed filtration by dimension:
- Truncation levels: dimZero, dimSucc, dimOmega — a dimension for each chain iterate
- F increments dimension by 1: applying the endofunctor raises dimension
- Stabilization at the fixed point: at L where F(L) ≅ L, dimension is invariant under F. The fixed point cannot have any finite dimension — it lives at the omega level.
- Graded filtration theorem: assembles increment, stabilization, and injectivity into a single structure
- Dimensional dissolution: the Yoneda embedding preserves and reflects
dimension — internal dimension in C equals embedded dimension in presheaves,
via Mathlib's
Adjunction.compYonedaIso - Divergence witnesses: FinSet divergence (cardinalities grow super-exponentially) and thin category triviality (at most one morphism contradicts reflexive structure)
- Convergence criterion: forward (FixedPointSpec implies omega + fixed-point equation) and converse (no initial algebra implies no pipeline)
- DimensionIncrement typeclass: every endofunctor satisfies it (the dimension-increment property is intrinsic to the chain construction)
HasAdamekFixedPoint F packages: carrier, Lambek iso, initiality. The
original conjecture — that any endofunctor with an Adamek fixed point must
be isomorphic to the internal hom — was investigated and found to be false.
Counterexamples: the powerset functor (Adamek FP but not right adjoint)
and the identity functor (right adjoint but left adjoint is not a tensor).
The precise result: terminal_characterization_from_adjunction proves that
if tensorLeft A ⊣ F, then F ≅ ihom A. The additional structure needed
is exactly the tensor-hom adjunction — uniqueness of right adjoints does
the rest.
The self-indexed terminal property refines this: SelfIndexedFixedPoint F
requires (𝟙_ C ⟶ D) ≃ (D ⟶ D) — global sections biject with endomorphisms.
This condition discriminates: the powerset functor and identity functor fail it,
while ihom(D) with the reflexive domain equation D ≅ [D, D] satisfies it.
selfIndexingEquiv constructs this from a reflexive object with A = carrier.
Coherent self-indexing (CoherentSelfIndexedFixedPoint) enriches self-indexing
with an evaluation map eval : D ⊗ D ⟶ D and naming-eval compatibility: evaluating
a named function recovers it. The bridge coherentFromReflexive constructs this from
a reflexive object with A = carrier, with both eval_compat and eval_id fully proved.
Density propagation (densityPropagation) proves Adamek-Rosicky Theorem 1.46:
endofunctors preserving filtered colimits that agree on finitely presentable objects
are naturally isomorphic. Fully proved by assembling Mathlib's IsDense,
isColimitOfPreserves, and IsColimit.coconePointsIsoOfNatIso.
Abstract ω-chain morphism framework and collapse-at-colimit theorem. Given two
endofunctor-generated chains (GeneratedChain M) related by an M-compatible
natural transformation, the induced morphism at the colimit is determined by
the colimit's universal property. When both chains share a fixed point, the
transformation collapses to an endomorphism of that fixed point.
Key results: collapseMap (induced map on colimits), collapseMap_unique
(uniqueness from universal property), collapseIso (levelwise iso gives
colimit iso), sharedCollapseEndo (endomorphism when chains share a colimit).
Tower initiality (adamekChain_initial): the Adamek chain from the initial
object is initial among all M-generated chains. For any process that generates
structural levels by iterating M from any starting point, there is a unique
chain morphism from the Adamek chain. Initiality is not a claim that no other
dimensional process exists — it is a claim that every other dimensional process
receives a unique map from this one. This is the load-bearing uniqueness
statement for the paper: all claims reference only chain objects and the colimit,
so tower initiality suffices. Global functor uniqueness (F ≅ ihom(A) on all of C
via the BV tensor) is a stronger statement that the paper does not require.
Instantiated end-to-end: given two FixedPointSpec instances for the same
closed object, the tower collapse recovers the canonical initial algebra
isomorphism (twoSpecCollapse_is_unique). The Adamek chain is also shown to
be a GeneratedChain for any endofunctor, with each level carrying its
canonical dimension from the graded filtration (DimensionTowerChain).
- Characterization theorem: any two acceptable numberings compute the same class of partial recursive functions
- Weak Rogers isomorphism: computable translations in both directions
- Kleene's recursion theorem: every computable transformation of programs has a semantic fixed point
- Effective Myhill Isomorphism Theorem: computable injections in both
directions plus computable padding yield a computable bijection. Full
back-and-forth construction with computability proved via
Primreccomposition. - Strong Rogers isomorphism: a computable bijection between any two CompModels, proved using the Effective Myhill theorem
BoardmanVogt.lean contains formal placeholder statements for the BV tensor
extension and Lawvere-Linton correspondence extension conjectures. The theorem
types are weak (existential witnesses are trivially constructible); the real
mathematical content is described in docstrings, not in the types.
See Status.md for a detailed walkthrough of what is proved, what is not, and why.
| Directory | What it contains |
|---|---|
Iteration/ |
Adamek's initial algebra theorem, chain construction, tower morphism framework, tower initiality (10 files) |
Specification/ |
Substrate-independent fixed-point existence and uniqueness |
Uniqueness/ |
Right adjoint uniqueness, monoidal uniqueness, terminal characterization, self-indexed terminal property, coherent self-indexing, density propagation (6 files) |
Accessibility/ |
AR Theorem 2.23 |
ChurchTuring/ |
CompModel, characterization, Myhill theorem, Rogers isomorphism |
Reflexive/ |
Reflexive object, Y combinator, containerization, identity loop, lambda model, Kleene bridge (8 files) |
Dimension/ |
Truncation levels, graded filtration, dissolution, divergence, dimension-tower bridge (10 files) |
Theories/ |
Essentially algebraic theory definitions |
Tensor/ |
Boardman-Vogt conjectures (isolated) |
# Build the project and check for errors
lake build
# Run the full audit (build + sorry check + axiom inventory)
./scripts/verify.sh- Lean 4 v4.28.0
- Mathlib v4.28.0
See repository license.