# 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.*

[![Lean Action CI](https://github.com/timbrigham/ZeroParadox/actions/workflows/lean_action_ci.yml/badge.svg)](https://github.com/timbrigham/ZeroParadox/actions/workflows/lean_action_ci.yml) [![Sponsor](https://img.shields.io/badge/Sponsor-%E2%9D%A4-ff69b4?logo=githubsponsors&logoColor=white)](https://github.com/sponsors/timbrigham) [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.20060860.svg)](https://doi.org/10.5281/zenodo.20060860)

For the framework's *object*, the bottom element ⊥, see its companion reference [The Bottom Element](BOTTOMELEMENT.md). For the formal framework index and Lean verification, see [README](README.md). For plain-language introductions and reading paths, see [GUIDE](GUIDE.md). For the claim-by-claim status of every result, see the [Claims Ledger](CLAIMS.md).

---

## 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](BOTTOMELEMENT.md): 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, takes its first step 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 first step'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](ZP-Q_The_Frame_Change.pdf).

> **See it - [The Snap Loop](snap-loop.html).** The snap-arc ⊥ → ε₀ as one interactive 2-adic loop: a single discrete step of ε₀ away from bottom, then a return to bottom (a new successor null). Floor and ceiling are both ⊥; ε₀ is the first step from bottom, opening the gap between them - never a bottom and never 0. It maps the trajectory as a whole, not the route between - that runs through internal state with no external description. Hover any point for the checkable Lean witness.

---

## 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`](ZeroParadox/Order/Snap.lean)): 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`](ZeroParadox/Order/Snap.lean), algebraic), and the same irreversibility is proved topologically in the 2-adics ([`c3_irreversible`](ZeroParadox/Valuation/Padic.lean)) and categorically in the probability functor ([`fC_no_return`](ZeroParadox/Multihomed/InfoFunctor.lean)). ⊥ 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`](ZeroParadox/Settheory/ForkFrameChange.lean)); this is the standard lfp/gfp duality, choice-free, claimed as no novelty. It is realized concretely in the valuation face ([`snap_is_frameflip`](ZeroParadox/Multihomed/SnapFrameChange.lean): one ω-tower's encodings converge to ⊥ in the encoding chart and diverge to ∞ through the 0 ↔ ∞ inversion) and the category face ([`catseam_is_frameflip`](ZeroParadox/Category/SeamFrameChange.lean)). (The abstract cross-domain reading - that these are one and the same frame-change - stays a conjecture; see below.)

**Proved - the first step from bottom, reached by a choice-free snap from below.** ε₀ is the least fixed point of omega-to-the-power reached from 0 ([`epsilonZero_eq_nfp`](ZeroParadox/Ordinal/Gentzen.lean)); on ordinal notations the snap climbs from below with no choice ([`exp_lt_term`](ZeroParadox/Ordinal/ConstructiveOrdinals.lean), [`omegaPow_no_fixedpoint`](ZeroParadox/Ordinal/ConstructiveOrdinals.lean), [`tower_strictMono`](ZeroParadox/Ordinal/ConstructiveOrdinals.lean), all `propext`-only), and the first step is co-witnessed with the 2-adic limit and the machine snap ([`zpm_triangle`](ZeroParadox/Ordinal/Incompleteness.lean)). (That ε₀ *is* the least fixed point - [`epsilonZero_eq_nfp`](ZeroParadox/Ordinal/Gentzen.lean) - 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`](ZeroParadox/Category/Lawvere.lean), [`q2_no_witness`](ZeroParadox/Category/Lawvere.lean)); their ⊥ is a proved fixed point of its own self-map ([`q2_unique_fp`](ZeroParadox/Computability/SelfApp.lean), [`selfApp_fp_set_eq_singleton`](ZeroParadox/Multihomed/SelfAppForkPlace.lean)), 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`](ZeroParadox/Category/Lawvere.lean), 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`](ZeroParadox/Ordinal/ConstructiveOrdinals.lean) inherits `Classical.choice`.

**A note on the frame-change faces.** [`snap_is_frameflip`](ZeroParadox/Multihomed/SnapFrameChange.lean), [`catseam_is_frameflip`](ZeroParadox/Category/SeamFrameChange.lean), and [`fork_is_frameflip`](ZeroParadox/Settheory/ForkFrameChange.lean) 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](ZP-Q_The_Frame_Change.pdf).

---

## 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`](ZeroParadox/Order/Snap.lean) |
| 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`](ZeroParadox/Order/Snap.lean), [`c3_irreversible`](ZeroParadox/Valuation/Padic.lean), [`fC_no_return`](ZeroParadox/Multihomed/InfoFunctor.lean) |
| verb | a *change of frame*, valuation face (probe): the same ω-tower's encodings descend to the 2-adic floor 0 = ⊥ (the ascent to ε₀ resolving onto a new bottom ⊥ₙ₊₁) and, through the Riemann-sphere inversion that swaps 0 ↔ ∞, rise to ∞. The inversion is the passage between the two charts | [`snap_is_frameflip`](ZeroParadox/Multihomed/SnapFrameChange.lean), [`snap_frameflip_tower_tendsto_infty`](ZeroParadox/Multihomed/SnapFrameChange.lean) |
| verb | a *change of frame*, category face (probe): the categorical seam realizes the same frame-flip as an op-self-dual zero object of the module category ModuleCat ℂ - initial and terminal at once, with the op-duality frame-change swapping the two | [`catseam_is_frameflip`](ZeroParadox/Category/SeamFrameChange.lean) |
| 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`](ZeroParadox/Settheory/ForkFrameChange.lean), [`fork_collapse_iff`](ZeroParadox/Settheory/FixedPointFork.lean) |
| verb | *generation*: the floor's first step off itself - ε₀ is the least fixed point of α ↦ ω^α, the first ordinal fixed by omega-to-the-power | [`epsilonZero_eq_nfp`](ZeroParadox/Ordinal/Gentzen.lean) |
| 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`](ZeroParadox/Ordinal/ConstructiveOrdinals.lean), [`omegaPow_no_fixedpoint`](ZeroParadox/Ordinal/ConstructiveOrdinals.lean), [`tower_strictMono`](ZeroParadox/Ordinal/ConstructiveOrdinals.lean) |
| noun | the first step reached, *co-witnessed*: ε₀ stands with the 2-adic limit and the machine snap in one triangle | [`zpm_triangle`](ZeroParadox/Ordinal/Incompleteness.lean) |
| 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`](ZeroParadox/Settheory/SetTheoryAFA.lean), [`t_comp`](ZeroParadox/Computability/Kleene.lean), [`kleene_quine_is_bot`](ZeroParadox/Computability/Kleene.lean) |

