hyperpolymath · hyperpolymath · Jun 16, 2026 · Jun 16, 2026
@@ -53,8 +53,8 @@ between 2026-04-13 (AST landed) and 2026-04-18 (verification).**
 | 8 | Effect-tracking | Effects.idr | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased.  Preorder + composition theorems added A5 (2026-04-18): `subsumeRefl` (alias of `effectSubsumesRefl`), `hasEffectTrans`, `subsumeTrans`, `hasEffectCombineL`/`CombineR`, `subsumePrepend`/`Append`, and the flagship `subsumeCompose` giving `EffectSubsumes d1 a1 -> EffectSubsumes d2 a2 -> EffectSubsumes (d1++d2) (a1++a2)` so L8 attestations compose.** |
 | 9 | Lifetime safety | Lifetime.idr | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased.  Preorder + load-safety theorems added A4 (2026-04-18): `outlivesRefl`, `outlivesTrans` (alias of pre-existing `outlivesTransitive` with 7-constructor case analysis), `loadSafe` proof-term, behavioural lemmas `loadSafeOffset` and `loadSafeIrrelevant` (proof irrelevance at the value level).** |
 | 10 | Linearity | Linear.idr (QTT q=1) | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased.  Propositional state-machine theorems added A3 (2026-04-18): distinctUsage, consumePreservesData, noReuse, noReuseEcho — usage-indexed handle `LinHandleU Fresh/Consumed tok` with `consume` state transition, alongside the QTT structural layer.** |
