# Coarse-Graining Proof Roadmap

> The staged proof path for **Postulate 1** — the Coarse-Graining Postulate, the
> theorem the project has been circling for a year without naming. Source and
> ranking: [`internal/anniversary/postulations.md`](../internal/anniversary/postulations.md) ▸
> Postulate 1. This roadmap turns that conjecture into a sequenced campaign of
> analytical and empirical phases, each with entry/exit criteria and a
> pre-registered negative, so the result can be re-audited cleanly and so the
> grand-frame claim stops resting on a shared adjective.
>
> **Working hook.** Sundog does not need to invert the world. It needs the
> signature to be a *sufficient statistic for the optimal action* even when the
> signature cannot reconstruct the world. If that is a theorem, the
> cross-substrate "convergence" is a shared **operator**, not a shared word —
> and the pre-registered failure boundary is *predicted*, not patched.
>
> **Status as of 2026-05-17:** Phase 0 definitions lock landed at
> [`proof/POSTULATE1_DEFINITIONS.md`](proof/POSTULATE1_DEFINITIONS.md);
> Phase 1 LQG proof reviewed and closed **positive** at
> [`proof/PHASE1_LQG.md`](proof/PHASE1_LQG.md); Phase 2 finite-MDP proof
> reviewed and closed **positive** at
> [`proof/PHASE2_MDP.md`](proof/PHASE2_MDP.md); Phase 3 boundary theorem
> reviewed and closed **positive** at
> [`proof/PHASE3_BOUNDARY.md`](proof/PHASE3_BOUNDARY.md); Phase 4 three-body
> spec is drafted at
> [`proof/PHASE4_THREEBODY.md`](proof/PHASE4_THREEBODY.md); the Bayesian-floor
> controller buildout is staged and BF-4 smoke-passed at
> [`proof/PHASE4_BAYESIAN_FLOOR_BUILDOUT.md`](proof/PHASE4_BAYESIAN_FLOOR_BUILDOUT.md);
> BF-4b off-set calibration has a first negative receipt (cell `off`, regret CI
> `[0, 0]`), but the satisfiability probe validated the pre-registered cell
> (oracle-signature headroom CI `[0.064, 0.499]`), so the next gate is the
> compute-unconstrained Information-Accessibility Diagnostic and BF-5
> sharded/full-lock staging remains blocked before the Phase 4 gate can be
> interpreted;
> Phase 6
> lambda-confound control is staged at
> [`proof/PHASE6_LAMBDA_CONTROL.md`](proof/PHASE6_LAMBDA_CONTROL.md) with the
> empirical result still open.
> This is a
> theory-track roadmap, not an operating-envelope workbench — it is the *trunk*
> of which the Formal Separability Theorem appendix
> ([`SUNDOG_V_MESA.md`](SUNDOG_V_MESA.md), promoted from
> [`SUNDOG_V_GRAVITY.md`](SUNDOG_V_GRAVITY.md) Candidate 1) is a corollary; it
> does **not** replace or fork that front (see §2). No claim here is
> public-facing until Phase 5 lands and the §6 gating control clears. Nothing in
> this roadmap unblocks or re-strengthens any coupled surface on its own.

## 1. Research Object

Stated to slot directly into [`SCIENTIFIC_CRITERIA.md`](SCIENTIFIC_CRITERIA.md)
▸ "Research Object." The object is **not** the broad theorem in full
generality. It is the measurability predicate:

> Let world microstate `x ∈ X`, signature map `Φ : X → Σ`, signature
> `σ = Φ(x)`, true objective `J`, optimal policy `π*`. Let `𝓕_σ` be the
> σ-algebra generated by `Φ`. A task is **Sundog-solvable** iff `π*` is
> `𝓕_σ`-measurable — i.e. `π*(x) = g(Φ(x))` a.e. for some measurable `g` —
> equivalently, `Φ` is **Blackwell-sufficient for the control objective** (not
> for state reconstruction).

