# Assumption ledger

Foundation snapshot: 2026-07-23

`UNVALIDATED` means the program has not yet proved, implemented, or
independently reviewed the assumption-to-interface bridge. A literature source
may show that an assumption is sufficient for a known theorem; it does not show
that the program’s earlier papers supply it.

## Paper 1 assumptions

| Assumption ID | Paper | Assumption | Needed by | Source or rationale | State | Required validation | Failure consequence |
|---|---|---|---|---|---|---|---|
| P1-A01 | categorical-locality | Physical contexts and processes have the chosen weak higher-categorical composition operations. | `P1-C01` | design choice; comparator `CAT-ATIYAH-1988` | UNVALIDATED | define objects/morphisms/higher morphisms and prove closure | coherence claim cannot be stated |
| P1-A02 | categorical-locality | A coverage on contexts is stable under the declared pullbacks/base changes. | `P1-C01`, `P1-C02` | descent prerequisites | UNVALIDATED | prove pretopology/Grothendieck axioms | locality and descent are ill-typed |
| P1-A03 | categorical-locality | The coefficient/observable assignment is a presheaf, stack, or higher analogue on that coverage. | `P1-C02` | `CAT-LURIE-HTT-2009` | UNVALIDATED | construct functor and verify coherence | no comparison functor to descent data |
| P1-A04 | categorical-locality | The chosen class of descent data is effective in the declared ambient category. | `P1-C02` | `DESC-STACKS-023N`; warning `DESC-STACKS-08KE` | UNVALIDATED | prove essential surjectivity and full faithfulness | target weakens to non-effective compatibility |
| P1-A05 | categorical-locality | Each comparator has an explicit structure-preserving realization functor from or to the Paper 1 interface. | `P1-C03` | avoid analogy-only comparison | UNVALIDATED | define and test functors | examples provide no evidence about the axioms |
| P1-A06 | categorical-locality | Geometric structure is excluded from the primitive signature. | `P1-C03` | approved design | ESTABLISHED | exact primitive-signature audit in `papers/latex/categorical-locality.tex`, Section `sec:signature`; independently verified by AGY round 5 `ACCEPT` in `reviews/categorical-locality-agy-review-round-5.md` | pre-geometric claim becomes circular |
| P1-A07 | categorical-locality | At least one model of the axioms lacks causal, dimensional, topological, and metric structure. | `P1-C04` | independence witness | UNVALIDATED | construct and verify an admissible model satisfying the exact statement; the Paper 1 diagnostic-annotation theorem is insufficient | non-derivability claim remains unsupported |

## Paper 2 assumptions

| Assumption ID | Paper | Assumption | Needed by | Source or rationale | State | Required validation | Failure consequence |
|---|---|---|---|---|---|---|---|
| P2-A01 | condensed-physical-contexts | Paper 1 contexts admit evaluation on profinite test objects compatible with jointly surjective covers. | `P2-C01` | `COND-CLAUSEN-SCHOLZE-2026` | UNVALIDATED | define evaluation and prove sheaf condition | no condensed realization |
| P2-A02 | condensed-physical-contexts | Universe/cardinality bounds are fixed and stable under all constructions used. | `P2-C01`, `P2-C02` | set-theoretic warnings in `COND-CLAUSEN-SCHOLZE-2026` | UNVALIDATED | universe audit | category may be ill-defined |
| P2-A03 | condensed-physical-contexts | Source objects lie in a class on which topological-to-condensed passage is fully faithful. | `P2-C01` | Theorem 2.16 in `COND-CLAUSEN-SCHOLZE-2026` | UNVALIDATED | prove compact-generation/quasiseparation hypotheses | information may be identified or lost |
| P2-A04 | condensed-physical-contexts | Required diagrams fall within the exact limit/colimit preservation range. | `P2-C02` | condensed exactness theorems | UNVALIDATED | enumerate diagrams and prove preservation | later gluing/limits cannot be imported |
| P2-A05 | condensed-physical-contexts | Paper 1 descent comparison commutes with condensed realization. | `P2-C02` | interface requirement | UNVALIDATED | naturality/base-change proof | P1 descent does not transfer |
| P2-A06 | condensed-physical-contexts | The selected data are abelian/module-valued where solidification is used. | `P2-C03` | type requirement | UNVALIDATED | type audit | solidification is inapplicable |
| P2-A07 | condensed-physical-contexts | The selected analytic ring or solid localization models the intended limit/distributional operation. | `P2-C03` | physical-interface hypothesis | UNVALIDATED | comparison with classical examples | mathematical object lacks stated physical meaning |
| P2-A08 | condensed-physical-contexts | The realization functor carries no undeclared causal, metric, probabilistic, or dynamical fields. | `P2-C04` | conservativity requirement | UNVALIDATED | data-model diff and forgetful-functor proof | later recovery is definitional |

