The Binary Snap (⊥ → ε₀) - Dictionary and Map
A dictionary and map of the framework’s central transition, the snap - 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 framework’s object, the bottom element ⊥, see its companion reference The Bottom Element. For the formal framework index and Lean verification, see README. For plain-language introductions 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 central transition, the snap - the forced move off the bottom element ⊥ into the first structured state, ε₀. It is the companion to The Bottom Element: that page maps the object ⊥ (the noun); this page maps the transition off it (the verb). Where the bottom dictionary is mostly nouns, this one is mostly verbs - the snap is an action.
It is a beginning, not a resolution. What is proved is that the snap is forced, one-way, generates its ceiling from below, realizes a frame-change in each domain, and that the domain snaps form one family (MC-1, membership proved per domain); what is retired is the reading that they are numerically one object (ill-typed - the members are provably distinct); and what stays open is the choice-freeness of the ceiling’s minimality. The frame-change faces are experimental probes; the abstract “the snap IS the change of frame” is a conjecture, written up in ZP-Q.
The short version: the snap, tiered by confidence
The snap is the framework’s one theorem - the forced, one-way departure from ⊥ into the first structured state ε₀ - and its central action. Everything provable is checkable: clone the repo and run #print axioms <name>.
Proved - the snap is forced, and adds no axiom. T-SNAP (t_snap_derived): the transition ⊥ → ε₀ (the minimum non-⊥ state) is a derived consequence of the bottom axiom A4 and the framework’s computational commitments, not an assumption. The Binary Snap that earlier layers posited as AX-1 is a theorem; no snap-specific axiom appears anywhere.
Proved - the snap is one-way. It does not reverse: no join returns to a strictly lower state (t_snap_irreversible, algebraic), and the same irreversibility is proved topologically in the 2-adics (c3_irreversible) and categorically in the probability functor (fC_no_return). ⊥ is a source, not a round trip.
Proved - a frame-change in each domain, and an order-theoretic universal. Over any complete lattice the order-duality frame-change swaps the fork’s two closures and the fork collapses at the diagonal fixed point (fork_is_frameflip); this is the standard lfp/gfp duality, choice-free, claimed as no novelty. It is realized concretely in the valuation face (snap_is_frameflip: one ω-tower is ε₀-as-⊥ in the encoding chart and ε₀-as-ceiling through the 0 ↔ ∞ inversion) and the category face (catseam_is_frameflip). (The abstract cross-domain reading - that these are one and the same frame-change - stays a conjecture; see below.)
Proved - the ceiling, reached by a choice-free snap from below. ε₀ is the closure of 0 under omega-to-the-power (epsilonZero_eq_nfp); on ordinal notations the snap climbs from below with no choice (exp_lt_term, omegaPow_no_fixedpoint, tower_strictMono, all propext-only), and the ceiling is co-witnessed with the 2-adic limit and the machine snap (zpm_triangle). (That ε₀ is the least fixed point - epsilonZero_eq_nfp - uses classical logic; whether that is avoidable at the notation level is the open item below.)
Proved - a wall: the snap is not one mechanism across categories. The per-domain frame-flips share a shape, not a single categorical map. In Set (all endofunctions) no nontrivial total type carries a Lawvere fixed-point witness - Cantor forbids it - so the lattice and 2-adic faces are provably not Set-level Lawvere instances (nontrivial_lattice_no_witness, q2_no_witness); their ⊥ is a proved fixed point of its own self-map (q2_unique_fp, selfApp_fp_set_eq_singleton), carrying the diagonal shape but not a genuine Set-level Lawvere instance. The computability face, by contrast, IS a genuine recursion fixed point (computability_face_fixedPoint, Kleene / Rogers) - but it lives in the effective category, where the fixed-point-free diagonal is not computable. Heterogeneous categories, heterogeneous verdicts: what unifies them is the diagonal shape, not one mechanism. The universality that holds is order-theoretic (the fork), not categorical - a proved obstruction.
The family (proved), the identity (retired), minimality (open). The domain snaps form one family (MC-1): per-domain membership is proved, the reading that they are numerically one transition is retired as ill-typed (a type boundary, not a theorem), and the members are provably distinct. Separately, whether ε₀-as-least-fixed-point is choice-free at the notation level is open: the syntax-to-semantics bridge tower_NF inherits Classical.choice.
A note on the frame-change faces. snap_is_frameflip, catseam_is_frameflip, and fork_is_frameflip are experimental probes in the bottom-diagram mapping campaign, not a finalized layer. The theorems build and are checkable, and they compose known results (no novelty is claimed); the abstract cross-domain statement “the snap ⊥ → ε₀ IS the change of point of view” remains a conjecture. The formal write-up is ZP-Q The Frame-Change.
Dictionary
The snap is (positive handles, with witnesses)
The handles sort by aspect: what the snap is (noun - the endpoints it joins) or what the snap does (verb - the action itself). Most are verbs; that is the point. The frame-change rows marked “(probe)” and the order-theoretic universal are experimental - the theorems are checkable, the abstract cross-domain reading is a conjecture.
| aspect | characterization of the snap | witness (links to Lean source) |
|---|---|---|
| theorem | the forced transition off ⊥ into the minimum non-⊥ state: the join c₀ ∨ c₁ = c₁ is a valid transition, and c₀, c₁ are provably distinct in both directions. AX-1 (the Binary Snap) is no longer an axiom, it is derived | t_snap_derived |
| verb | one-way: the departure from ⊥ does not reverse. No join can return to a strictly lower state (algebraic form), and the 2-adic and Kleisli faces prove the same irreversibility topologically and categorically | t_snap_irreversible, c3_irreversible, fC_no_return |
| verb | a change of frame, valuation face (probe): the same ω-tower descends to the 2-adic floor 0 (ε₀ realized as ⊥) and, through the Riemann-sphere inversion that swaps 0 ↔ ∞, rises to ∞ (ε₀ realized as the ceiling). The inversion is the passage between the two charts | snap_is_frameflip, snap_frameflip_tower_tendsto_infty |
| verb | a change of frame, category face (probe): the categorical seam realizes the same frame-flip via the zero object of the linear functor | catseam_is_frameflip |
| verb | a change of frame, order-theoretic universal (choice-free): order-duality swaps the fork’s two closures (least fixed point ↔ greatest fixed point), and the fork collapses to the diagonal fixed point exactly when the map has a unique fixed point. This is the standard lfp/gfp duality, bundled - the domain-independent shape the valuation and category faces realize concretely | fork_is_frameflip, fork_collapse_iff |
| verb | generation: the floor generates the ceiling - ε₀ is the closure of 0 under omega-to-the-power (the least fixed point of α ↦ ω^α) | epsilonZero_eq_nfp |
| verb | constructive, from below, choice-free: on ordinal notations, each tower term strictly exceeds the last, ω^x has no fixed point, and the tower is strictly monotone - all propext-only, free even of Quot.sound |
exp_lt_term, omegaPow_no_fixedpoint, tower_strictMono |
| noun | the ceiling reached, co-witnessed: ε₀ stands with the 2-adic limit and the machine snap in one triangle | zpm_triangle |
| noun | what departs: the floor the snap leaves - the three-name identity (Quine atom = order-bottom ⊥ = join-identity, axiom-free), extended to the Kleene self-reproducing fixed point | t_exec, t_comp, kleene_quine_is_bot |
The snap is not (characterization by exclusion)
Each exclusion is either a proved obstruction (a Lean-checked wall), a retired or out-of-scope reading (dropped as ill-typed, like the cross-frame identity, or outside what the framework claims), or an open question. The value is here as much as in the positive handles: the walls are what keep the synthesis honest.
| the snap is not… | witness (or meta / open) |
|---|---|
| one mechanism across categories. The per-domain frame-flips share a shape, not a single categorical map. In Set no nontrivial total type carries a Lawvere fixed-point witness (Cantor), so the lattice and 2-adic faces are provably not Set-level Lawvere instances - their ⊥ is a proved fixed point of its own self-map (q2_unique_fp, selfApp_fp_set_eq_singleton), carrying the diagonal shape but not a genuine Set-level Lawvere instance. The computability face is instead a genuine recursion fixed point, but in the effective category, where the diagonal is not computable. Heterogeneous categories, heterogeneous verdicts: what unifies the faces is the diagonal shape, not one mechanism - order-theoretic, not categorical. A proved obstruction, not a gap | nontrivial_lattice_no_witness, q2_no_witness, computability_face_fixedPoint |
numerically one transition across its carriers. The valuation, categorical, order, and computability snaps form one family (MC-1), not one object: each is a member (membership proved per domain), but the reading that they are numerically 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). What they share is the diagonal-fixed-point shape, not an identity |
meta (no Lean witness) |
| a physical, temporal, or causal event. The framework is silent on physics. The snap is an order and derivation transition, not a process unfolding in time; which specific state emerges first is outside its scope | meta (no Lean witness) |
| dependent on a snap-specific axiom. T-SNAP is derived from the bottom axiom A4 (the join identity ∀ x, ⊥ ∨ x = x) and the framework’s computational commitments. No snap axiom appears anywhere in the development | t_snap_derived |
proved to be a choice-free minimal ceiling. The from-below snap on ordinal notations is choice-free, but ε₀ as the least fixed point via the syntax-to-semantics bridge (tower_NF) inherits Classical.choice. Whether the minimality is choice-free at the notation level is open |
meta (no Lean witness) |
The boundary map
The dictionary above sorts the snap by aspect - what it is, what it does. This section re-cuts the same results by field. Walk into any one of the framework’s domains and ask a single question: is the departure from ⊥ mandatory here, or is it walled? Every cell has a verdict; nothing is left merely posited.
The pattern is worth stating plainly. The self-referential shape - the diagonal fixed point - recurs across every face, but the faces are not one object across them - they are one family (MC-1): the numerical identity is retired as ill-typed and the members are provably distinct. What is mandatory across almost every field is the snap itself, and each field compels it by its own native mechanism. One field is the telling exception: in the real numbers the snap provably fails, and the failure is a theorem.
Two notions, kept apart. There is a narrower, stronger one - a genuine Lawvere fixed point, self-application with no escape - and it is walled across almost every field: Cantor forbids the Set-level witness for any nontrivial total type (nontrivial_lattice_no_witness, q2_no_witness), so only the computability face carries a genuine one (computability_face_fixedPoint, in the effective category). The snap is mandatory far more widely than that fixed point is genuine. “The Lawvere fixed point is genuine in only one field” (read off the Lawvere register) and “the snap is mandatory across almost every field” (read off the table below) are both true - they measure different things. One shared technique; a different procedure in each field.
| field | the snap here is… | by what mechanism, or against what wall | witness (links to Lean source) |
|---|---|---|---|
| computability | Mandatory | a genuine self-reference fixed point - a machine run on its own code, whose halting is undecidable, so ⊥ cannot describe its own escape | self_halting_undecidable, computability_face_fixedPoint |
| valuation (p-adic) | Mandatory | the ultrametric sends the floor to v(0) = ⊤, and the doubling dynamics contracts every starting law onto that floor | addVal_bot, attracting_attractor |
| proof theory (ordinals) | Mandatory, and minimal | ε₀ is the proof-theoretic ordinal of PA; the ω-tower climbs from below choice-free, ε₀ is the least fixed point of α ↦ ω^α, and the tower is cofinal in it (the from-below climb is choice-free; the least-fixed-point and cofinality facts use classical logic) | tower_strictMono, epsilonZero_eq_nfp, epsilonZero_le_fixedPoint, fundamentalSeq_cofinal |
| information | Mandatory | surprisal is unbounded at the floor - the bottom carries no finite description to stay at | info_bottom_diverges |
| category | Mandatory, one-way | the initial object has a unique morphism out to every object and none back; ⊥ is a pure source, not a round trip | t2_universal_constituent, t4_chains_forward_only |
| order / set theory | Mandatory (choice-free spine) | the fork collapses to the diagonal fixed point exactly when the map has a unique fixed point, and the self-containing ⊥ = {⊥} realizes it. The field snaps form one family (MC-1); the reading that they are numerically one object is retired as ill-typed, the members provably distinct | fork_collapse_iff, selfMem_eq_singleton_bot |
| real numbers | Walled - the snap fails | density: between 0 and any positive lies a smaller positive, so there is no minimum non-⊥ to snap to. The one field where the transition provably cannot happen - and that impossibility is itself a theorem | f_snap_impossible, f_no_minimal_positive |
The cross-cutting walls - Cantor for the Lawvere fixed point, the MC-1 type boundary that retires the cross-frame identity, and the absence of a measure-preserving comparison between the two attracting bottoms (no_mp_attractor_to_markov) - are catalogued in The snap is not above. The walls are not failures of the program; locating them exactly is the program.
Generated by build_snap_map.py. Witness names are resolved against the Lean source at generation time and link to the file that declares them; a name that does not resolve fails loud as a warning, and the meta / open entries (marked as such) have no Lean witness. To update: edit the catalogue and rerun. The links render natively on GitHub.