hyperpolymath · hyperpolymath · May 30, 2026 · May 30, 2026 · May 30, 2026
@@ -0,0 +1,39 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
+
+# Handoff — paste into a Claude Code session scoped to hyperpolymath/maa-framework
+
+Resolve issue #84 ("is `absolute-zero/` a deliberate fork or stale vendor copy?").
+
+DECISION (made, HIGH confidence, verified by real `git diff` of both clones):
+**(B) stale vendor copy — convert `absolute-zero/` to a git submodule. NO extraction needed.**
+
+Authoritative findings — maa@9dbf56b subtree vs upstream `absolute-zero`@7da92b360deacb31d6fc8a2121da57ed6f47f4f9:
+- 1 file only in maa: `.github/workflows/jekyll-gh-pages.yml` (inert nested Pages workflow → drop)
+- 15 differing files: 6 proof files + 9 stale infra files. ALL 6 proof files are UPSTREAM-AHEAD:
+  0 maa-only theorems, 0 maa-only proofs, 0 sorry/admit/Admitted either side. maa just has more
+  inlined axioms because it predates upstream's refactor of kB/temperature/Shannon axioms into the
+  new shared modules proofs/coq/common/PhysicsConstants.v + StatMechBasis.v.
+- 2 files only upstream: those two new common/ modules.
+=> No maa-only proof work anywhere. Submodule swap loses nothing but the inert CI file.
+
+#84's premise is STALE (pre-PR #83 "re-vendor to upstream HEAD"). The files it calls "unique to maa"
+(EchoBridge*.agda, ECHIDNA_*, examples/go, proofs/coq/quantum/) are now byte-identical to upstream
+(sha256-verified). maa is simply behind.
+
+DO THIS:
+1. Re-verify (gates everything):
+   git clone https://github.com/hyperpolymath/absolute-zero /tmp/az
+   git -C /tmp/az checkout 7da92b360deacb31d6fc8a2121da57ed6f47f4f9
+   diff -rq --exclude=.git absolute-zero /tmp/az   # expect 1 only-in-maa (jekyll), 15 differ, 2 only-upstream
+   Eyeball jekyll-gh-pages.yml; if stock Pages deploy, drop it.
+2. git rm -r absolute-zero
+3. git submodule add https://github.com/hyperpolymath/absolute-zero absolute-zero
+   git -C absolute-zero checkout 7da92b360deacb31d6fc8a2121da57ed6f47f4f9
+   (optional: sparse-checkout set proofs/coq proofs/lean4 proofs/agda)
+4. Add `git submodule update --init --recursive` to CI/checkout; fix any Justfile/CI/build paths.
+   Keep repo-root docs/proof-debt.md (PR #82); note the 150 markers' canonical home is now the submodule.
+5. Open a DRAFT PR; post the prepared comment on #84 (it's in §5 of ISSUE-84-RESOLUTION.md) and close #84
+   referencing the PR.
+
+Guarded script for steps 1–3: convert-to-submodule.sh (has a hard stop if any unexpected maa-only path appears).
@@ -0,0 +1,135 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
+
+# Issue #84 — Resolution: `absolute-zero/` is a STALE VENDOR COPY (Option B, pure submodule)
+
+**Repo:** hyperpolymath/maa-framework · **Issue:** #84 · **Related:** PR #82 (merged, classifies markers), PR #83 (re-vendor to upstream)
+**Decision:** **(B) Stale vendor copy.** Replace the in-tree `absolute-zero/` subtree with a git
+submodule pinned to upstream `hyperpolymath/absolute-zero`. **Nothing needs to be extracted first.**
+
+> **Evidence basis = authoritative.** Both repos were `git clone`d and compared with real `diff` on
+> local disk. Earlier figures in this thread that came from the WebFetch summariser / async sub-agents
+> were unreliable (one hallucinated a 1047-line `QuantumCNO.v`; another invented a `ci.yml`). **Ignore
+> those. Only the numbers below — from `diff` against the clones — are real.**
+
+Compared: `maa @ 9dbf56b` (subtree `absolute-zero/`) vs `upstream @ 7da92b360deacb31d6fc8a2121da57ed6f47f4f9` (2026-05-30).
+
+---
+
+## 1. Decision & rationale (one paragraph)
+
+maa-framework's `absolute-zero/` is a **clean, slightly-stale subset of upstream** — a vendor copy,
+**not a fork, not a hybrid**. A full recursive diff of the whole subtree shows only **1 maa-unique
+file** (an inert nested CI workflow), **15 differing files** (every one of which is *upstream-ahead*),
+and **2 upstream-only files**. Critically, **no proof file contains any maa-only theorem or any proof
+that upstream leaves open** — so converting the subtree to a submodule **destroys no proof work**. This
+keeps PR #82's `§(e) VENDORED` classification correct and makes "resolution path = upstream"
+structurally true. Hybrid (C) is ruled out because there is no fork component anywhere in the tree.
+
+**#84's premise is stale.** Its "files unique to maa / missing from maa / 3 drifted proof files" lists
+describe the state **before PR #83** ("re-vendor absolute-zero/ subtree to upstream HEAD", 27 May). The
+files it calls "unique to maa" (`EchoBridgeCNO.agda`, `EchoBridgeScaffold.agda`, `ECHIDNA_*`,
+`examples/go`, …) are now **byte-identical to upstream** (verified by sha256) — they are *not* maa-only.
+#83 already did the convergence; the submodule swap is the clean finish.
+
+---
+
+## 2. Authoritative whole-subtree diff
+
+| Category | Count | Detail |
+|---|---:|---|
+| **Only in maa** | **1** | `.github/workflows/jekyll-gh-pages.yml` — a Pages workflow in the *nested* vendored `.github/` (inert: nested workflows don't run). The only human-glance item; near-certainly disposable. |
+| **Differ** | **15** | 6 proof files (all upstream-ahead, §3) + 9 infra files: `.github/workflows/{governance,hypatia-scan,rust-ci,scorecard}.yml`, `.gitignore`, `.machine_readable/META.scm`, `docs/proof-debt-triage.md`, `docs/proof-debt.md`, `proofs/coq/_CoqProject`. All are stale vendored-copy infra, not maa customisations. |
+| **Only in upstream** | **2** | `proofs/coq/common/PhysicsConstants.v`, `proofs/coq/common/StatMechBasis.v` — the refactored shared-axiom modules maa predates (see §3). |
+
+`docs/proof-debt.md` note: the *differing* one here is the copy **inside** `absolute-zero/` (upstream's
+own, maa's is the 246-line pre-refactor version vs upstream's 423-line current; neither mentions
+"maa-framework"). maa-framework's **own** repo-root `docs/proof-debt.md` from PR #82 lives **outside**
+the subtree and is **not touched** by the swap.
+
+---
+
+## 3. The 6 differing proof files — direction = upstream-ahead (safe)
+
+Open-goal counts (`Admitted/admit/Axiom/Parameter/sorry`) and maa-only proven-theorem counts, both
+sides, from `grep`/`diff` on the clones:
+
+| File | maa (Ax/Param, lines) | upstream (Ax/Param, lines) | maa-only theorems | maa-only proofs | Verdict |
+|---|---|---|---:|---:|---|
+| coq/physics/LandauerDerivation.v | 14 / 7, 353 | 7 / 4, 349 | 0 | 0 | **BEHIND** |
+| coq/physics/StatMech.v | 10 / 4, 411 | 3 / 1, 385 | 0 | 0 | **BEHIND** |
+| coq/quantum/QuantumCNO.v | 29 / 16, 622 | 27 / 14, 691 | 0 | 0 | **BEHIND** |
+| coq/quantum/QuantumMechanicsExact.v | 3 / 1, 423 | 1 / 1, 428 | 0 | 0 | **BEHIND** |
+| lean4/QuantumCNO.lean | 0 / 0, 260 | 0 / 0, 292 | 0 | 0 | **BEHIND** |
+| lean4/StatMech.lean | 0 / 0, 203 | 0 / 0, 237 | 0 | 0 | **BEHIND** (strict subset: 0 maa-only lines) |
+
+- **0 sorry / 0 admit / 0 Admitted** on either side, every file.
+- maa shows *more* axioms only because it's **pre-refactor**: maa inlines `kB`, `temperature`,
+  `prob_nonneg`, `shannon_entropy_*`, etc.; upstream factored these into the new shared modules
+  `common/PhysicsConstants.v` ("Single source of truth for [kB] and [temperature]") and
+  `common/StatMechBasis.v` ("Shared Probability + Entropy Axioms"), wired via upstream's `_CoqProject`
+  (`+common/PhysicsConstants.v`, `+common/StatMechBasis.v`). The 2 maa-only quantum axioms
+  (`kB_positive`, `temperature_positive`) are ABSENT upstream for exactly this reason.
+- maa's only unique lines in the two flagged quantum files are **comments** ("X gate is NOT a CNO",
+  "Hadamard gate is NOT a CNO") — no proof content.
+
+→ **Every overlapping proof is equal-or-behind upstream. The submodule swap loses nothing.** This is
+the disambiguator #84 requested ("inspect the drifted files") — it resolves cleanly to **vendor**.
+
+Corroborating intent-to-track (not fork): PR #82 (merged) labels all 150 markers `§(e) VENDORED`;
+history goes `"Fix stale submodule pointers after repo cleanup"` (3 Mar) → `"re-vendor … to upstream
+HEAD"` (#83, 27 May); vendored files still carry `Project: Absolute Zero` + original author (no rebrand).
+
+---
+
+## 4. Plan (pure submodule conversion — no extraction step)
+
+1. **Re-verify in the maa checkout** (the one command that gates everything):
+   ```bash
+   git clone https://github.com/hyperpolymath/absolute-zero /tmp/az
+   git -C /tmp/az checkout 7da92b360deacb31d6fc8a2121da57ed6f47f4f9
+   diff -rq --exclude=.git absolute-zero /tmp/az
+   # expect: 1 "Only in absolute-zero" (jekyll-gh-pages.yml), 15 "differ", 2 "Only in /tmp/az"
+   ```
+   Eyeball `jekyll-gh-pages.yml`; if it's a stock Pages deploy (it is), let it go.
+2. `git rm -r absolute-zero`
+3. `git submodule add https://github.com/hyperpolymath/absolute-zero absolute-zero` then
+   `git -C absolute-zero checkout 7da92b360deacb31d6fc8a2121da57ed6f47f4f9`.
+   Optional `sparse-checkout set proofs/coq proofs/lean4 proofs/agda` if only the proof subset is wanted
+   (default recommendation: take the whole sibling — that's the point of an estate-sibling submodule).
+4. Wire `git submodule update --init --recursive` into checkout/CI; update any `Justfile`/CI/build paths
+   that referenced `absolute-zero/…`. Keep maa-framework's repo-root `docs/proof-debt.md` (#82) as-is;
+   add a note that the 150 markers' canonical home is now the submodule.
+5. Open a **draft PR** for the conversion; **close #84** with the §5 comment.
+
+Guarded script for steps 1–3: `convert-to-submodule.sh`.
+
+---
+
+## 5. Paste-ready comment for #84
+
+> **Decision: (B) — stale vendor copy. Convert `absolute-zero/` to a submodule. No extraction needed.**
+>
+> Cloned both repos and diffed the whole subtree against upstream `absolute-zero@7da92b3` (current
+> HEAD). Authoritative result:
+>
+> | category | count | what |
+> |---|---:|---|
+> | only in maa's `absolute-zero/` | 1 | `.github/workflows/jekyll-gh-pages.yml` (inert nested Pages workflow) |
+> | differ | 15 | 6 proof files + 9 stale infra files |
+> | only upstream | 2 | `proofs/coq/common/{PhysicsConstants,StatMechBasis}.v` |
+>
+> **All 6 differing proof files are upstream-ahead** — 0 maa-only theorems, 0 maa-only proofs, 0
+> `sorry`/`admit`/`Admitted` on either side. maa simply carries *more inlined axioms* because it predates
+> upstream's refactor of `kB`/`temperature`/Shannon axioms into the two new shared `common/` modules.
+> So there's **no maa-only proof work and no fork** — a submodule swap loses nothing but an inert CI file.
+>
+> Heads-up: this issue's unique/missing-file lists are **stale** — they predate PR #83 ("re-vendor to
+> upstream HEAD"). The files it calls "unique to maa" (`EchoBridge*.agda`, `ECHIDNA_*`, `examples/go`,
+> `proofs/coq/quantum/`) are now byte-identical to upstream (sha256-verified); maa is just behind.
+>
+> **Plan:** (1) `git rm -r absolute-zero`; (2) re-add as a submodule pinned to `7da92b3`; (3) wire
+> `git submodule update --init` into CI; (4) keep PR #82's `§(e) VENDORED` classification — the submodule
+> makes "resolve upstream" structurally true.
+>
+> Resolves #84 (completing what #83 started).
@@ -0,0 +1,32 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
+
+# Investigation: maa-framework issue #84 (cross-repo)
+
+These documents resolve **`hyperpolymath/maa-framework` issue #84** — "Decide: is
+`absolute-zero/` a deliberate fork or stale vendor copy?". They are parked here in
+`typed-wasm` only because the analysis session was scoped to this repo; the actual
+changes land in `maa-framework` (see the handoff).
+
+**Sibling-estate context:** typed-wasm, maa-framework, and `absolute-zero` are sibling
+projects in the hyperpolymath estate (ECHIDNA property-based testing of proof soundness
+is a shared integration point per this repo's CLAUDE.md).
+
+## Verdict
+
+**(B) stale vendor copy** — convert `maa-framework/absolute-zero/` to a git submodule
+pinned to upstream `hyperpolymath/absolute-zero`. No extraction needed; no maa-only proof
+work exists. Established via real `git diff` of both clones (not summaries).
+
+## Contents
+
+| File | Purpose |
+|---|---|
+| `ISSUE-84-RESOLUTION.md` | Full decision, authoritative diff tables, paste-ready #84 comment |
+| `convert-to-submodule.sh` | Guarded conversion script (re-verifies the diff; hard-stops on any unexpected maa-only path). Run inside a maa-framework checkout. |
+| `HANDOFF-maa-framework-session.md` | Drop-in prompt for a Claude Code session scoped to maa-framework to execute the conversion + close #84 |
+
+## Status
+
+Analysis complete. Execution (PR + closing #84) must run from a maa-framework-scoped
+session — this typed-wasm session lacks write access to that repo.
@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Issue #84 — convert maa-framework's vendored absolute-zero/ subtree into a submodule (Option B).
+# RUN INSIDE A maa-framework CHECKOUT, on a feature branch. Review each step; nothing is forced.
+#
+# Authoritative local-diff audit (maa@9dbf56b subtree vs upstream@7da92b3) established:
+#   * 1 file only in maa: .github/workflows/jekyll-gh-pages.yml (inert nested Pages workflow) -> drop
+#   * 15 differing files: 6 proof files (ALL upstream-ahead: 0 maa-only theorems/proofs, 0 sorry)
+#                         + 9 stale vendored-infra files
+#   * 2 files only upstream: proofs/coq/common/{PhysicsConstants,StatMechBasis}.v (refactor maa predates)
+#   => no maa-only proof work anywhere; the swap loses nothing but the inert CI file.
+set -euo pipefail
+
+UPSTREAM_URL="https://github.com/hyperpolymath/absolute-zero.git"
+SUBTREE="absolute-zero"
+PIN_SHA="7da92b360deacb31d6fc8a2121da57ed6f47f4f9"   # upstream HEAD at audit (2026-05-30); bump if desired
+
+echo "==> 0. Safety: clean tree on a feature branch"
+git rev-parse --abbrev-ref HEAD
+git diff --quiet || { echo "Working tree dirty — commit/stash first."; exit 1; }
+
+echo "==> 1. RE-VERIFY the audit before destroying anything"
+TMP="$(mktemp -d)"; git clone --quiet "$UPSTREAM_URL" "$TMP/az"; git -C "$TMP/az" checkout --quiet "$PIN_SHA"
+ONLY_MAA=$(diff -rq --exclude=.git "$SUBTREE" "$TMP/az" | grep "^Only in $SUBTREE" || true)
+N_ONLY_MAA=$(printf '%s\n' "$ONLY_MAA" | grep -c . || true)
+echo "    files only in maa subtree (expected: just jekyll-gh-pages.yml):"
+printf '      %s\n' "$ONLY_MAA"
+# Guard: anything maa-only OTHER than the known inert workflow must be inspected before proceeding.
+UNEXPECTED=$(printf '%s\n' "$ONLY_MAA" | grep -v 'jekyll-gh-pages.yml' | grep . || true)
+if [ -n "$UNEXPECTED" ]; then
+  echo "    !! UNEXPECTED maa-only path(s) — STOP and inspect (may be un-upstreamed maa work):"
+  printf '      %s\n' "$UNEXPECTED"; exit 1
+fi
+echo "    (differing proof files are upstream-ahead per audit; nothing maa-only to rescue.)"
+
+echo "==> 2. Remove the vendored subtree (pure subset of upstream — safe)"
+git rm -r "$SUBTREE"
+
+echo "==> 3. Add the submodule, pinned"
+git submodule add "$UPSTREAM_URL" "$SUBTREE"
+git -C "$SUBTREE" checkout "$PIN_SHA"
+git add .gitmodules "$SUBTREE"
+# Optional: keep only the previously-vendored proof subset instead of the whole sibling:
+#   git -C "$SUBTREE" sparse-checkout init --cone
+#   git -C "$SUBTREE" sparse-checkout set proofs/coq proofs/lean4 proofs/agda
+
+echo "==> 4. Manual follow-ups (NOT automated):"
+echo "    - CI/checkout: add 'git submodule update --init --recursive'."
+echo "    - Update any Justfile / CI / build paths referencing $SUBTREE/..."
+echo "    - Keep repo-root docs/proof-debt.md (PR #82); note canonical marker home is now the submodule."
+
+echo "==> 5. Review, then commit"
+git status
+echo "Suggested commit:"
+echo "  git commit -m 'refactor(absolute-zero): convert vendored subtree to submodule pinned upstream (#84)'"
+rm -rf "$TMP"