## Paper 3 assumptions

| Assumption ID | Paper | Assumption | Needed by | Source or rationale | State | Required validation | Failure consequence |
|---|---|---|---|---|---|---|---|
| P3-A01 | representation-theoretic-measurement | The selected main-line category is a strict symmetric monoidal C-star category with conjugates. | `P3-C01` | `TAN-DOPLICHER-ROBERTS-1989` | UNVALIDATED | construct the actual category and verify strictness, symmetry, C-star enrichment, and conjugates | Doplicher-Roberts reconstruction is inapplicable |
| P3-A02 | representation-theoretic-measurement | A faithful exact tensor fibre functor to the declared linear target exists when the neutral Tannakian comparator is invoked. | `P3-C01` | `TAN-DELIGNE-MILNE-1982` | UNVALIDATED | construct and prove faithfulness/exactness for that comparator; do not attach it to the Doplicher-Roberts theorem | no neutral Tannakian reconstruction |
| P3-A03 | representation-theoretic-measurement | Subobjects, direct sums, scalar unit endomorphisms, and all remaining branch-specific hypotheses satisfy the selected reconstruction theorem. | `P3-C01` | `TAN-DOPLICHER-ROBERTS-1989` | UNVALIDATED | verify subobjects, direct sums, `End(1)=C`, and the exact compact-group output | compact-group existence or uniqueness is overclaimed |
| P3-A04 | representation-theoretic-measurement | A context-indexed unital C-star or star-algebra functor of observables is separately declared or constructed. | `P3-C02` | bridge requirement; reverse-direction comparators `TAN-DOPLICHER-ROBERTS-ANNALS-1989`, `AQFT-DOPLICHER-ROBERTS-FIELD-1990` | UNVALIDATED | define the functor, algebra laws, and context maps without deriving it from bare representation data | no observable interface |
| P3-A05 | representation-theoretic-measurement | A continuous symmetry action by unital star-automorphisms is natural in context and equivariant with any monoidal comparison maps used. | `P3-C02` | covariance requirement | UNVALIDATED | prove group, star, continuity, naturality, and tensor-equivariance laws | action is not a compositional observable action |
| P3-A06 | representation-theoretic-measurement | Each state used is an exhibited positive normalized functional; compatible state families require a separate naturality condition. | `P3-C03` | `AQFT-BFV-2003`; compact averaging boundary | UNVALIDATED | exhibit states, prove positivity/normalization, and separately prove any context compatibility | state existence or naturality is being inferred |
| P3-A07 | representation-theoretic-measurement | The symmetry action has the continuity needed for averaging, while any conservation statement uses a separately declared strongly continuous one-parameter dynamics and generator domain. | `P3-C03` | `DYN-STONE-1932`, `AQFT-NOETHER-BDL-1986` | UNVALIDATED | split symmetry, dynamics, fixed points, generator domain, and any later Noether hypotheses | invariance is conflated with conservation |
| P3-A08 | representation-theoretic-measurement | A separately declared strong monoidal finite outcome-label functor composes labels and contains no evaluation into ordered normalized scalars. | `P3-C04` | `OUT-ABRAMSKY-HEUNEN-2019`; terminology contract | UNVALIDATED | construct the functor and coherence maps, then audit the signature for evaluation, dagger, trace, effect, and probability fields | outcomes or probability are smuggled into monoidality |
| P3-A09 | representation-theoretic-measurement | Later spacetime, algebra, and physical-outcome realization functors and natural comparison maps are separately declared without identifying pre-geometric labels with ordinary measurements. | `P3-C05` | `AQFT-BFV-2003`; approved dependency distinction | UNVALIDATED | define each functor/map and prove naturality, equivariance, and adequacy after Paper 4 supplies spacetime | measurement claims become equivocal |

