backlog(B-0548): QG isomorphism Step 1.5 — construct strength θ:M(Ω)→Ω + A-lifting Ã:Zeta→Zeta

docs/backlog/P2/B-0548-qg-isomorphism-step-1-5-construct-strength-and-a-lifting-2026-05-16.md

@@ -0,0 +1,157 @@
+---
+id: B-0548
+title: QG isomorphism Step 1.5 — Construct strength θ:M(Ω)→Ω and A-lifting Ã:Zeta→Zeta for type-correct M/A coherence laws
+priority: P2
+status: open
+type: research
+created: 2026-05-16
+ask: Otto
+effort: L
+tags: [research, category-theory, topos-theory, axiomatization, qg-isomorphism, step-1-5, lawvere-tierney, strength, eilenberg-moore]
+depends_on: [B-0544]
+composes_with: [B-0543]
+last_updated: 2026-05-16
+---
+
+## Context
+
+This row exists because of the substrate-honest deferral pattern that surfaced
+in the [PR #3614](https://github.com/Lucent-Financial-Group/Zeta/pull/3614)
+review cycle (closed across 7 ticks 00:08Z–00:43Z on 2026-05-16). Codex
+correctly identified in [PR #3614](https://github.com/Lucent-Financial-Group/Zeta/pull/3614)
+that the three originally-proposed M/A coherence laws in the Step 1
+research doc were not well-typed under the stated signatures:
+
+- `M : Zeta → Zeta` (functor/monad on the topos)
+- `A : Ω → Ω` (modal operator on the subobject classifier)
+
+Specifically:
+
+- `M(A(p)) = A(M(p))`: `A(M(p))` needs `M(p) ∈ Ω`, but `M(p) : M(1) → M(Ω)`
+  under `M`'s functor-action on the morphism `p : 1 → Ω`
+- `A(μ_X) = μ_{A(X)} ∘ A(M(A(X)))`: `A(μ_X)` applies `A` to a morphism, but
+  `A` acts on `Ω` only; `A(X)` treats `X` as input to `A`, also untyped
+- `A(η_X) = η_{A(X)}`: same untyped problem
+
+[PR #3636](https://github.com/Lucent-Financial-Group/Zeta/pull/3636) struck
+the untyped laws and provided a substrate-honest reformulation:
+
+- **Provisional Law 1'** (type-correct for propositions only): for any `X`
+  in `Zeta` and any `p : X → Ω`, define `A_*(p) := A ∘ p` and
+  `M_*(p) := θ ∘ M(p)`. Memory-attention coherence:
+  `A_*(M_*(p)) = M_*(A_*(p))` — both sides type `M(X) → Ω`, contingent on a
+  strength `θ : M(Ω) → Ω`.
+- **Laws 2 and 3 (μ-coherence and η-coherence) deferred** to this Step 1.5
+  pending an `A`-lifting `Ã : Zeta → Zeta`.
+
+## Why this matters
+
+Without Step 1.5, the combined structure `Zeta_{RA}` (topos + memory monad +
+attention modal operator) has only propositional-level coherence (Law 1'),
+not full categorical coherence. The QG isomorphism proof path (B-0543) needs
+the full structure to ground the cosmology in falsifiable physics.
+
+## Goal
+
+Provide type-correct formulations of the three M/A coherence laws under
+either:
+
+- (a) An `A`-lifting `Ã : Zeta → Zeta` induced by `A` through the
+  subobject classifier
+- (b) A strength `θ : M(Ω) → Ω` plus appropriate Eilenberg-Moore algebra
+  structure on `Ω`
+- (c) A demonstration that propositional coherence (Law 1' only) suffices
+  for the infinite-poker semantics — Laws 2 and 3 are NOT actually needed
+
+## Resolution paths
+
+| Path | Construction | Cost | Status |
+|---|---|---|---|
+| (a) Lawvere-Tierney-style lifting | Define `Ã : Zeta → Zeta` induced by `A` through `Ω`; restate Laws 2, 3 using `Ã` | Standard for closure operators; needs adaptation since `A` is *not* a closure operator (no `p ≤ A(p)`) | Open — research-grade |
+| (b) Strength data on `M` | Define `θ : M(Ω) → Ω` ("Heyting strength"); restate Law 1' rigorously | Standard for monads on toposes when one wants Eilenberg-Moore semantics | Open — needs explicit `θ` construction; partial Provisional-Law-1' in [PR #3636](https://github.com/Lucent-Financial-Group/Zeta/pull/3636) |
+| (c) Restrict to propositional content | Phrase laws only for `p : X → Ω`; demonstrate Laws 2, 3 aren't needed for infinite-poker | Loses originally-intended structure but may suffice | Provisional Law 1' landed in [PR #3636](https://github.com/Lucent-Financial-Group/Zeta/pull/3636); requires semantic argument |
+
+## The closure-operator obstruction
+
+The standard Lawvere-Tierney construction requires `A` to be a **closure
+operator** (`p ≤ A(p)`). The Step 1 research doc explicitly denies this
+(line 76 of the research doc: "`A` is **not** a closure operator (it
+doesn't satisfy `p ≤ A(p)`)").
+
+This is the central technical obstruction for path (a). Possible workarounds:
+
+- A modified/weakened lifting that handles non-closure modal operators
+- Restriction to a sub-topos where `A` IS a closure operator
+- Using a different categorical machinery (e.g., factorization systems,
+  monads-with-cohomology) that doesn't require closure
+- Demonstrating that path (c) is the right path — Laws 2, 3 are formally
+  unnecessary
+
+**Note**: this obstruction is **closure-operator failure**, NOT
+non-monotonicity (which the research doc explicitly disclaims at line 84:
+"this is not non-monotonicity within a single context").
+
+## Acceptance criteria
+
+This row closes when ONE of the following is true:
+
+1. **(a) lands**: `Ã : Zeta → Zeta` constructed with explicit categorical
+   machinery; Laws 2 and 3 restated and provably type-correct using `Ã`;
+   construction handles the closure-operator-failure obstruction (or
+   restricts to a sub-topos where it doesn't apply)
+2. **(b) lands**: `θ : M(Ω) → Ω` constructed with explicit reference to
+   `M`'s preservation properties on `Ω`; Provisional Law 1' upgraded from
+   "provisional contingent on θ" to "proven for this θ"; Laws 2, 3 may
+   remain deferred
+3. **(c) lands**: Semantic argument that the infinite-poker semantics
+   requires only propositional coherence (Law 1'); Laws 2 and 3 formally
+   dropped from the combined structure `Zeta_{RA}`; updated Step 1 research
+   doc + B-0544 + B-0543 to reflect the reduced scope
+
+## Effort estimate: L (1-3 weeks)
+
+This is pure research. The work is:
+
+- Reading category theory literature on:
+  - Lawvere-Tierney topologies + modal operators on toposes (Mac Lane–Moerdijk
+    "Sheaves in Geometry and Logic" ch. V)
+  - Strength data on monads (Kock's papers on strong functors and
+    distributive laws)
+  - Eilenberg-Moore algebras on subobject classifiers
+- Investigating whether the closure-operator obstruction is fatal for path (a)
+  or admits workarounds
+- Constructing the concrete machinery (or proving it doesn't exist)
+- Updating the Step 1 research doc, B-0544, and Round 45 history entry
+
+Effort is "L" because the literature is well-established; the open question
+is whether the modal operator `A`'s specific properties (preserves finite
+limits within an observer-context; observer-relative across contexts) admit
+a lifting at all.
+
+## Prior art to investigate
+
+- **Lawvere-Tierney topologies** (closure operators on Ω) — the standard case
+- **Awodey-Kishida** on modal logic in toposes (covers non-closure operators?)
+- **Kock**'s monad-strength papers (for path b)
+- **Joyal-Tierney** on Galois theory of toposes (alternative liftings?)
+- **Goldblatt** "Topoi: The Categorial Analysis of Logic" — covers internal
+  modal logic
+- **QBism literature** — does the QBism observer-relative basis-shift give
+  any hint about which categorical machinery is appropriate?
+
+## Substrate composition
+
+- Composes with B-0543 (the proof-strategy umbrella row this work serves)
+- Depends on B-0544 (the Step 1 row this is a sub-task of)
+- Composes with `algebra-owner` skill (Z-set algebra, DBSP relationship)
+- Composes with `category-theory-expert` skill
+- Composes with `lean4-expert` skill (for eventual mechanical verification of
+  the constructed laws)
+- Composes with `theoretical-physics-expert` skill (for QBism connections)
+- Composes with the [PR #3614](https://github.com/Lucent-Financial-Group/Zeta/pull/3614)
+  → [#3626](https://github.com/Lucent-Financial-Group/Zeta/pull/3626)
+  → [#3636](https://github.com/Lucent-Financial-Group/Zeta/pull/3636)
+  → [#3639](https://github.com/Lucent-Financial-Group/Zeta/pull/3639)
+  → [#3646](https://github.com/Lucent-Financial-Group/Zeta/pull/3646)
+  → [#3650](https://github.com/Lucent-Financial-Group/Zeta/pull/3650) PR
+  chain that produced the substrate-honest formulation this row depends on