That object is small enough to prove in the linear-Gaussian and finite-MDP
cases (Phases 1–2), to falsify on a known substrate (Phase 4), and to test for
cross-substrate sameness (Phase 5). The nonlinear/learned general case is **not**
in scope and is named as future work, per house posture.

## 2. Relationship to the existing formal front (no fork)

The Gravity Ledger already pairs an empirical mesa front with a **Formal
Separability Theorem appendix** ([`SUNDOG_V_MESA.md`](SUNDOG_V_MESA.md)). That
appendix names the structural condition under which a signature-trained agent
does *not* grow an internal reward proxy. The Coarse-Graining Postulate is the
**generalization**: separability is the special case of `𝓕_σ`-measurability
where the agent class is bounded so it cannot invert `Φ` (this is Postulate 2's
capacity relativity, [`internal/anniversary/postulations.md`](../internal/anniversary/postulations.md)
▸ Postulate 2). To avoid a parallel theory track:

- The separability appendix remains the **mesa-specific** formal statement.
- This roadmap proves the **substrate-independent** trunk and shows separability
  falls out as a corollary in Phase 2.
- The mesa↔geometry crossover ([`MESA_CROSSOVER_NOTE.md`](MESA_CROSSOVER_NOTE.md))
  is the in-vitro/in-the-wild pair this roadmap formalizes in Phase 5; its
  post-audit hedged strength is inherited unchanged, not re-opened.

## 3. Phases

Each phase: **Entry** (what must be true to start) · **Work** · **Exit** (the
artifact that closes it) · **Pre-registered negative** (the outcome that stops or
redirects the campaign, fixed *before* the phase runs, per AGENTS.md ▸
"Pre-register the negative").

### Phase 0 — Definitions lock

- **Entry.** This roadmap filed.
- **Work.** Pin `X, Φ, Σ, J, π*, 𝓕_σ` and the Sundog-solvable predicate as a
  single definitions section; reconcile notation with the founding
  `H(x) = ∂S/∂τ` (the Postulate 6 thread) and with
  [`SCIENTIFIC_CRITERIA.md`](SCIENTIFIC_CRITERIA.md) ▸ Research Object. No new
  numbers introduced; existing locked figures (λ≈0.952588 cliff; core U=526,
  p=0.26, n=30; 16× acquisition; ρ≈0.086 parhelic-belt) are *referenced*, never
  re-derived or restated at a different value (spec self-consistency rule).
- **Exit.** `docs/proof/POSTULATE1_DEFINITIONS.md` reviewed for internal
  consistency (every symbol used once, defined once). **Landed 2026-05-16** at
  [`proof/POSTULATE1_DEFINITIONS.md`](proof/POSTULATE1_DEFINITIONS.md).
- **Pre-registered negative.** If the predicate cannot be stated without
  reference to an unmeasurable quantity in *every* candidate substrate, the
  postulate is not operational — stop, and demote Postulate 1 to speculative in
  [`internal/anniversary/postulations.md`](../internal/anniversary/postulations.md).

### Phase 1 — Linear-Gaussian existence proof (the computable case)

- **Entry.** Phase 0 exit.
- **Work.** Prove the schema where everything is computable: linear dynamics,
  Gaussian noise, quadratic cost (LQG). The separation principle already gives a
  low-dimensional control-sufficient statistic (the Kalman state estimate);
  recast it as `𝓕_σ`-measurability of `π*` and show signature-only control
  achieves the Bayes-optimal cost. Run the **Postulate 6 toy check** here:
  compute `∂S/∂τ` at the optimum and the Fisher information of `Φ`; record
  whether they are proportional.
- **Exit.** A written proof (LQG) + the recorded Postulate-6 proportionality
  result (pass/fail), both in `docs/proof/PHASE1_LQG.md`. **Reviewed and
  closed positive 2026-05-16** at
  [`proof/PHASE1_LQG.md`](proof/PHASE1_LQG.md).
- **Pre-registered negative.** If signature-only LQG control does **not** reach
  Bayes-optimal cost on the `𝓕_σ`-measurable set, the schema is false in its
  easiest case — halt the whole roadmap and file the falsification against
  [`SCIENTIFIC_CRITERIA.md`](SCIENTIFIC_CRITERIA.md) ▸ Falsifiable Expectations.