## Paper 4 assumptions

| Assumption ID | Paper | Assumption | Needed by | Source or rationale | State | Required validation | Failure consequence |
|---|---|---|---|---|---|---|---|
| P4-A01 | lorentzian-geometry-realization | A typed map from the prior context interface to an event object is supplied and is well defined with respect to any event equivalence. | `P4-C01` | physical bridge | UNVALIDATED | explicit construction and quotient well-definedness proof | causal reconstruction cannot begin |
| P4-A02 | lorentzian-geometry-realization | The primitive relation is declared as chronology for the Malament branch or causality for the Levichev branch, with exact orientation and bidirectional preservation conditions. | `P4-C01` | `LOR-MALAMENT-1977`, `LOR-LEVICHEV-1987` | UNVALIDATED | prove the selected relation and map satisfy each theorem hypothesis | rigidity theorem is inapplicable |
| P4-A03 | lorentzian-geometry-realization | The realization already has the smooth Lorentzian-spacetime, dimension, regularity, and past- and future-distinguishing hypotheses required by the selected rigidity theorem. | `P4-C01`, `P4-C02` | `LOR-HKM-1976`, `LOR-MALAMENT-1977`, `LOR-MINGUZZI-2019` | UNVALIDATED | construct the smooth spacetime and prove all selected rigidity hypotheses | theorem scope violated |
| P4-A04 | lorentzian-geometry-realization | Independent physical light-ray incidence and smoothness data determine a nondegenerate indefinite conformal class in the stated EPS scope. | `P4-C02` | `LOR-EPS-1972` | UNVALIDATED | construct light histories and verify incidence, smoothness, nondegeneracy, and signature | no conformal structure is available |
| P4-A05 | lorentzian-geometry-realization | Independent regular massive free-fall histories determine a torsion-free projective class and satisfy the selected light-cone compatibility condition. | `P4-C02`, `P4-C03` | `LOR-EPS-1972`, `LOR-MATVEEV-SCHOLZ-2020` | UNVALIDATED | construct path family, projective regularity, torsion-free scope, and compatibility | Weyl connection is not recovered |
| P4-A06 | lorentzian-geometry-realization | A named EPS or Perlick clock law, no-second-clock-effect condition, local closedness, global exactness topology, and unit normalization are supplied as separate certificates. | `P4-C02` | `LOR-PERLICK-1987`, `LOR-AVALOS-DAHIA-ROMERO-2018`, `LOR-HOBSON-LASENBY-2021` | UNVALIDATED | validate clock model, path independence, local closedness, global topology, and residual unit choice | conformal/Weyl ambiguity remains |
| P4-A07 | lorentzian-geometry-realization | Metric nondegeneracy, Lorentz signature, regularity, local or global coframe scope, orientation, time orientation, connection policy, torsion, and nonmetricity are declared at the level needed for curvature. | `P4-C03` | `DG-GEROCH-TETRAD-1968`, `DG-LEFLOCH-MARDARE-2007`, `GR-TRAUTMAN-EC-2006` | UNVALIDATED | separate topology, regularity, coframe, and connection-policy certificates | curvature expressions are undefined or use the wrong branch |
| P4-A08 | lorentzian-geometry-realization | Spacetime dimension is four for the stated Lovelock specialization. | `P4-C04` | `GR-LOVELOCK-1971` | UNVALIDATED | dimension derivation or explicit realization input | uniqueness theorem changes |
| P4-A09 | lorentzian-geometry-realization | The gravitational comparison tensor is metric-only, symmetric, Levi-Civita divergence-free, natural, and second order in the exact metric two-jet sense. | `P4-C04` | `GR-LOVELOCK-1971`, `GR-NAVARRO-LOVELOCK-2011` | UNVALIDATED | prove membership in the second-order natural metric tensor class | higher-curvature or extra-field alternatives remain |
| P4-A10 | lorentzian-geometry-realization | Lovelock classification, coefficient selection, and variational origin are treated as different obligations, and a complete action is separately exhibited. | `P4-C04` | `GR-NAVARRO-LOVELOCK-2011`, `GR-IYER-WALD-1994` | UNVALIDATED | tensor classification, coefficient, and action-variation proofs | Einstein tensor or action is not selected |
| P4-A11 | lorentzian-geometry-realization | Matter fields and action, stress-tensor convention, admissible variations, boundary class and terms, matter equations, and on-shell conservation are specified consistently. | `P4-C04` | `GR-GIBBONS-HAWKING-1977`, `GR-IYER-WALD-1994`, `GR-HAYWARD-1993`, `GR-LEHNER-ETAL-2016` | UNVALIDATED | complete action, boundary, matter, and on-shell Noether audit | Einstein equation statement is incomplete |
| P4-A12 | lorentzian-geometry-realization | The comparison class admits the explicit local covariant metric action `R - 2 Lambda + alpha R^2`, with nonzero `alpha`, which drops the second-order field-equation restriction. | `P4-C05` | `GR-BUCHDAHL-1970` | UNVALIDATED | registered analytic counterexample and independent paper review | obstruction lacks a concrete witness |

