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 - the same element, four names. In any Kleene-structured ZP lattice, the Quine atom (a set that is its own only member, set theory / AFA), the Kleene fixed point (a program that reproduces itself, computability), the order-bottom ⊥, and the algebraic join-identity are proved to be the same element. The three-name core - Quine atom = order-bottom ⊥ = join-identity - is axiom-free (t_exec); adding the fourth name, the Kleene fixed point, is proved via t_comp and kleene_quine_is_bot, which inherit Classical.choice from Mathlib’s recursion theorem. The set that is its own only member is the program that prints itself - a theorem here, not an analogy.

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 (mc1_correspondence); and the case where the coincidence fails, ℝ vs ℚ₂ by Ostrowski (completions_exhaustive, real_not_equiv_padic). They all instantiate one abstract schema, choice-free (fork_collapse_iff); and the ε₀ ceiling 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 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: ✓ Lean-verified - a machine-checked proof, with the witness theorem linked in Why each cell below · ✗ refuted (a proved obstruction, also Lean-checked) · ∅ not-applicable by structure (a category error - e.g. asking a ν-limit for a μ-generation property - not a gap). A trailing * on any mark (✓*, ↑*, ↓*) means conditional - established via a bridge or inherited from a sibling layer. The last column, dynamics, is DIRECTIONAL instead: ↓ inbound (converges to ⊥ - a sink), ↑ outbound (departs from ⊥ irreversibly - a source), ↕ both (a seam). (Witnessing theorems, with links to the Lean source, are in the dictionary above.)

The honest 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), and a ✓* holds only via a bridge. 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 value is in the non-✓ cells - the proved obstructions (✗) and the structural non-applicabilities (∅), 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.

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.