>_PROJECT.MAGMATIC_UNIVERSE

The Magmatic Universe
Tzouvaras's ZFA Inseparable Collections

Athanassios Tzouvaras | formalized as HeytingLean.Magma | March 13, 2026

IPFS PERMANENT STORAGEcontent-addressed · immutable

LEAN (IPFS)C (IPFS)RUST (IPFS)ALL (IPFS)

CID: bafybeic6n5hteyispd4px4ttraolzrd66hh22moylnexeszpbpzamfm65q

Abstract

The magmatic universe $\mathbb{M}$ is a ZFA-based hierarchy of inseparable collections introduced by Tzouvaras and inspired by Castoriadis's “magma” concept. In $\mathbb{M}$ there are no finite sets, no empty set, and no singletons — every element has infinitely many predecessors. Ordered pairs are constructed via atom-tagged markers on incomparable atoms, with injectivity proved by three-case elimination. The formalization covers the full hierarchy (atoms, lower topology, predecessor map, pairs, products, relations, functions), number representations (naturals, ordinals, countable generation), separation (magmatic classes, scale invariance, the magmatic separation scheme, replacement failure with explicit counterexample), and the bridge to Heyting nucleus theory (omega_R, irreducible complement, Heyting gap measure, computational irreducibility, scale invariance triple equivalence, pre-distinction domain).

Modules

22

12 categories

Theorems

23

Machine-verified

Definitions

22

Type-checked

Lines

698

Proof code

Sorry

0

Zero gaps

>_VERIFICATION.SEAL

Formal Verification Certificate

Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.

23 THEOREMS VERIFIED22 MODULES0 SORRY2 HOSTILE AUDITS

Magmatic Universe (Tzouvaras) • Lean 4 + Mathlib • Apoth3osis Labs

>_PROOF.FLOW

Paper ↔ Proof Correspondence

Every section of Tzouvaras's paper that defines a structure, axiom, or theorem has a corresponding Lean 4 module with a machine-checked proof. Sections without a Lean counterpart are expository.

Section	Title	Lean Module	Status
1	Introduction	expository	N/A
2	Magmatic Atoms	Atoms.lean	PROVED
2.1	Lower-Open Sets	LowerTopology.lean	PROVED
3	Hierarchy & Universe	Hierarchy.lean	PROVED
3.1	Predecessor Map	PredecessorMap.lean	PROVED
3.2	Intended vs Collateral	IntendedCollateral.lean	PROVED
3.3	Relations	Relation.lean	PROVED
3.4	Ordered Pairs	OrderedPair.lean	PROVED
3.5	Products	Product.lean	PROVED
3.6	Functions	Function.lean	PROVED
4–5	Numbers (Natural, Ordinal, Countable)	Numbers/	PROVED
6	Separation & Scale Invariance	Separation/	PROVED
6.2	Replacement Failure	ReplacementFailure.lean	PROVED
7	Bridge to Heyting Nucleus	Bridge/	PROVED
7.1	Heyting Gap Measure	HeytingGapMeasure.lean	PROVED
7.2	Computational Irreducibility	ComputationalIrreducibility.lean	PROVED
7.3	Scale Invariance Triple Equivalence	ScaleInvariance.lean	PROVED
7.4	Pre-Distinction Bridge	PreDistinction.lean	PROVED

>_KEY.MATHEMATICS

Key Definitions & Results

The Magmatic Universe

\mathbb{M} = \text{ZFA hierarchy where } \forall x \in \mathbb{M},\; |\\{y \mid y \leq x\\}| = \infty \;\wedge\; \nexists\, \emptyset \;\wedge\; \nexists\, \\{a\\}

No finite sets, no empty set, no singletons. Every element has infinitely many predecessors.

Theorem A: Pair Injectivity (Theorem 3.4)

\langle x, y \rangle_{a_0, a_1} = \langle x', y' \rangle_{a_0, a_1} \;\Longleftrightarrow\; x = x' \wedge y = y'

Ordered pairs are injective despite collateral subpairs. Proved by three-case elimination: same-side survives (Case I), cross-side excluded by $\operatorname{Incomparable}(a_0, a_1)$ .

Theorem B: Gap-Fixed Point Equivalence

\Delta_R(x) = \emptyset \;\Longleftrightarrow\; x \in \Omega_R

The Heyting gap is empty iff $x$ is a fixed point of the nucleus. Irreducible elements (outside $\Omega_R$ ) have non-zero gap.

Theorem C: Replacement Failure

\neg\,\operatorname{ImageClosed}(\operatorname{predecessorImage}(u_0))

ZFA's Replacement axiom fails in $\mathbb{M}$ . Proved via explicit $\operatorname{ReplacementCounterexample}$ : a subfamily that escapes the predecessor image.

>_PROOF.BLUEPRINT

Proof Modules

Each module can be expanded to show its definitions (mathematical notation) and verified theorems. Click to expand.

>_DEPENDENCY.GRAPH

Module Dependencies

Hover over a module to trace its imports. Solid lines show direct dependencies; dashed lines show transitive imports.

Foundation Structure Functions Theory Bridge Synthesisimportstransitive

>_VERIFIED.C

Verified C Artifacts

Faithful C11 transpilation of computational content. Compiled with gcc -std=c11 -Wall -Wextra -Werror (0 warnings). 6 self-test suites.

C

magmatic_universe.h

Core types and interfaces | from All

The Magmatic UniverseTzouvaras's ZFA Inseparable Collections