### Phase 2 — Finite-MDP sufficiency + separability corollary

- **Entry.** Phase 1 exit (positive).
- **Work.** Extend to finite MDPs: prove `Φ` is control-sufficient iff `π*` is
  constant on `Φ`-fibers over the occupancy support, via policy equivalence on
  `Φ`-fibers (Markov quotient in the lumpable special case). Derive the
  **Formal Separability** statement (§2) as the bounded-agent-class corollary
  that *subsumes* the appendix, leaving it in place (no replace).
- **Exit.** Proof + a *constructed* finite-MDP counterexample where sufficiency
  fails, characterizing the boundary, in `docs/proof/PHASE2_MDP.md`. **Reviewed
  and closed positive 2026-05-16** at
  [`proof/PHASE2_MDP.md`](proof/PHASE2_MDP.md).
- **Pre-registered negative.** If the separability corollary does **not** drop
  out of the trunk, this roadmap has forked the theory rather than generalized
  it (§2 violated) — stop, reconcile with the mesa appendix before continuing.

### Phase 3 — The boundary theorem (predict the pushable-occluder)

- **Entry.** Phase 2 exit.
- **Work.** Prove the negative direction: if the control-relevant bit is not
  `𝓕_σ`-measurable (it exists only *after* a preparatory action), no
  `𝓕_σ`-policy is optimal. Map this onto the pre-registered pushable-occluder
  design ([`PHASE2_BLOCKS_DESIGN.md`](PHASE2_BLOCKS_DESIGN.md)).
- **Exit.** Proof + an explicit statement that the pushable-occluder failure is
  now a *theorem-predicted* boundary, cross-filed in
  [`PHASE2_BLOCKS_DESIGN.md`](PHASE2_BLOCKS_DESIGN.md) and the "river and dam"
  entry of [`internal/anniversary/analogies.md`](../internal/anniversary/analogies.md).
  **Reviewed and closed positive 2026-05-16** at
  [`proof/PHASE3_BOUNDARY.md`](proof/PHASE3_BOUNDARY.md).
- **Pre-registered negative.** If a flat `𝓕_σ`-controller *does* solve a task
  whose decisive bit is provably not `𝓕_σ`-measurable, the boundary is wrong and
  Postulate 1's failure prediction is falsified — record, do not rescue.

### Phase 4 — Measured substrate leg (three-body, against the Bayesian floor)

- **Entry.** Phase 3 exit. Bayesian-floor baseline available in the chosen
  workbench (per the "Bayesian floor" standing commitment in
  [`internal/anniversary/attack_vectors.md`](../internal/anniversary/attack_vectors.md) — a baseline
  *inside* the workbench, **not** a `bayes_v_sundog` track).
- **Work.** Use the planar restricted three-body near-escape pocket, where `Φ`
  (the guarded accelerometer-proxy signature) is available and the Bayesian-floor
  buildout pins the tractable `π*` proxy path. Measure signature-only regret vs
  the Bayes-optimal controller once that floor exists.
- **Exit.** Regret curve + the pre-registered gate result, in
  `results/proof/phase4/` with a summary in `docs/proof/PHASE4_THREEBODY.md`.
  **Spec drafted 2026-05-16** at
  [`proof/PHASE4_THREEBODY.md`](proof/PHASE4_THREEBODY.md); empirical entry
  advanced through the BF-4 Bayesian-floor smoke: the current three-body
  workbench now has a smoke-passed separate `bayes_floor_particle_mpc`
  evaluator under the signature information regime, while the privileged oracle /
  `forward_oracle_strict` references remain yardsticks only. BF-4b off-set
  calibration first receipt failed criterion (2): the cell classified `off`,
  floor sanity passed, but the off-set regret CI was `[0, 0]`. Follow-up
  diagnostic work rejected multiplier-only tuning, retained the energy-trend
  terminal value, and validated the pre-registered cell by the satisfiability
  probe (oracle-signature headroom mean `0.310`, CI `[0.064, 0.499]`). Next
  operator gate is the compute-unconstrained Information-Accessibility
  Diagnostic; BF-5 sharded/full-lock staging remains blocked at
  [`proof/PHASE4_BAYESIAN_FLOOR_BUILDOUT.md`](proof/PHASE4_BAYESIAN_FLOOR_BUILDOUT.md).