## Paper 5 assumptions

| Assumption ID | Paper | Assumption | Needed by | Source or rationale | State | Required validation | Failure consequence |
|---|---|---|---|---|---|---|---|
| P5-A01 | categorical-quantum-mechanics | An `OperationalBridge` explicitly supplies systems, tests with finite outcomes, transformations, states, effects, closed-circuit evaluation, and a map from selected Paper 3 labels to effects. | `P5-C01`, `P5-C02` | `QM-CDP-2011`, `OUT-ABRAMSKY-HEUNEN-2019` | UNVALIDATED | construct the bridge from a Paper 3 model | labels still have no probability semantics |
| P5-A02 | categorical-quantum-mechanics | Sequential and parallel composition, operational equivalence, interchange, coarse-graining, convex mixing, and monoidal discarding satisfy the declared congruence laws. | `P5-C01`, `P5-C02` | operational framework laws | UNVALIDATED | prove every composition and quotient law | tests and transformations do not form an OPT |
| P5-A03 | categorical-quantum-mechanics | Operational state and effect quotients are finite-dimensional ordered real vector spaces, and positive normalized evaluation assigns every closed circuit a probability. | `P5-C01`, `P5-C02` | `QM-CDP-2011` | UNVALIDATED | construct ordered quotients and prove finite tomography | CDP theorem is outside scope |
| P5-A04 | categorical-quantum-mechanics | Causality holds: preparation probabilities are independent of later observation choice, equivalently each system has a unique deterministic effect. | `P5-C02` | `QM-CDP-2011` Axiom 1 | UNVALIDATED | prove unique discarding | signalling from future test choice remains possible |
| P5-A05 | categorical-quantum-mechanics | Perfect distinguishability holds for every state that is not completely mixed. | `P5-C02` | `QM-CDP-2011` Axiom 2 | UNVALIDATED | verify the exact state-space principle | the CDP reconstruction cannot be invoked |
| P5-A06 | categorical-quantum-mechanics | Ideal compression exists for every state, lossless on its face and maximally efficient. | `P5-C02` | `QM-CDP-2011` Axiom 3 | UNVALIDATED | construct encodings and decodings with both properties | the CDP reconstruction cannot be invoked |
| P5-A07 | categorical-quantum-mechanics | Local distinguishability holds for every relevant composite, giving finite-dimensional local tomography. | `P5-C02` | `QM-CDP-2011` Axiom 4 | UNVALIDATED | prove product effects separate bipartite states | real and other nonlocal alternatives survive |
| P5-A08 | categorical-quantum-mechanics | Pure conditioning holds: a nonzero conditional state of a pure bipartite state under an atomic effect is pure. | `P5-C02` | `QM-CDP-2011` Axiom 5 | UNVALIDATED | prove atomic-effect conditioning | the CDP reconstruction cannot be invoked |
| P5-A09 | categorical-quantum-mechanics | Every state has a purification, and purifications on a fixed purifying system are related by a reversible transformation on that system. | `P5-C02` | `QM-CDP-2011` Purification Postulate | UNVALIDATED | prove existence and essential uniqueness separately | the complex quantum conclusion is unavailable |
| P5-A10 | categorical-quantum-mechanics | On an already supplied separable real or complex Hilbert space of dimension at least three, probabilities are normalized countably additive noncontextual measures on closed subspaces/projections. | `P5-C04` | `QM-GLEASON-1957` | UNVALIDATED | verify Hilbert, dimension, normalization, and sigma-additivity hypotheses | standard Gleason is unavailable |
| P5-A11 | categorical-quantum-mechanics | For dimension two, a positive normalized valuation is defined on all effects, additive and noncontextual across all finite POVMs. | `P5-C04` | `QM-BUSCH-2003`, `QM-CFMR-2004` | UNVALIDATED | construct the all-effects valuation and prove POVM noncontextuality | qubit Born form has a gap |
| P5-A12 | categorical-quantum-mechanics | One theorem covers real, complex, quaternionic, low-dimensional, infinite-dimensional, and superselection cases. | `P5-C05` | master-classification target | UNVALIDATED | exhibit one theorem with a single compatible hypothesis class | incompatible theorem scopes obstruct the target |
| P5-A13 | categorical-quantum-mechanics | The reconstruction signature contains no collapse law, beable, preferred branch or outcome, observer cut, or ontology for the density operator. | `P5-C06` | interpretation-boundary audit | UNVALIDATED | mechanical signature and prose audit | the measurement nonclaim may be overstated |
| P5-A14 | categorical-quantum-mechanics | The Barnum-Wilce comparison uses finite-dimensional state-complete order-unit probabilistic models. | `P5-C03` | `QM-BARNUM-WILCE-2012` | UNVALIDATED | construct the order-unit models and prove state completeness | the Jordan comparison is ill-typed |
| P5-A15 | categorical-quantum-mechanics | Every comparison-route state cone is homogeneous. | `P5-C03` | Koecher-Vinberg hypothesis | UNVALIDATED | prove automorphism transitivity on the cone interior | Euclidean Jordan structure is unavailable |
| P5-A16 | categorical-quantum-mechanics | Every comparison-route state cone has a supplied self-dualizing inner product. | `P5-C03` | Koecher-Vinberg hypothesis | UNVALIDATED | construct and prove self-duality | Euclidean Jordan structure is unavailable |
| P5-A17 | categorical-quantum-mechanics | Composite self-dualizing forms factorize, or the theory has the full dagger-HSD structure required by the selected Barnum-Wilce proposition. | `P5-C03` | `QM-BARNUM-WILCE-2012` Propositions 1 and 16 | UNVALIDATED | verify one route without mixing their premises | complex selection does not follow |
| P5-A18 | categorical-quantum-mechanics | Relevant composites are allowed non-signalling probabilistic models and are locally tomographic for every pair retained in the theory. | `P5-C03` | `QM-BARNUM-WILCE-2012` | UNVALIDATED | prove closure, non-signalling, and tomography | real/quaternionic Jordan alternatives remain |
| P5-A19 | categorical-quantum-mechanics | The comparison theory contains an actual Euclidean-Jordan qubit object `M_2(C)_sa`. | `P5-C03` | `QM-HANCHE-OLSEN-1985`, `QM-BARNUM-WILCE-2012` | UNVALIDATED | construct the qubit object and its composites | Hanche-Olsen complex selection is inapplicable |
| P5-A20 | categorical-quantum-mechanics | The quantum-logic comparator is an irreducible complete atomistic orthomodular lattice with covering law and rank at least four. | none | `QM-PIRON-EXPOSITION-2007` | UNVALIDATED | exact lattice and rank audit | Piron representation theorem is unavailable |
| P5-A21 | categorical-quantum-mechanics | The Solèr comparator has an involutive division ring, an orthomodular Hermitian form, and an infinite orthonormal sequence. | none | `QM-SOLER-1995`, `QM-HOLLAND-SOLER-1995` | UNVALIDATED | verify all form and sequence hypotheses | exotic division-ring models remain |
| P5-A22 | categorical-quantum-mechanics | Any time evolution is a separately chosen strongly continuous one-parameter automorphism or unitary group with a declared generator domain. | none | `DYN-STONE-1932` | UNVALIDATED | construct the dynamics and prove continuity | reversible-map classification selects no Hamiltonian |
| P5-A23 | categorical-quantum-mechanics | Conditional state updates are supplied by an instrument or measurement process, not inferred from a POVM alone. | none | `QM-DAVIES-LEWIS-1970`, `QM-OZAWA-1984` | UNVALIDATED | construct the instrument and show its outcome effects | measurement probabilities do not fix updates |

