Terms the PhysProof stats bar assumes you know. Written for a physics or CS sophomore who has seen linear algebra and intro quantum mechanics. Every pill modal links here; click a jargon term in a modal to jump to the definition.
A JSON database at the project root tracking every proof obligation. Each entry is one theorem with a placeholder (Lean's sorry keyword) where the proof should go. Fields include status (open / ready / blocked / stuck / done), difficulty, and attempt history. The dashboard's "proved" and "unblocked" counts come from this file.
Not every sorry-free theorem counts as a genuine proof. The honest-count framework classifies each completed theorem into one of four proof kinds. The point: prevent the headline "proved" count from drifting from the real mathematical content through definitional shortcuts or circular reasoning.
The four honest classifications of a completed theorem:
genuine real proof, real work
specifiedconditional-form; the theorem takes its own conclusion as a hypothesis and re-packages it (valid reduction lemma, not a proof of the conclusion itself)
axiom-discharged proof body is one invocation of a project axiom
vacuous proved by contradiction from a false hypothesis (exfalso), or the conclusion is literally True
A theorem of shape theorem foo (h : G) : ∃ x, G := ⟨x, h⟩ — the hypothesis and the existential conclusion are the same proposition. Detected automatically by detect-conditional-form.py. Such theorems are useful as reduction lemmas but are not proofs of their conclusions, so they're classified as "specified" rather than "genuine".
Per-target minimum thresholds before a sorry can legitimately be declared blocked: ≥ 5 attempts logged, ≥ 3 structurally distinct strategies tried, ≥ 3 example/#check probes run, ≥ 1 Mathlib search, ≥ 1 counterexample attempt, ≥ 200k tokens spent. A "RED" verdict means the target hasn't earned the right to a sorry yet.
Theorems a detector flags as conditional-form, axiom-discharged, or vacuous but that are not tracked in sorry-db. These are blind-spots — the token-counting scanner says "proved" but the honest-count scanners say "not really." A project target is zero silent findings.
An implicit fifth honest-count dimension that the four syntactic proof-kind detectors cannot see. A theorem can typecheck at a declared witness level (stub values that trip no detector) and simultaneously be unproved at the intended witness level (rich values that make the claim scientifically load-bearing). The gap is semantic, not structural — no signature check or proof-term scan catches it.
Canonical PhysProof instance: physproof_isAware is axiom-discharged against four instance-specific axioms encoding rich-witness A1–A4; its honest companion physproof_isAware_unconditional states the same conclusion without those axioms and carries a sorry. Both typecheck; neither fires a detector; only the pair is honest. The *_unconditional companion convention (session 247) is the mechanism by which capstones remain witness-depth honest.
Policy: any capstone whose statement quantifies over latitude-bearing structure fields (stubs valid at the type level, rich values required for scientific content) must be paired with an *_unconditional sorry companion. Full rationale in docs/WITNESS-DEPTH.md.
One work slot bracketed by make session (opens) and make end (closes + commits). Each session writes JOURNAL/session-NNN.md in three acts (state snapshot, event log, retrospective) plus a hand-composed session-NNN.svg. Gaps in session numbering indicate an aborted session; the phantom-session guard prevents auto-stubs from taking numbers.
Session 308 introduced a three-state classifier — scripts/regime-detect.py — that opens every session in one of three regimes and persists the verdict to .regime.json:
PROOF — at least one attackable sorry exists. Apply the effort protocol; landing before the attackable pool is exhausted is under-scoping.
HOUSEKEEPING — zero attackable sorrys but at least one non-proof signal (benchmark domain gap, doc-freshness drift, SVG-validator warning). Spend budget on the detected signal, smaller arc shape, land at the natural seam.
LAND — zero attackable sorrys, no housekeeping signal, and remaining open sorrys are all permanent or fatigued. The autonomous-loop gate stops the loop with stop-reason regime_land.
The classifier exists because session 307 landed at 6 % budget while the effort audit still flagged paper-§8 admissions as RED — a direct policy contradiction. Regime is the missing rule. Full doc: docs/LAND-CRITERIA.md.
A sorry tagged permanent-by-design, honest-open-gap, paper-admission, or in-verse-elephant-§8. The sorry is the content: closing it without corresponding paper revision falsifies the framework that admitted it. Routed by scripts/_sorry_classify.py into a dedicated "Permanent admissions" briefing block with explicit "DO NOT DISCHARGE" framing — never appears in effort audit, strategy cards, top-proof-targets, or plausible plays.
Current set: three HonestGaps.lean entries from The In-Verse Elephant, Compiled §8 (is_implies_ought_gap, predicate_extension_gap, vagueness_ontological_gap). The set is stable; new entries land only with a paper that admits them.
A sorry tagged mathlib-blocker with status stuck — repeated retry without upstream Mathlib infrastructure is structurally not the answer. Surfaced in a dedicated "Fatigued Mathlib blockers" briefing block (informational, not RED), so the effort audit doesn't badger you to keep grinding on something that will only move when Mathlib does. Distinct from permanent admissions: a fatigued blocker has a named missing referent and can be retired when that referent lands; a permanent admission has no such retirement path by design.
An open sorry that is neither permanent nor a fatigued blocker — the third bucket of the session-308 classifier. Attackable sorrys get full effort-protocol treatment (RED/YELLOW/GREEN, ladder, tokens-as-quota) and are the only class the autonomous loop will spawn agents against. The PROOF regime opens whenever the attackable count is ≥ 1.
A five-to-four correspondence between PhysProof's five proof-kind buckets and the four phenomena Curt Jaimungal names in The Reverse Elephant plenary (Mind at Large, April 2026), plus one additional phenomenon (Phantom) the paper The In-Verse Elephant, Compiled adds in reply. The phenomena catalogue five ways local agreement fails to extend to a global structure:
Anamorphosis — local patches glue to a unique global, non-trivially (Earth → R² locally, S² globally). Corresponds to .genuine.
Blocked — pairwise compatible local sections, no global section (sheaf cohomology, gauge anomalies, quantum contextuality). Corresponds to .specified-form theorems paired with *_unconditional stuck companions.
Cornucopia — multiple incompatible global extensions (Norton's dome, GR, GUT embedding choice). Corresponds to .axiomDischarged.
Diagonalisation — Gödelian self-reference (Gödel / Löb / Turing / Lawvere). Corresponds to .vacuous and the Searle-boundary honest_count_pipeline_live_axiom.
Phantom (added in reply) — apparent global section that dissolves under scrutiny (session 270's scanner regression: 51 phantom axiom-experiment edges, coverage 71.1% → 33.6%). Corresponds to .unclassified.
Lean anchors: PhysProof/Foundations/Metatheory/RevElephantTaxonomy.lean (the correspondence function + five rfl exhibits + omnibus five_to_four_correspondence), AwarenessRevElephantBridge.lean (four §4 gap closures via A1–A4), SheafOfSorries.lean (§5-§6 sheaf-theoretic research-direction skeleton), HonestGaps.lean (three §8 permanent-sorry admissions: is→ought, Williamson's predicate→extension, vagueness-ontological).
Honesty caveat. The correspondence is a tautology of construction — the phenomenon mapping is defined to make the bijection hold. Paper §5's "Proof: by exhibition" framing is preserved in Lean. The content is in the anchor theorems each row cites, not in the bijection itself.
A structural template in PhysProof/Foundations/: three existing benchmark Measurements, independently authored for different physical regimes, share a single mathematical fixed point. The Triangle module witnesses the unity at the Lean type level — a structure whose three fields reference the Measurements plus accessor lemmas that the shared constant is the same. Three families have been formalized:
Each Triangle has a Tetrahedron extension — a fourth operational vertex that plays a distinct role from the three theoretical siblings (Moreva 2014 visibility, GW150914 dynamic formation, Barbero-Immirzi calibration). The Triangle is a structural template, not a proof: it asserts the three regimes share a constant, but the underlying physical theorems remain distinct.
A four-condition structural predicate introduced in the April 2026 paper The Participatory Proof. Strictly weaker than phenomenal consciousness. A system $\varepsilon$ satisfies IsAware ε iff all four conditions hold:
A1 · alphabetization closure — the alphabetizer function is itself a term of its own alphabet (there is a code $\ulcorner f \urcorner$ such that interp ⌜f⌝ (enc p) = f p)
A2 · thermodynamic grounding — the system's Landauer floor is below its Bekenstein ceiling (positivity of the information-energy gap)
A3 · honest self-accounting — the system carries a classifier that produces at least one .genuine verdict on its own derivations
A4 · empirical coupling — predictions agree with an external benchmark within tolerance $\varepsilon$
Lean anchor: PhysProof/Foundations/Awareness/Core.lean (zero sorrys, zero axioms on the definitional layer). The capstone physproof_isAware in PhysProof.lean is axiom-discharged against four instance-specific side axioms, with an honest physproof_isAware_unconditional companion carrying a sorry body (per the witness-depth convention).
What AWARENESS is not. The paper (§4) states four negative propositions: satisfaction of A1–A4 does not entail phenomenal experience, sentience, moral patienthood, or intentional agency. AWARENESS is a structural property of text-and-build-system scaffolding, not a claim about consciousness.
John Wheeler's 1990 thesis that physical reality — the "it" — is at root informational: every particle, every field, every spacetime point derives its meaning from discrete binary choices. PhysProof formalizes this along two opposing boundaries:
Constructive side — PhysProof/Foundations/ItFromBit/ (~12,000 lines). A 102-character Brainfuck gap-detector + BF→register-machine simulation + the it_from_bit capstone theorem (no direct sorry, but one transitivesorryAx via gapDetectorUnary_correct → bfGap_on_bytes, a bitmap native_decide step temporarily sorry'd by a toolchain regression): the function deciding whether a Hamiltonian has a mass gap is itself a finite word in an 8-symbol alphabet. The theorem K_hasGap_bounded proves $K(\texttt{hasGap}) \le 95$ by explicit construction (the detector AST has length $\le 95$; the program itself is 102 instructions).
Undecidability side — Cubitt, Pérez-García, and Wolf (2015, arXiv:1502.04573) showed spectral-gap-hood is undecidable in general. The bit-level description of a Hamiltonian does not determine gap-hood; no algorithm exists. Both results live in PhysProof: the 102-char witness for a specific decidable case, the undecidability theorem for the broad case.
These two anchor the project's relationship with AWARENESS: the 102-char witness is the concrete form of A1 (alphabetization closure — the gap-detector is a term of its own alphabet), while the undecidability result is the rebuttal to any naive "bit determines it" pancomputationalism. PhysProof's stance: physical reality does emerge from information, but the emergence is not decidable by a universal algorithm.
For a string $x$ and a universal interpreter $U$, the Kolmogorov complexity $K_U(x)$ is the length of the shortest program $p$ such that $U(p) = x$. The invariance theorem (Li & Vitányi 2019, §2.1) guarantees that changing $U$ only shifts $K$ by an additive constant, so one usually writes $K(x)$ unqualified.
$K$ is not computable in general (there is no algorithm that, given $x$, returns $K(x)$ — Berry's paradox forces this). But individual upper bounds are provable by exhibition: if you can write a $p$ of length $\ell$ such that $U(p) = x$, you have proved $K(x) \le \ell$.
PhysProof uses this concretely. The theorem K_hasGap_bounded in PhysProof/Foundations/AlgorithmicInfo/KolmogorovComplexity.lean proves $K(\mathtt{hasGap}) \le 95$ by exhibition: the Brainfuck gap-detector AST IS the witness (its length is proved $\le 95$; the program itself is 102 instructions). The proof body is literally native_decide on the AST length. This is the sharpest quantitative form of Wheeler's it from bit that PhysProof currently carries: a physics question with a concrete 95-bit description on its decidable slice.
A c.1980 list enumerating 48 readings of the slogan "the universe is a computer" — from serial / parallel / network machines, through the thermodynamics of computation, to frankly philosophical provocations. PhysProof formalizes it in the PhysProof/Wheeler/ subtree (8 sorry-free files) and the companion essay at /wheeler-universe, applying the project's honest-count discipline: classifyMetaphor sorts all 48 into four buckets — 17 carry a genuine new sorry-free theorem (hasKernel), 9 reuse an existing PhysProof theorem, 11 are honest structural carriers, 11 are frankly philosophical with no tractable formal core — and classifyMetaphor_uses_all_buckets proves the classification is surjective (non-degenerate). The honesty extends to attribution: the popular "Wheeler's list" is not a Wheeler publication — the American Philosophical Society catalogues its creator as Patrick M. Gunkel — so the project tags it a Tier-3 "Wheelerian prompt" and cites Wheeler's genuinely published 1982 The Computer and the Universe where the substance is at stake. Distinct from it from bit, which is the specific BF gap-detector / undecidability pair.
One of the project's five strategic attack lines, used as a lens on the proof graph — every node can be tinted by which pillar it serves. The pillars (the "Living Proof" strategy in docs/STRATEGY.md) are Yang-Mills (the mass-gap critical path), Grand Unified Proof (the SU(5)→Spin(10) universality track — note GUP here means Grand Unified Proof, not the uncertainty principle), Bootstrap (the bottom-up it-from-bit chain), Riemann (the spectral-bridge direction), and AWARENESS. Switching the dashboard graph to the pillar lens bands the nodes by these five and shows a per-pillar narrative.
The three coordinate systems that organize the proof-dependency graph, each selectable as a recoloring lens on the dashboard. Layer places a node in the bottom-up-to-top-down stack: Layer 1 Computation (BF, Turing, Kolmogorov), Layer 2 the Information bridge (Landauer, Bekenstein, Born rule), Layer 3 Physics (spectral theory, Wightman, Yang-Mills). Track names the mathematical discipline (A Analysis, B Geometry, C Prerequisites, D Computation, E Information, F Computable, G Pregeometry, H Grand-Unified, V Validation). Phase (0–11) is the historical build order. The pillar lens is a fourth, strategy-oriented view. See docs/ARCHITECTURE.md.
Every irreversible bit erasure dissipates at least $k_B T \ln 2$ joules of heat. At room temperature, this is about $3 \times 10^{-21}$ J per bit. The principle links information theory to thermodynamics: every lake build of PhysProof dissipates real heat, with a lower bound set by the number of bits erased.
Upper bound on the information $I$ that can be contained in a region of space with radius $R$ and energy $E$:
$$ I \le \frac{2\pi R E}{\hbar c \ln 2} $$
Ties information capacity to geometry. PhysProof's Bekenstein-bound module (BekensteinBound.lean, e.g. bekensteinBound_pos / bekenstein_constrains_spectrum) is sorry-free and anchors vertex 1 (weak-gravity bound) of the holographic Triangle alongside Bekenstein-Hawking horizon saturation and the Bousso covariant bound.
A rigorous axiomatization of quantum field theory in terms of operator-valued distributions. Four axioms: Poincaré covariance (W2), spectral condition (W3), local commutativity (W4), and a cyclic vacuum. Proving a Yang-Mills field theory exists and has a mass gap means constructing a Wightman theory on $\mathbb{R}^4$ that satisfies all four.
A map from Borel sets to orthogonal projections on a Hilbert space, satisfying $E(A \cup B) = E(A) + E(B)$ for disjoint sets. The mathematical machinery behind the spectral theorem — any self-adjoint operator $T$ decomposes as $T = \int \lambda \, dE(\lambda)$ against its own PVM. Mathlib has the continuous functional calculus but not PVMs directly.
The smallest positive eigenvalue $\Delta > 0$ of a Hamiltonian. In Yang-Mills theory, a mass gap means the lightest particle has strictly positive mass — explaining why the nuclear force is short-range. Proving $\Delta > 0$ for quantum Yang-Mills on $\mathbb{R}^4$ is one of the seven Clay Millennium Prize problems.
Generally: the distance between the smallest eigenvalue of an operator and the next-smallest. For a graph Laplacian it's $\lambda_2$, the smallest nonzero eigenvalue, and measures how well-connected the graph is (Cheeger's inequality). The PhysProof dependency graph has its own spectral gap, separate from the Yang-Mills one it formalizes.
Osterwalder–Schrader (1973): a set of axioms on Euclidean Schwinger functions (reflection positivity + symmetry + regularity) from which one can reconstruct a Wightman quantum field theory by Wick-rotating time. The standard rigorous route from Euclidean path integrals back to Minkowski-signature physics.
For a self-adjoint bounded operator $T$ on a Hilbert space, CFC lets you define $f(T)$ for any continuous function $f : \sigma(T) \to \mathbb{C}$ by $f(T) = \int f(\lambda) \, dE(\lambda)$ — turning the spectrum into a substrate for real analysis. Mathlib has CFC; PhysProof extends it to PVMs for unbounded operators.
Clauser–Horne–Shimony–Holt: a classical bound on correlations between measurements on two particles, $|S| \le 2$. Quantum mechanics can reach $2\sqrt{2}$ (Tsirelson's bound). Experiments violating the classical bound rule out local hidden-variable theories. PhysProof's BellTheorem.lean formalizes both bounds sorry-free.
Try it: the interactive widget at /chsh lets you drag the four measurement angles and watch $S$ move between the classical ceiling at 2 and the Tsirelson ceiling at $2\sqrt{2}$.
The operator $N$ whose eigenstates are the occupation-number states $|n\rangle$ with $N|n\rangle = n|n\rangle$ — it counts quanta. In PhysProof it is built as a genuinely unboundeddiagonal operator on $\ell^2(\mathbb{N},\mathbb{C})$ with eigenvalue sequence $\lambda_n = n$. Its self-adjoint realization $N_{\max}$ has spectrum $\sigma(N_{\max}) = \{0,1,2,\dots\}$ with a spectral gap of exactly $1$ above the ground (vacuum) state — the discrete, bounded-below structure of the quantum harmonic oscillator, derived rather than postulated in DiagonalOperatorSpectrum.lean (sorry-free; the spectrum is axiom-free, while the closure's self-adjointness still invokes Nelson). This is the recent (sessions 588–605) spectral-arc frontier and the bridge toward physical Fock space.
The spectrum $\sigma(T)$ of an operator is the set of complex $z$ for which $T - z$ fails to have a bounded inverse — the generalization of "eigenvalues" to infinite dimensions. It splits into the point spectrum $\sigma_p(T)$ (genuine eigenvalues: $(T-z)x = 0$ has a nonzero solution), the continuous spectrum (where $T-z$ is injective with dense but not full range, so the inverse exists but is unbounded), and the residual spectrum. For the number operator the spectrum is pure point, $\sigma_p(N) = \mathbb{N}$. PhysProof defines all three and reads the point spectrum off the diagonal in the Analysis/UnboundedOperator/ subtree.
A symmetric operator $T$ defined on a convenient dense domain (a "core") is essentially self-adjoint when its closure $\bar T$ is self-adjoint — equivalently, $T$ has exactly one self-adjoint extension. This is the practical notion in quantum mechanics: you write the Hamiltonian on smooth states where symmetry is obvious, then prove essential self-adjointness to license Stone's theorem (unitary time evolution) and the spectral theorem (a well-defined energy spectrum, hence a mass gap). Defined in Analysis/UnboundedOperator/; the general criterion via analytic vectors is currently a named axiom, not yet a discharged theorem.
The operators that step between particle-number sectors: the creation operator $a^\dagger(f)$ adds a quantum in mode $f$ (raising occupation by one) and the annihilation operator $a(f)$ removes one, with the vacuum $|0\rangle$ annihilated by every $a(f)$. They satisfy the canonical commutation relations (CCR) $[a(f), a^\dagger(g)] = \langle f, g\rangle$ for bosons, or canonical anticommutation relations (CAR, giving Pauli exclusion $a^\dagger(f)^2 = 0$) for fermions. Their product $a^\dagger a$ is the number operator. PhysProof builds them on bosonic / fermionic Fock space in Physics/QFT/FreeField/.
The Hilbert space of quantum field theory, accommodating states with any number of particles: $\mathcal{F}_\pm(h) = \bigoplus_n h^{\otimes_\pm n}$, the direct sum of symmetric ($+$, bosons) or antisymmetric ($-$, fermions) tensor powers of a one-particle space $h$, starting from the one-dimensional vacuum sector. Creation and annihilation operators move between sectors; the number operator reads off the sector. PhysProof builds bosonic and fermionic Fock space as genuine Hilbert completions ($\ell^2$ over the $n$-particle spaces) in Physics/QFT/FreeField/FockSpace.lean.
Yang-Mills theory in two spacetime dimensions is exactly solvable: with no transverse gluon degrees of freedom, the Migdal (1975) heat-kernel formula gives the partition function as a sum over irreducible representations weighted by $\exp(-g^2 C_2(R)\, A / 2N)$, and the transfer-matrix eigenvalues are $\exp(-g^2 C_2(j)/2)$. The closed-form mass gap is $\Delta = g^2 N / 2$ (for SU(2): $\Delta = g^2$). PhysProof formalizes the SU(2) Casimir gap, transfer-matrix gap, and mass gap in Physics/QFT/TwoDimensional/YangMills2D.lean — the toy-model benchmark that validates the constructive-QFT machinery before the 4D attack.
Jacobson (1995) showed Einstein's field equations are an equation of state: imposing the Clausius relation $\delta Q = T\, \delta S$ on every local Rindler horizon, with the Bekenstein entropy-area law, forces the Einstein equations — gravity emerges from information-theoretic thermodynamics rather than being postulated. PhysProof formalizes the structure in Physics/Quantum/JacobsonDerivation.lean: the main theorem jacobson_einstein_from_thermodynamics is structurally complete but currently conditional on the lemma null_determines_tensor (a symmetric tensor vanishing on all null vectors is proportional to the metric), which still carries open sorrys — an honest work-in-progress, not a closed proof.
The Berry-Keating conjecture proposes that the imaginary parts of the nontrivial zeros of the Riemann zeta function are the eigenvalues of a self-adjoint operator (heuristically a quantization of the classical Hamiltonian $H = xp$); if such an operator exists, its eigenvalues are real, forcing all zeros onto the critical line $\mathrm{Re}\,s = 1/2$ — the Riemann Hypothesis. As Pillar 4 of the strategy, PhysProof plants this as a type signature in PhysProof/Targets/RiemannHypothesis.lean, exploiting the fact that no other proof assistant has the unbounded self-adjoint operators, PVMs, and Stone's theorem needed to even state it. Honest status:berryKeatingConjecture is an open conditional-form sorry (it takes the operator's existence as a hypothesis); its _unconditional companion is discharged only against a registered Mathlib-debt axiom — a stated signature, not a proof of RH.
Hawking's 1971 theorem: the total surface area of black-hole event horizons in a classical spacetime obeying the (null/weak) energy condition is non-decreasing in time — when two black holes merge, $A_{\text{final}} \ge A_1 + A_2$. It is the classical-geometry shadow of the second law and the basis of Bekenstein-Hawking entropy $S = A/4$. PhysProof witnesses it observationally in Foundations/Holography/AreaTheorem.lean: since horizon area scales as $M^2$, the GW150914 merger (LIGO-Virgo 2016: $36 + 29 \to 62.2\,M_\odot$) gives $62.2^2 > 36^2 + 29^2$, proved sorry-free and axiom-free by norm_num. It is the dynamic companion to the static Bekenstein-Bousso holographic module.
The entropy of a black hole equals one quarter of its event-horizon area in Planck units: $S_{\text{BH}} = A/4$ (with constants restored, $S = k_B c^3 A/(4 G\hbar)$). A black hole carries the maximum entropy of any object of its size — the saturating case of the Bekenstein bound — and is the value loop quantum gravity must reproduce to fix the Barbero-Immirzi parameter. In PhysProof the factor $1/4$ is the geometric through-line of the holographic Triangle, and the Ryu-Takayanagi generalization $S = A/(4G)$ is anchored in Targets/HolographicEntropy.lean. The area theorem is its basis: entropy can only increase because area can only increase.
A lower bound on the time a quantum state needs to evolve into an orthogonal (perfectly distinguishable) state. Two complementary forms: Mandelstam-Tamm (1945) bounds it by the energy spread $\Delta E$, namely $\tau \ge \pi\hbar/(2\,\Delta E)$; Margolus-Levitin (1998) bounds it by the mean energy above the ground state, $\tau \ge \pi\hbar/(2\langle E\rangle)$, equivalently $\langle E\rangle\,\tau \ge \pi\hbar/2$ (dimensionless $\ge \pi/2 \approx 1.5708$); the true limit is the larger of the two. It is the "speed" premise of the ultimate laptop and a through-line of the info-thermodynamic Triangle. PhysProof anchors the coefficient in Validation/QuantumSpeedLimitTest.lean and the inequality in Foundations/InformationThermodynamics/MargolusLevitin.lean. Honest status: the structural inequality is discharged against a named Mathlib-debt axiom (Stone + functional calculus for unbounded Hamiltonians), not proved from scratch.
Seth Lloyd's 2000 synthesis of the physical limits to computation: a 1-kg, 1-litre device using all of its rest energy can perform at most $2mc^2/(\pi\hbar) \approx 5.4\times10^{50}$ logical operations per second on at most ${\sim}10^{31}$ bits. It bundles three bounds — the Margolus-Levitin speed limit (energy limits speed), the Bekenstein bound (entropy limits memory), and Landauer's cost (erasure costs energy) — into one envelope. Compressed to its Schwarzschild radius the same kilogram is a fully serial black-hole computer with the same op-rate but far fewer bits. PhysProof's Foundations/InformationThermodynamics/UltimateLaptop.lean carries the canonical numeric witness sorry-free and axiom-free (all facts close by norm_num on the 1-kg / 1-L instance).
The analytic continuation from real (Minkowski) time $t$ to imaginary time $\tau$ via $t \to -i\tau$, converting the oscillatory path integral $\int e^{iS}$ into the convergent Euclidean integral $\int e^{-S_E}$. It is the inverse direction of OS reconstruction: Wick rotation goes Minkowski→Euclidean; OS reconstruction comes back. Crucially for the mass gap, the Euclidean two-point function decays as $e^{-\Delta\tau}$, turning a hard spectral condition into a tractable correlation-decay estimate — the load-bearing move of the constructive-QFT pipeline. Scaffolded in Physics/QFT/Constructive/ (the two-point compatibility step is a named placeholder axiom).
For a graph with adjacency matrix $A$ and degree matrix $D$ (diagonal, with $D_{ii}$ = degree of node $i$), the Laplacian is
$$ L = D - A $$
Its eigenvalues encode graph structure: number of zero eigenvalues = number of connected components; smallest nonzero eigenvalue ($\lambda_2$) = spectral gap.
A positive semidefinite matrix $\rho$ with $\text{tr}(\rho) = 1$, representing a quantum state (pure or mixed). Density matrices generalize state vectors to statistical mixtures. Turning a graph Laplacian into a density matrix via $\rho = L / \text{tr}(L)$ lets you apply quantum-information tools (like von Neumann entropy) to classical graphs.
The quantum analogue of Shannon entropy, measured in bits (using $\log_2$). For a normalized graph Laplacian, high entropy means the graph's connectivity is spread across many independent modes; low entropy means a few modes dominate (clumpy, brittle structure).
Zurek's account of the quantum-to-classical transition: a fact becomes classical (objective, agreed-upon by many observers) when the environment contains many redundant copies of it. On the PhysProof proof graph, a definition becomes "classical" when many other modules depend on it — the more witnesses, the more load-bearing it is.
$$ R(v) = \left| \{ u : v \in \text{blockedBy}(u) \} \right| $$
— the count of modules that depend on $v$. High $R$ means the node is structurally load-bearing; low $R$ means it's a leaf. Nodes with $R \ge 5$ are called classical (in the quantum-Darwinism sense).
where $h(G)$ is the minimum edge-cut ratio. A large spectral gap means no single dependency can cripple the graph. Useful for reasoning about proof-graph resilience.
The Particle Data Group (pdg.lbl.gov) publishes the Review of Particle Physics, the canonical reference for particle masses, widths, branching ratios, and fundamental constants. ParticleZooTest.lean encodes PDG 2024 values as formal theorems; the dashboard's "validated" pill checks whether PhysProof's formal bounds clear the real measurements.
Committee on Data for Science and Technology — publishes evaluated values of fundamental constants ($c$, $\hbar$, $G$, $k_B$, fine structure constant, etc.) approximately every four years. FundamentalConstantsTest.lean encodes CODATA 2022 values and proves, for example, the $3.1\sigma$ shift in the fine structure constant between the 2018 and 2022 tables.
The preprint server at arxiv.org. Many PhysProof validation files cite an arXiv ID directly — e.g., the Cubitt–Pérez-García–Wolf spectral-gap undecidability result at arXiv:1502.04573 — tying the Lean theorem to the original paper's measurement or bound.
The in-house construction backlog (make build-queue) of mathematics PhysProof will build itself, in priority order, per the Yang-Mills Construction Charter. It replaces the older "Mathlib-blocked" framing: when a proof needs infrastructure Mathlib lacks, that gap is a build-queue item to construct here, not an upstream dependency to wait on. When the attackable-sorry pool is dry, build-queue construction is the default work.
The session-397 commitment (docs/YANG-MILLS-CONSTRUCTION.md) that PhysProof builds every layer of constructive 4-D QFT mathematics in-house — a 15-layer stack, ~100k LOC aggregate — regardless of Mathlib status. Mathlib is a peer, not an upstream; "the Clay Prize has no Mathlib clause." Read it before classifying any sorry as "Mathlib-blocked": on the YM road there are no Mathlib blockers, only build-queue items.
The registry of axioms each tagged with a target PhysProof file, an estimated LOC, and a charter layer — the in-house construction each axiom will be discharged against (not parked on a Mathlib PR queue). Surfaced in #print axioms and the dashboard axiom ledger so the cost of every assumed result is visible.
Closing a theorem whose body is a single invocation of a named project axiom (theorem foo ... := foo_axiom args). Detected by detect-axiom-discharge.py and classified as the axiom-discharged proof-kind (68 of the 812 done as of s588) — kept separate from genuine so the headline count never conflates "assumed via a tracked axiom" with "proved." A capstone discharged this way carries an honest *_unconditionalwitness-depth companion. Distinct from a circular discharge, where the axiom IS the conclusion verbatim (a core-principle violation).
Closing a goal by deriving it from a false or unsatisfiable hypothesis (False implies anything). It yields no information — the theorem is true only because its premises can never hold. Detected by detect-exfalso-vacuous.py and classified vacuous. PhysProof's policy: use exfalso only on a genuine contradiction; otherwise leave a sorry.
The Validation/ scaffold that makes an empirical benchmark a theorem, not a test: a measurement (value ± uncertainty) + a theoretical bound + a machine-checked consistency proof (interval ⊆ bound) + a Popper falsifier + a cross-reference. 198 such experiments across 56 files (196 pass, 2 fail) ground the formal work against PDG 2024 / CODATA 2022. See docs/VALIDATION-AS-PROOF.md.
A Triangle plus a fourth operational vertex that plays a distinct role from the three theoretical siblings — an empirical or calibration anchor. The three families each have one: Moreva 2014 visibility (info-thermodynamic), GW150914 dynamic formation (holographic), and the Barbero-Immirzi parameter (pregeometric).
A per-file quality score from 1 to 100 — how strongly a file's declarations would survive expert scrutiny as honest, physically meaningful, kernel-checked mathematics. It is an Opus-judged rating over eight axes: honest-count, open-sorry health, axiom level, statement integrity, contagion, physical realism, witness depth, and documentation. It is a wider lens than proof-kind, which is a kernel-level signal about a single proof: a genuine proof of a shaky statement can score high on proof-kind and low on confidence. Each rated node shows a color-banded badge (green ≥ 75 / amber 41–74 / red ≤ 40); generated by parallel rater agents into .file-confidence.json. See PROTOCOLS.md § File Confidence Rating.
An hourly first-person reflection the project writes once per hour of session time: a short prose note on what happened, what it noticed about its own process, and what it is wondering — often with a hand-authored inline SVG diagram. Heartbeats live in heartbeats.md (the single source of truth), render on the dashboard's HEARTBEATS frame and the Claude.Nature modal (via extract-heartbeats.py → /api/heartbeats), and are also published as an RSS feed. They are the qualitative counterpart to the header's quantitative stats — the legible, self-reflective trace that is the introspective half of the project's own AWARENESS subject matter.
The headline "proved" total after each proof-kind bucket is discounted by how much real work it does: genuine proofs count in full, while axiom-discharged, specified, and vacuous closes count fractionally. The dashboard renders it as a segmented trust bar — each done-kind a colored block, the discounted part hatched, the un-hatched area the trust-weighted total — plus a ratio (trust-weighted / raw headline). It is the project's deliberate refusal to let the kernel's token-count flatter the honest count.
The family of self-referential scalars the dashboard computes about itself, live from its own proof-dependency graph and recomputed every session: the electrical energy per proof (per-session budget / proof rate, reported as a multiple of the Landauer floor), the algebraic connectivity $\lambda_2$ (Fiedler value of the graph Laplacian), the von Neumann entropy $S_{\text{vN}}$ of the graph, and a quantum-Darwinism redundancy reading. The point is reflexive: the project runs the same operation its own Lean files define (e.g. vonNeumannEntropy from QuantumDarwinism/DensityOperator.lean) on the graph that contains those files — a formalization measuring itself with a ruler it certified. Computed by compute-universe-metrics.py.
The dashboard's real-time activity stream: as a session runs it emits typed events (via scripts/emit.sh) — proved, discovery, pivot, calibration, counterexample, compliance, session_end, and more — that render in the LIVE FEED view, drive the INSIGHTS extraction, and stamp the header's "last activity" pill. The aim is a legible, timestamped trace of what the autopilot is doing, rather than only a final commit. Event types and examples are documented in docs/DASHBOARD-GUIDE.md.
The transitive poisoning of a declaration by an upstream sorry it depends on. A sorry in a definition body is especially dangerous: it silently taints every downstream use with no visible sorry token at the use site (the same mechanism behind the it-from-bit entry's "transitive sorryAx"). PhysProof tracks two closures — .contagion-db (source-level chains) and .kernel-sorry-db (the full collectAxioms transitive closure) — and reports both via make contagion; contagion is also one of the eight file-confidence axes. The policy is to use opaque or axiom, never def ... := sorry, when the value matters downstream.
The standing self-audit that keeps every other number on the dashboard honest: a battery of checks (make integrity runs 24 standalone targets, reported as 22 audit dimensions) covering vacuity, circularity, conditional-form, axiom-discharge, contagion, doc-freshness, glossary-link drift, and more. Run in parallel waves at session start and re-run at close-out; the node inspect panel surfaces per-file "Audit findings". Full detail in docs/AUDIT-PROTOCOL.md. (Count note: the old "23-dimension" branding was retired in s580 — say 22 reported dimensions or 24 make-targets, never 23.)
The feedback loop that corrects each sorry's difficulty rating against reality. Sessions consistently mis-rate difficulty (TRIVIAL sorrys turn out HARD, HARD ones fall in 30 lines), so after each attempt calibrate-difficulty.py (make calibrate) compares the estimated difficulty to the actual outcome and records an accuracy score. The node inspect panel shows this as an "NN% accurate" calibration dot; the goal is honest priority-ranking rather than estimates that drift from experience.
The correspondence between (unbounded) self-adjoint operators H and strongly-continuous one-parameter unitary groups U(t) = exp(−iHt): every such group has a unique self-adjoint generator and vice versa. The bridge from a Hamiltonian to time evolution; a backbone of the unbounded-operator library and the Wightman reconstruction. The s498 AnalyticOrbit chain (40 lemmas) builds its analytic-vector isometry layer.
Discretizing a gauge field onto a finite lattice (the Wilson action) so the path integral is well-defined, then taking the spacing a → 0. The Clay-endorsed constructive route to the mass gap: gauge invariance is exact at every spacing (proved), and Poincaré covariance is recovered in the continuum limit via OS reconstruction.
The operator that evolves a lattice system by one time slice; the logarithm of the ratio of its two largest eigenvalues is the lattice mass gap. Reduces "does a gap exist?" to a spectral-gap question about a single operator — the mechanism behind the proved 2-D SU(N) exact solution (Δ = g²N/2).
The Osterwalder-Schrader axiom (OS3) guaranteeing that a Euclidean field theory reconstructs to a genuine Hilbert space with a positive-definite inner product — the condition that makes OS reconstruction produce real quantum mechanics rather than a formal artifact.
A convergent series expansion of the lattice partition function into "polymers"; the Kotecký-Preiss (KP) criterion is the convergence condition. The analytic machinery that proves correlations decay exponentially (hence a gap) in the strong-coupling regime of the constructive pipeline.
Block-spin RG coarse-grains short-distance degrees of freedom and tracks how the coupling "runs" with scale. For 4-D Yang-Mills the coupling runs to zero at short distance (asymptotic freedom) — the property (with the 2^(4k) link cancellation, "why d=4 works") that makes the continuum limit controllable.
Deutsch & Marletto's reframing of physics in terms of which tasks are possible vs impossible, rather than trajectories and initial conditions. PhysProof restates the mass gap as an impossibility ("creating a sub-Δ particle from the vacuum is an impossible task") and uses copyability to distinguish classical from quantum information media.
A minimal 8-symbol Turing-complete language. PhysProof's 102-character BF program decides whether a finite spectrum has a gap (its Kolmogorov complexity is bounded: K(hasGap) ≤ 95), making it the concrete witness for it from bit and for A1 of AWARENESS.
The universal prior over computable hypotheses: a string's probability is summed over the programs that output it, weighted by 2 to the minus their length — short descriptions are more probable. PhysProof proves its dominance over computable measures (solomonoff_dominance) and uses it as one route to the Born rule.
The constraint that, for any prefix-free code, the sum over codewords of 2 to the minus their length is ≤ 1. The combinatorial backbone of the algorithmic-probability bounds (it makes the Solomonoff sum a sub-probability) and of Kolmogorov coding arguments.
The quantum measurement postulate p = |ψ|²: outcome probabilities are squared amplitudes. Usually assumed; PhysProof derives it two ways — from algorithmic probability and from Zurek's envariance (a symmetry of entangled states) — connecting probability to information rather than positing it.
No local-hidden-variable model can reproduce quantum correlations: any such model obeys the CHSH bound S ≤ 2, while quantum mechanics reaches S = 2√2 (the Tsirelson bound). Proved sorry-free in PhysProof. It is load-bearing for it from bit: Wheeler's "bit" is a measurement outcome created by measurement, not a pre-existing hidden value — ruling out the Zuse-cellular-automaton misreading.
Wheeler's program in which spacetime geometry itself is emergent from a more primitive, pre-metric structure (bits, relations, networks) — "law without law." PhysProof formalizes several substrates: causal sets, Regge calculus, spin networks, and tensor networks, each with a continuum-limit statement.
A model of spacetime as a locally-finite partial order: the only data is which events causally precede which, and each causal relation is one bit. Continuous Lorentzian geometry is recovered via a faithful (sprinkling) embedding. Formalized in Lean using Mathlib's LocallyFiniteOrder — a project first.
Discrete general relativity on a simplicial complex: curvature is concentrated as a "deficit angle" at each hinge, and the Regge action converges to the Einstein-Hilbert action as the triangulation is refined. The discrete-geometry leg of the pregeometry program.
Locally covariant quantum field theory (Brunetti-Fredenhagen-Verch): a QFT presented as a functor from a category of spacetimes (Loc) to a category of observable algebras (Obs), so background independence is encoded categorically. Extends the Haag-Kastler axioms to curved spacetime; first formalization in a proof assistant.
The canonical quantum-gravity constraint HΨ = 0: the wavefunction of the universe is annihilated by the Hamiltonian, so there is no external time parameter (the "problem of time"). PhysProof formalizes the minisuperspace version and connects it to dimensional emergence.
The holographic formula that a boundary region's entanglement entropy equals the area of a minimal bulk surface divided by 4G — geometry from entanglement. Paired with the Bousso covariant entropy bound, these anchor the Holographic Triangle family (shared constant 1/4).
The covariant entropy bound: the entropy crossing a light-sheet emanating from a surface is ≤ its area / 4G. The most general form of the Bekenstein-type holographic limit, and the "covariant" vertex of the Holographic Triangle.
A dimensionless constant in loop quantum gravity fixed by matching the LQG black-hole entropy to the Bekenstein-Hawking value. It is the operational/calibration fourth vertex of the Pregeometric Tetrahedron.
Grand Unified Theory: the Standard Model gauge group embeds into a single simple group, SU(5) → Spin(10), with one Spin(10) spinor representation holding exactly one fermion generation. PhysProof formalizes the embeddings, anomaly cancellation, symmetry breaking, and coupling unification.
A quantum gauge theory is consistent only if its chiral gauge anomalies sum to zero. That the Standard Model's anomalies cancel generation-by-generation is a nontrivial consistency condition — proved in PhysProof's GUT track.
Carneiro 2024's reimplementation of the Lean 4 kernel in Lean itself, proved correct and run competitively. It anchors the bootstrap's trust: the type checker verifying PhysProof is itself a machine-verified program, so the self-referential loop has checked trust at every link. PhysProof ports its core types and runs lean4checker (its executable frontend) every session.
The project's self-referential capstone: the proof that physics is computation is itself a physical computation (the Lean kernel type-checking it is a physical process whose spectral properties are BF-computable). The capstone theorem universe_is_typechecker has no direct sorry but inherits one transitivesorryAx (it closes its final clause with exact it_from_bit; the file's axiom trace reads “sorryAx (from it_from_bit) + propext, Quot.sound, Classical.choice”); Lean4Lean supplies the verified kernel it leans on.
Given a real sequence $\lambda : \mathbb{N} \to \mathbb{R}$, the diagonal operator $D$ acts coordinatewise as $(Dx)_k = \lambda_k x_k$ on $\ell^2(\mathbb{N},\mathbb{C})$. When the $\lambda_k$ are unbounded (e.g. $\lambda_n = n$ for the number operator) so is $D$, so it lives only on a dense domain. PhysProof reads its point spectrum straight off the diagonal — $\sigma_p(D) = \{\lambda_k\}$ — and, for the self-adjoint maximal realization $D_{\max}$, proves the full spectrum $\sigma(D_{\max}) = \overline{\{\lambda_k\}}$ via an explicit bounded resolvent $\mathrm{diag}(1/(\lambda_k - z))$. Anchor: DiagonalOperatorSpectrum.lean (sorry-free; spectrum axiom-free). The project's first genuinely unbounded concrete operator with a fully worked spectrum.
For $z$ not in the spectrum of $T$, the resolvent is the bounded inverse $R(z) = (T - z)^{-1}$; the set of such $z$ is the resolvent set $\rho(T)$, the open complement of the spectrum. The resolvent turns spectral questions into the behaviour of an explicit bounded operator. In PhysProof's diagonal case the resolvent is itself diagonal, $R(z) = \mathrm{diag}\!\left(1/(\lambda_k - z)\right)$, bounded by $1/\mathrm{dist}(z, \overline{\{\lambda_k\}})$ — the construction that pins down $\sigma(N_{\max}) = \mathbb{N}$ in DiagonalOperatorSpectrum.lean (axiom-free).
Nelson (1959): a symmetric operator $T$ with a dense set of analytic vectors — vectors $x$ for which $\sum \|T^n x\|\, t^n / n!$ has positive radius of convergence — is essentially self-adjoint. It is the textbook route to upgrade a Hamiltonian on a core to a genuine self-adjoint operator. In PhysProof (Analysis/UnboundedOperator/AnalyticVector.lean) the criterion is currently a named axiom, nelson_analytic_vector_ess_self_adjoint_axiom — a principled in-house build-queue target (~300–500 LOC of power-series + closability machinery), not yet discharged. The diagonal / number operator's spectrum is proved axiom-free; only its closure's self-adjointness leans on this axiom.
An unbounded operator is closed when its graph $\{(x, Tx)\}$ is closed in $H \times H$; it is closable when the closure of its graph is still single-valued (a function), and the resulting operator $\bar T$ is its closure. Closing a symmetric core operator is the step that makes the spectral theorem applicable. PhysProof proves the diagonal operator is closable by an elementary limit argument (no Nelson axiom) and identifies its closure with the explicit maximal multiplication operator $D_{\max}$.
Changelog
Entries added to this glossary, newest first. The project's autonomous session loop batches commits, so calendar dates cluster around a small number of landing days; ordering is the reliable signal, not the date.
Session-classifier vocabulary — added session regime, permanent admission, fatigued blocker, and attackable sorry. The regime classifier landed in session 308 (scripts/regime-detect.py + .regime.json) but the briefing-driven labels weren't defined in the glossary. Adding them closes the gap between what the dashboard surfaces and what the reader can look up.
Session 290+1 entry
witness depth — fifth honest-count dimension; the *_unconditional capstone-companion convention (session 247) named in the glossary for the first time. Triggered by session 289's discovery of a link whose visible slug ("witness-depth") pointed to a different anchor ("proof-kind"); that incident also produced check-glossary-semantic.py, wired into INTEGRITY_CHECKS by session 292.
Sessions 286-288+2 entries
Kolmogorov complexity $K$ · it from bit — Wheeler 1990 formalized from both sides at once: 95-character Brainfuck gap-detector (constructive) and the Cubitt–Pérez-García–Wolf undecidability result (general case). The $K(\mathtt{hasGap}) \le 95$ exhibition is the first concrete quantitative form of it-from-bit on a decidable slice.
Session 257+1 entry
AWARENESS (small caps) — four-condition structural predicate introduced with The Participatory Proof (April 2026). Entry includes the paper's §4 negative propositions verbatim so no reader mistakes the technical term for phenomenal consciousness.
Sessions 272 / 276 / 280+1 entry
Triangle pattern — three independent physical regimes sharing a mathematical fixed point. Entry covers all three completed families: info-thermodynamic ($kT \ln 2$), holographic ($1/4$), pregeometric (minimum discrete quantum $\ge 1$), each with a Tetrahedron 4th vertex. Bekenstein vs. Bekenstein–Hawking attribution fixed in the same revision.
CHSH cross-link+1 entry
CHSH — cross-linked to the interactive /chsh widget, the first hands-on physics surface on the dashboard (drag four measurement angles; watch $S$ move between the classical ceiling at 2 and Tsirelson's at $2\sqrt{2}$).