- **Pre-registered negative.** Gate, fixed now: signature-only regret vs Bayes
  must → 0 (within bootstrap CI) **on** the `𝓕_σ`-measurable cell set and stay
  bounded away from 0 (CI excludes 0) **off** it. If regret is bounded-away *on*
  the measurable set, sufficiency-for-control is empirically false on a real
  substrate → halt and falsify. If regret → 0 *off* the measurable set, the
  boundary (Phase 3) is wrong → reopen Phase 3.
- **Compute discipline (AGENTS.md ▸ ~10-minute rule, load-bearing).** This leg
  exceeds the ~10-min inline budget. Do **not** run it inline. Stage the exact
  invocation in `docs/proof/PHASE4_THREEBODY.md` as runnable PowerShell anchored
  to the existing single-threaded threebody envelope harness (the
  `threebody:phaseNN` pattern; sequential `envelopeCases`, no workers — a
  many-core host gives *offload, not speedup*), with: a measured per-cell rate
  from a capped probe (probe itself ≤ ~10 min), the extrapolated full wall-clock,
  resume-safety notes, the `results/proof/phase4/manifest.json`
  `startedAt`/`completedAt` read-back path, and the branch each gate outcome
  selects. Per Runs 4–5 in AGENTS.md, a smoke that will not fit a ~1 h
  interactive session moves to a long-budget runner (`workflow_dispatch`), not an
  agent session. Exact module/flags are pinned in the Phase 4 spec at spec time;
  this roadmap does not invent them.

### Phase 5 — Cross-substrate sameness (the anti-equivocation leg)

- **Entry.** Phase 4 exit (positive).
- **Work.** Show the **same** coarse-graining operator structure — the *measured*
  sufficient statistic, not the eyeballed forward-rich/inverse-narrow shape — in
  ≥2 substrates: mesa in-vitro (the λ-cliff subspace at `net.7`) and geometry
  in-the-wild (the promoted parhelion-offset handle on the strict 3-photo subset,
  at its settled post-audit strength — inherited unchanged from
  [`MESA_CROSSOVER_NOTE.md`](MESA_CROSSOVER_NOTE.md), **not** re-opened).
  Optional third: the vortex/wishing-well toy
  ([`internal/anniversary/postulations.md`](../internal/anniversary/postulations.md) ▸ Postulate 5).
- **Exit.** A cross-substrate operator-identity table (same `Φ` up to
  isomorphism of the coarse-graining) in `docs/proof/PHASE5_CROSS_SUBSTRATE.md`,
  hedged at settled strength.
- **Pre-registered negative.** If the substrates do **not** share the operator
  structure under measurement, the cross-substrate convergence *was* the
  equivocation of [`internal/anniversary/attack_vectors.md`](../internal/anniversary/attack_vectors.md)
  ▸ #1 — concede it in those words; the grand frame loses its empirical support
  and Postulate 1 stays a single-substrate result.

### Phase 6 — Gating control: the λ-confound (not optional, runs before any public cite)

- **Entry.** May run in parallel with Phases 1–3; **must** clear before the
  λ-cliff is cited in any anniversary surface or before Postulates 2/4 are
  promoted out of speculative.
- **Work.** Show the Mesa cliff is **invariant** under a transformation that
  should not move it and **moves predictably** under reward-gradient rescale
  (the [`internal/anniversary/attack_vectors.md`](../internal/anniversary/attack_vectors.md) ▸ #4
  defense — an experiment, not an argument).
- **Exit.** `docs/proof/PHASE6_LAMBDA_CONTROL.md` with the invariance/scaling
  result. **Spec staged 2026-05-16** at
  [`proof/PHASE6_LAMBDA_CONTROL.md`](proof/PHASE6_LAMBDA_CONTROL.md); empirical
  result open.