## Paper 6 assumptions

| Assumption ID | Paper | Assumption | Needed by | Source or rationale | State | Required validation | Failure consequence |
|---|---|---|---|---|---|---|---|
| P6-A01 | categorical-coarse-graining | The analytic model is the version 3 grand-canonical system of deterministic hard spheres of diameter epsilon in R^d, d at least 2, with the source's pathological null set excluded and its initial law. | `P6-C01`, `P6-C01c`, `P6-C03`, `P6-C04` | `KIN-DENG-HANI-MA-2024` | UNVALIDATED | full model and law construction from earlier interfaces | physical realization branch remains open |
| P6-A02 | categorical-coarse-graining | Fixed-N probability marginals, grand-canonical rescaled correlations, and finite executable states inhabit distinct declared categories with explicit comparison maps. | `P6-C01`, `P6-C01c` | categorical type discipline | UNVALIDATED | measurable categories, variance, identities, and composition | no full functor can be claimed |
| P6-A03 | categorical-coarse-graining | Each claimed coarse map is linear or affine, positive, mass preserving where normalized, permutation compatible, and compositional, with nonfaithfulness and lost correlations explicit. | `P6-C01`, `P6-C01c` | `CE-P6-01`, `CE-P6-08` | UNVALIDATED | full interface proof beyond the finite rational model | registered physical coarse-graining claim remains open |
| P6-A04 | categorical-coarse-graining | The hard-sphere map uses a unit normal and conserves vector momentum and kinetic energy; the Kac comparator conserves energy only; law-level measurability and kernel symmetry are separate. | `P6-C02` | `KIN-KAC-1956`, `KIN-DENG-HANI-MA-2024` | UNVALIDATED | measurable physical realization and domain proof | bundled physical invariant claim remains open |
| P6-A05 | categorical-coarse-graining | Executable evidence is restricted to finite generated cases, adversarial inputs, and the exported floating-point tolerance. | `P6-C02`, `P6-C02b` | computational evidence boundary | UNVALIDATED | independent code review and repeated native test gate | computational status cannot be maintained |
| P6-A06 | categorical-coarse-graining | The initial density is nonnegative and normalized, the grand-canonical law is exactly the version 3 law, and the required initial spatial and Maxwellian bounds hold. | `P6-C03`, `P6-C04` | `KIN-DENG-HANI-MA-2024` | UNVALIDATED | exhibit data satisfying the theorem hypotheses | conditional correlation theorem cannot be applied |
| P6-A07 | categorical-coarse-graining | The deterministic hard-sphere flow exists and is measure preserving outside the source's null pathological set on the selected interval. | `P6-C03`, `P6-C04` | `KIN-DENG-HANI-MA-2024` | UNVALIDATED | flow and null-set dependency audit | ensemble evolution is unavailable |
| P6-A08 | categorical-coarse-graining | The analytic branch uses E(N) epsilon^(d-1) approximately 1, while the canonical comparator uses N epsilon^(d-1)=1; neither is an unspecified large-N limit. | `P6-C03`, `P6-C04` | `KIN-GALLAGHER-SAINT-RAYMOND-TEXIER-2013`, `KIN-DENG-HANI-MA-2024` | UNVALIDATED | scaling realization audit | limiting equation may differ |
| P6-A09 | categorical-coarse-graining | The imported dependency is Deng-Hani-Ma arXiv:2408.07818 version 3, Theorem 1, including its own cumulant and collision-history proof package. | `P6-C03`, `P6-C04` | `KIN-DENG-HANI-MA-2024` | UNVALIDATED | version and theorem-scope audit | conditional theorem reference is invalid |
| P6-A10 | categorical-coarse-graining | Classical balances use a sufficiently regular and integrable solution, while renormalized conclusions use their distinct weak formulation and defect structure. | `P6-C05`, `P6-C05b`, `P6-C05c` | `KIN-GALLAGHER-SAINT-RAYMOND-TEXIER-2013`, `KIN-DIPERNA-LIONS-1989` | UNVALIDATED | exact solution-class audit | equalities or inequalities may be unjustified |
| P6-A11 | categorical-coarse-graining | The hard-sphere kernel has the nonnegativity, exchange and pre/post symmetries, unit Jacobians, collision invariants, integrability, and boundary behavior needed by each conservation and entropy formula. | `P6-C05`, `P6-C05b`, `P6-C05c` | `KIN-BOLTZMANN-1872`, `KIN-GALLAGHER-SAINT-RAYMOND-TEXIER-2013` | UNVALIDATED | kernel and integral audit | H identity or conservation laws fail |
| P6-A12 | categorical-coarse-graining | On a selected finite interval, the Boltzmann solution exists, the uniform exp(2 beta \lVert v \rVert^2) L-infinity bound and finite Bol_(2 beta) initial spatial norms hold, and epsilon is small enough depending on (d,tfin,beta,A,B0). | `P6-C03`, `P6-C04`, `P6-C06` | `KIN-DENG-HANI-MA-2024` | UNVALIDATED | exhibit the full interval-specific theorem package | conditional long-time statement cannot be applied |

