# Counterexample and obstruction register

Last audited: 2026-07-23

Each entry attacks a specific overclaim. A counterexample does not refute a
weaker theorem whose assumptions explicitly exclude it.

| ID | Attacks | Construction or obstruction | Consequence | Sources | State |
|---|---|---|---|---|---|
| CE-P1-01 | “Every compatible descent datum is effective in the original category.” | Étale-local projective scheme data can fail to descend to a scheme while descending to an algebraic space. | The ambient category and effectiveness theorem must be explicit. | `DESC-STACKS-08KE` | active |
| CE-P1-02 | “Categorical composition is already physical locality.” | A one-object monoidal category has composition but no nontrivial coverage or separation relation. | Composition alone cannot supply covers, disjointness, or local-to-global gluing. | elementary construction; compare `CAT-ATIYAH-1988` | active |
| CE-P1-03 | “A coverage determines causal order.” | Ordinary sheaf sites support descent with no causal relation on objects. | Causality requires an independent relation or realization interface. | `CAT-LURIE-HTT-2009` | active |
| CE-P2-01 | “Condensed mathematics selects physical geometry.” | The same topological or algebraic object has a condensed avatar without acquiring a metric, causal order, or dynamics. | Condensation is a mathematical change of ambient category, not a physical-selection principle. | `COND-CLAUSEN-SCHOLZE-2026` | active |
| CE-P2-02 | “The topological-to-condensed functor is fully faithful on all topological spaces.” | Full faithfulness is stated only on controlled compactly generated classes; the stable notes include warnings outside them. | The physical source category must be restricted and audited. | `COND-CLAUSEN-SCHOLZE-2026` | active |
| CE-P3-01 | “Every monoidal category reconstructs a unique compact group.” | Non-rigid or non-symmetric monoidal categories, or categories with non-scalar unit endomorphisms, fail Doplicher–Roberts hypotheses. | Rigidity, symmetry, conjugates, closures, and unit scalars are assumptions, not notation. | `TAN-DOPLICHER-ROBERTS-1989` | active |
| CE-P3-02 | “The representation category alone gives a canonical group scheme.” | Neutral Tannakian reconstruction uses a fibre functor; changing or lacking neutralization changes the reconstruction problem. | Fibre-functor existence and choice must be tracked. | `TAN-DELIGNE-MILNE-1982` | active |
| CE-P3-03 | “AQFT reconstructs spacetime from observables by definition.” | Haag–Kastler nets are indexed by regions and BFV starts from globally hyperbolic spacetimes. | These are realization comparators, not pre-geometric reconstruction theorems. | `AQFT-HAAG-KASTLER-1964`, `AQFT-BFV-2003` | active |
| CE-P3-04 | “A reconstructed compact group selects its observable algebra.” | The trivial action exists on every unital C-star algebra, while the same group also has inequivalent nontrivial actions on many algebras. | The context-indexed observable functor and its action are separate data. | `TAN-DOPLICHER-ROBERTS-ANNALS-1989`, `AQFT-DOPLICHER-ROBERTS-FIELD-1990` | active |
| CE-P3-05 | “Every continuous automorphic action admits an invariant state.” | Left translation of the nonamenable free group `F_2` on `l-infinity(F_2)` would turn an invariant state into a left-invariant mean, which does not exist. | Compactness, amenability, or an exhibited invariant state is required. | `AMEN-VON-NEUMANN-1929`, `AMEN-DAY-1957`, `AMEN-DAY-1961` | active |
| CE-P3-06 | “Symmetry invariance is conservation.” | A symmetry-fixed observable need not be fixed by an unrelated one-parameter dynamics, and a symmetry action may be given with no dynamics at all. | Symmetry, dynamics, fixed points, generator domains, and Noether claims must remain separate. | `DYN-STONE-1932`, `AQFT-NOETHER-BDL-1986`, `REF-BARTLETT-RUDOLPH-SPEKKENS-2007` | active |
| CE-P3-07 | “Monoidality produces outcomes.” | A monoidal context category can be specified without any outcome-label functor. | Declare the outcome functor and its coherence maps independently. | `OUT-ABRAMSKY-HEUNEN-2019` | active |
| CE-P3-08 | “A fibre functor is a physical reference frame.” | Fibre functors are algebraic neutralizations and their comparison objects are torsors; operational quantum frames already assume Hilbert, density-operator, and measurement structure. | Use algebraic frame data until a separate physical realization theorem is proved. | `TAN-DELIGNE-MILNE-1982`, `REF-BARTLETT-RUDOLPH-SPEKKENS-2007` | active |
| CE-P3-09 | “Outcome labels, effects, and probabilities are the same type.” | A label is a typed result name, an effect is an ordered algebra element, and a state-effect scalar has no probability interpretation without an evaluation postulate. | Keep labels, effects, scalar evaluation, and operational probability in separate interfaces. | `OUT-ABRAMSKY-HEUNEN-2019`, `QM-ABRAMSKY-COECKE-2004` | active |
| CE-P4-01 | “Causal order determines the Lorentzian metric uniquely.” | For `g_tilde = Omega^2 g` with positive `Omega`, the null cones and causal relations agree. | Causal rigidity yields at most a conformal class without scale-setting data. | `LOR-HKM-1976`, `LOR-MALAMENT-1977` | active |
| CE-P4-02 | “Light rays alone determine free fall and the metric connection.” | Light rays determine conformal structure, while unparametrized massive trajectories supply a separate torsion-free projective class in EPS. | Both interfaces plus compatibility and clock assumptions are required. | `LOR-EPS-1972`, `LOR-MATVEEV-SCHOLZ-2020` | active |
| CE-P4-03 | “Locality and covariance select Einstein gravity.” | The Buchdahl action `R - 2 Lambda + alpha R^2`, with nonzero `alpha`, is local, metric-only, diffeomorphism-covariant, and variational but has a generic fourth-order field equation different from Einstein’s. | Einstein dynamics requires the restricted second-order natural metric-tensor class or another explicit selection principle. | `GR-BUCHDAHL-1970`, `GR-STELLE-1977` | active |
| CE-P4-04 | “Lovelock uniqueness is assumption-free.” | The classification changes with dimension and excludes higher derivatives, additional fields, independent connections, and nonlocal terms. | Every uniqueness statement must quote the exact Lovelock tensor hypotheses. | `GR-LOVELOCK-1971`, `GR-NAVARRO-LOVELOCK-2011` | active |
| CE-P4-05 | “HKM or Malament constructs spacetime from the Papers 1–3 relation.” | HKM, Malament, and Levichev begin with smooth Lorentzian spacetimes and prove rigidity between them. | A typed event, manifold, and metric realization is an independent bridge. | `LOR-HKM-1976`, `LOR-MALAMENT-1977`, `LOR-LEVICHEV-1987` | active |
| CE-P4-06 | “Free-fall paths determine the full affine connection.” | Adding a lower-index antisymmetric tensor `K` to a connection leaves the path contraction unchanged but changes torsion and generally curvature. | Declare torsion-free projective scope or supply torsion observables. | `LOR-EPS-1972`, `GR-TRAUTMAN-EC-2006` | active |
| CE-P4-07 | “A Lorentz metric canonically gives a global coframe.” | Coframes are locally Lorentz-nonunique, and a global coframe trivializes the tangent bundle. | Use local coframes or add a global parallelizability or spin certificate. | `DG-GEROCH-TETRAD-1968` | active |
| CE-P4-08 | “No second-clock effect automatically gives one global metric.” | Under the selected clock law it first gives local closedness; global exactness needs topology, a unit remains, and competing Weyl-covariant clock models change the inference. | State clock dynamics, topology, and residual scale separately. | `LOR-AVALOS-DAHIA-ROMERO-2018`, `LOR-HOBSON-LASENBY-2021` | active |
| CE-P4-09 | “Lovelock proves that the Einstein–Hilbert action is unique.” | Exact or boundary terms and the four-dimensional topological Euler density can leave the bulk metric equation unchanged. | Separate field-equation classification from action uniqueness. | `GR-LOVELOCK-1971`, `GR-IYER-WALD-1994` | active |
| CE-P4-10 | “The contracted Bianchi identity alone proves matter conservation.” | Bianchi gives divergence-freedom of the Einstein tensor; ordinary matter conservation also uses matter diffeomorphism invariance and matter equations, and torsion changes the identity. | State the on-shell matter and connection hypotheses. | `GR-IYER-WALD-1994`, `GR-TRAUTMAN-EC-2006` | active |
| CE-P4-11 | “The GHY term handles every spacetime boundary.” | Null segments and nonsmooth joints require additional terms and choices. | Parameterize the boundary class in the variational theorem. | `GR-HAYWARD-1993`, `GR-LEHNER-ETAL-2016` | active |
| CE-P5-01 | “Orthomodular quantum logic forces complex Hilbert space.” | Solèr’s conclusion admits real, complex, and quaternionic Hilbert spaces. | A complex-scalar selection principle is still required. | `QM-SOLER-1995`, `QM-ADLER-1995` | active |
| CE-P5-02 | “Gleason proves the Born rule in every dimension.” | The standard theorem requires dimension at least three. | Qubit/two-dimensional cases need separate assumptions or theorems. | `QM-GLEASON-1957` | active |
| CE-P5-03 | “Compact closure and biproducts uniquely characterize quantum theory.” | The structures give a categorical semantics for protocols but are shared by models not equivalent to finite-dimensional complex quantum mechanics. | A semantics theorem is not a reconstruction uniqueness theorem. | `QM-ABRAMSKY-COECKE-2004` | active |
| CE-P5-04 | “Compositionality rules out real or quaternionic quantum theory.” | Real and quaternionic Hilbert-space models exist; composite/tomography behavior must do the discriminating. | Scalar and local-tomography assumptions must be explicit. | `QM-ADLER-1995`, `QM-BARNUM-WILCE-2012` | active |
| CE-P5-05 | “Probability follows from categorical scalars.” | A scalar semiring need not carry a normalized positive probability interpretation. | Positivity, normalization, effects, and operational interpretation are independent assumptions. | compare `QM-HARDY-2001`, `QM-CDP-2011` | active |
| CE-P5-06 | “Paper 3 outcome labels canonically define probabilities.” | The same finite label set admits distinct normalized state-effect evaluations and also admits no evaluation map at all. | Supply an actual operational evaluation, tests, positivity, normalization, and operational equivalence; the Lean schema projection does not supply them. | `OUT-ABRAMSKY-HEUNEN-2019`; generic finite Haskell `LabelEvaluation` witness and direct test | active |
| CE-P5-07 | “Local tomography and a qubit alone imply complex quantum mechanics.” | Barnum-Wilce also requires finite state-complete HSD models and factorizable self-duality or the complete dagger-HSD structure. | State the ambient class and every complex-selection hypothesis. | `QM-BARNUM-WILCE-2012` | active |
| CE-P5-08 | “Complex selection removes superselection.” | Finite-dimensional complex C-star algebras can be direct sums of matrix algebras, and Barnum-Wilce retains superselection rules. | Add irreducibility or a trivial-center premise to obtain a simple factor, or retain sectors. | `QM-BARNUM-WILCE-2012` | active |
| CE-P5-09 | “Reconstructing reversible transformations selects time evolution and a Hamiltonian.” | One Hilbert space admits many one-parameter unitary groups and self-adjoint generators. | Choose a continuous dynamics separately and apply Stone only afterward. | `DYN-STONE-1932`, `QM-HARDY-2001` | active |
| CE-P5-10 | “A POVM fixes post-measurement collapse.” | Measure-and-prepare instruments can have the same outcome effects and probabilities but different conditional output states. | Treat operations and instruments as additional process data. | `QM-DAVIES-LEWIS-1970`, `QM-OZAWA-1984`; finite Haskell witness | active |
| CE-P5-11 | “Gleason reconstructs Hilbert space or complex scalars.” | Gleason starts with a real or complex Hilbert projection lattice of dimension at least three. | Use Gleason only downstream of Hilbert structure and scalar selection. | `QM-GLEASON-1957` | active |
| CE-P5-12 | “One theorem covers finite, infinite, low-dimensional, and superselection alternatives.” | CDP and Barnum-Wilce are finite; Piron has a rank bound; Solèr is infinite and leaves real, complex, or quaternionic scalars; standard Gleason misses dimension two; Barnum-Wilce keeps direct sums. | Replace the master theorem by a route-and-case table. | `QM-CDP-2011`, `QM-BARNUM-WILCE-2012`, `QM-GLEASON-1957`, `QM-SOLER-1995` | active |
| CE-P5-13 | “Operational reconstruction solves the measurement problem.” | The operational signature lacks an ontology or collapse law, while Everett, Bohm, and GRW add mutually different structures or dynamics. | Keep interpretation and collapse as explicit nonclaims. | `QM-EVERETT-1957`, `QM-BOHM-1952`, `QM-GRW-1986` | active |
| CE-P6-01 | “A coarse-graining functor implies molecular chaos.” | A correlated N-particle distribution can have the same chosen one-particle coarse-graining as a product distribution. | Marginalization forgets correlations; propagation of chaos must be proved. | `KIN-SZNITMAN-1991` | active |
| CE-P6-02 | “Large N alone yields the Boltzmann collision operator.” | Mean-field and Boltzmann–Grad scalings produce different limiting equations. | The microscopic interaction and scaling are theorem hypotheses. | `KIN-LANFORD-1975`, `KIN-GALLAGHER-SAINT-RAYMOND-TEXIER-2013` | active |
| CE-P6-03 | “Collision histories remain independent automatically.” | Recollisions create correlations and are a central analytic obstruction in hard-sphere limits. | Collision-tree and bad-set estimates cannot be replaced by functoriality. | `KIN-GALLAGHER-SAINT-RAYMOND-TEXIER-2013` | active |
| CE-P6-04 | “Global Boltzmann PDE existence is a global particle derivation.” | DiPerna–Lions constructs renormalized PDE solutions without deriving them from N-particle hard-sphere dynamics. | PDE well-posedness and microscopic derivation are separate gates. | `KIN-DIPERNA-LIONS-1989` | active |
| CE-P6-05 | “All rigorous hard-sphere derivations are short-time.” | Deng–Hani–Ma obtain a long-time derivation over the lifespan of the required regular solution. | Paper 6 must use current prior art and state the remaining regularity/model restrictions. | `KIN-DENG-HANI-MA-2024` | active |
| CE-P6-06 | “Kac propagation transfers to deterministic hard spheres.” | Kac's simplified stochastic homogeneous scalar-velocity model drops physical momentum, and Kac separates its propagation argument from the hard-sphere problem. | Kac is an executable comparator, not evidence for the deterministic hard-sphere limit. | `KIN-KAC-1956` | active |
| CE-P6-07 | “A static entropy calculation verifies the H-theorem.” | A finite normalized list has a computable Shannon entropy without any transition law or monotone evolution. | An H claim needs a collision evolution, solution class, and entropy-production sign. | `KIN-BOLTZMANN-1872`, `KIN-GALLAGHER-SAINT-RAYMOND-TEXIER-2013` | active |
| CE-P6-08 | “Marginalization preserves or detects independence.” | The product fair-bit law and perfectly correlated fair-bit law have the same one-particle marginal. | Coarse-graining loses correlations, so chaos needs a separate limit theorem. | `FoundationalReformulation/Kinetic.lean` | active |
| CE-P6-09 | “Arbitrarily long means one unconditional all-time limit.” | Deng-Hani-Ma Theorem 1 first fixes a finite horizon and its solution bounds, then chooses epsilon small enough depending on that package. | Preserve the theorem's quantifier order and do not claim convergence at t=infinity. | `KIN-DENG-HANI-MA-2024` | active |
| CE-P6-10 | “Renormalized solutions satisfy the classical conservation equalities.” | The renormalized formulation has a momentum defect measure and an entropy inequality in the audited cutoff presentation. | Split the classical and renormalized solution classes. | `KIN-DIPERNA-LIONS-1989`, `KIN-GALLAGHER-SAINT-RAYMOND-TEXIER-2013` | active |
| CE-PS-01 | “Verified branch theorems automatically compose.” | P4, P5, and P6 can rely on mutually unproved or incompatible realizations of the P1–P3 interfaces. | The synthesis must check joint satisfiability and exact dependency versions. | claim and assumption ledgers | active |

## Adversarial test protocol

Before strengthening a claim, attempt at least:

1. the smallest/lowest-dimensional object allowed by the statement;
2. a change of scalar field;
3. a non-effective descent datum;
4. a conformal rescaling or higher-derivative action;
5. correlated microscopic states with identical coarse observables;
6. a different limiting scaling;
7. a model that satisfies the categorical axioms but lacks the intended
   physical interpretation.

Record a new `CE-*` row whenever one of these changes the theorem statement.