The famous "Wheeler's list of forty-eight ways the universe is like a computer" is not a Wheeler publication. Tracing it to a primary source turns up one physical artifact: an unpublished, roughly seven-page typed note titled Universe as a computer, circa 1980, held in the John Archibald Wheeler Papers (call no. Mss.B.W564) at the American Philosophical Society and digitized in 2021 [1]. The catalogue credits its creator as Patrick M. Gunkel — an MIT-adjacent futurist who built a combinatorial "ideonomy" of long structured lists — not Wheeler, although it is filed among Wheeler's papers. The popular "Wheeler's list" framing traces only to a 2024 blog transcription that itself concedes the note "never made it into a paper." We therefore treat the list as a Wheelerian prompt, tag its attribution as Tier 3, and cite the genuine published anchor for the metaphor — Wheeler's 1982 The Computer and the Universe [2] and his 1989 "It from Bit" essay [3] — wherever the metaphor's substance is at stake. Not fabricating a citation for a list that has none is the first move of the honesty method this essay is built on.
Late in his life, the physicist John Wheeler became fascinated by a single slogan: maybe the universe is, at bottom, something like a computer. He didn't mean it literally — he meant it as a question-generator. If you take the slogan seriously, what could it possibly mean? It turns out there are dozens of different things it might mean, and they range from solid physics to pure poetry. This essay sorts them out and, where there's real mathematics hiding inside a metaphor, pins it down with a proof a computer can check.
The metaphor sits in the lineage of Wheeler's "participatory universe" and his "It from Bit" doctrine — the idea that "every it … derives its function, its meaning, its very existence … from … bits" [3]T2. By around 1980 Wheeler had moved from geometrodynamics (matter as curved spacetime) toward information as the more fundamental currency, a shift he later narrated in his autobiography [6]. The "computer" metaphor is the engineering face of that shift: if reality is information, then whatever processes the information is computer-like. The list catalogues the many non-equivalent ways one might cash that out — from "the universe is literally a Turing machine" to "the universe is half-mental."
Three Wheeler threads converge in the metaphor. (i) Delayed-choice: the 1978 thought experiment [5]T1 showing the experimenter's late choice fixes whether a quantum left a "wave" or "particle" record — empirically established, but Wheeler's observer-participancy reading [4] is the contested interpretive layer. (ii) Law without Law [4]: physical law as emergent rather than fundamental, mutable "mutability." (iii) The 1982 programmatic essay The Computer and the Universe [2], which builds physics from elementary quantum "yes/no" registrations — the closest published cousin of the apocryphal 48-list. The metaphor is best read not as an ontological thesis but as a research heuristic: a forcing function for asking which information-theoretic limits are physical law (Landauer, Bekenstein, Margolus–Levitin) and which are category mistakes (information as substance).
A list this promiscuous needs a discipline, or it collapses into either uncritical enthusiasm or blanket dismissal. We borrow PhysProof's honest-count discipline and apply it twice over.
First, every claim carries an epistemic tier.
Use the Tiers control at the top: click T3 speculation to dim every speculative passage, and watch how much — and how little — survives as settled physics.
Second, every metaphor with a genuine mathematical kernel is compiled in Lean 4, inside the PhysProof library, against the same toolchain as the rest of the project. What does "compiled" actually buy?
It buys exactly one thing: a proof assistant's kernel has verified that a precisely-stated proposition follows from its stated hypotheses. It does not buy that the proposition is about the physical universe. Each embedded proof below is paired with a blunt Establishes / Does NOT establish pair naming the gap between the idealized theorem and Wheeler's physical claim. The honesty is in the gap, not the green checkmark — a lesson the project learned the hard way, and which bit us again while writing this very essay (see §6).
Where a metaphor has no tractable formal core — most of the mind-and-process entries — the honest output is a labeled definition with no theorem, or a plain admission. We refuse to manufacture a theorem to make a philosophical provocation look settled. A machine-checked omnibus (§9) proves we used all four honesty buckets: genuine theorem, reuse, structural-only, and "no formal core."
Wheeler's first seven metaphors ask what kind of computer: serial (a Turing tape, 1), arrays of sub-computers (2), a fully parallel machine (3), a hybrid (4), a network or hierarchy (5), a finite or infinite collection (6–7), homogeneous or heterogeneous (13).
Is the cosmos one machine working through steps one at a time, like a person following a recipe? Or a vast crowd of little machines all working at once? Or a web with no central clock, each part nudging its neighbors? These are genuinely different blueprints. The pieces we can make exact are humble but real: running a step-machine for "m then n" steps is the same as running it for "m+n," and a finite array of finite gadgets is itself a finite gadget with a countable number of possible states.
A serial computer is the iteration of one step map $f:S\to S$; "run for $n$ steps" is $f^{\,n}$ (the $n$-fold composition). A parallel array assigns each site $i$ its own map $f_i$ and updates all sites at once. A network lets a site's update read its neighbors — and, crucially, may have no global clock, which is where the trouble for relativity begins (§10). The formalizable kernels are the algebra of these constructions: the serial semigroup law $f^{\,m+n}=f^{\,m}\circ f^{\,n}$ T1, and the fact that the parallel array's evolution factors through its components — the precise meaning of "the sub-computers run independently."
The independence theorem is a statement that the iteration functor commutes with the product: for a family $\{f_i:S_i\to S_i\}$, the diagonal action on $\prod_i S_i$ satisfies $\big(\textstyle\prod_i f_i\big)^{n}=\prod_i f_i^{\,n}$ pointwise. Cardinality of the homogeneous array, $\#(S^{\,\mathrm{Fin}\,n})=(\#S)^n$, is the finite-combinatorics shadow of metaphor 7's "infinite componentry": a finite homogeneous array has a finite, exactly-counted configuration space, so unbounded capacity requires genuinely infinite componentry — whose physical cost §7 then bounds. The network with no global clock is the structural carrier where the independence factorization provably fails; it is also where Lorentz covariance becomes the central obstruction (Mattingly's review of modern Lorentz-invariance tests [26]T1 catalogues the constraints).
def parallelRun {ι : Type*} {S : ι → Type*} (f : ∀ i, S i → S i) :
(∀ i, S i) → (∀ i, S i) :=
fun s i => f i (s i)
theorem parallelRun_iterate {ι : Type*} {S : ι → Type*} (f : ∀ i, S i → S i)
(n : ℕ) (s : ∀ i, S i) (i : ι) :
(parallelRun f)^[n] s i = (f i)^[n] (s i) := by
induction n generalizing s with
| zero => rfl
| succ n ih => rw [Function.iterate_succ_apply, Function.iterate_succ_apply, ih]; rfl"It from bit" says that, deep down, everything might be yes/no answers. Two pieces of that are exactly true. First: a single logical operation — NAND, "not both" — is enough to build every other logical operation. One rule generates all of logic. Second: a string of bits and a number a computer could pick out of a list are really the same object wearing two hats. Information and computation are, at the finite level, interchangeable.
Metaphor 25 — "reduce to Boolean logic" — has a precise kernel: functional completeness. The Sheffer stroke $a\mathbin{\uparrow}b=\lnot(a\wedge b)$ generates negation, conjunction, and disjunction, hence (with $\{\lnot,\wedge,\vee\}$ generating all Boolean functions) every Boolean function whatsoever. Metaphor 34 — "information and computation are fundamentally indistinguishable" — has the kernel of a bijection: a length-$n$ bit-string and an element of $\{0,\dots,2^n-1\}$ encode each other, $ \{0,1\}^{n}\;\cong\;\mathbb{Z}/2^n. $ Metaphors 8 and 24 ("reduce to mathematics / to a single calculation") lean on a real but subtler fact — that algorithmic information content (Kolmogorov complexity) is machine-independent up to a constant [19]T1, already proved in PhysProof and cited here rather than re-derived.
Functional completeness of $\{\uparrow\}$ is a statement about the free Boolean algebra on $n$ generators; the two-element case is decidable, and our Lean proof discharges it by exhaustive evaluation (by decide). The information–computation equivalence is the standard binary encoding $\mathrm{Fin}\,n\to\mathrm{Fin}\,2$ folded into $\mathrm{Fin}\,2^n$, an explicit Equiv. The deep version of metaphor 34 — that information, computation, energy, mass, space and time are "in a similar way equivalent" — is exactly where the honest line falls: equinumerosity of finite encodings is necessary for an identity claim and nowhere near sufficient. Timpson's monograph [28]T2 argues "information" is an abstract noun that names no physical substance, so the strong ontological reading is a category mistake — the principal counterweight to literal "it from bit."
def nand (a b : Bool) : Bool := !(a && b)
theorem nand_functional_completeness :
∀ a b : Bool,
(!a = nand a a) ∧
((a && b) = nand (nand a b) (nand a b)) ∧
((a || b) = nand (nand a a) (nand b b)) := by
decideMaybe space is a grid and time ticks, and the universe is a giant pattern of pixels updating by a fixed rule — a "cellular automaton," the picture Konrad Zuse drew in 1969 [21]. The deepest exact fact here is about finiteness: if the universe has only finitely many possible states and evolves by a fixed deterministic rule, it cannot keep producing genuinely new arrangements forever. By sheer counting it must eventually revisit a state — and from then on it loops. A finite, clockwork cosmos repeats.
Metaphor 46 — "totally finitistic" — is the load-bearing kernel. For any map $g:S\to S$ on a finite set $S$, the orbit $x,g x,g^2x,\dots$ cannot be injective (pigeonhole), so there exist $m$ and $p>0$ with $g^{\,m+p}(x)=g^{\,m}(x)$: the orbit is eventually periodic. If $g$ is moreover reversible (injective), the transient vanishes and the orbit is purely periodic, $g^{\,p}(x)=x$ — the discrete shadow of the Poincaré recurrence theorem. Cellular automata (28) and lattices (30) reuse PhysProof's existing result that a reversible CA's evolution is injective, so no information is destroyed. Digital approximation of the analogue (15) is the density of $\mathbb{Q}$ in $\mathbb{R}$: any real is within $\varepsilon$ of a finite (rational) description.
Eventual periodicity is the statement that any endomorphism of a finite object has a finite orbit closure; with injectivity it is an automorphism of finite order on each orbit. The map to physics is an idealization: quantum recurrence on an infinite-dimensional Hilbert space is only approximate and astronomically slow, and the "state space is finite" premise is metaphor 46 itself, which we do not settle — we prove its consequence. A methodological aside that became a real correction: the existing PhysProof CA module exports a theorem named CA_deterministic whose body is, by its own lint annotation, the vacuous tautology evolve c n = evolve c n. We refused to cite a tautology as content and proved the lemma the name was promising instead — that one step of evolution is one application of the global rule.
theorem finitism_eventual_periodicity {S : Type*} [Finite S] (g : S → S) (x : S) :
∃ m p : ℕ, 0 < p ∧ g^[m + p] x = g^[m] x := by
obtain ⟨a, b, hab, hfx⟩ :=
Finite.exists_ne_map_eq_of_infinite (fun n : ℕ => g^[n] x)
rcases lt_or_gt_of_ne hab with h | h
· exact ⟨a, b - a, Nat.sub_pos_of_lt h, by rw [Nat.add_sub_cancel' h.le]; exact hfx.symm⟩
· exact ⟨b, a - b, Nat.sub_pos_of_lt h, by rw [Nat.add_sub_cancel' h.le]; exact hfx⟩sorry). Does NOT establish — that physical state space is finite; that premise is metaphor 46 itself, left open. We prove what finitism would entail, not that the world is finite."Reversible" can mean three things: the dynamics never loses information (no two states merge), never makes a state unreachable, and can always be run backward. On a finite state space these three are the same thing. A finite clockwork that never destroys information automatically can be rewound and reaches everything — the toy-model echo of why quantum evolution is reversible.
For a self-map $f:S\to S$ of a finite set, $\textsf{injective}\iff\textsf{bijective}\iff\textsf{surjective}$. Injectivity is "no information loss," surjectivity is "every state reachable," bijectivity is "invertible" — and finiteness fuses them. This is the discrete shadow of unitarity (quantum) and Liouville's theorem (classical). The Fredkin and Toffoli gates — universal reversible logic [20]T2 — are concrete finite instances, already proved bijective in PhysProof and reused here. Synchrony (22) is the parallel/global step; asynchrony (35) updates one node at a time; indeterminism (36) is precisely the failure of the transition relation to be a function.
The trichotomy is Finite.injective_iff_surjective packaged with its bijective corollary; finiteness is essential, and the unilateral shift on $\ell^2$ is the standard infinite-dimensional counterexample (injective, not surjective) — so the clean equivalence is the finite idealization of physical reversibility, where unitaries on infinite-dimensional Hilbert space are the real objects. This section is also where the essay's own honesty method earned its keep: writing it, we nearly cited the vacuous CA_deterministic from §5 as "determinism, formalized." A citation is a claim too; the discipline that catches a fake theorem must also catch a fake reuse.
theorem finite_reversible_trichotomy {S : Type*} [Finite S] (f : S → S) :
(Function.Injective f ↔ Function.Bijective f) ∧
(Function.Surjective f ↔ Function.Bijective f) :=
⟨⟨fun h => ⟨h, (Finite.injective_iff_surjective).mp h⟩, fun h => h.injective⟩,
⟨fun h => ⟨(Finite.injective_iff_surjective).mpr h, h⟩, fun h => h.surjective⟩⟩Metaphor 7 dreams of a computer of "infinite power." Physics says no — and says so with numbers. Erasing one bit of information must release at least a fixed dribble of heat (Landauer). A system with limited energy can only flip between truly different states so fast (Margolus–Levitin). A region of space can only hold so much information at all, set by its surface area, not its volume (Bekenstein, holography). The universe-as-computer has a finite, calculable budget.
Three ceilings. Landauer [7]T1: erasing a bit costs at least $k_B T\ln 2$ of heat — confirmed to high precision (Bérut 2012 [10]; Jun 2014 [11]). Margolus–Levitin [16]T1: a state of mean energy $E$ above its ground state needs time $\tau\ge \pi\hbar/2E$ to reach an orthogonal (perfectly distinguishable) state, so the rate of distinct operations is at most $2E/\pi\hbar$. Bekenstein / holography [12]T1[13]T2: a bounded region's entropy obeys $S\le 2\pi k_B R E/\hbar c$, and black-hole entropy scales as area, $S=k_B c^3 A/4G\hbar$. Lloyd assembled these into the "ultimate laptop" and a budget for the whole universe — about $10^{120}$ operations on $10^{90}$ bits [17][18]T2.
Our Lean kernel derives the operation-time floor directly from PhysProof's structural Margolus–Levitin bound $E\cdot\tau\ge \pi\hbar/2$: dividing by $E>0$ gives $\tau\ge (\pi\hbar/2)/E$, a strictly positive minimum — there is no infinite-speed computer at finite energy. This theorem is honestly axiom-discharged: it rests on a named physical axiom (the ML bound, whose retirement awaits Stone's theorem and spectral calculus for unbounded Hamiltonians in the underlying library), not on a sorry. Running #print axioms shows the ML axiom and Lean's three standard axioms, nothing else — so we guard it with assert_no_sorry, not assert_pure_kernel (which it would correctly fail). The footprint is the honesty certificate. The holographic side [14][15] remains T2: the covariant entropy bound is well-tested, but holography as a principle is unproven.
landauer_jun_szilard_normalized_agree [11]).BekensteinBousso.lean.theorem wheeler_finite_energy_bounds_orthogonalization_time (e : OrthogonalizingEvolution) :
piHbarHalfJouleSeconds / e.meanEnergyJoules ≤ e.durationSeconds := by
have hE := e.meanEnergyJoules_pos
have h := margolus_levitin_action_lower_bound e
rw [div_le_iff₀ hE]
linarith [h, mul_comm e.meanEnergyJoules e.durationSeconds]sorry). Does NOT establish — the ML bound from first principles (that is the named axiom), nor a bound on all conceivable processes — only on orthogonalizing steps.The wildest metaphors live here: the universe as a program running on some "real" computer (20), as a simulation (19), as something with a model of itself (18), even as "half-mental" (43). One piece is exact and reassuring: if a simulation gets a single step right — if it faithfully mirrors one tick of the real dynamics — then it gets the entire history right, forever, by induction. Fidelity at one step propagates to all steps. The rest of this cluster is where honesty means not writing a theorem.
Call $h:A\to B$ a simulation of $f$ by $g$ if it intertwines one step, $h\circ f=g\circ h$ (a semiconjugacy). Then it intertwines every number of steps: $h(f^{n}a)=g^{n}(h\,a)$. That is the precise content of "simulated with arbitrarily great accuracy" (19): one-step fidelity is enough. The existence half — that a countable, finitely-describable world admits a faithful encoding into $\mathbb{N}$ — is the static side of the Church–Turing–Deutsch principle [22]T2. But the self-model (18), the participatory/mind metaphors (26, 43), and the simulation hypothesis (Bostrom [27]T3) have no tractable formal core. We give them honest structural carriers — a SelfModel, a ProgrammaticProjection — and a plain admission, not a manufactured theorem.
$\textsf{simulation\_preserves\_orbits}$ is the functoriality of iteration along a semiconjugacy; it presumes the intertwining map exists and says nothing about whether physical law admits one (the Church–Turing–Deutsch conjecture). The self-model has a genuine formal cousin in PhysProof's AWARENESS condition A1 (alphabetization closure: a system whose own describer is a term of the alphabet it describes) — explicitly weaker than phenomenal mind, which is exactly why metaphors 26/43 stay in the philosophical bucket. The simulation hypothesis is metaphysics, not physics; and a literal simulation on a fixed lattice collides with the Lorentz-invariance constraints of §10. The honest move is to formalize the consequence-of-being-a-simulation while declining to assert the world is one.
def Simulates {A B : Type*} (h : A → B) (f : A → A) (g : B → B) : Prop :=
∀ a, h (f a) = g (h a)
theorem simulation_preserves_orbits {A B : Type*} (h : A → B) (f : A → A) (g : B → B)
(hsim : Simulates h f g) (n : ℕ) (a : A) :
h (f^[n] a) = g^[n] (h a) := by
induction n with
| zero => rfl
| succ n ih => rw [Function.iterate_succ_apply', Function.iterate_succ_apply', hsim, ih]Every metaphor receives one honest status, compiled into Lean as classifyMetaphor, and a machine-checked omnibus proves the classification is surjective — all four buckets are genuinely used. The tally: 17 genuine kernel, 9 reuse, 11 structural, 11 philosophical. The content is in the anchors, not in the surjection — that is the reading-guide discipline this project inherited from its RevElephant taxonomy.
| # | Metaphor (abbreviated) | Status | Anchor / why | Tier |
|---|---|---|---|---|
| 1 | serial / Turing-like | kernel | serialRun_add | T2 |
| 2 | parallel array of sub-computers | kernel | parallelRun_iterate | T2 |
| 3 | completely parallel machine | reuse | parallelRun | T2 |
| 4 | hybrid serial + parallel | structural | product carrier | T3 |
| 5 | hierarchy / network | structural | NetworkMachine | T3 |
| 6 | finite / infinite set of computers | kernel | homogeneous_array_card | T2 |
| 7 | infinite power / sophistication | kernel | …orthogonalization_time (refutes) | T1 |
| 8 | reduce to math / numbers / order | reuse | Kolmogorov invariance_theorem | T1 |
| 9 | reduce to information / symbols | philosophical | too broad to formalize | T3 |
| 10 | instructible / programmable | structural | Programmable | T2 |
| 11 | reduce at higher / lower level | philosophical | no formal core | T3 |
| 12 | equivalent if treatment elaborate | kernel | simulation_exists_injective_encoding | T2 |
| 13 | homogeneous / heterogeneous set | kernel | heterogeneous_array_card | T2 |
| 14 | digital / binary computer | reuse | info_computation_card | T2 |
| 15 | analogue, self-similar | kernel | digital_approximates_analogue | T1 |
| 16 | mechanical / deterministic / reversible | kernel | finite_reversible_trichotomy | T1 |
| 17 | computer-like on occasion | structural | Programmable | T2 |
| 18 | central model of itself | structural | SelfModel (cf. AWARENESS A1) | T3 |
| 19 | simulated with arbitrary accuracy | kernel | simulation_preserves_orbits | T2 |
| 20 | superficial pattern / projection | structural | ProgrammaticProjection | T3 |
| 21 | all phenomena are computers | philosophical | no formal core | T3 |
| 22 | clock-like / synchronized | reuse | parallelRun (synchronous) | T2 |
| 23 | laws controlled by higher laws | structural | AdminHierarchy | T3 |
| 24 | reducible to computation | reuse | Lloyd capacity [18] | T2 |
| 25 | reduce to Boolean logic | kernel | nand_functional_completeness | T1 |
| 26 | a mind / mind-like | philosophical | no tractable core | T3 |
| 27 | computer-like memory | structural | Memory | T2 |
| 28 | cellular automata | reuse | reversible_CA_information_conservation | T2 |
| 29 | computational illusion | structural | ProgrammaticProjection | T3 |
| 30 | lattice / quantized spacetime | kernel | ca_evolve_globalRule_comm | T2 |
| 31 | quantum numbers reduce to one | philosophical | physics, no kernel here | T3 |
| 32 | a single iterative operation | reuse | recursive_iteration_semigroup | T2 |
| 33 | iterative / recursive processes | reuse | recursive_iteration_semigroup | T2 |
| 34 | information ⇔ computation | kernel | infoComputation_bijective | T2 |
| 35 | asynchronous computer | kernel | asyncStep_eq_of_ne | T2 |
| 36 | statistical / indeterministic | kernel | funRel_deterministic | T2 |
| 37 | lifelike / biological | philosophical | no formal core | T3 |
| 38 | total computational reliance | philosophical | sociological claim | T3 |
| 39 | ultimate computers unknown | philosophical | open-ended, no core | T3 |
| 40 | cognitive processes | philosophical | no tractable core | T3 |
| 41 | holonomic / content-addressable memory | structural | Memory | T3 |
| 42 | anastomotic causal network | philosophical | causal-set program [25] | T2 |
| 43 | half-mental, "addressed" | philosophical | no tractable core | T3 |
| 44 | controlled from a distance | structural | AdminHierarchy | T3 |
| 45 | administrative hierarchy | structural | AdminHierarchy | T3 |
| 46 | totally finitistic | kernel | finitism_eventual_periodicity | T2 |
| 47 | centralized / bounded | reuse | Bekenstein bound [12] | T1 |
| 48 | time-asymmetric process | kernel | finitism_periodic_of_bijective | T3 |
theorem classifyMetaphor_uses_all_buckets : Function.Surjective classifyMetaphor := by
intro s
cases s with
| hasKernel => exact ⟨⟨0, by norm_num⟩, rfl⟩ -- metaphor 1
| reuseCited => exact ⟨⟨2, by norm_num⟩, rfl⟩ -- metaphor 3
| structuralOnly => exact ⟨⟨3, by norm_num⟩, rfl⟩ -- metaphor 4
| philosophical => exact ⟨⟨8, by norm_num⟩, rfl⟩ -- metaphor 9A trustworthy essay on this metaphor must give the strongest objections at least as much room as the enthusiasms.
The Church–Turing–Deutsch principle [22]T2 says every finitely-realizable physical system can be simulated by a universal computer — a statement about description. Sliding from "is describable as a computation" to "is a computation" is the move most philosophers of physics reject. Description is not constitution; a weather model is not weather.
The sharpest physical objection. A fundamental lattice or minimum length generically modifies the dispersion relation and breaks Lorentz symmetry, and the experimental bounds on such violation are extraordinarily tight — Mattingly's peer-reviewed review [26]T1 catalogues the constraints across the standard-model sector. So the most literal versions of metaphors 28/30 (spacetime as a cellular automaton or lattice) face severe empirical pressure; 't Hooft's cellular-automaton interpretation of quantum mechanics [24]T3 takes the program seriously but remains a contested minority position, leaning on superdeterminism to evade Bell's theorem. Our discreteness theorems are deliberately stated about abstract lattices $\mathbb{Z}\to S$ — they carry no commitment that physical spacetime is one.
Landauer caps the cost of erasure; Bekenstein caps the capacity of a region; Margolus–Levitin caps the rate of distinguishing operations. Every one of these is a bound on physical processes described information-theoretically. None of them makes reality be information. Timpson [28]T2 argues that "information" is an abstract noun naming a structure, not a stuff — so "it from bit," read as substance-ontology, mistakes a way of describing the world for what the world is made of. The information-theoretic limits are real physics; the ontological inference is a separate, much weaker step.
Every embedded proof above carries its own gap; gathered, the pattern is uniform. The finite-state theorems (16, 46) assume finiteness — exactly the premise the metaphors only posit. The simulation theorem (19) assumes the intertwining map exists. The thermodynamic bound (7) rests on a named physical axiom, honestly disclosed. The classification omnibus describes our bookkeeping, not the cosmos. In every case the Lean kernel certifies an idealization; the distance from idealization to Wheeler's physical claim is the content we have tried hardest to keep visible.
Wheeler's gift was never an answer; it was a machine for generating good questions, and the forty-eight readings are its output. Treated as ontology, most of them overreach. Treated as a forcing function — which information-theoretic limits are physical law, and which inferences are category mistakes — the list is genuinely productive: it points straight at Landauer, Bekenstein, Margolus–Levitin, the Church–Turing–Deutsch principle, and the Lorentz-invariance problem, each a real result or a real open question.
The tier system is the honest way to hold a metaphor this generative: keep the established physics, flag the contested interpretations, and call speculation speculation. Compiling the genuine kernels to machine-checked Lean adds one more discipline on top — it forces us to say exactly what each metaphor would mean if it were a theorem, and then to admit, in the gap beneath each green checkmark, everything it still does not say. The list, in the end, is not Wheeler's; it is a Gunkel ideonomic catalogue filed in Wheeler's papers. But the questions are recognizably Wheeler's, and they are still worth asking — carefully.
All sources below were verified against primary or authoritative records (publisher pages, DOIs, arXiv, ADS, APS catalogue) during a dedicated research pass; ✓ verified marks a confirmed locator. Page ranges that vary across printings are flagged in the project's research log.