## Synthesis assumptions

| Assumption ID | Paper | Assumption | Needed by | Source or rationale | State | Required validation | Failure consequence |
|---|---|---|---|---|---|---|---|
| PS-A01 | synthesis | Every cross-paper input/output is typed and versioned by stable claim and assumption IDs. | `PS-C01` | durable composition | UNVALIDATED | dependency graph audit | hidden dependency |
| PS-A02 | synthesis | Terms shared across papers use the terminology contract or declare an explicit conversion. | `PS-C01` | prevent equivocation | UNVALIDATED | terminology audit | invalid cross-paper inference |
| PS-A03 | synthesis | Each realization branch consumes an actually established P1–P3 interface. | `PS-C02` | approved dependency structure | UNVALIDATED | evidence/review check | branch theorem is disconnected |
| PS-A04 | synthesis | Branch-specific assumption sets are preserved in the final conditional statement. | `PS-C02` | status discipline | UNVALIDATED | quantifier/assumption audit | synthesis overclaims |
| PS-A05 | synthesis | Composed claims refer to compatible artifact versions and jointly satisfiable assumptions. | `PS-C03` | `CE-PS-01` | UNVALIDATED | consistency and version audit | composition invalid |
| PS-A06 | synthesis | Every composed claim has current evidence and terminal independent review required by the execution plan. | `PS-C03` | review contract | UNVALIDATED | gate check | synthesis cannot cite it as passed |
| PS-A07 | synthesis | Open and obstructed bridges remain explicit in text, diagrams, metadata, and public summaries. | `PS-C04` | scientific stance | UNVALIDATED | multi-artifact status audit | missing proof is hidden |

## Update rules

1. Never reuse an assumption ID for a different proposition.
2. When an assumption is proved from earlier claims, set its state to
   `ESTABLISHED` and record exact claim/evidence paths.
3. When retained as physical input, set state to `POSTULATED` and explain why
   it is independently defensible.
4. When contradicted, set state to `REFUTED` and update every dependent claim.
5. A theorem may be at most `CONDITIONAL` while any dependency is merely
   `POSTULATED`; it remains `OPEN` while proof/evidence is absent.