-| 11 | Tropical cost-tracking | Tropical.idr | Not yet | None | **In package (A1, 2026-04-18).  Commutative-semiring closure PROVEN (A2, 2026-04-18): all 12 axioms — tropAddLeftId/RightId/Comm/Assoc, tropMulLeftId/RightId/Comm/Assoc, tropMulLeftAnn/RightAnn, tropMulDistrib/DistribR.  Uses structural `tropMin` (007-lang template).  Zero dangerous patterns.** |
-| 12 | Epistemic safety | Epistemic.idr | Not yet | None | **In package (A1, 2026-04-18); A10 (2026-05-26) closes the previously-deferred "freshness propagation under concurrent writes" gap with the flagship `freshnessPropagatesUnderWrites` plus the supporting `concurrentWriteStales`, `resyncRecoversFresh`, `freshNotStale`, `freshImpliesEqual`, `staleImpliesLT`, `syncChainEndsFresh`, and the `epistemicFreshness` projector (closes PROOF-NEEDS §P1.2 "Level12Proof implies freshness"). 11 named theorems total.** |
+| 11 | Tropical cost-tracking | Tropical.idr | Not yet | None | **In package (A1, 2026-04-18).  Commutative-semiring closure PROVEN (A2, 2026-04-18): all 12 axioms.  Uses structural `tropMin` (007-lang template).  Zero dangerous patterns.  A16 (2026-06-16) estate accommodation: added the canonical dioid ORDER layer (`tropLe` refl/trans + add/mul monotonicity, mirrors `tropical-resource-typing` `Resource.Algebra.Ordered`), the MinMax BOTTLENECK layer (`tropMax` + `hubCeiling`, mirrors `Resource.Instances.MinMax` + `Bridge.hub_ceiling_le`), `ResidueMeasure` (E→R, mirrors `Resource.EchoBridge`), and `Level11BottleneckProof` + `bottleneckCeilsEdges` wired into `Proofs.attestL11_Bottleneck`/`_Sound`.** |
+| 12 | Epistemic safety | Epistemic.idr | Not yet | None | **In package (A1, 2026-04-18); A10 (2026-05-26) closes the "freshness propagation under concurrent writes" gap with `freshnessPropagatesUnderWrites` + supporting theorems (11 total; closes PROOF-NEEDS §P1.2).  A15 (2026-06-16) estate accommodation: ADDITIVE `syncGrade` layer reusing sibling `Tropical.TropCost` (∞ = never-synced) + `neverSyncedInfeasible`/`observedFeasible`/`observedNotInfeasible` — extant Nat-indexed proofs untouched.  Header IS-NOT note: this read-consistency model is a DIFFERENT problem from canonical `epistemic-types`' standpoint-indexed modality.** |
 | 13 | Module isolation | ModuleIsolation.idr | (per-module handles, future) | 12 parser/Checker tests | **v1.2 — Idris2 proof + surface checker live; 007 lowering DONE (task #5)** |
 | 14 | Session protocols | SessionProtocol.idr | (typed-state handles, future) | 13 parser/Checker tests | **v1.3 — Idris2 proof + surface checker live; 007 send/receive lowering DONE (task #7)** |
 | 15 | Resource capabilities | ResourceCapabilities.idr | (future) | 13 parser/Checker tests | **v1.4 — Idris2 proof + surface checker (L15-A + L15-B) live; L15-C call-graph check deferred to v1.4.x; 007 lowering DONE (task #9)** |
@@ -104,7 +104,7 @@ toolchain remains future work.
 | Proofs.idr | 0 | 0 | 0 | In package.  Attestation API hardened A7 (2026-04-18): every L1-L10 attestation now requires a witness from its level module (Schema / FieldIn / WasmTypeCompat / Ptr-NonNull / InBounds / AccessResult / ExclusiveWitness / EffectSubsumes / Lifetime.Outlives / CompletedProtocol).  `simpleReadCert` / `fullCert12` / `fullCert15` thread witnesses per level; the certificate cannot be constructed without real proof artefacts.  Level-achievement layer added A8 (2026-04-18): `LevelAchievedIn` predicate, `achievedAppendL` / `achievedAppendR` list-append preservation, `LevelAchieved n cert` lifted to certificates, `composeAchievedL` / `composeAchievedR` proving any level achieved in either component of `composeCertificates` is still achieved in the composition.  Attestation soundness A9 (2026-05-18): per-level `attestLN_Sound` family proving `LevelAchievedIn N [attestLN_X w]` — the weak "certificate claims level N" face.  A11 (2026-05-26): partial laws for `composeCertificates` — `achievedAppendSplit`, `composeAssocLists`, `composeAchievedSym`.  A12 (2026-05-26): switched `composeCertificates` from Ord-derived `Prelude.min` to structural `Data.Nat.minimum`; **full** `composeAssoc`; `composeHighProvenComm`.  Closes post-A10 audit item 4 in full.  **Witness-indexed redesign 2026-05-27 (PR #80, closes standards#130 long-tail)**: `LevelAttestationW : (n : Nat) -> Type` GADT with one ctor per level packaging the actual witness; 15 `attestLNW_*` smart ctors; 15 `attestLNW_Entails<Property>` extractors (a consumer holding `LevelAttestationW 7` can now discharge L7 alias-freeness via `ExclusiveWitness s`, not just the weak claim-predicate); `toLegacy` bridge; 15 round-trip `Refl`s; uniform `attestLW_AchievedIn` subsuming the A9 family.  **`WitnessCertificate` lift 2026-05-27 (PR #80, folded from #83)**: existential `SomeAttestationW` wrapper, `record WitnessCertificate` mirror of `ProofCertificate` with witness-carrying levels, `witnessToLegacy` bridge, `composeWitness` mirror, `composeWitnessLegacyAgree` compat lemma, `WitnessAchieved` predicate. |
 | Tropical.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) |
 | Epistemic.idr | 0 | 0 | 0 | In package (A1, 2026-04-18).  A10 (2026-05-26): propagation theorems added — `freshImpliesEqual`, `staleImpliesLT`, `freshNotStale` (mutual exclusion via local `ltIrreflexive`), `concurrentWriteStales`, `resyncRecoversFresh`, the flagship `freshnessPropagatesUnderWrites`, `syncChainEndsFresh`, and the `epistemicFreshness` projector on `Level12Proof` (closes PROOF-NEEDS §P1.2).  A11 (2026-05-26): constructor-tightening pass — `WriteSync` now demands a `FieldVersion` witness with three equality components (`field`/`version`/`lastWriter`), and `Knowledge.Observed` is grounded in a `Sync` event (no more unfounded versions).  Corollaries: `writeSyncIdentifiesWriter` returns the `FieldVersion` (+ the three projections) for an explicit-or-implicit Sync; `observedHasProvenance` extracts the witnessing prior-version and `Sync` from any `Observed` value. |
-| Echo.idr | 0 | 0 | 0 | In package (A0, 2026-04-18) |
+| Echo.idr | 0 | 0 | 0 | In package (A0, 2026-04-18).  A16 (2026-06-16) estate accommodation: header re-characterised to the accurate echo-types definition — a **tropically-graded modality of structured information loss** (grade = min-plus = `Tropical.TropCost` = irrecoverability), exact-on-a-fiber recoverability; monad/comonad/adjunction VARIANCE explicitly deferred to upstream `--safe` Agda (cf echo-types RETRACTION R-2026-05-18 + experimental R0–R4).  Added `EchoR` + `echoToResidue` (mirrors `echo-types` `EchoResidue.agda`; an attestation = a retained residue).  Categorical base remains the settled fiber/slice structure. |
 | VerifierSpec.idr | 0 | 0 | 0 | Introduced A13 (2026-05-26, PR #72) as statement-level spec-of-record for post-A10 items 7+8.  **Promoted to total bodies 2026-05-27 (PR #79)**: same `ModuleSummary` / `FunctionSummary` / `OwnershipIntent` shapes, plus structural acceptance predicates `TokenFresh` / `IntentsLinearAcceptable` / `FunctionsAccepted`, the three acceptance predicates `SpecAccepts` / `VerifierAccepts` / `SourceAccepts` (the latter two carry a `TrustedFixture` inline so the differential ctor still terminates in a structural witness), the two **agreement records `VerifierSpecAgreement` (item 7) and `SourceVerifierAgreement` (item 8)** with totally-proven bodies, concrete inhabitants `verifierSpecAgreement` / `sourceVerifierAgreement` (the first total no-`believe_me` agreement values in the codebase), end-to-end composition lemmas `sourceImpliesSpec` / `specImpliesSource` and `*Concrete` specialisations, demo modules (empty / `allocFreeModule` / `allocFreeWithBorrowModule` / `fixtureCleanLinearConsumerModule` mirrored from cross_compat row 1), and four discrimination proofs (`notSpecAcceptsBadDoubleConsume`, `notVerifierAcceptsBadDoubleConsume` ruling out BOTH ctors, `notSourceAcceptsBadDoubleConsume` ruling out BOTH ctors, `notSpecAcceptsBadDoubleProduce`) showing L10 has teeth and the differential escape hatch cannot smuggle a bad module past the verifier. |
 
 ## Post-codegen verifier (Rust)
@@ -190,3 +190,39 @@ failing differential-harness fixture or as an absent
   `typedwasm.ownership` section on every compile
 - `hyperpolymath/ephapax:src/ephapax-cli/` — exposes the verifier via
   `ephapax compile --verify-ownership`
+
+## Estate-axis accommodation (A15/A16 — 2026-06-16)
+
+An adversarially-verified audit (idris2 ground-truth) found that L11/L12 and
+the Echo module were internally sound and compiling but **not accommodated** to
+the canonical estate repos — each had been sourced/ported from somewhere *other*
+than the canonical repo (Tropical from `007-lang`, Echo from a dead
+`~/Desktop/EchoFibers.agda`, Epistemic independently reinvented), with stale or
+absent cross-references. This is the estate boundary-erosion pattern. The
+following accommodation work landed **local, unpushed, all type-checking under
+idris2 0.8.0** (`%default total`, no `believe_me`); the full `typed-wasm.ipkg`
+package builds green (22 modules):
+
+| Axis | Canonical repo | Accommodation |
+|------|----------------|---------------|
+| L11 Tropical | `tropical-resource-typing` (Lean4 `Resource.*`) @ `2e35229` | cross-doc fixed (was stale `f6c5a6f`, Isabelle-only); added `tropLe` dioid order (refl/trans/monotonicity ~ `Resource.Algebra.Ordered`), `tropMax` MinMax bottleneck + `hubCeiling` (~ `Resource.Instances.MinMax` + `Bridge.hub_ceiling_le`), `ResidueMeasure` (~ `Resource.EchoBridge`), `Level11BottleneckProof` + `bottleneckCeilsEdges` wired into `Proofs.attestL11_Bottleneck`/`_Sound` |
+| Echo | `echo-types` (Agda) @ `2bbdb49` | header re-characterised to the accurate definition — a **tropically-graded modality of structured information loss** (grade = min-plus = `Tropical.TropCost`), exact-on-a-fiber recoverability, variance (monad/comonad/adjunction) **deferred to upstream `--safe` Agda** (cf RETRACTION R-2026-05-18 + experimental R0–R4); added `EchoR` + `echoToResidue` (~ `EchoResidue.agda`) |
+| L12 Epistemic | `epistemic-types` (Agda) @ `87ff8b4` | cross-doc + IS-NOT note (read-consistency is a *different* problem from canonical standpoint-indexed modality); **additive** `syncGrade` reusing sibling `Tropical.TropCost` (∞ = never-synced) — extant A10–A14 proofs untouched |
+
+The min-plus grade is the **same object** across all three axes
+(`echo-types` loss grade ≡ `Resource.Instances.MinPlus` ≡ `epistemic-types`
+`EchoBridge.Grade` ≡ `Tropical.TropCost`) — echo/tropical/epistemic are one
+graded structure.
+
+**Upstream drafts prepped (local, unpushed, await owner review)** — three
+extend-upstream candidates, each verified by its own prover:
+
+- `tropical-resource-typing/Resource/Closure.lean` — Kleene/Floyd-Warshall
+  all-pairs closure functor over `[ResourceAlgebra R]` (order/monotonicity/bound
+  half proved; star-equation algebra deferred). `lake build` green, no axioms.
+- `epistemic-types/src/EpistemicTypes/ReadConsistency.agda` — version-monotone
+  re-sync liveness as a concrete `AccessibleModality` instance. `--safe`, closed.
+- `echo-types/proofs/agda/EchoDisplayed.agda` — `Displayed`/`DispHom`/
+  `fromHomOver` fibration packaging (no comonad claims). `--safe`, closed.
+
+Nothing pushed or PR'd — drafts are for owner review per the stop-first rule.
@@ -23,6 +23,33 @@ compile time" (true) and "here is a lemma proving it is forbidden"
 claims — a reviewer asking _"where is the theorem?"_ currently has no
 answer to point at.
 
+## RECONCILIATION 2026-06-16 (A15/A16 — estate-axis accommodation)
+
+> L11/L12/Echo have been **cross-documented and mirrored to the canonical
+> estate repos** after an adversarially-verified audit found them
+> internally-sound but un-accommodated (sourced/ported from non-canonical
+> origins). New, machine-checked (idris2 0.8.0, full `typed-wasm.ipkg` green):
+>
+> - **Tropical.idr** — dioid order `tropLe` (refl/trans + add/mul monotonicity),
+>   MinMax bottleneck `tropMax` + `hubCeiling`, `ResidueMeasure`, and a new
+>   `Level11BottleneckProof` + `bottleneckCeilsEdges` wired into
+>   `Proofs.attestL11_Bottleneck`/`_Sound`. Mirrors `tropical-resource-typing`
+>   `Resource.{Algebra.Ordered, Instances.MinMax, Bridge, EchoBridge}` @ 2e35229.
+> - **Echo.idr** — `EchoR` + `echoToResidue` (mirrors `echo-types`
+>   `EchoResidue.agda` @ 2bbdb49); header re-characterised: an echo-type is a
+>   **tropically-graded modality of structured information loss** (grade = min-plus
+>   = `Tropical.TropCost`), exact-on-a-fiber recoverability — the
+>   monad/comonad/adjunction VARIANCE is deferred to upstream `--safe` Agda
+>   (RETRACTION R-2026-05-18 + experimental R0–R4), NOT asserted here.
+> - **Epistemic.idr** — ADDITIVE `syncGrade` (∞ = never-synced) reusing the
+>   sibling `Tropical.TropCost`; extant A10–A14 Nat-indexed proofs untouched.
+>   Header IS-NOT note: read-consistency is a *different* problem from canonical
+>   `epistemic-types`' standpoint-indexed modality.
+>
+> Three extend-upstream drafts prepped local/unpushed (Lean closure functor;
+> Agda re-sync liveness `AccessibleModality` instance; Agda `DispHom` packaging),
+> each verified by its own prover. See LEVEL-STATUS.md "Estate-axis accommodation".
+
 ## RECONCILIATION 2026-06-02 (audit-boundary half of post-A10 items 7 + 8 promoted to ADR-0005 — read this FIRST)
 
 > **The "Full proof bodies for `VerifierSpecAgreement` /

@@ -49,13 +49,22 @@ Key capabilities delivered:
 * Example `.twasm` files for the checked core, plus draft higher-level examples
 * Whitepaper drafts (docs/WHITEPAPER.md + docs/arxiv/typed-wasm.tex) under audit
 * No unsound escape hatches in the checked Idris2 core (`believe_me`, `assert_total`)
+* Estate-axis accommodation (A15/A16, 2026-06-16): L11/L12/Echo now cross-document
+  and mirror the canonical estate repos -- `tropical-resource-typing` (Lean4
+  `Resource.*`: dioid order, MinMax/`hubCeiling` bottleneck, `ResidueMeasure`),
+  `echo-types` (Echo re-characterised as a tropically-graded loss modality;
+  `EchoR`/`echoToResidue`), `epistemic-types` (additive `syncGrade`). The min-plus
+  grade is one shared object across all three. See LEVEL-STATUS.md "Estate-axis
+  accommodation". Three upstream drafts prepped local/unpushed for owner review.
 
 Known audit constraints:
 
 * L11 (Tropical) and L12 (Epistemic) are in `typed-wasm.ipkg` since 2026-04-18
   (commit A1) and build clean under Idris2 0.8.0 (PROOF-NEEDS.md reconciliation
   2026-05-18). Treat them as research/draft for surface semantics, not for
-  ipkg membership.
+  ipkg membership. (A15/A16 2026-06-16 added the canonical estate cross-doc +
+  order/bottleneck/residue/sync-grade mirrors; the monad/comonad/adjunction
+  variance of the echo grade remains deferred to upstream `--safe` Agda.)
 * Release/build/container metadata still contains template residue
 * Benchmark and venue-facing paper claims require evidence cleanup before submission