Morphisms between instances: typed-wasm needs them for cross-level grade transport (L11 → L16) #3

Need

typed-wasm (PWL-01) now uses this repository's kernel as the grade kernel for several levels. It takes it by pin at cf9235c and re-proves it as an Idris2 port in src/abi/TypedWasm/ABI/ResourceAlgebra*. The port came in with hyperpolymath/typed-wasm#271, #273 and #274; main is at 117bbf8. Each level picks one instance:

The PWL-01 roadmap has the item "resource-algebra homomorphisms (OPEN) → cross-level grade transport (L11 → L16) as a theorem". typed-wasm consumes definitions by pin and does not re-declare them. So the morphism notion should live here, not be invented downstream. PROOF-STATUS lists it as Open: "Homomorphisms between instances are not defined".

What would unblock it

1. A strict morphism record in Core.agda. h 𝟘 ≡ 𝟘, h 𝟙 ≡ 𝟙, h (a ⊕ b) ≡ h a ⊕ h b, h (a ⊗ b) ≡ h a ⊗ h b, plus identity and composition. With it, transport through K-CUT is one induction on the global type: gradeAt p (map h G) ≡ h (gradeAt p G). That lemma would sit on the choreographic-types side.

2. A lax variant for ordered algebras. h monotone, h 𝟙 ≡ 𝟙, h (a ⊕ b) ≡ h a ⊕ h b, h (a ⊗ b) ≼ h a ⊗ h b. h 𝟘 ≽ 𝟘 holds automatically, since 𝟘 is least. This is the variant typed-wasm can actually use. The one map between instances already in use is lax, and it cannot be strict:

   • peak : HWM → MaxPlus preserves ⊕ (componentwise max) and 𝟙.
   • On ⊗ it is lax: max p₁ (n₁ + p₂) ≤ p₁ + p₂, which needs drift ≤ peak. This is S-1 as a law. occupancy-types states it as R-3 occupancy≤cost; typed-wasm re-proves it as Occupancy.occupancyLeCost / protocolOccupancyLeCost.
   • It cannot be strict, because HWM's 𝟘 ≡ 𝟙 would force bot ≡ val 0 (C-4 / H-3). The same holds for every map out of HWM into Loss or MaxPlus.

3. The separation as a theorem about morphisms (proof sketch, not mechanised). Every strict morphism between Loss and MaxPlus, in either direction, sends all positive grades to a single point. Loss → MaxPlus:

   • fin n is fin 1 ⊗-iterated n times. Write x = h (fin 1).
   • fin 1 = fin 1 ⊕ fin 2 gives x = max x (x + x).
   • So x = bot (the zero test: fin 0 ↦ val 0, everything else ↦ bot) or x = val 0 (the support map: fin _ ↦ val 0, inf ↦ bot).
   • Both of these are strict morphisms and there are no others. The direction MaxPlus → Loss is symmetric.

   This is the precise form of "no grade-preserving identification on the embedded naturals". It also says cross-level transport between Loss and MaxPlus can only be lax or degenerate.

Related question: a MinMax instance?

typed-wasm's L11 bottleneck (Tropical.tropMax) is the min-max semiring on the Loss carrier: ⊕ = min, ⊗ = max, 𝟘 = +∞ (absorbing), 𝟙 = fin 0. It is neither min-plus nor max-plus. Because no instance here covers it, it is the one allowlisted exception to typed-wasm's one-min-plus/one-max-plus gate (tools/grade-kernel.allow).

If it became an instance here, typed-wasm would drop the allowlist entry and consume it by pin. The identity on the carrier, Loss → MinMax, is then a lax morphism (max a b ≤ a + b). That is the bridge between typed-wasm's two L11 readings: path bound and bottleneck. Whether to add it is your call.

Status in typed-wasm until this lands

typed-wasm claims no cross-level transport:

• No LEVEL-STATUS row asserts one.
• occupancyLeCost is stated as a lemma about HWM and MaxPlus, not as a morphism law.
• ResourceAlgebra/Separation.idr keeps the three grades apart.