The Bottom Element (⊥) - Dictionary and Map

A dictionary and map of the framework’s bottom element ⊥ - what it is, what it is not, and where each characterization is established, most with a machine-checked Lean witness linked to the source.

For the formal framework index and Lean verification, see README. For plain-language introductions, companions, and reading paths, see GUIDE. For the claim-by-claim status of every result, see the Claims Ledger.

What this is

This is a reference for the framework’s bottom element ⊥: a dictionary (what ⊥ is and is not) and a map (where each characterization is established). It is a beginning, not a resolution. What is proved is that each construction’s bottom belongs to the family and that the slot structure recurs; the reading that the various bottoms are one object is retired as ill-typed - they are provably distinct as structures (the “walls”). It closes a standing gap: a framework built on ⊥ that had not yet characterized ⊥ itself.

The short version: concepts that should not coincide, but do

One self-referential structure - a thing that is its own fixed point - keeps turning up in fields that do not expect to meet. Here is each coincidence, ordered by how sure we are of it. Everything provable is checkable: clone the repo and run #print axioms <name>.

Proved, with one commitment - the same element. In any Kleene-structured ZP lattice, the Quine atom (a set that is its own only member, set theory / AFA), the order-bottom ⊥, and the algebraic join-identity are proved to be the same element - the three-name core, axiom-free (t_exec). The fourth name, the Kleene fixed point (a program that reproduces itself, computability), is joined to the other three by an explicit structural commitment: the KleeneStructure typeclass names the computational fixed point as the same role - the motivating commitment, not a derived theorem. So the set that is its own only member is identified with the program that prints itself by that commitment, not proved equal. The computational witness rests on Mathlib’s recursion theorem, which carries Classical.choice; the three-name core needs none.

Proved - each field’s own floor. 0 in the 2-adics, where v₂(0) = ∞ (addVal_bot); unbounded surprisal, the state with no finite description (t2_diverges); the categorical bottom of each real Mathlib category, an inverse limit or initial object (fD_zero_isInitial, fC_zero_isInitial and fB_bottom_is_limit, collected in mc1_correspondence); and the case where the coincidence fails, ℝ vs ℚ₂ by Ostrowski (completions_exhaustive, real_not_equiv_padic). They share a SHAPE (Statement: COINCIDENCE, per field’s own witness above) - one object carrying both extremal characterisations at once - and a shared shape across distinct structures is a type boundary, never a common theorem. (The order-theoretic form of that shape is fork_collapse_iff, choice-free, but none of these satisfies its hypotheses of a complete lattice and a monotone map, so none is an instance of it.) ε₀ is co-witnessed with the 2-adic limit and the machine snap (zpm_triangle).

Mostly proved - a narrow residue argued. The framework’s set-theoretic commitment is not AFA specifically but a fragment it assumes of its host theory: a unique Quine atom ⊥ = {⊥}. That fragment is a checkable object, the QuineHost typeclass. Foundation-freeness is forced by the Quine atom (quineHost_not_wellFounded, axiom-free - a self-loop cannot live in a well-founded world); ordinary set theory (Foundation) is excluded in-kernel about the real theory (zfSet_no_quine_bottom - no set is self-membered under Foundation); Boffa’s axiom is set aside because it admits a proper class of Quine atoms rather than one (Boffa 1968), a gap a toy model makes concrete (boffa_fails_unique) rather than an in-kernel fact about Boffa’s axiom; and AFA is exhibited as the example meeting all three (afaStructure_isQuineHost). What remains argued is only that a Quine atom and its uniqueness are the right two requirements - a Forced Metatheoretic Commitment with a named falsifier, stronger than a free choice and weaker than a theorem. The set-membership face ⊥ ∈ ⊥ stays metatheoretic; the structural fixed point is machine-checked and axiom-free (t_exec).

The family - MC-1. MC-1 names not one object but one family. Each of these floors is a member: it satisfies the shared criteria mapped in the slots below, with per-domain membership machine-verified where marked (the categorical criterion is carried by the per-domain witnesses fD_zero_isInitial, fC_zero_isInitial and fB_bottom_is_limit, collected in mc1_correspondence). The choice of criteria is a design principle; that they characterize the family is an argument. The cross-category numerical identity - that the bottoms are one and the same object - is retired as ill-typed (x = y across distinct categories is not a well-formed proposition), and the members are provably distinct (the “walls” below). What survives is the proved leaves and the proved walls; the only oneness is the shared self-referential shape - the diagonal fixed point - which lives in the apophatic register, never as a formal identity. Within-frame identities stand (the three-name core above; 0 = ∞ under rInv in ℚ₂).

Reading key (for a reader with no prior context)