### 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`](ZeroParadox/Category/Lawvere.lean), [`q2_no_witness`](ZeroParadox/Category/Lawvere.lean), [`computability_face_fixedPoint`](ZeroParadox/Category/Lawvere.lean) |
| *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`](ZeroParadox/Order/Snap.lean) |
| *proved to be a choice-free minimal first step*. 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`](ZeroParadox/Category/Lawvere.lean), [`q2_no_witness`](ZeroParadox/Category/Lawvere.lean)), so only the computability face carries a genuine one ([`computability_face_fixedPoint`](ZeroParadox/Category/Lawvere.lean), 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`](ZeroParadox/Computability/Kleene.lean), [`computability_face_fixedPoint`](ZeroParadox/Category/Lawvere.lean) |
| 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`](ZeroParadox/Valuation/FloorWitness.lean), [`attracting_attractor`](ZeroParadox/Valuation/BottomInvariant.lean) |
| 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`](ZeroParadox/Ordinal/ConstructiveOrdinals.lean), [`epsilonZero_eq_nfp`](ZeroParadox/Ordinal/Gentzen.lean), [`epsilonZero_le_fixedPoint`](ZeroParadox/Ordinal/Gentzen.lean), [`fundamentalSeq_cofinal`](ZeroParadox/Ordinal/Gentzen.lean) |
| information | **Mandatory** | surprisal is unbounded at the floor - the bottom carries no finite description to stay at | [`info_bottom_diverges`](ZeroParadox/Information/BottomMeasure.lean) |
| 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`](ZeroParadox/Category/Category.lean), [`t4_chains_forward_only`](ZeroParadox/Category/Category.lean) |
| 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`](ZeroParadox/Settheory/FixedPointFork.lean), [`selfMem_eq_singleton_bot`](ZeroParadox/Computability/SelfApp.lean) |
| 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`](ZeroParadox/Reals/OrderedField.lean), [`f_no_minimal_positive`](ZeroParadox/Reals/OrderedField.lean) |

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`](ZeroParadox/Valuation/BottomInvariant.lean)) - 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.*