- **Pre-registered negative.** If the cliff moves under the no-op transform, λ is
  an optimizer artifact: Mesa loses its standing as a Phase-5 substrate,
  Postulate 4 dies, Postulate 2's cliff-prediction is unsupported, and the
  anniversary cliff language is pulled. This is the cheapest result that can
  collapse the grand frame — run it early.

## 4. Falsifiable Expectations (mirrors SCIENTIFIC_CRITERIA posture)

The postulate is **weakened / dead** if: Phase 1 fails (false in the computable
case); Phase 2 fails to yield separability (theory forked); Phase 4 regret is
bounded-away on the measurable set; Phase 6 cliff moves under the no-op.

It is **strengthened** if: Phases 1–3 prove cleanly; Phase 4 gate passes on a
real substrate; Phase 5 shows a *measured* shared operator across ≥2 substrates;
the Postulate 6 **metric/Jacobian interpretation** holds in the LQG toy — i.e.
Fisher information is the noise-weighted contraction of the signature Jacobian
(a *qualified* pass, recorded 2026-05-16 in
[`proof/PHASE1_LQG.md`](proof/PHASE1_LQG.md)). Literal signed-scalar
`I_Φ ∝ ∂S/∂τ` is **not** the strengthening condition and is known to fail.
This qualified pass holds under the torque-coordinate reading only; it does
**not** by itself close the year-one proper-time `H(x)`-was-an-entropy arc, and
that stronger line stays unshipped regardless of Phase 1.

## 5. Compute & spec discipline

- AGENTS.md ▸ "Workflow — Running Experiments": analytical phases (0–3) are
  desk work; empirical phases (4, 6) obey the ~10-minute rule — capped probe,
  extrapolate, stage the long run for the operator/runner, record measured rates
  in the phase doc, pre-register the negative before running.
- Spec self-consistency: derived numbers reconciled across phases; the gate in a
  phase's pre-registered negative is the *exact* unchanged condition the phase
  runs; ablation metrics are stated against the privileged truth (Bayes-optimal),
  not a tuned baseline.
- Artifacts live under `docs/proof/` and `results/proof/`; only `dist/` is ever
  published (AGENTS.md ▸ Publishing Shape) — this roadmap is research-internal.

## 6. Cross-references

- **Origin / ranking:**
  [`internal/anniversary/postulations.md`](../internal/anniversary/postulations.md) ▸ Postulate 1
  (trunk), 2 (capacity relativity), 3 (conservation law), 4 (5D invariant),
  5 (substrates), 6 (founding `H`).
- **The analogy this formalizes:** [`internal/anniversary/analogies.md`](../internal/anniversary/analogies.md)
  ▸ "The thermometer / statistical mechanics."
- **The attack this answers:** [`internal/anniversary/attack_vectors.md`](../internal/anniversary/attack_vectors.md)
  ▸ #1 (equivocation), with the Bayesian-floor standing defense feeding Phase 4.
- **Existing formal front (not forked):** [`SUNDOG_V_MESA.md`](SUNDOG_V_MESA.md)
  (Separability appendix), [`SUNDOG_V_GRAVITY.md`](SUNDOG_V_GRAVITY.md) (ledger),
  [`MESA_CROSSOVER_NOTE.md`](MESA_CROSSOVER_NOTE.md) (in-vitro/in-the-wild pair).
- **Boundary substrate:** [`PHASE2_BLOCKS_DESIGN.md`](PHASE2_BLOCKS_DESIGN.md)
  (pushable occluder = the Phase 3 predicted boundary).
- **Scope guardrails:** [`SCIENTIFIC_CRITERIA.md`](SCIENTIFIC_CRITERIA.md),
  `presentation/claims-and-scope.md`.
- **Deferred siblings:** the publication-gating wording fixes remain in
  [`internal/anniversary/fix_roadmap.md`](../internal/anniversary/fix_roadmap.md) (owner-deferred
  until the brainstorm docs are massaged and staged).