diff --git a/docs/backlog/P2/B-0548-qg-isomorphism-step-1-5-construct-strength-and-a-lifting-2026-05-16.md b/docs/backlog/P2/B-0548-qg-isomorphism-step-1-5-construct-strength-and-a-lifting-2026-05-16.md new file mode 100644 index 000000000..6ff70eb6e --- /dev/null +++ b/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