Slot codes (the map columns, and the positive dictionary entries):

Constructions (the map rows). A #N prefix (#2 Markov, #3 TopCat/p-adic limit, #4 Kleisli, #5 Hilbert seam) cross-references the bottom-diagram-tree nodes used throughout the Lean source (node #4, seam node #5, …). Only those four appear as numbered rows; the tree’s order-floor node #1 is the abstract Lat ⊥ row (shown here without the number), and the other rows (Info, Kleene, ε₀, selfApp, the p-adic valuation) come from other layers. The partial numbering is scoped, not missing data:

A few recurring terms:

Dictionary

⊥ cannot be (characterization by exclusion)

⊥ is (positive handles - the slots)

The handles sort by aspect: what ⊥ is (noun), what ⊥ does (verb), or both at once (hinge). The hinge is ⊥’s signature: at the floor the two collapse - the fixed point that is a thing and acts on itself in one step (operation = result). This noun-and-verb reading, and the claim that they collapse at ⊥, is the framework’s interpretation; the slot witnesses below are proved, the lens over them is not.

Map - slot × construction

Where each characterization stands. Most columns are a claim with a status, not a checkbox: ✓ the witness states a proposition and the kernel checked it · ≝ the cell’s own sentence in Why each cell below says what the witness is · ✗ refuted (a proved obstruction) · ∅ not-applicable by structure (a category error - e.g. asking a ν-limit for a μ-generation property - not a gap). A trailing * (✓*, ≝*, ↑*, ↓*) means conditional - established via a bridge or inherited from a sibling layer, a separate axis from ✓/≝. The last column, dynamics, is DIRECTIONAL instead: ↓ inbound (converges to ⊥ - a sink), ↑ outbound (departs from ⊥ irreversibly - a source), ↕ both (a seam). (The dictionary above links the witnesses it cites; each map cell’s own witness, or the reason it has none, is in Why each cell below.)

The informative content is in the non-✓ cells, and splitting them is the point: a ∅ is a settled structural fact (a category error, not a gap), a ✗ is news (a proved obstruction), a ✓* holds only via a bridge, and a ≝ sends you to that cell’s sentence. Two things worth reading off the table: (1) generation (GEN) is the μ / build-up-from-the-floor side, so the ν-bottoms (p-adic, Markov, the TopCat point-limit) read ∅ there - a ν-object has no μ-property - and the self-coincident fixed points (Kleene, selfApp) carry SELF rather than GEN; GEN’s one live cell is ε₀, where the floor generates a distinct ceiling. (2) The dynamics column is single-directional - ↓ for a sink (ν), ↑ for a source (μ) - and ↕ (both) appears only at a seam (μ=ν): the zero-object seam #5 Hilbert, and ε₀, whose row is itself the snap-arc 0→ε₀. So ⊥’s dynamics has one direction, fixed by whether ⊥ is a source or a sink.

The structural reading is in the non-✓ cells - the proved obstructions (✗), the structural non-applicabilities (∅), the ✓* cells that are conditional, and the ≝ cells, whose witness is named in its own sentence - not the filled count. The full reasoning behind the GEN and dynamics columns is written up in Structural Findings; the reason or witness behind every mark is below.

The diagonal family - the self-reference arguments as one fixed point

The classical self-reference arguments are not separate theorems that happen to rhyme; they are one diagonal fixed point seen under different conditions (Lawvere 1969; Yanofsky 2003). The framework maps the full roster against ⊥, organized by the μ/ν fork and built off a single engine - negation_no_fixedpoint / lawvere_fixedpoint, both axiom-free. On the wall side (μ) self-reference cannot close: the argument runs as a proof that no reflexive object exists. On the floor side (ν) it does close - the fixed point is genuinely produced, and lands at ⊥. Cantor, Russell, Turing, Tarski, Curry, Löb, and Gödel’s second incompleteness are all axiom-free; only the two computability floor faces (the Kleene quine and Rice’s exists-but-undecidable) carry Classical.choice, inherited from Mathlib’s recursion theory. This roster is ZP-R (the Cross-Category Fixed Point layer and its Diagonal Family Addendum) - a placement of ⊥ among recognized results, not a new theorem; the cross-face identity stays a type boundary, the same walls the map above records.

See it: the interactive Diagonal Family map renders this roster as one engine forking into walls (μ) and floors (ν), each node linking its Lean witness and axiom footprint.

Generated from bottom_cannot_be.md and the matrix data by build_dictionary_map.py. Witness names are resolved against the Lean source at generation time and link to the file that declares them; the meta entries (marked as such) have no Lean witness. To update: edit a source and rerun. The links render natively on GitHub.