diff --git a/.github/workflows/soft-closed-form.yml b/.github/workflows/soft-closed-form.yml
new file mode 100644
index 000000000..da14cfb6e
--- /dev/null
+++ b/.github/workflows/soft-closed-form.yml
@@ -0,0 +1,162 @@
+name: Soft closed form exact controls
+
+'on':
+  pull_request:
+    paths:
+      - 'frontiers/soft_closed_form_20261002/**'
+      - '.github/workflows/soft-closed-form.yml'
+      # bound merged sources (consumed in SOURCES.json); the unmerged sources are bound through the API
+      - 'frontiers/local_elder_geometry_20260930/PROOF.md'
+      - 'frontiers/planar_cubic_cluster_20260929/PROOF.md'
+      # the consumed unmerged #242 PROOF and the cited unmerged #243 PROOF are bound through the API
+      - 'frontiers/soft_rejected_pairs_20261002/PROOF.md'
+      - 'frontiers/soft_fold_limit_20261002/PROOF.md'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pull-requests: read
+
+jobs:
+  exact-controls:
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065
+        with:
+          python-version: '3.11.16'
+      - name: Verify sources, replay both modes, reject mutants
+        env:
+          PYTHONDONTWRITEBYTECODE: '1'
+          GH_TOKEN: ${{ github.token }}
+          GH_REPOSITORY: ${{ github.repository }}
+        run: |
+          set -euo pipefail
+          python -B -S - <<'PY'
+          import base64, hashlib, json, os, pathlib, subprocess, sys, urllib.parse, urllib.request
+          root = pathlib.Path('frontiers/soft_closed_form_20261002').resolve()
+          manifest = json.loads((root / 'SOURCES.json').read_text())
+          present = sorted(p.name for p in root.iterdir())
+          expected_names = sorted([e['path'] for e in manifest['files']] + ['SOURCES.json'])
+          if present != expected_names:
+              raise ValueError('packet tree differs from manifest: ' + repr(present))
+          for entry in manifest['files']:
+              path = root / entry['path']
+              if path.is_symlink():
+                  raise ValueError('symlink: ' + entry['path'])
+              data = path.read_bytes()
+              if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']:
+                  raise ValueError('packet file identity mismatch: ' + entry['path'])
+          def same(data, entry):
+              framed = b'blob ' + str(len(data)).encode() + b'\0' + data
+              return len(data) == entry['bytes'] and hashlib.sha256(data).hexdigest() == entry['sha256'] and hashlib.sha1(framed).hexdigest() == entry['git_blob']
+          def tree_entry(path):
+              # the checked-out commit's tree entry for path: (mode, type, blob) or None; symlinks have mode 120000
+              out = subprocess.run(['git', 'ls-tree', '-z', 'HEAD', '--', path], check=True, capture_output=True).stdout
+              if not out:
+                  return None
+              meta, name = out.rstrip(b'\0').split(b'\t', 1)
+              if name.decode() != path:
+                  raise ValueError('unexpected tree entry for ' + path)
+              mode, kind, sha = meta.decode().split()
+              return mode, kind, sha
+          def tree_bytes(entry):
+              # a source read from the checkout must be a regular file whose tree blob is the recorded one
+              te = tree_entry(entry['path'])
+              if te is None:
+                  return None
+              mode, kind, sha = te
+              if mode != '100644' or kind != 'blob' or sha != entry['git_blob']:
+                  raise ValueError('tree entry is not the recorded regular-file blob (mode/type/blob ' + ' '.join(te) + '): ' + entry['path'])
+              path = pathlib.Path(entry['path'])
+              if path.is_symlink() or not path.is_file():
+                  raise ValueError('checkout path is not a regular file: ' + entry['path'])
+              return path.read_bytes()
+          for entry in manifest['consumed'] + manifest['cited_only']:
+              data = tree_bytes(entry)
+              if data is None or not same(data, entry):
+                  raise ValueError('merged source drifted or absent: ' + entry['path'])
+          # unmerged sources are bound to their recorded commit, path and blob through the repository API: the head must
+          # resolve, the path in that head's tree must be a file with the recorded blob id and size, and the bytes must have
+          # the recorded sha256; a consumed dependency that has landed is instead read from the tree and must be identical
+          # to the pinned version (else this packet needs rebinding)
+          api = 'https://api.github.com/repos/' + os.environ['GH_REPOSITORY']
+          def get_json(url):
+              req = urllib.request.Request(url, headers={'Authorization': 'Bearer ' + os.environ['GH_TOKEN'],
+                                                         'Accept': 'application/vnd.github+json'})
+              with urllib.request.urlopen(req, timeout=60) as resp:
+                  return json.load(resp)
+          def bound(entry):
+              commit = get_json(api + '/commits/' + entry['head'])
+              if commit.get('sha') != entry['head']:
+                  raise ValueError('recorded head does not resolve: ' + entry['head'])
+              node = get_json(api + '/contents/' + urllib.parse.quote(entry['path']) + '?ref=' + entry['head'])
+              if (node.get('type') != 'file' or node.get('path') != entry['path'] or node.get('sha') != entry['git_blob']
+                      or node.get('size') != entry['bytes']):
+                  raise ValueError('recorded head/path does not map to the recorded blob: ' + entry['path'])
+              blob = get_json(api + '/git/blobs/' + entry['git_blob'])
+              if blob.get('encoding') != 'base64':
+                  raise ValueError('unexpected blob encoding for ' + entry['path'])
+              return base64.b64decode(blob['content'])
+          def current(entry):
+              # drift gate (as on #220, after Copilot's review there): the recorded head keeps resolving after a dependency PR advances, so
+              # also resolve the dependency PR now. Open: the file at its current head must be the pinned blob. Merged:
+              # the file at its merge commit must be the pinned blob. Closed unmerged: rebinding is required.
+              pr = get_json(api + '/pulls/' + entry['pr'].split('#', 1)[1])
+              merged = bool(pr.get('merged'))
+              if merged:
+                  ref = pr.get('merge_commit_sha')
+              elif pr.get('state') == 'open':
+                  ref = pr['head']['sha']
+              else:
+                  raise ValueError('dependency ' + entry['pr'] + ' closed without merge: rebind required')
+              node = get_json(api + '/contents/' + urllib.parse.quote(entry['path']) + '?ref=' + ref)
+              if node.get('type') != 'file' or node.get('sha') != entry['git_blob'] or node.get('size') != entry['bytes']:
+                  raise ValueError('dependency ' + entry['pr'] + ' advanced: ' + entry['path'] + ' at ' + ref
+                                   + ' is not the pinned blob (rebind required)')
+              return ref, merged
+          for kind in ('consumed_unmerged', 'cited_unmerged'):
+              for entry in manifest.get(kind, []):
+                  # a consumed dependency's PR is resolved first (Codex review 4167121714 on #244). Once it has merged,
+                  # its source must be the recorded regular-file blob in this tree: a deleted, renamed or changed landed
+                  # source fails, and there is no fallback to the historical head. While it is open, the source is bound
+                  # through the API. Cited sources are bound through the API.
+                  now, merged = current(entry) if kind == 'consumed_unmerged' else (None, False)
+                  landed = tree_bytes(entry) if kind == 'consumed_unmerged' else None
+                  if merged and landed is None:
+                      raise ValueError('dependency ' + entry['pr'] + ' has merged but its pinned source is absent from this '
+                                       'tree: ' + entry['path'])
+                  if landed is not None:
+                      data, where = landed, 'tree'
+                  else:
+                      if os.path.lexists(entry['path']) and kind == 'consumed_unmerged':
+                          raise ValueError('path present in the checkout but not as a tracked blob: ' + entry['path'])
+                      data, where = bound(entry), 'head/path/blob api'
+                  if not same(data, entry):
+                      raise ValueError(kind + ' source differs from its pinned blob (rebind required): ' + entry['path'] + ' via ' + where)
+                  print(json.dumps({kind + '_bound': entry['path'], 'git_blob': entry['git_blob'], 'head': entry['head'],
+                                    'via': where, 'current_ref_checked': now, 'dependency_merged': merged}))
+          script = str(root / 'closed_form_check.py')
+          expected = (root / 'RESULTS.json').read_bytes()
+          for flags in (['-B', '-S'], ['-B', '-O', '-S']):
+              out = subprocess.run([sys.executable, *flags, script], check=True, capture_output=True, timeout=600).stdout
+              if out != expected:
+                  raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags))
+              for m, control in manifest['mutants'].items():
+                  run = subprocess.run([sys.executable, *flags, script, '--mutant', m], capture_output=True, timeout=600)
+                  if run.returncode != 1:
+                      raise RuntimeError('mutant ' + m + ' not rejected')
+                  # each mutant must fail exactly its own control (named first on the checker's stderr line)
+                  line = run.stderr.decode().strip().splitlines()[-1]
+                  failing = line.split('failing controls ', 1)[1].split(', ')
+                  if len(failing) != 1 or failing[0].split('_', 1)[0] != control:
+                      raise RuntimeError('mutant ' + m + ' fails ' + repr(failing) + ', expected only ' + control)
+              rc = subprocess.run([sys.executable, *flags, script, '--mutant', 'M99'], capture_output=True, timeout=600).returncode
+              if rc != 2:
+                  raise RuntimeError('unknown mutant label not rejected with exit 2')
+          print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False}))
+          PY
+          git diff --exit-code
diff --git a/frontiers/soft_closed_form_20261002/PROOF.md b/frontiers/soft_closed_form_20261002/PROOF.md
new file mode 100644
index 000000000..c69f92b10
--- /dev/null
+++ b/frontiers/soft_closed_form_20261002/PROOF.md
@@ -0,0 +1,760 @@
+# The closed form of the soft rejected set: an explicit `I(t, χ₀)`, `t* = 2/3`, and the expansion of `H` to `k⁴`
+
+Object: CL-SOFT-CLOSED-FORM-20261002-v1.2. Versions:
+- v1, `1781c0f` (PROOF blob `310ef828`). OpenAI Codex's nonauthor Slices A, B and C reviewed it.
+- v1.1 applies their findings:
+  - OA-244-A-01: the Cardano wording;
+  - OA-244-B-01: a direct proof on the fibre `t = 3/4`, `χ₀ = 0`, which lies on `Δ`. It also answers Codex's automated
+    finding 4167121706. The argument is the Slice B reviewer's.
+  - OA-244-B-02: the range in Corollary A.3;
+  - OA-244-C-01 and C-02: wording in Lemmas B.1 and B.2.
+
+  It also corrects one sentence of §6 and rebinds #242 v1.3, whose §§0–3 are byte-identical to v1.2. No statement
+  changes, except that Corollary A.1 now covers `t = 3/4`. §9 lists the changed bytes.
+- v1.2 (2 October 2026), after the delta readbacks of v1.1 and Slice D (review 5394484567):
+  - **OA-244-D-01:** the checker emits the current object (RESULTS changes accordingly).
+  - **OA-244-D-02:** C5's row in §7 describes its two rejection branches.
+  - **OA-244-D-03:** the floating-point branches are labelled completely, in the checker and in §7.
+  - **Rebinding:** #242 v1.5 (`ee56652`, blob `271412db`) and #243 v1.5 (`3a188be`). The consumed #242 §§0–3 are unchanged.
+  - **Remark A.1′ (cited):** records OpenAI Codex's lemma on the whole curve `Δ` (5957328502; nonauthor ACCEPT 5957356693).
+    On `Δ`, the elder switch is at `ψ = 3c′`, and `I = (20/3)c′³`, which is Theorem A's formula with `ψ_e = 3c′`. C3
+    checks its identities exactly.
+
+  The proofs of Theorems A and B and of Corollaries A.1–A.4 are unchanged. §9 lists the changed bytes.
+
+Author: Anthropic Claude (configured model `claude-opus-5-5`), session https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU,
+2 October 2026.
+Disposition: AUTHOR-SIDE PROOF CANDIDATE. Theorem A and everything after it are conditional on merged author-side candidates,
+at their stated conditional scope:
+- #170 Theorem E(1);
+- [CUB] Theorem C;
+- [CUB]'s height identities (C8)–(C11), with its `B = 0` paragraph.
+
+Nonauthor review is required. Scientific effect: NONE. No register, graph, STATUS, PROOF_INDEX, prize or Boolean change.
+
+## 0. Summary
+
+**The object.** Math- #242 (open) studies the fold-scale soft model. For `φ > 0` and `(t, χ₀) ∈ R²` it is the cubic (#242
+(2.3))
+
+    G(X, z) = A₀(X) + ½(X² − ¼)z − ½(1 − βX)z² + (χ/6)z³,    A₀(X) = 2(X + ½)²(X − 1)/(24φ),    β = 2tφ,  χ = χ₀φ².     (0.1)
+
+Its pins are the maximum `M = (−½, 0)` at level `0` and the saddle `S = (½, 0)` at level `L_S = −1/(24φ)`. The configuration is
+typed iff `φ < 1/|1 − t|` (#242 (2.4)). It is *elder* (`e = 1`) iff `S` kills `M` in the superlevel filtration of `G`.
+
+#242 defines the rejected set `𝓡(t, χ₀) := {φ ∈ (0, 1/|1 − t|): e = 0}` and
+
+    I(t, χ₀) := ∫_{𝓡(t, χ₀)} φ^{−2}(φ^{−2} − (1 − t)²) dφ                                                            (#242 (2.5))
+
+and computes `I` numerically by a one-dimensional scan. `I` determines:
+- the Gaussian fold-scale rejection function `H(k) = e^{−12k²}E[γ⁶I(t, χ₀)]/800` (#242 Proposition 4);
+- the coefficient `R_{2/3} = (∫∫F₀ db dσ)·Ĩ`, with `Ĩ = ∫_0^∞ v⁴[H(v^{−3}) − 1]dv` (#242 (4.2)).
+
+**Notation.** Throughout,
+
+    ψ := 1/φ,    c′ := 1 − t,    R := χ₀ + 8 − 12t,    σ := R/8,    g_{c′}(ψ) := 16(ψ − 2c′)²(ψ + c′).                 (0.2)
+
+**What is new.**
+
+| | Statement | Status |
+|---|---|---|
+| **Theorem A** | For `(t, χ₀)` off the curve `Δ = {σ² = c′³}`, and all but at most three `φ`: the configuration is elder iff `ψ ≥ 2c′` and `R² ≤ g_{c′}(ψ)`. Hence `𝓡(t, χ₀) = (1/ψ_e, 1/\|c′\|)`, where `ψ_e` is the largest real root of `g_{c′}(ψ) = R²` (explicit, (2.6)), and `I(t, χ₀) = Φ(c′, R) := \|c′\|δ² + δ³/3` with `δ = ψ_e − \|c′\|`. | proof, conditional (above) |
+| **Corollary A.1** | `χ₀ = 0`: the cubic factors, `ψ_e = 3/2 − 2t + (3/2)√(1 − 4t/3)` for `t ≤ 2/3` and `ψ_e = t` for `t ≥ 2/3`. So `t* = 2/3` exactly: for `t ≥ 2/3` the elder edge is `β = 2`. `I(t, 0)` is elementary, with minimum `4/81` at `t = 2/3`, and `I(t, 0) = t − 2/3` for `t ≥ 1`. The Taylor coefficients of `ψ_e` at `0` are Catalan numbers. | proof (as Theorem A) |
+| **Corollaries A.2–A.4** | `I(1, χ₀) = (χ₀ − 4)²/48`. For fixed `t`, `I` is (off `Δ`) a nondecreasing function of `\|R\|`; everywhere `I ≥ (4/3)(1 − t)₊³`, with equality at `χ₀ = 12t − 8`, and `I = 0` exactly on the half-line `t ≥ 1`, `χ₀ = 12t − 8`. `I` has a convex kink along `χ₀ = 12t − 8`, `t < 1`. Exact asymptotics as `t → ±∞` and `\|χ₀\| → ∞`. For `β > 2` and `χ ≤ 0`, every typed configuration is rejected. | proof (as Theorem A) |
+| **Theorem B** | `H(k) = 1 + (12/25)k² + h_{7/2}k^{7/2} + (728/25)k⁴ + o(k⁴)`, with `h_{7/2} = 16Γ(9/4)(1728√6 − 4332√2 − 2721)/(2625π) = −10.14404402…`. This is the sharp fractional term that OA-242-C-01 left open, together with the next term. | proof, conditional on Theorem A |
+
+**Prior statements recovered.** #242 obtained the following, by series or numerically:
+- `φ_e = 1/3 + t/3 + 10t²/27 + O(t³)`;
+- `I(t, 0) = 20/3 − 20t + 52t²/3 + O(t³)`;
+- `t* ∈ (0.65, 0.68)`;
+- `φ_e|t| → 1/2` and `φ_e|χ₀|^{2/3} → 16^{1/3}`;
+- `I(t, 0) ~ (4/3)|t|³` and `I(0, χ₀) ~ χ₀²/48`.
+
+All of these follow from Theorem A, most with exact next terms.
+
+**Numerics** (§5, exploration, outside the repository). Theorem A makes `H` a Gaussian integral of an explicit algebraic
+function. Nested Gauss–Legendre quadrature gives:
+- `Ĩ = −0.5336676`;
+- `R_{2/3} = −0.048779` in `d = 2` and `−0.061375` in `d = 3`.
+
+They lie inside #242 v1.2's stated ranges (`−0.536`, `−0.049 ± 0.003`, `−0.062 ± 0.004`). Most of the difference in `Ĩ`
+comes from #242's assembly of `Ĩ`, not from its `H` values (§5).
+
+**Not claimed.**
+- No unconditional statement: Theorem A rests on the sources named in the disposition.
+- On the curve `Δ`, only what §3 proves separately (the zero set, the minimum over `χ₀`, `(0, 0)`, and the fibre `(3/4, 0)`),
+  and, through the cited lemma of Remark A.1′, `I = (20/3)c′³` on all of `Δ` (v1.2).
+- No field statement. Conjecture 7 of #242 is not addressed.
+- No certification of the §5 numbers.
+- No change to #242, #243, #170, [CUB] or any other packet.
+
+## 1. Sources
+
+- **#242** (open; consumed at head `ee56652`, PROOF blob `271412db`, v1.5). Its §§0–3 are byte-identical to v1.2's `ad4beb84`
+  (43,505 bytes, SHA-256 `7548a21d…`), which Slices A–C of this packet read; v1.3–v1.5 changed only #242's header, §4's
+  numerical sentences (v1.3) and §§5–9. Used:
+  - (2.2)–(2.4): the normalization `φ, t, β, χ₀, χ`, the model (0.1) and typing;
+  - the elder rule ("`S` kills `M` in the superlevel filtration of `G`"), read as in Step 1 of Lemma 2's proof: `S` kills
+    `M` iff the maximin level of `M` is `L_S`;
+  - (2.5): `𝓡` and `I`;
+  - Proposition 4: the definition of `H`, with `(γ, B, C₃)` independent `N(0, 2)`, `N(0, 2)`, `N(0, 6)` and
+    `(t, χ₀) = (12kB/γ², 576k²C₃/γ³)`;
+  - (4.2): `Ĩ`, `R_{2/3}`;
+  - §§2, 3 and 5: the values compared.
+
+  Lemma 2's scan is not used. Lemma 3 is compared, not consumed: the finiteness in §4 uses (2.8).
+- **#170** (merged author-side candidate, OpenAI; `frontiers/local_elder_geometry_20260930/PROOF.md`, blob `ef2aa579`). Used:
+  - §2: the typed cubic `P_θ`, the shear quantities `B`, `D`, the null sets `Σ_k`, `Δ_k`, the set `C(P)` of additional
+    critical points with values in `(−k, 0)`, and `h_*(P) = max({−k} ∪ P(C(P)))`;
+  - **Theorem E(1)**: off `Σ_k ∪ Δ_k`, the maximin connection level of `M` to a point higher than `M` is `h_*(P)`;
+  - §3: the critical-chord bound `d_P(M) ≥ h_*(P)`, which holds for every typed cubic. It is used only on `Δ`, in Corollary
+    A.2.
+- **[CUB]** (merged author-side candidate, OpenAI; `frontiers/planar_cubic_cluster_20260929/PROOF.md`, blob `bb446d08`). Used:
+  - §2 (C1)–(C6), **Theorem C**: `n(θ) := #C(P_θ)` satisfies `n = 0` iff `s ≤ B` and `D² ≤ T`, where
+    `T = −(s − B)²(B + 2s)/(12k)`. This includes `Δ_k`.
+  - the height identities (C8)–(C11) and the `B = 0` paragraph of §2: off `Σ_k`, the only critical points at the heights `0`
+    and `−k` are the pins. (This is also used in the proof of [CUB]'s Lemma S.)
+- **#243** (open; cited). Its Proposition FL.7 identifies #242's model with #170's cubic in #243's normalization. Lemma 1
+  below re-derives that identification in #242's normalization, so this packet does not consume #243.
+- **OpenAI Codex's reviews of #242.**
+  - The Slice C review (5390667993) proves `H(k) = 1 + (12/25)k² + O(k^{7/2})` (§5 there) and records OA-242-C-01: a sharp
+    fractional term would need "analysis of the `γ ≈ √k` transition and a nonzero residual coefficient". Theorem B
+    supplies both, conditionally on Theorem A.
+  - The complementary v1.2 review (5391986303, §3, D.1) uses the same identification for the coefficient `F = kA∗a_fail`.
+- **This packet's clean-context referee** (an Anthropic Claude subagent, same family; report in the project archive)
+  contributed three things, credited where they are used:
+  - the `k⁴` coefficient of Theorem B, with its two constants;
+  - the arguments on `Δ` in Corollary A.2;
+  - the decomposition of #242's `Ĩ` error in §5.
+
+## 2. The identification and Theorem A
+
+**Lemma 1 (#242's model is #170's cubic; cf. #243 FL.7).** Fix `φ > 0` and `(t, χ₀)`. Put `k = 1` and
+
+    θ = (s, a, β′, c) := (−1/(24φ), 1, t/12, χ₀/576),                                                                   (2.1)
+
+where `c` is [CUB]'s cubic coefficient, not `c′`. Let `P_θ(X, Z) = 2X³ − 3X/2 − ½ + sZ²/2 + (a/2)(X² − ¼)Z + (β′/2)XZ² +
+(c/6)Z³` be #170's typed cubic. Then:
+- (i) `G(X, z) = P_θ(X, 24φz)/(24φ)` identically.
+- (ii) [CUB]'s shear quantities are
+
+      B := β′ − a²/12 = −c′/12,    D := (c − aβ′/4 + a³/72)/2 = R/1152,    s = −ψ/24,                                (2.2)
+
+  and
+
+      T := −(s − B)²(B + 2s)/12 = (ψ − 2c′)²(ψ + c′)/82944,    1327104(T − D²) = g_{c′}(ψ) − R²,                       (2.3)
+
+      12D² + B³ = (R² − 64c′³)/110592,    12D² + (s − B)²(B + 2s) = (R² − g_{c′}(ψ))/110592.                        (2.4)
+
+  So `θ` is typed (`s < −|B|/2`) iff `ψ > |c′|`, which is #242's typing. Also `θ ∈ Δ₁` iff `σ² = c′³`, and `θ ∈ Σ₁` iff
+  `R² = g_{c′}(ψ)`.
+- (iii) If `θ` is typed and `θ ∉ Σ₁ ∪ Δ₁`, then `e(G) = 1` iff `n(θ) = 0`.
+
+*Proof.*
+- (i) Expand. With `Z = 24φz`:
+  - `sZ²/2 = −12φz²`;
+  - `(a/2)(X² − ¼)Z = 12φ(X² − ¼)z`;
+  - `(β′/2)XZ² = 24tφ²Xz²`;
+  - `(c/6)Z³ = 4χ₀φ³z³`.
+
+  Dividing by `24φ` gives `A₀(X) + ½(X² − ¼)z − ½z² + tφXz² + (χ₀φ²/6)z³`, which is (0.1). Here
+  `2X³ − 3X/2 − ½ = 2(X + ½)²(X − 1)` (control C1).
+- (ii) Substitute (2.1) into [CUB] (C2) and (C5). The identities are polynomial (C1).
+- (iii) The map `L(X, z) = (X, 24φz)` is linear and invertible, and fixes `M` and `S`. By (i), `G = (P_θ∘L)/(24φ)`, and
+  `24φ > 0`. Paths from `M` to `{G > 0}` correspond under `L` to paths from `M` to `{P_θ > 0}`. Hence the maximin level
+  satisfies `d_G(M) = d_{P_θ}(M)/(24φ)`. By #170 Theorem E(1), `d_{P_θ}(M) = h_*(P_θ) ≥ −1`, so
+  `d_G(M) = L_S·(−h_*(P_θ))`.
+  - Off `Σ₁`, [CUB] (C8)–(C11) and its `B = 0` paragraph make `S` the only critical point at level `−1` and `M` the only one
+    at level `0`. Explicitly:
+    - a critical value `0` off `Z = 0` would need `u = −½` (which is `M`) or `u = ½ − B/(2s)`, which lies outside the conic's
+      real range;
+    - a critical value `−1` needs `u = ½` (which is `S`) or `u = u_w` with `D² = T`, that is `Σ₁`.
+  - So `S` kills `M` iff `d_G(M) = L_S`, iff `h_* = −1`, iff `C(P_θ) = ∅`, iff `n(θ) = 0`. ∎
+
+Lemma 1 is #243's Proposition FL.7(i)–(iii) with `k = 1` and `γ = 1`. Since `G` depends only on `(φ, β, χ)`, this choice is
+no restriction.
+
+**Theorem A (the closed form).** Let `(t, χ₀) ∈ R²` with `σ² ≠ c′³`, and let `φ ∈ (0, 1/|c′|)` with `R² ≠ g_{c′}(1/φ)`; this
+excludes at most three values of `φ`. Then
+
+    e = 1   iff   ψ ≥ 2c′  and  R² ≤ 16(ψ − 2c′)²(ψ + c′).                                                            (A)
+
+Let `ψ₀ := max(2c′, −c′)`; note that `ψ₀ ≥ |c′|`. On `[ψ₀, ∞)`, `g_{c′}` increases from `0` to `∞`. Let `ψ_e(t, χ₀)` be its
+unique point with `g_{c′}(ψ_e) = R²` (`ψ_e = ψ₀` if `R = 0`); it is the largest real root of `g_{c′}(ψ) = R²`. Then
+
+    𝓡(t, χ₀) = (1/ψ_e, 1/|c′|)  (up to finitely many points),    I(t, χ₀) = Φ(c′, R) := |c′|δ² + δ³/3,    δ := ψ_e − |c′| ≥ 0.   (2.5)
+
+Explicitly, with `y := ψ_e − c′`:
+
+    y = 2c′·cos(⅔·arccos(|σ|c′^{−3/2}))                            if c′ > 0 and σ² ≤ c′³,
+    y = A^{2/3} + c′²A^{−2/3},    A := |σ| + √(σ² − c′³),        otherwise (y := 0 if σ = c′ = 0).                      (2.6)
+
+*Proof.*
+- **The test.** Off `Δ₁ ∪ Σ₁`, Lemma 1(iii) and [CUB] (C6) give `e = 1` iff `s ≤ B` and `D² ≤ T`. By (2.2)–(2.3), this is
+  (A). The excluded `θ` are, by (2.4), `σ² = c′³` and the at most three roots `ψ` of `g_{c′}(ψ) = R²`.
+- **Monotonicity.** `g_{c′}′(ψ) = 48ψ(ψ − 2c′)`. This is `> 0` on `(ψ₀, ∞)`: there `ψ > 2c′`, and `ψ > ψ₀ ≥ |c′| ≥ 0`. At
+  `ψ₀` one factor of `g_{c′}` vanishes, so `g_{c′}(ψ₀) = 0`.
+- **The elder set within the typed range.**
+  - For `c′ > 0`, (A) requires `ψ ≥ 2c′ = ψ₀`.
+  - For `c′ ≤ 0`, `ψ ≥ 2c′` holds automatically, and typing gives `ψ > −c′ = ψ₀`.
+  - In both cases the elder set is `{ψ > |c′|: ψ ≥ ψ₀, g_{c′}(ψ) ≥ R²} = [ψ_e, ∞) ∩ (|c′|, ∞)`.
+  - So `𝓡 = {φ: |c′| < 1/φ < ψ_e}`, which is empty iff `ψ_e = |c′|`.
+- **The integral.** Under `φ = 1/ψ`, `φ^{−2}(φ^{−2} − c′²)dφ = −(ψ² − c′²)dψ`. So
+  `I = ∫_{|c′|}^{ψ_e}(ψ² − c′²)dψ = |c′|δ² + δ³/3`.
+- **The roots.** With `ψ = c′ + y`, `g_{c′}/16 = (y − c′)²(y + 2c′) = y³ − 3c′²y + 2c′³`. So `g_{c′}(ψ) = R²` reads
+  `y³ − 3c′²y + 2c′³ − 4σ² = 0`.
+  - Its discriminant is `432σ²(c′³ − σ²)` (C2).
+  - For `c′ > 0` and `σ² ≤ c′³` all roots are real. Viète's form `y = 2c′cos(⅓arccos(2σ²/c′³ − 1) − 2πm/3)` gives the
+    largest for `m = 0`. Since `arccos(2x² − 1) = 2arccos x` on `[0, 1]`, this is (2.6).
+  - Otherwise, Cardano's formula gives the largest real root.
+    - Generically there is one simple real root.
+    - When `σ = 0 < −c′`, there is also a double root `y = c′` below it, and Cardano's value is `2|c′|`.
+    - For `y³ + py + q = 0` with `p = −3c′²` and `q = 2c′³ − 4σ²`, the two radicands are
+      `−q/2 ± √(q²/4 + p³/27) = 2σ² − c′³ ± 2|σ|√(σ² − c′³) = (|σ| ± √(σ² − c′³))²`.
+    - The unsquared conjugate factors satisfy `(|σ| + √(σ² − c′³))(|σ| − √(σ² − c′³)) = c′³`. So the two real cube-root
+      terms are `A^{2/3}` and `(c′³/A)^{2/3} = c′²A^{−2/3}`, and their product is `c′² = −p/3`, as Cardano requires
+      (OA-244-A-01).
+  - On `σ² = c′³` both formulas give `y = 2c′`. ∎
+
+**Remarks.**
+1. *The parameters.* Only `(t, χ₀)` enters; `k` and `γ` have been scaled out by #242's normalization. In #242's Gaussian
+   setting, `(t, χ₀)` has a density, so `Δ` and the excluded `φ` do not affect `I` or `H`.
+2. *The point `(0, 0)` lies on `Δ`.* There #242 proves `I(0, 0) = 20/3` directly (elder iff `φ < 1/3`). (2.5) gives `ψ_e = 3`
+   and `I = 20/3` there too.
+3. *A second form.* Using the cubic for `y`, (2.5) is equivalent to
+
+       Φ(c′, R) = R²/48 + c′y(y + c′) + (2/3)|c′|³ − (4/3)c′³,    y = ψ_e − c′                                     (2.7)
+
+   (C4). At `(0, 0)`: `64/48 + 6 + 2/3 − 4/3 = 20/3`.
+4. *A bound.* On `[ψ₀, ∞)`, `g_{c′}(ψ) ≥ 16(ψ − ψ₀)³`, because `ψ − 2c′ ≥ ψ − ψ₀` and `ψ + c′ ≥ ψ − ψ₀`. So
+   `ψ_e ≤ ψ₀ + (R²/16)^{1/3}`, `δ ≤ |c′| + (R²/16)^{1/3}`, and
+
+       Φ(c′, R) ≤ C(|c′|³ + R²).                                                                                        (2.8)
+
+   This is the counterpart of #242 Lemma 3's `I ≤ (8000/3)max(1, |t|³, χ₀²)`.
+
+## 3. Consequences
+
+Write `I₀(t) := Φ(1 − t, 8 − 12t)`. On the line `χ₀ = 0`, the curve `Δ` meets only `t = 0` and `t = 3/4`, because
+`σ² − c′³ = t²(t − 3/4)` there. By Theorem A, `I(t, 0) = I₀(t)` for `t ∉ {0, 3/4}`. By Remark 2 it also holds at `t = 0`.
+At `t = 3/4` every typed `φ` lies on `Δ`, and the last item of the proof of Corollary A.1 proves it directly
+(OA-244-B-01).
+
+**Corollary A.1 (`χ₀ = 0`).** Here `R = 4(2 − 3t)`, and
+
+    (ψ − 2c′)²(ψ + c′) − (2 − 3t)² = (ψ − t)(ψ² + (4t − 3)ψ + 4t² − 3t),                                               (3.1)
+
+with roots `t` and `ψ_± = 3/2 − 2t ± (3/2)S`, where `S := √(1 − 4t/3)` (real for `t ≤ 3/4`). Hence:
+
+    ψ_e(t, 0) = 3/2 − 2t + (3/2)√(1 − 4t/3)   (t ≤ 2/3),        ψ_e(t, 0) = t   (t ≥ 2/3).                                (3.2)
+
+    I₀(t) = 11/3 − 21t/2 + 17t²/2 − 4t³/3 + (3/2)(1 − t)(2 − 3t)√(1 − 4t/3)      (t ≤ 2/3),
+    I₀(t) = (2t − 1)²(2 − t)/3                                                (2/3 ≤ t ≤ 1),                             (3.3)
+    I₀(t) = t − 2/3                                                           (t ≥ 1).
+
+In particular:
+- **The edge switch is at exactly `t* = 2/3`.** For `t ≥ 2/3` the elder edge is `φ_e = 1/t`, that is `β = 2`.
+  #242 §2 (the numerical list after Lemma 3) located `t*` in `(0.65, 0.68)`.
+- `I₀` is strictly decreasing on `(−∞, 2/3]` and strictly increasing on `[2/3, ∞)`. Its minimum is `I₀(2/3) = 4/81`.
+  - At `t = 2/3` it has a convex kink, with slopes `−13/9` and `5/9`.
+  - It is `C²` at `t = 1`, with `I₀′ = 1` and `I₀″ = 0`, but not `C³`.
+- **The Catalan series.** For `−3/4 < t ≤ 2/3`, with `C_m` the Catalan numbers `1, 1, 2, 5, 14, …`,
+
+      ψ_e(t, 0) = 3 − 3t − Σ_{m≥1} C_m t^{m+1}/3^m = 3 − 3t − t²/3 − 2t³/9 − 5t⁴/27 − …,
+      I₀(t) = 20/3 − 20t + 52t²/3 − 28t³/9 − 7t⁴/27 − 7t⁵/81 − ….                                                         (3.4)
+
+  On `(2/3, 3/4)` the series sums to `ψ_+`, the smaller root. This recovers #242's `φ_e = 1/3 + t/3 + 10t²/27 + O(t³)` and
+  `I(t, 0) = 20/3 − 20t + (52/3)t² + O(t³)`.
+
+*Proof.*
+- **(3.1).** It is a polynomial identity (C3). Both sides equal `ψ³ − 3c′ψ² + 4c′³ − (2 − 3t)²`, and
+  `4(1 − t)³ − (2 − 3t)² = 3t² − 4t³`.
+- **(3.2).**
+  - `ψ_e` is the largest real root of (3.1).
+  - For `t ≤ 2/3`, `ψ_+ ≥ t`. This is clear if `t ≤ ½`. On `[½, 2/3]`, `S² − (2t − 1)² = 4t(2/3 − t) ≥ 0`, so
+    `S ≥ 2t − 1`.
+  - For `t ∈ (2/3, 3/4]`, `S < 2t − 1`, so `t > ψ_+`. For `t > 3/4`, `ψ_±` are not real.
+- **(3.3).**
+  - On `t ≤ 2/3`, `|c′| = 1 − t` and `δ = ½ − t + (3/2)S`. Expanding `(1 − t)δ² + δ³/3` and reducing with
+    `S² = 1 − 4t/3` gives (3.3) (C3).
+  - On `[2/3, 1]`, `δ = 2t − 1`. For `t ≥ 1`, `δ = t − (t − 1) = 1`.
+- **Monotonicity, the kink and the slopes.**
+  - On `t < 2/3`, differentiate `I₀ = ∫_{c′}^{ψ_e}(ψ² − c′²)dψ` with `dc′/dt = −1` and `ψ_e′ = −2 − 1/S`. This gives
+    `I₀′ = −δ[2ψ_e + (ψ_e + c′)/S] < 0`, since `δ > 0` there (C3).
+  - On `[2/3, 1]`, `I₀′ = (2t − 1)(3 − 2t) > 0` and `I₀″ = 8 − 8t`. On `[1, ∞)`, `I₀′ = 1`.
+  - At `t = 2/3` (`δ = S = 1/3`, `ψ_e = 2/3`, `c′ = 1/3`) both sides of (3.3) equal `4/81`. The one-sided slopes are `−13/9`
+    and `5/9`. Their jump, `2`, is the kink of Corollary A.2(c) at `c′ = 1/3`: crossing `R = 0` changes `∂_tI = −∂_{c′}Φ −
+    12∂_RΦ` by `12κ(1/3) = 2`.
+- **(3.4).**
+  - Expand `S = √(1 − 4x)` with `x = t/3`, using `√(1 − 4x) = 1 − 2Σ_{m≥0}C_m x^{m+1}`. This is the Taylor series of `ψ_+`,
+    convergent for `|t| ≤ 3/4`.
+  - By (3.2), `ψ_e = ψ_+` exactly on `t ≤ 2/3`.
+  - The coefficients of `I₀` follow (C3).
+- **The fibre `t = 3/4` (on `Δ`; OA-244-B-01).** The argument is the Slice B reviewer's (review 5393778724, OpenAI Codex),
+  checked here exactly (C3). Here `c′ = 1/4`, `R = −1` and `σ² = c′³`, so every typed `φ` lies on `Δ` and Theorem A does
+  not apply.
+  - Put `ψ = 1/φ > 1/4`, `P := 24φG`, `Z := 24φz` and `v := X + Z/8`. Then
+  
+        P = F_ψ(v) − (ψ/48)(Z − m_ψ(v))²,    m_ψ(v) = (3/(2ψ))(1 − 4v²),    F_ψ(v) = 2v³ − 3v/2 − ½ + (3/(64ψ))(1 − 4v²)²,
+
+    and `F_ψ′(v) = (3/ψ)(v² − ¼)(v + 2ψ)`.
+  - The critical points of `P` are the points `Z = m_ψ(v)` with `v ∈ {−2ψ, −½, ½}`. They are an extra saddle `Y`, the
+    maximum `M` and the saddle `S`.
+    - Their levels are `P(M) = 0`, `P(S) = −1` and `h_Y := P(Y) = −(4ψ − 1)³(4ψ + 3)/(64ψ)`. So
+      `h_Y + 1 = −(4ψ − 3)(4ψ + 1)³/(64ψ)`.
+    - In #242's coordinates, `Y = (ψ − 3/(16ψ), 1/16 − ψ²)`.
+    - The Hessian determinants of `G` at `M`, `S` and `Y` are `(4ψ − 1)/16`, `−(4ψ + 1)/16` and `(1 − 16ψ²)/32`. So all
+      three points are nondegenerate for `ψ > 1/4`.
+  - On `[−2ψ, ½]`, `F_ψ` increases to `F_ψ(−½) = 0` and then decreases, so `F_ψ ≤ 0` there, and `P ≤ F_ψ`. A path from `M`
+    to `{P > 0}` therefore crosses `v = −2ψ`, where `P ≤ h_Y`, or `v = ½`, where `P ≤ −1`.
+  - Along the ridge `Z = m_ψ(v)`, `P = F_ψ(v) → +∞` as `v → ±∞`, so both bounds are attained. Hence
+    `d_P(M) = max(h_Y, −1)`.
+  - So `S` kills `M` iff `h_Y ≤ −1`, iff `ψ ≥ 3/4`.
+    - At `ψ = 3/4` the saddles `S` and `Y` tie at level `−1`. The maximin mark is `1` there, and a single `φ` does not
+      affect `I`.
+    - Thus `𝓡(3/4, 0) = (4/3, 4)` and `ψ_e = 3/4 = t`.
+    - `I(3/4, 0) = ∫_{1/4}^{3/4}(ψ² − 1/16)dψ = 5/48 = I₀(3/4)`, as (3.2)–(3.3) state. ∎
+
+**Remark A.1′ (the whole curve `Δ`; v1.2, cited).** OpenAI Codex extended the fibre argument to every typed point of `Δ`
+(Math- #244 comment 5957328502). A separate OpenAI reviewer accepted it at its deterministic polynomial scope (5957356693).
+It uses only [CUB] (C3)–(C4), not #170 Theorem E(1) or [CUB] Theorem C (5957339141). This packet cites it and does not
+re-prove it. The organizational independence of both is 0.
+- *Statement in this packet's variables.* Take `(t, χ₀) ∈ Δ` with `c′ > 0`. Then `σ = ±c′^{3/2}`. Put
+  `q := ∓c′^{1/2}/12`, the sign chosen so that `D = −12q³`. For typed `ψ > c′` put `ρ := c′/ψ ∈ (0, 1)`. In
+  `v := X + (1/12 + q)Z`, with `Z := 24φz`,
+
+      24φG = f_ρ(v) − (ψ/48)(Z − m(v))²,    f_ρ(v) = 2v³ − 3v/2 − ½ + 3ρ(v² − ¼)²,    m(v) = −(144q/ψ)(v² − ¼),
+
+  and `f_ρ′(v) = 6(v² − ¼)(1 + 2ρv)`. The critical points are `M`, `S` and one extra saddle `Y` at `v = −1/(2ρ)`, of level
+  `h(ρ) = −(1 − ρ)³(1 + 3ρ)/(16ρ³)`, with `h(ρ) + 1 = −(1 − 3ρ)(1 + ρ)³/(16ρ³)`. The barrier-and-ridge argument of the
+  fibre `t = 3/4` gives `d_P(M) = max(h(ρ), −1)`.
+- *So:*
+  - `S` kills `M` iff `ψ ≥ 3c′`, with a two-saddle tie at `ψ = 3c′` (maximin mark 1; one `φ` does not affect `I`);
+  - `𝓡(t, χ₀) = (1/(3c′), 1/c′)`;
+  - `I(t, χ₀) = ∫_{c′}^{3c′}(ψ² − c′²)dψ = (20/3)c′³`.
+
+  This is Theorem A's `Φ(c′, R)` with `ψ_e = 3c′`, the largest root of `g_{c′}(ψ) = R² = 64c′³`. At `c′ = 0`, `Δ` is the
+  point `(1, 4)`, where `B = D = 0`, every typed `φ` is elder, and `I = 0 = Φ(0, 0)`. The fibre `t = 3/4` is the case
+  `c′ = 1/4` (`q = 1/24`, `ρ = 1/(4ψ)`), and `(0, 0)` is the case `c′ = 1` (`ψ_e = 3`, `I = 20/3`; Remark 2).
+- *Consequence.* At this deterministic scope, `I(t, χ₀) = Φ(c′, R)` for every `(t, χ₀)`, on `Δ` as well as off it. This
+  changes nothing in `H` or `Ĩ`, because `Δ` is null for #242's Gaussian law (Remark 1).
+- *Checks.* C3 (v1.2) checks the completed square, `f_ρ′`, `h` and `h + 1`, `f_ρ″` at the three critical points, the
+  saddle `Y` with `G(Y) = h(ρ)ψ/24`, the switch at `ψ = 3c′`, and `Φ = (20/3)c′³`. It does so exactly, at 32 rational
+  points: `c′ ∈ {1/9, 1/4, 1, 9/4}`, both signs of `σ`, and four `ψ` each.
+
+**Corollary A.2 (the dependence on `χ₀`).** Fix `t`.
+- (a) **Minimum and zero set.** `Φ(c′, ·)` depends on `R` only through `|R|`, and is nondecreasing in `|R|`, with minimum
+  `Φ(c′, 0) = (4/3)(c′₊)³`. These hold for all `(t, χ₀)`, including `Δ`:
+  - `I(t, χ₀) ≥ (4/3)(1 − t)₊³`, with equality at `χ₀ = 12t − 8`;
+  - `I(t, χ₀) = 0` iff `t ≥ 1` and `χ₀ = 12t − 8`.
+
+  On that half-line every typed configuration is elder, except for finitely many `φ`.
+- (b) `I(1, χ₀) = (χ₀ − 4)²/48`.
+- (c) **The kink.** For fixed `c′`, `Φ(c′, ·)` is even, convex, and smooth on `R ≠ 0`, with `0 ≤ ∂_R²Φ ≤ 1/16` there (Lemma
+  B.2). At `R = 0` its derivative jumps by `κ(c′) := (3c′₊)^{3/2}/6`. So `I` has a convex kink along the half-line
+  `χ₀ = 12t − 8`, `t < 1`.
+  - Moreover `Φ(λ²c′, λ³R) = λ⁶Φ(c′, R)` for `λ > 0`.
+  - Across `t = 1`, away from `χ₀ = 4`, `I` is `C²` but not `C³`: by (2.7), `I` is an analytic function of `(c′, R)` plus
+    `(2/3)|c′|³`.
+
+*Proof.*
+- **Off `Δ`.** Theorem A involves `χ₀` only through `R²`, and `ψ_e` increases with `R²`.
+  - At `R = 0`, `ψ_e = ψ₀`. For `c′ > 0` this gives `δ = c′` and `Φ = (4/3)c′³`. For `c′ ≤ 0` it gives `δ = 0` and `Φ = 0`.
+  - For `c′ ≤ 0` and `R ≠ 0`, `ψ_e > ψ₀ = |c′|`, so `I > 0`.
+  - The minimizing points `R = 0` are not on `Δ`, except `(1, 4)`.
+- **On `Δ`** (the referee's arguments).
+  - *`c′ > 0`.* For typed `ψ ∈ (c′, 2c′)`, `s > B`, so `n ≥ 1` by (C6), which covers `Δ_k`. #170 §3's critical-chord bound
+    `d_P(M) ≥ h_* > −1` holds for every typed cubic. So these `φ` are rejected, and
+    `I ≥ ∫_{c′}^{2c′}(ψ² − c′²)dψ = (4/3)c′³ > 0`.
+  - *The only point with `c′ ≤ 0`.* This is `(1, 4)`, where `B = D = 0`. In [CUB]'s sheared variables,
+    `P = 2u³ − 3u/2 − ½ + (s/2)Z²` with `s < 0`, so `P ≤ 2(u + ½)²(u − 1)`.
+    - A path from `M` to `{P > 0}` must reach `u > 1`, hence cross `u = ½`, where `P ≤ −1`.
+    - So `d_P(M) ≤ −1`, and with the chord bound `d_P(M) = −1`.
+    - By [CUB]'s `B = D = 0` case there are no extra critical points, so `S` kills `M` for every typed `φ`, and
+      `I(1, 4) = 0`.
+- **(b).** At `c′ = 0`, `g₀(ψ) = 16ψ³`, so `ψ_e³ = R²/16` and `I = ψ_e³/3 = R²/48`. At `χ₀ = 4` this is `0`, as in (a).
+- **(c).** This is Lemma B.2 below. The homogeneity holds because `g_{λ²c′}(λ²ψ) = λ⁶g_{c′}(ψ)`. ∎
+
+**Corollary A.3 (asymptotics, exact leading terms).**
+- **As `t → −∞` at fixed `χ₀`.** `ψ_e = 2|t| + √(3|t|) + 3/2 + O(|t|^{−1/2})`, so `φ_e|t| → 1/2`. Also
+
+      I = (4/3)|t|³ + 3√3|t|^{5/2} + (17/2)t² + O(|t|^{3/2}).
+
+  #242 §5(4) uses `|t|³(4/3 + 5.74|t|^{−1/2})` beyond its table on `|t| ≤ 400`; it does not record how the constant `5.74`
+  was obtained. With the exact terms, `3√3 + (17/2)|t|^{−1/2} ∈ [5.62, 6.05]` for `100 ≤ |t| ≤ 400` (OA-244-B-02); at
+  `|t| = 1` it is about `13.70`.
+- **As `|χ₀| → ∞` at fixed `t`.** `ψ_e = (R²/16)^{1/3} + c′ + O(|R|^{−2/3})`, so `φ_e|χ₀|^{2/3} → 16^{1/3}`. Also
+  `I = R²/48 + c′(R²/16)^{2/3} + O(|R|^{2/3})`. At `t = 0` this is `I(0, χ₀) = χ₀²/48 + 16^{−2/3}|χ₀|^{4/3} + O(|χ₀|)`.
+- **As `t → +∞` at fixed `χ₀`.** `I = t − 2/3 − χ₀/3 + O(1/t)`.
+
+*Proof.*
+- **`t → −∞`.** Write `m = 1 + |t|` and `ψ_e = 2m + ρ`. Then `16ρ²(ρ + 3m) = (12m + χ₀ − 4)²`. Matching the orders `m²` and
+  `m^{3/2}` gives `ρ = √(3m) − ½ + O(m^{−1/2})`. Then `I = mδ² + δ³/3` with `δ = m + ρ`.
+- **`|χ₀| → ∞`.** In `y³ − 3c′²y + 2c′³ = R²/16`, `y = (R²/16)^{1/3} + O(|R|^{−2/3})`. Insert this into (2.7).
+- **`t → +∞`.** Write `m = t − 1 = −c′` and `ψ_e = m + δ`. Then `16(3m + δ)²δ = (12m − (χ₀ − 4))²` gives
+  `δ = 1 − χ₀/(6m) + O(m^{−2})`, and `I = mδ² + δ³/3`.
+
+These expansions, including the `(17/2)t²` term, were checked in 40- and 60-digit arithmetic (exploration; the referee). ∎
+
+**Corollary A.4 (`β > 2`, `χ ≤ 0`).** If the configuration is typed with `β > 2` and `χ₀ ≤ 0`, it is rejected (off the null
+sets of Theorem A).
+
+This reproves, at Theorem A's conditional scope, #242 Lemma 2's statement that case (D′) needs `χ > 0`. Codex's v1.2 readback
+(5952577050) gives a direct finite-path proof.
+
+*Proof.* `β > 2` means `ψ < t`.
+- If `t < 2/3`, (A) would need `ψ ≥ 2c′ = 2 − 2t > t`, which is impossible.
+- If `t ≥ 2/3`:
+  - then `t ≥ ψ₀`, and `g_{c′}(t) = 16(3t − 2)²`;
+  - and `R = χ₀ + 8 − 12t ≤ −4(3t − 2) ≤ 0`, so `R² ≥ g_{c′}(t)`;
+  - an elder `ψ` would satisfy `ψ ≥ ψ₀` and `g_{c′}(ψ) ≥ R² ≥ g_{c′}(t)`, so `ψ ≥ t` because `g_{c′}` is strictly increasing
+    on `[ψ₀, ∞)`;
+  - this contradicts `ψ < t`. ∎
+
+## 4. Theorem B: the expansion of `H` to order `k⁴`
+
+Let `(γ, B, C₃)` be independent `N(0, 2)`, `N(0, 2)`, `N(0, 6)`, `t = 12kB/γ²`, `χ₀ = 576k²C₃/γ³`, and
+`p(γ) = (4π)^{−1/2}e^{−γ²/4}`. #242 Proposition 4 defines `H(k) := e^{−12k²}E[γ⁶I(t, χ₀)]/800`.
+
+Put `T₂(τ) := 20/3 − 20τ + (52/3)τ²` and `R₂(τ) := I₀(τ) − T₂(τ)`. By (3.3) and (3.4), `R₂` is explicit, and
+`R₂(τ) = −(28/9)τ³ + O(τ⁴)` at `0`.
+
+**Theorem B.** As `k → 0`,
+
+    H(k) = 1 + (12/25)k² + h_{7/2}k^{7/2} + h₄k⁴ + o(k⁴),    h₄ = 728/25,                                            (4.1)
+
+    h_{7/2} = (216√6/(25π))·Γ(9/4)·Λ = 16Γ(9/4)(1728√6 − 4332√2 − 2721)/(2625π) = −10.144044022514828…,                     (4.2)
+
+    Λ := ∫_0^∞ τ^{−9/2}[R₂(τ) + R₂(−τ)] dτ = 128/105 − (2888√3 + 907√6)/2835 = −1.3290475939905679572…              (4.3)
+
+This is conditional on Theorem A, through `I = Φ(c′, R)` almost surely. The coefficient `h₄` was derived by this packet's
+referee; its proof is given below.
+
+**Lemma B.1 (the line `χ₀ = 0`).**
+- (a) `R₂(τ) + R₂(−τ) = −(14/27)τ⁴ + O(τ⁶)` near `0`.
+  - Hence `|R₂(τ) + R₂(−τ)| ≤ C_Rτ⁴` and `|R₂(τ) + R₂(−τ) + (14/27)τ⁴| ≤ C_Rτ⁶` for all `τ ≥ 0`.
+  - Also `|R₂(τ)| ≤ C_R(1 + |τ|³)`.
+- (b) The integral (4.3) converges, and equals the value stated.
+
+*Proof of (a).* Put `E(τ) := R₂(τ) + R₂(−τ)`, which is even.
+- *Near `0`.* `R₂` is analytic in a neighbourhood of `0`. For `τ < 2/3` it is the first line of (3.3) minus `T₂`, which is
+  analytic for `τ < 3/4`. The piecewise `R₂` has the kink of Corollary A.1 at `+2/3`, so it is not analytic through that
+  point (OA-244-C-01).
+  - Its Taylor polynomial of degree `2` vanishes, and the series (3.4) gives the expansion of `E`.
+  - So `|E(τ)| ≤ Cτ⁴` and `|E(τ) + (14/27)τ⁴| ≤ Cτ⁶` near `0`.
+- *For `τ ≥ 2/3`.* `|E(τ)| ≤ C(1 + τ³) ≤ C₁τ⁴`, by (2.8), or by (3.3) for `τ ≥ 1`. Also
+  `|E(τ) + (14/27)τ⁴| ≤ C(1 + τ³) + (14/27)τ⁴ ≤ C₂τ⁶`.
+- *In between.* On any compact interval in `(0, 2/3]` both functions are continuous and the powers of `τ` are bounded
+  below. So the two bounds hold for all `τ ≥ 0`.
+- *Growth.* `|R₂(τ)| ≤ C_R(1 + |τ|³)` follows from (2.8) and `T₂(τ) = O(1 + τ²)`.
+
+*Proof of (b).*
+- **The pieces.** On `0 < τ ≤ 2/3`, (3.3) gives
+
+      R₂(τ) + R₂(−τ) = −6 − (53/3)τ² + P₁(τ)S₋(τ) + P₁(−τ)S₊(τ),    P₁(τ) := (3/2)(1 − τ)(2 − 3τ),  S_∓ := √(1 ∓ 4τ/3).
+
+  For `τ > 2/3`:
+  - `R₂(τ)` is the polynomial `(2τ − 1)²(2 − τ)/3 − T₂(τ)` on `(2/3, 1]`, and `τ − 2/3 − T₂(τ)` on `(1, ∞)`;
+  - `R₂(−τ) = P₀(−τ) + P₁(−τ)S₊(τ) − T₂(−τ)`, where `P₀(τ) = 11/3 − 21τ/2 + 17τ²/2 − 4τ³/3`.
+- **The square-root terms have algebraic antiderivatives** (C7; each is a polynomial identity after multiplying by
+  `τ^{9/2}S`):
+
+      F₋(τ) := S₋(τ)(1444τ³ − 3711τ² + 3051τ − 810)/(945τ^{7/2}),     F₋′ = τ^{−9/2}P₁(τ)S₋(τ),
+      F₊(τ) := −S₊(τ)(1444τ³ + 3711τ² + 3051τ + 810)/(945τ^{7/2}),    F₊′ = τ^{−9/2}P₁(−τ)S₊(τ).
+
+  The polynomial terms integrate termwise to sums of powers `τ^{n−7/2}`.
+- **No contribution from `τ = 0`.**
+  - Near `0` the total antiderivative `G(τ)` is `τ^{−7/2}` times a power series in `τ`.
+  - The integral converges at `0` by (a), so `lim_{τ→0}G(τ)` exists.
+  - With only half-integer powers present, this forces `G(τ) = Σ_{j≥4}g_jτ^{j−7/2} → 0`.
+- **The endpoints.**
+  - At infinity, every polynomial antiderivative vanishes, and `F₊(∞) = −2888√3/2835`.
+  - At `2/3`, `S₋ = 1/3` and `τ^{−7/2} = 27√6/16`.
+  - Summing the endpoint values exactly in `Q(√3, √6)` gives (4.3) (C7).
+  - A floating-point quadrature agrees to `10⁻¹²` (C7), and mpmath quadratures to 39 and 27 digits (exploration; the
+    referee). ∎
+
+**Lemma B.2 (`Φ` in `R`).** Fix `c′`. For `R ≠ 0` put `ρ := ψ_e − 2c′`. Then `ρ ≥ max(0, −3c′)`, with `ρ > 0` if `c′ ≤ 0`,
+and `R² = 16ρ²(ρ + 3c′)`. Moreover:
+- (a) `∂_RΦ = sgn(R)·F(ρ)`, where `F(ρ) := (ρ + c′)(ρ + 3c′)^{3/2}/(6(ρ + 2c′))`.
+- (b) `∂_R²Φ = 1/24 + (2x + x² + 2x³)/72` with `x := c′/ψ_e ∈ [−1, ½]`. Hence `0 ≤ ∂_R²Φ ≤ 1/16`, and `∂_R²Φ` is continuous
+  on `R ≠ 0`.
+- (c) `F` is nondecreasing, and `∂_RΦ(c′, 0±) = ±(3c′₊)^{3/2}/12`. So `Φ(c′, ·)` is convex, and its derivative jumps by
+  `κ(c′) = (3c′₊)^{3/2}/6` at `R = 0`.
+- (d) For all `r, h`, the symmetric second difference satisfies
+
+      0 ≤ Δ₂ := ½[Φ(c′, r + h) + Φ(c′, r − h)] − Φ(c′, r) ≤ h²/32 + (κ(c′)/2)|h|·1{|r| < |h|}.                        (4.4)
+
+  If `h = 0`, then `Δ₂ = 0`. If `h ≠ 0` and `|r| ≥ |h|`, then `Δ₂ = (h²/2)∂_R²Φ(c′, ξ)` for some `ξ` strictly between
+  `r − h` and `r + h` (OA-244-C-02).
+
+*Proof.*
+- **The relation.** `ψ_e − 2c′ = ρ` and `ψ_e + c′ = ρ + 3c′`, so `g_{c′}(ψ_e) = R²` reads `R² = 16ρ²(ρ + 3c′)`.
+  - For `c′ ≥ 0`, `ρ ≥ 0`.
+  - For `c′ < 0`, `ψ_e ≥ |c′|` gives `ρ ≥ 3|c′| > 0`, and `ρ + 3c′ = ψ_e − |c′| ≥ 0`.
+- **(a).** `∂_RΦ = (ψ_e² − c′²)∂_Rψ_e`. Differentiating `g_{c′}(ψ_e) = R²` gives
+  `∂_Rψ_e = 2R/g_{c′}′(ψ_e) = R/(24ψ_eρ) = sgn(R)√(ρ + 3c′)/(6ψ_e)`. Also `ψ_e² − c′² = (ρ + c′)(ρ + 3c′)`.
+- **(b).** `∂_R²Φ = F′(ρ)·dρ/dR`, with `dR/dρ = 6ψ_e/√(ρ + 3c′)`. With `p = ψ_e = ρ + 2c′`, this reduces to the rational
+  identity `∂_R²Φ = (3p³ + 2c′p² + c′²p + 2c′³)/(72p³)` (C6), which is (b).
+  - The range `x ∈ [−1, ½]` follows from `p ≥ 2c′` when `c′ > 0` and `p ≥ |c′|` when `c′ < 0`.
+  - `2x + x² + 2x³` is increasing, since its derivative `2 + 2x + 6x²` has negative discriminant. It equals `−3` at `−1` and
+    `3/2` at `½`.
+- **(c).** `(log F)′ = 1/(ρ + c′) + (3/2)/(ρ + 3c′) − 1/(ρ + 2c′)`.
+  - For `c′ ≥ 0` this is positive, since `1/(ρ + c′) ≥ 1/(ρ + 2c′)`.
+  - For `c′ = −m < 0` and `ρ > 3m`: `1/(ρ − m) − 1/(ρ − 2m) = −m/((ρ − m)(ρ − 2m))`. This is smaller in absolute value
+    than `(3/2)/(ρ − 3m)`, because `(3/2)(ρ − m)(ρ − 2m) > 3m(ρ − 2m) > m(ρ − 3m)`.
+  - The limits at `R → 0±` are `F(0) = (3c′)^{3/2}/12` (`c′ > 0`) and `0` (`c′ ≤ 0`).
+- **(d).** `Δ₂ = ½∫_0^{|h|}[∂_RΦ(r + u) − ∂_RΦ(r − u)]du`. The bracket is at most `∫_{r−u}^{r+u}∂_R²Φ + κ·1{|r| < u}`, which
+  is at most `u/8 + κ·1{|r| < u}`.
+  - Now let `h ≠ 0` and `|r| ≥ |h|`. The open interval `(r − |h|, r + |h|)` does not contain the kink `R = 0`; it may touch
+    it at an endpoint when `|r| = |h|`.
+  - On that interval `Φ` is `C²`, and `Δ₂ = ½∫_0^{|h|}(|h| − u)[∂_R²Φ(r + u) + ∂_R²Φ(r − u)]du`.
+  - `∂_R²Φ` is continuous there, with finite one-sided limits at the ends by (b). The weight `|h| − u` is positive on
+    `[0, |h|)`. So the weighted mean-value theorem gives `ξ` strictly inside the interval. ∎
+
+*Proof of Theorem B.* By Theorem A, for almost every `(γ, B, C₃)`, `I(t, χ₀) = Φ(c′, r + χ₀)` with `c′ = 1 − t` and
+`r := 8 − 12t`. By (2.8), `γ⁶Φ ≤ C(γ⁶ + 1728k³|B|³ + 331776k⁴C₃²)`, so every expectation below is finite. Write
+
+    E[γ⁶I] = E[γ⁶T₂(t)] + 𝒥_t(k) + 𝒥_χ(k),    𝒥_t(k) := E[γ⁶R₂(t)],    𝒥_χ(k) := E[γ⁶(Φ(c′, r + χ₀) − Φ(c′, r))].   (4.5)
+
+**Step 1 (the quadratic part).** `E[γ⁶] = 120`, `E[γ⁶t] = 0` and `E[γ⁶t²] = 144k²E[B²]E[γ²] = 576k²`. So
+`E[γ⁶T₂(t)] = 800 + 9984k²`, as in #242 Proposition 4.
+
+**Step 2 (the `γ ≈ √k` region: `𝒥_t(k) = p(0)Kk^{7/2} + 32256k⁴ + O(k^{9/2})`).**
+- Put `γ = √k·g`. Then
+
+      𝒥_t(k) = k^{7/2}∫_R p(√k g) g⁶ ϱ(g) dg,    ϱ(g) := E_B[R₂(12B/g²)] = E[½(R₂(τ) + R₂(−τ))]|_{τ = 12|B|/g²}.
+
+  The second form uses that `B` is symmetric and independent of `γ`.
+- **Bounds.** By Lemma B.1(a) and `E[B⁴] = 12`, `|g⁶ϱ(g)| ≤ C·min(1, g^{−2})` and
+  `|g⁶ϱ(g) + 64512g^{−2}| ≤ Cg^{−6}` for `|g| ≥ 1`. Here `64512 = (7/27)·12⁴·E[B⁴]`.
+- **The leading term.** Since `0 < p(√k g) ≤ p(0)`, dominated convergence and `|p(√k g) − p(0)| ≤ p(0)min(1, kg²/4)` give
+  `𝒥_t(k) = p(0)Kk^{7/2} + k^{7/2}∫(p(√k g) − p(0))g⁶ϱ(g)dg`, with `K := ∫_R g⁶ϱ(g)dg`.
+- **The correction.**
+  - Replace `g⁶ϱ` by `−64512g^{−2}` on `|g| ≥ 1`. By the second bound this costs `O(k^{7/2}·k)`.
+  - In the remainder, substitute `w = √k g`. It becomes `−64512√k∫_{|w|≥√k}(p(w) − p(0))w^{−2}dw = 32256√k + O(k)`, since
+    `∫_R(p(w) − p(0))w^{−2}dw = −½`.
+- **The constant `K`.** For fixed `|B|`, substitute `g = (12|B|/τ)^{1/2}` on `g > 0`; this is justified by the bounds. It
+  gives `∫_0^∞ g⁶·½[R₂ + R₂(−·)](12|B|/g²) dg = ¼(12|B|)^{7/2}Λ`. Hence
+
+      K = ½·12^{7/2}·E|B|^{7/2}·Λ,    E|B|^{7/2} = 2^{7/2}Γ(9/4)/√π,
+
+  and `p(0)K/800 = 24^{7/2}Γ(9/4)Λ/(3200π) = h_{7/2}`, using `24^{7/2} = 27648√6`.
+
+**Step 3 (the `χ₀` dependence: `𝒥_χ(k) = 53248k⁴ + o(k⁴)`).**
+- Given `(γ, B)`, `χ₀` is symmetric, so `𝒥_χ(k) = E[γ⁶Δ₂(c′, r, χ₀)]`.
+- **Away from the kink.** On `{|r| ≥ |χ₀|}`, Lemma B.2(d) gives `γ⁶Δ₂ = 165888k⁴C₃²·∂_R²Φ(c′, ξ)`, with `ξ` between
+  `r ± χ₀`.
+  - As `k → 0` at fixed `(γ ≠ 0, B, C₃)`: `t → 0`, `χ₀ → 0`, `ξ → 8` and `c′ → 1`.
+  - `∂_R²Φ` is continuous at `(1, 8)` and bounded by `1/16`. At `(1, 8)`, `x = 1/3` gives `∂_R²Φ(1, 8) = 13/243`.
+  - The indicator tends to `1`.
+  - By dominated convergence this part is `165888·(13/243)·E[C₃²]·k⁴ + o(k⁴) = 53248k⁴ + o(k⁴)`.
+- **At the kink**, `{|r| < |χ₀|}`. By (4.4), the integrand is at most `γ⁶χ₀²/32 + γ⁶κ(c′)|χ₀|/2`.
+  - **The first term.** `γ⁶χ₀² = 331776k⁴C₃²`, and the indicator tends to `0` pointwise, so this term is `o(k⁴)`.
+  - **The second term on `|χ₀| ≤ 4`.**
+    - The event forces `1/3 < t < 1`, so `κ ≤ 2^{3/2}/6 < ½`.
+    - Given `(γ, C₃)`, it puts `B` in an interval of length `8k|C₃|/|γ|` centred at `γ²/(18k)`. This interval lies in
+      `{B ≥ γ²/(36k)}`, exactly when `|χ₀| ≤ 4`.
+    - So its probability is at most `(8k|C₃|/|γ|)e^{−γ⁴/(5184k²)}`.
+    - With `γ⁶|χ₀| = 576k²|C₃||γ|³`, this part is at most `Ck³E[C₃²]∫γ²e^{−γ⁴/(5184k²)}dγ = O(k^{9/2})`.
+  - **The second term on `|χ₀| > 4`**, that is `|γ|³ < 144k²|C₃|`.
+    - Use `κ(c′) ≤ C(1 + |t|^{3/2})`. Then `γ⁶κ|χ₀| ≤ Ck²|C₃|(|γ|³ + (12k|B|)^{3/2})`.
+    - Integrate over `|γ| < (144k²|C₃|)^{1/3}`, where the density of `γ` is at most `p(0)`. This gives
+      `O(k^{14/3} + k^{25/6})`.
+
+**Step 4.**
+- `E[γ⁶I]/800 = 1 + (312/25)k² + h_{7/2}k^{7/2} + (32256 + 53248)k⁴/800 + o(k⁴)`.
+- Multiplying by `e^{−12k²} = 1 − 12k² + 72k⁴ + O(k⁶)` gives (4.1), with `h₄ = 106.88 − 149.76 + 72 = 728/25`. ∎
+
+**Remarks.**
+1. *The sign.* `h_{7/2} < 0`, so `H(k) < 1 + (12/25)k²` for small `k`. The fractional term comes from the region `γ ≈ √k`,
+   where `|t|` is of order one. There the elder edge is the branch (3.2) of Corollary A.1, which is not analytic across
+   `t = 2/3`.
+2. *Compared with OA-242-C-01.* Codex's toy function `I_* = T₂` has the same local data and no `k^{7/2}` term. Theorem B shows
+   that the actual `I` has one, with coefficient `p(0)K/800`. `K ≠ 0` because `Λ ≠ 0`.
+3. *The `C₃` contribution.* Step 3 shows `(H − H₀)(k) = (53248/800)k⁴ + o(k⁴) = 66.56k⁴ + o(k⁴)`, where `H₀` is `H` with
+   `C₃ = 0`. #242 §5 used a fitted `Δ_χ ≈ 62.24k⁴` below `k = 0.1` (see §5).
+4. *Weaker hypotheses.* The `k^{7/2}` term needs only Step 2, that is, `I(t, 0)` along `χ₀ = 0` together with the symmetry in
+   `C₃`. Step 3 needs `Φ`'s convexity and curvature bound.
+
+## 5. Numerical consequences (exploration; outside the repository)
+
+These use numpy, scipy, mpmath and sympy, and are not part of the proof. The scripts and logs are in the project archive,
+under `V2_2/frontiers_soft_closed_form_20261002/exploration/`, with a README; SOURCES.json pins their hashes. The referee's
+independent scripts are in `referee_checks/` there.
+
+**Theorem A against #242's numerics.**
+- *The 101 × 121 table* `Itab2d_v2.npz` (#242 §5(3)). The relative difference has median `1.8·10⁻⁷`.
+- *Larger disagreements.* 97 of the 12,221 entries differ by more than `10⁻³` relative. They fall into three classes:
+  - **7 entries** with `I < 10⁻⁵`, where the table's grid misses a tiny rejected interval.
+  - **54 entries** that are table resolution. Rerunning the same scanner on a finer grid agrees with Theorem A to
+    `10⁻⁴`.
+  - **36 entries** in thin layers around `β = 2`, where #242's scanner `dec1d.py` itself errs:
+    - *Just above `β = 2`, it falsely rejects.* For `a(½) = 1 − β/2 < 0`, the slices just right of `X = ½` lose their
+      maximum at a fold at distance `≈ a(½)²/χ`. This distance can be far below the scan's grid step. `dec1d` treats "the
+      first grid point is a slice without a maximum" as a trigger. But if the fold value `A₀ + a³/(6χ²)` is below `L_S`,
+      the band closes before the fold, and `S` kills `M`. Example: at `(t, χ₀) = (9.005434, 193.926947)` the scanner
+      rejects `φ ∈ (0.11104, 0.12491)`; Theorem A gives `(0.11245, 0.12491)`.
+    - *Just below `β = 2`, it falsely accepts.* Its tolerance `δ = 10⁻³` treats a band that ends within `10⁻³` of `X = ½`
+      as ending at `S`. For `χ < 0` the slices just left of `X = ½` open (at distance `≈ a(½)²/|χ|`), and there the axial
+      segment joins `M` to the far region above `L_S`. So the configuration is rejected. Example: at
+      `(t, χ₀) = (11.464348642908552, −0.426511285632118)`, a table node, the scanner's edge is `φ = 0.0871798` and
+      Theorem A's is `0.0871797`. The table, with its coarser grid, is off by `0.018` in `I`.
+- *A fold-aware version of the scan* (with a geometric grid to `10⁻¹⁵` around `½` and bisection for the fold) agrees with
+  (A):
+  - on 6,000 general typed points, with 0 disagreements;
+  - on 6,000 points concentrated in `β ∈ (2, 2.15)`, where `dec1d` itself disagrees on 1,221. The fold-aware scan disagrees
+    only within `1.1·10⁻⁵` of `β = 2`, below double precision there. At six of those points an 80-digit version of the same
+    scan agrees with (A).
+- *The two-dimensional flood fill* `model2d.py` errs the other way near `β = 2`. Its level offset `ε = 2·10⁻³|L_S|` exceeds
+  the relevant level gaps. This is why #242's validation did not expose the scanner artifacts. #243's v1.1 referee did
+  record that the scanner needed refinement near `X = ½`.
+- *A direct maximin computation* by the referee compared (A) with the maximin level computed on a grid, using neither #170,
+  [CUB] nor any scan. It found no disagreement at 2,400 typed points in three families (broad, near `β = 2`, and the
+  Gaussian law at `k = 0.5`). It also agreed at 400 points on `Δ`, which Theorem A excludes; this is evidence, not proof.
+
+**The function `H`.**
+- *Method.* With Theorem A in [CUB]'s variables,
+
+      γ⁶I = 13824k³[(b/2)ξ² + ξ³/3],    b := |B′|,  B′ := B − γ²/(12k),
+
+  where `ξ := x_e − b/2 ≥ 0`, `x_e` is the root `≥ max(−B′, B′/2)` of `(x + B′)²(2x − B′) = 12kD²`, and
+  `D = (C₃ − γB/(4k) + γ³/(72k²))/2`.
+  - `H` is evaluated by nested Gauss–Legendre quadrature, split at the kinks `B′ = 0` and `D = 0`. Raising the node counts
+    from `60³` to `100³` changes `H` by less than `10⁻¹⁰`.
+  - The referee's independent quadrature reproduces every printed digit of the `H` row.
+- *Values.*
+
+  | `k` | 0.1 | 0.2 | 0.3 | 0.4 | 0.5 | 0.6 | 0.7 | 0.8 | 1.0 |
+  |---|---|---|---|---|---|---|---|---|---|
+  | `H` (Theorem A) | 1.0039609 | 1.0040821 | 0.9343640 | 0.7269471 | 0.4395370 | 0.2005857 | 0.0686747 | 0.0176869 | 0.0005098 |
+  | #242 v1.2, §5 | 1.0039 | 1.0041 | 0.9345 | 0.7271 | 0.4397 | 0.2007 | 0.0687 | 0.0177 | 0.0005 |
+  | `H₀` (`C₃ = 0`) | 0.9976233 | 0.9333611 | 0.7402788 | 0.4662446 | 0.2268015 | 0.0845012 | 0.0241003 | 0.0052729 | 0.0001152 |
+
+- *Comparison with #242.* `H` differs from #242's values by at most `2.0·10⁻⁴`, at `k = 0.4`; this is the scanner artifacts.
+  `H₀` agrees with #242's to `1.2·10⁻⁵`, which is table interpolation, since `dec1d` is exact at `χ = 0`.
+- *Small `k`.*
+  - `(H − 1 − (12/25)k² − h_{7/2}k^{7/2})/k⁴ = 28.94, 28.99, 29.01` at `k = 0.004, 0.002, 0.001` (140 nodes). This is consistent with
+    `h₄ = 728/25 = 29.12` and the `√k`-size corrections of Step 2.
+  - The referee finds the two `k⁴` constants separately. `𝒥_t` gives `J(k)/√k → 32256`, and `𝒥_χ(k)/k⁴` decreases towards
+    `53248`.
+
+**The coefficient `R_{2/3}`.**
+- *Method.* `Ĩ = ∫_0^∞q^{−6}[H(q³) − 1]dq`, by Gauss–Legendre on 11 segments of `q ∈ [0.1, 1.2]`.
+  - Below `q = 0.1`, the expansion (4.1) is used; this piece contributes `0.04799`. The run used early fitted values
+    `−10.13` and `28.7` for `h_{7/2}` and `h₄`; the exact values change `Ĩ` by `−2·10⁻⁹`.
+  - Above `q = 1.2`, `H < 2·10⁻¹³`, and the tail contributes `−1.2^{−5}/5`.
+- *Accuracy.* With 16 and 24 nodes per segment the results agree to `2.5·10⁻⁸`.
+
+      Ĩ = −0.5336676,    R_{2/3} = 0.0914028·Ĩ = −0.048779 (d = 2),    R_{2/3} = 0.1150058·Ĩ = −0.061375 (d = 3),
+
+  with #242's prefactors (Corollary 1′ there). The referee's independent reconstruction gives `Ĩ ≈ −0.53372`, which agrees
+  within its interpolation error of `5·10⁻⁵`.
+- *Comparison with #242.* #242 v1.2 reports `Ĩ = −0.536`, `R_{2/3} = −0.049 ± 0.003` (`d = 2`) and `−0.0617`
+  (`−0.062 ± 0.004`; `d = 3`). Its ranges contain these values.
+- *Where the difference comes from* (the referee's decomposition of `Ĩ_{#242} − Ĩ`, about `−0.0024`):
+  - about `−0.0019` from #242's interpolation of `Δ_χ = H − H₀` between its nodes at `k = 0.1, 0.15, 0.2`;
+  - about `−0.0008` net from #242's small-`k` model `Δ_χ ≈ 62.24k⁴`, against the exact `66.56k⁴` of Remark 3;
+  - only about `+0.0002` from the range `k = 0.25–0.7`, where the scanner artifacts move `H`.
+
+## 6. Relation to other packets
+
+- **#242 (open).** Theorem A describes #242's `𝓡` and `I` exactly, at the conditional scope above. It changes none of #242's
+  stated results. It sharpens several:
+  - `t*` (§2 there) is exactly `2/3`;
+  - the asymptotic constants of §5(3)–(4) there are replaced by exact expansions;
+  - at four decimals, #242 v1.2's `H` row changes at `k = 0.1` and `0.3–0.6`, and its `H₀` row at `k = 0.4` (§5 here);
+  - the small-`k` coefficient of `Δ_χ` is `66.56`, not `≈ 62`;
+  - `Ĩ` is `−0.5337`.
+
+  #242's author disclosed the scanner artifact on #242 (comment 5953336662). That comment attributes the `Ĩ` change to the
+  scanner; §5 above corrects this. #242 Proposition 4's `H(k) = 1 + (12/25)k² + O(k³)`, and Codex's `O(k^{7/2})`, are
+  sharpened by Theorem B. #242 v1.3 (`d504cdb`) adopts the corrected §5 values and records both scanner artifacts. v1.4
+  (`ffc7005`) and v1.5 (`ee56652`) refine its reporting after Codex's C78 and C80 reviews. Its §§0–3, which this packet
+  consumes, are unchanged.
+- **#243 (open).** FL.7 is the same identification as Lemma 1. Through Theorem FL, `F(k; b, u) = F₀H(k)` for the Gaussian kernel
+  is now an explicit Gaussian integral of an algebraic function.
+- **#170 and [CUB] (merged, at their stated conditional scope).** Theorem E(1), Theorem C and the height identities are
+  consumed in Lemma 1(iii) and Theorem A; #170 §3 also in Corollary A.2. The translation (2.2)–(2.4) is new bookkeeping, not
+  a new classification.
+- **Codex's D.1 (5391986303 §3).** It uses the same classifier identity to identify `F = kA∗a_fail` directly in every fixed
+  `d`. Combined with D.1, Theorem A makes `a_fail` explicit for the Gaussian kernel.
+
+## 7. Controls
+
+`closed_form_check.py` uses the Python standard library: exact `Fraction` arithmetic, plus floating point where noted. The
+floating-point branches are C2, C4, C6, C7, C8 and C9 (each labelled below; OA-244-D-03), and everything else is exact. Its
+output is `RESULTS.json`, byte-identical under `-O`. Mutants `M1`–`M9` each fail only their own control. CI checks this by
+parsing the checker's stderr against `SOURCES.json`. An unknown label exits 2.
+
+| Control | Checks |
+|---|---|
+| C1 | Lemma 1: (i) as a polynomial identity in `(X, z)` at 30 random rational `(φ, t, χ₀)`; (2.2)–(2.4) exactly; typing iff `ψ > \|c′\|`, and `s ≤ B` iff `ψ ≥ 2c′` |
+| C2 | `g′ = 48ψ(ψ − 2c′)`, `g(ψ₀) = 0`; the shift `y = ψ − c′`; the discriminant `432σ²(c′³ − σ²)`; (2.6) against bisection (floating point) on 600 points, including both branches, `c′ = 0` and `σ = 0`, with the formula's value `≥ ψ₀`; (2.8) at rational points |
+| C3 | Corollary A.1: (3.1) as a polynomial identity; (3.3) from (2.5) at rational `S` (`t = 3(1 − S²)/4`); the root ordering behind `t* = 2/3`; the values `20/3`, `4/81`, `1/3`; the derivative formula `I₀′ = −δ[2ψ_e + (ψ_e + c′)/S]` against the exact derivative of (3.3) at rational `S`; the slopes `−13/9`, `5/9`, `1` and `I₀″(1) = 0`; strict monotonicity on a rational grid; the Catalan series (3.4) and the series of `I₀` to order 12. The fibre `t = 3/4` (v1.1): `σ² = c′³`, and at eight rational `ψ > 1/4` the completed square as a polynomial identity in `(v, Z)`, `F_ψ′`, `h_Y` and `h_Y + 1`, `F_ψ(±½)`, the critical point `Y` and `G(Y) = h_Yψ/24`, the three Hessian determinants, and the sign of `h_Y + 1`; `I(3/4, 0) = 5/48`. The whole curve `Δ` (v1.2, Remark A.1′): at `c′ ∈ {1/9, 1/4, 1, 9/4}`, both signs of `σ` and four typed `ψ` each, the completed square, `f_ρ′`, `h(ρ)` and `h(ρ) + 1`, `f_ρ″` at the three critical points, `Y` and `G(Y)`, the switch at `ψ = 3c′`, and `Φ = (20/3)c′³`; at `c′ = 0`, every typed `ψ` is elder |
+| C4 | Corollary A.2: `g₀(ψ) = 16ψ³`, and `I(1, χ₀) = (χ₀ − 4)²/48` with `ψ_e` found independently by bisection (floating point); the minimum `(4/3)c′³` and the zero set in both directions (the positivity of `I` off the zero set at 200 points by bisection, floating point); (2.7) as a polynomial identity given the cubic; `∫_{c′}^{2c′}(ψ² − c′²)dψ = (4/3)c′³` |
+| C5 | Corollary A.4 at 400 rational typed points with `β > 2`, `χ₀ ≤ 0`: `g_{c′}(t) = 16(3t − 2)²` (an identity in `t`), and the rejection through either branch of (A). For `t ≥ 2/3`, `R² ≥ g_{c′}(t)`, and either `ψ < 2c′` (the first inequality of (A) fails) or `g_{c′}(ψ) < g_{c′}(t) ≤ R²` (the second fails). For `t < 2/3`, `ψ < 2c′`. At two of the 400 points `ψ < 2c′` and `g_{c′}(ψ) > g_{c′}(t)`, so the chain `g_{c′}(t) > g_{c′}(ψ)` is not claimed at every point (OA-244-D-02). The exact test (A) rejects all 400 |
+| C6 | Lemma B.2: (a) at rational points with rational square roots; the reduction of `∂_R²Φ` to `(3p³ + 2c′p² + c′²p + 2c′³)/(72p³)` as a polynomial identity; the range `[0, 1/16]` and `∂_R²Φ(1, 8) = 13/243`; the one-sided limits of `F` (jump `κ`, and `0` for `c′ ≤ 0`) as exact values of `F`; (4.4) at 300 random points (floating point) |
+| C7 | Lemma B.1(b): `F₋′`, `F₊′` as polynomial identities after multiplying by `τ^{9/2}S`; the even series of `R₂(τ) + R₂(−τ)`; the exact assembly of `Λ` in `Q(√3, √6)`; a floating-point quadrature of (4.3) (exact series near `0`, Gauss–Legendre elsewhere) within `10⁻¹²`; the two forms of `h_{7/2}` in (4.2), exactly in `Q(√2, √6)`, and its value |
+| C8 | Theorem B's bookkeeping: `E[γ⁶] = 120`, `E[γ⁶t²] = 576k²`, `800 + 9984k²`, `312/25 − 12 = 12/25`, `24^{7/2} = 27648√6`; `E\|B\|^{7/2} = 2^{7/2}Γ(9/4)/√π` against a quadrature (floating point); `64512`, `∫(p(w) − p(0))w^{−2}dw = −½` (a quadrature, floating point), `32256`, `53248` and `h₄ = 728/25`; the exponents `7/2`, `4`, `9/2`, `14/3`, `25/6` |
+| C9 | Fixed points: #242's exact (D′) witness `(φ, β, χ) = (3/2, 8/3, 20/3)` is elder (exact); `(0, 0)` gives `ψ_e = 3`, `I = 20/3` (exact; Remark 2; on `Δ`); #242's 16 control-S8 decisions (five of them at `(0, 0)`) and both §5 examples, whose decimal inputs are evaluated as Python floats (floating point) |
+
+## 8. Not claimed (expanded)
+
+- Theorem A is conditional on #170 Theorem E(1), [CUB] Theorem C and [CUB]'s height identities (C8)–(C11) (merged author-side
+  candidates at their stated conditional scope). Lemma 1(iii) and, on `Δ`, Corollary A.2 (with #170 §3) are where they enter.
+  Everything after Theorem A inherits this condition.
+- On `Δ`, this packet proves only Corollary A.2(a)–(b), `(0, 0)` and the fibre `(3/4, 0)` (the last item of Corollary
+  A.1's proof). For the rest of `Δ` it cites OpenAI Codex's lemma (Remark A.1′; 5957328502, reviewed in 5957356693). The
+  lemma is not re-proved here.
+- No statement about the actual Gaussian field. The fold-scale limit is #243 (open) and #170/#175 (merged).
+- The §5 values are numerical, uncertified exploration.
+- Conjecture 7 of #242 (the `ℓ^{2/3}` term of `ρ_rej`) is not addressed. Its missing inputs (i)–(iii) are unchanged.
+- No priority for the identification of #242's model with #170's cubic (#243 FL.7, which credits #170).
+
+## 9. Review slices (nonauthor)
+
+- **A** — §§1–2: Lemma 1 against #170 §2 and [CUB] §2, and Theorem A including (2.6).
+- **B** — §3: Corollaries A.1–A.4, including the arguments on `Δ`.
+- **C** — §4: Lemmas B.1–B.2 and Theorem B (the split (4.5), Step 2's domination and correction, Step 3).
+- **D** — §§5–7: whether the numerics are described accurately and kept apart from the proofs, and whether the controls
+  match their claims.
+
+Per slice, record ACCEPT, ACCEPT WITH FIXES (with a list), or REJECT (with the failing step).
+
+**Nonauthor reviews of v1** (`1781c0f`, PROOF blob `310ef828`; OpenAI Codex, same account, organizational independence 0):
+A (5393530365), B (5393778724) and C (5393825372), each ACCEPT WITH FIXES; and Codex's automated review (5393535561, two P2
+findings, one on the workflow). Slice D was then open; it reviewed v1.1 (below).
+
+**Nonauthor reviews of v1.1** (`446ea03`, PROOF blob `e0aff5ad`; OpenAI Codex, same account, organizational independence 0):
+the A/B affected-delta readback (5394322266), the C affected-delta readback (5394321246, PASS_TECHNICAL_SCOPED), and Slice
+D (5394484567, ACCEPT WITH FIXES: D-01, D-02, D-03). The full-`Δ` lemma (5957328502) has its own nonauthor review
+(5957356693).
+
+**Changed bytes in v1.2** (for a delta check against those reviews):
+- *Header:* the object label and the v1.2 entry.
+- *§0:* the "Not claimed" item on `Δ`.
+- *§1:* the #242 binding (v1.5).
+- *§3:* Remark A.1′ (new; cited), after Corollary A.1's proof.
+- *§6:* the #242 item's last sentence.
+- *§7:* the opening sentence (D-03), and the C3 (Remark A.1′), C4, C5 (D-02), C8 and C9 (D-03) rows.
+- *§§8–9:* the `Δ` item of §8, the Slice D sentence of the v1 review record, the v1.1 review record, and this list.
+- *Checker:* the docstring (D-03; the C3 item), `delta_fibre` and its loop in C3, and the emitted object (D-01).
+  `RESULTS.json` changes only in `object` and the new `C3.Delta_curve` entry.
+
+The statements and proofs of Lemma 1, Theorems A and B, Corollaries A.1–A.4 and Lemmas B.1–B.2, §§2 and 4–5, and the
+other controls are unchanged.
+
+**Changed bytes in v1.1** (for delta checks against those reviews):
+- *Header:* the object label and versions.
+- *§0:* the "Not claimed" item on `Δ`.
+- *§1:* the #242 binding (v1.3) and the Lemma 3 sentence.
+- *§2 (slice A):* the Cardano items in the proof of Theorem A (A-01).
+- *§3 (slice B):*
+  - the sentence before Corollary A.1, and its edge-switch item;
+  - the new last item of its proof (B-01);
+  - the sentence after the `t → −∞` expansion in Corollary A.3 (B-02).
+- *§4 (slice C):* the proof of Lemma B.1(a) (C-01); the last sentence of Lemma B.2(d), and the proof of (d) (C-02).
+- *§§6–9:* the #242 item of §6, the C3 row of §7, the `Δ` item of §8, and this list.
+
+The statements of Theorems A and B and Corollaries A.2–A.4 are unchanged. So are §5 and the other proofs.
diff --git a/frontiers/soft_closed_form_20261002/README.md b/frontiers/soft_closed_form_20261002/README.md
new file mode 100644
index 000000000..9714b92a0
--- /dev/null
+++ b/frontiers/soft_closed_form_20261002/README.md
@@ -0,0 +1,136 @@
+# The closed form of the soft rejected set: an explicit `I(t, χ₀)`, `t* = 2/3`, and the expansion of `H` to `k⁴`
+
+**Author-side proof candidate (Anthropic Claude). Scientific effect: NONE. Conditional on merged author-side candidates at
+their stated conditional scope: #170 Theorem E(1), [CUB] Theorem C, and [CUB]'s height identities (C8)–(C11). Nonauthor
+review required.**
+
+Object `CL-SOFT-CLOSED-FORM-20261002-v1.2`. Full text: [`PROOF.md`](PROOF.md).
+
+Versions:
+- v1 `1781c0f`.
+- v1.1 applies the findings of OpenAI Codex's nonauthor Slices A–C:
+  - OA-244-A-01, the Cardano wording;
+  - OA-244-B-01, a direct proof on the fibre `t = 3/4`, `χ₀ = 0`, which lies on `Δ` (the reviewer's argument). This also
+    answers the automated finding 4167121706.
+  - OA-244-B-02, a range in Corollary A.3;
+  - OA-244-C-01 and C-02, wording in Lemmas B.1–B.2.
+
+  It also applies the automated finding 4167121714: once #242 merges, the workflow requires #242's pinned source in the
+  tree. It rebinds #242 v1.3 (`d504cdb`), whose consumed §§0–3 are byte-identical to v1.2.
+- v1.2 applies Slice D (5394484567).
+  - OA-244-D-01: the checker emits the current object.
+  - OA-244-D-02: C5's two rejection branches are described as the code checks them.
+  - OA-244-D-03: the floating-point branches C2, C4, C6–C9 are all labelled.
+
+  It rebinds #242 v1.5 (`ee56652`) and #243 v1.5 (`3a188be`). It also adds **Remark A.1′**, which cites OpenAI Codex's
+  lemma on the whole curve `Δ` (5957328502, nonauthor ACCEPT 5957356693): on `Δ`, `S` kills `M` iff `ψ ≥ 3c′`, and
+  `I = (20/3)c′³`. That is Theorem A's formula with `ψ_e = 3c′`. C3 checks the lemma's identities exactly at 32 points.
+
+## Result
+
+Math- #242 (open) defines the rejected set `𝓡(t, χ₀)` of its fold-scale soft model and the integral `I(t, χ₀)` (#242 (2.5)).
+These feed the Gaussian fold-scale rejection function `H(k)` and the coefficient `R_{2/3}`. #242 computes `I` with a
+one-dimensional scan.
+
+Through #243 Proposition FL.7's identification of #242's model with #170's cubic (re-derived here as Lemma 1), #170 Theorem E(1)
+and [CUB] Theorem C decide the model exactly. Put `ψ = 1/φ`, `c′ = 1 − t` and `R = χ₀ + 8 − 12t`.
+
+| | Statement | Status |
+|---|---|---|
+| **Theorem A** | Elder iff `ψ ≥ 2c′` and `R² ≤ 16(ψ − 2c′)²(ψ + c′)`, off the curve `Δ = {(R/8)² = c′³}` and finitely many `φ`. So `𝓡(t, χ₀) = (1/ψ_e, 1/\|c′\|)`, where `ψ_e` is the largest root of that cubic (trigonometric or Cardano form), and `I = \|c′\|δ² + δ³/3` with `δ = ψ_e − \|c′\|`. | proof, conditional |
+| **Corollary A.1** | At `χ₀ = 0` the cubic factors, so `t* = 2/3` exactly (#242 had `(0.65, 0.68)`). The fibre `t = 3/4`, which lies on `Δ`, is proved directly (v1.1). The rest of `Δ` is covered by a cited lemma: `I = (20/3)c′³` there (Remark A.1′, v1.2). `I(t, 0)` is elementary: an algebraic expression for `t ≤ 2/3`, then `(2t − 1)²(2 − t)/3`, then `t − 2/3` for `t ≥ 1`. Its minimum is `4/81`, and `ψ_e`'s Taylor coefficients are Catalan numbers. | proof (as Theorem A) |
+| **Corollaries A.2–A.4** | `I(1, χ₀) = (χ₀ − 4)²/48`. `I ≥ (4/3)(1 − t)₊³`, and `I = 0` exactly on `t ≥ 1`, `χ₀ = 12t − 8`; this includes `Δ`. There is a convex kink along `χ₀ = 12t − 8`, `t < 1`. Exact asymptotics, for example `I = (4/3)\|t\|³ + 3√3\|t\|^{5/2} + (17/2)t² + O(\|t\|^{3/2})` as `t → −∞`. For `β > 2`, `χ ≤ 0` the pair is always rejected. | proof (as Theorem A) |
+| **Theorem B** | `H(k) = 1 + (12/25)k² + h_{7/2}k^{7/2} + (728/25)k⁴ + o(k⁴)` with `h_{7/2} = 16Γ(9/4)(1728√6 − 4332√2 − 2721)/(2625π) = −10.1440440…`. The `k^{7/2}` term comes from the `γ ≈ √k` region. This is the sharp term that Codex's OA-242-C-01 left open. The `k⁴` coefficient is the referee's. | proof, conditional on Theorem A |
+
+## Numerics (exploration; outside the repository; not certified)
+
+| | Value |
+|---|---|
+| `Ĩ = ∫_0^∞v⁴[H(v^{−3}) − 1]dv` | `−0.5336676` (#242 v1.2: `−0.536`) |
+| `R_{2/3}` | `−0.048779` (`d = 2`), `−0.061375` (`d = 3`). #242's sensitivity ranges were `−0.049 ± 0.003` and `−0.062 ± 0.004`. |
+| `H(0.4)` | `0.7269471` (#242 v1.2: `0.7271`) |
+| small-`k` coefficient of `H − H₀` (the `C₃` part) | exactly `66.56` (#242 used a fitted `62.24`) |
+
+**#242's own `I` table.** Theorem A agrees with it with median relative difference `1.8·10⁻⁷`. All 97 entries that differ by
+more than `10⁻³` are explained:
+- 7 are tiny intervals the grid misses;
+- 54 are table resolution;
+- 36 are two artifacts of #242's scanner in thin layers on either side of `β = 2`. Just above, it handles the fold
+  incorrectly; just below, its `10⁻³` tolerance is too loose.
+
+**A corrected scan** agrees with Theorem A on 12,000 random points, except within `1.1·10⁻⁵` of `β = 2`. At six of those points,
+80-digit arithmetic agrees. The referee's direct maximin computation, which uses neither #170 nor [CUB], agrees at 2,400
+points.
+
+**Why `Ĩ` changed.** #242's `H` artifacts move `Ĩ` by only about `2·10⁻⁴`. The rest of the difference comes from #242's
+assembly of `Ĩ`: its small-`k` model `62.24k⁴` and its interpolation of the `C₃` correction between `k = 0.1` and `0.2`.
+
+## Controls
+
+`closed_form_check.py` uses the standard library: exact rationals, with floating point only where noted in PROOF §7. Its
+output is `RESULTS.json`, byte-identical under `-O`.
+
+| Control | Checks |
+|---|---|
+| C1 | Lemma 1: `G(X, z) = P_θ(X, 24φz)/(24φ)` exactly; [CUB]'s `B`, `D`, `T`, `Σ₁`, `Δ₁` in #242's variables; typing |
+| C2 | Theorem A: monotonicity, the shifted cubic, the discriminant, (2.6) against bisection on 600 points, and the bound (2.8) |
+| C3 | Corollary A.1: the factorization (3.1), the formulas (3.3), the derivative formula, the values and slopes, monotonicity, the Catalan series; the fibre `t = 3/4`; the whole curve `Δ` (v1.2, 32 exact points) |
+| C4 | Corollary A.2: `I(1, χ₀)` with `ψ_e` found independently, the minimum, the zero set in both directions, and the identity (2.7) |
+| C5 | Corollary A.4 on 400 rational points, with the inequalities used |
+| C6 | Lemma B.2: `∂_RΦ`, `∂_R²Φ ∈ [0, 1/16]`, `∂_R²Φ(1, 8) = 13/243`, the one-sided limits, and the bound (4.4) |
+| C7 | Lemma B.1: the algebraic antiderivatives, `Λ` exactly in `Q(√3, √6)`, a quadrature to `10⁻¹²`, and `h_{7/2}` |
+| C8 | Theorem B's bookkeeping: moments, `E\|B\|^{7/2}` by quadrature, the `k⁴` constants `32256` and `53248`, and `h₄ = 728/25` |
+| C9 | Fixed points: #242's exact (D′) witness, `(0, 0)`, #242's 16 control-S8 decisions, and both §5 examples |
+
+Mutants `M1`–`M9` each fail only their own control, and CI checks this. An unknown label exits 2:
+
+    python3 -B -S closed_form_check.py                  # exit 0, output = RESULTS.json
+    python3 -B -S closed_form_check.py --mutant M1      # exit 1
+
+## Review record
+
+**Same-family clean-context referee (an Anthropic Claude subagent; organizational independence 0).**
+- Verdict: **ACCEPT WITH FIXES**. It found no BLOCKING or MAJOR finding: 6 MINOR and 10 NIT. All are applied.
+- The MINOR findings were:
+  - the domain of the Catalan series;
+  - statements on `Δ`, now proved separately with its arguments;
+  - the attribution of the `Ĩ` change;
+  - the accuracy of the `H₀` row;
+  - the exploration archive;
+  - vacuous or mislabelled checker items, and CI's mutant isolation.
+- It also derived the `k⁴` coefficient `728/25` with its two constants. Theorem B now includes that coefficient, with proof.
+- Its independent checks:
+  - Lemma 1, Theorem A and the corollaries, symbolically;
+  - (2.6) against `numpy.roots` at 200,000 points;
+  - `Λ` and `h_{7/2}` four ways;
+  - a direct maximin computation at 2,800 points (400 of them on `Δ`);
+  - an independent quadrature of `H` that reproduces the `H` row;
+  - the checker's modes and mutants.
+
+The report and scripts are in the project archive.
+
+**Nonauthor reviews of v1 (`1781c0f`; OpenAI Codex, same account, organizational independence 0).**
+- Slice A, §§1–2 (5393530365): ACCEPT WITH FIXES. It has one NIT, A-01: the Cardano wording. Its independent checks include
+  (2.6) against bisection on 10,008 cases.
+- Slice B, §3 (5393778724): ACCEPT WITH FIXES.
+  - B-01 (MINOR) confirms automated finding 4167121706: the fibre `t = 3/4`, `χ₀ = 0` lies on `Δ`. The review supplies
+    the direct proof that v1.1 inserts, and v1.1 checks it exactly (C3) and with sympy (exploration).
+  - B-02 (MINOR) corrects a range in Corollary A.3.
+- Slice C, §4 (5393825372): ACCEPT WITH FIXES. Its findings are C-01 (MINOR), the local-analytic wording and the large-`τ`
+  bounds in Lemma B.1(a), and C-02 (NIT), `h = 0` and the one-sided endpoint in Lemma B.2(d). It independently reconstructs
+  `Λ`, `h_{7/2}`, `32256`, `53248` and `728/25`, and proves that the kink contributes only `o(k⁴)`.
+- Automated review (5393535561): the two P2 findings above, 4167121706 and 4167121714 (the workflow). Both are applied in
+  v1.1.
+- Delta readbacks of v1.1 (`446ea03`): A/B (5394322266) and C (5394321246, PASS_TECHNICAL_SCOPED).
+- Slice D, §§5–7 (5394484567): ACCEPT WITH FIXES. D-01, D-02 and D-03 are applied in v1.2. The workflow fixtures
+  (5957180884) reproduce the v1 historical-fallback failure and confirm the v1.1 fix.
+
+## Not claimed
+
+- No unconditional statement: everything rests on #170 Theorem E(1) and [CUB].
+- On `Δ`, this packet proves only the zero set, the minimum over `χ₀`, `I(1, χ₀)`, `(0, 0)` and the fibre `(3/4, 0)`. For
+  the rest of `Δ` it cites OpenAI Codex's lemma (Remark A.1′), without re-proving it.
+- No field statement, and nothing on #242's Conjecture 7.
+- No certification of the numerics.
+- No priority for the identification of #242's model with #170's cubic (#243 FL.7).
+- No change to #242, #243, #170, [CUB] or any other packet.
diff --git a/frontiers/soft_closed_form_20261002/RESULTS.json b/frontiers/soft_closed_form_20261002/RESULTS.json
new file mode 100644
index 000000000..d64fe8686
--- /dev/null
+++ b/frontiers/soft_closed_form_20261002/RESULTS.json
@@ -0,0 +1,117 @@
+{
+ "C1": {
+  "CUB_B": "-cp/12",
+  "CUB_D": "R/1152",
+  "CUB_T": "(psi-2cp)^2(psi+cp)/82944",
+  "Delta_1": "sigma^2 = cp^3",
+  "Sigma_1": "R^2 = g(psi)",
+  "identities_G_eq_P": 30
+ },
+ "C2": {
+  "bound_2_8": "(16/3)|cp|^3 + R^2/3",
+  "branches": {
+   "cardano": 371,
+   "trig": 229
+  },
+  "max_rel_dev_formula_vs_bisection_lt_1e-9": true,
+  "points": 600
+ },
+ "C3": {
+  "Delta_curve": {
+   "I_on_Delta": "(20/3) c'^3",
+   "points": 32,
+   "switch_at_psi": "3c'"
+  },
+  "I(0,0)": "20/3",
+  "I(2/3,0)": "4/81",
+  "I_series": [
+   "20/3",
+   "-20",
+   "52/3",
+   "-28/9",
+   "-7/27",
+   "-7/81"
+  ],
+  "catalan_terms": 12,
+  "fibre_3/4": {
+   "I(3/4,0)": "5/48",
+   "psi_points": 8,
+   "tie_at_psi": "3/4"
+  },
+  "identity_3_1": true,
+  "phi_e_series": [
+   "1/3",
+   "1/3",
+   "10/27"
+  ],
+  "points_3_3": 54,
+  "points_derivative": 54,
+  "slopes_at_2/3": [
+   "-13/9",
+   "5/9"
+  ],
+  "t_star": "2/3"
+ },
+ "C4": {
+  "I(1,chi0)": "(chi0 - 4)^2/48",
+  "identity_2_7": true,
+  "min_over_chi0": "(4/3)(1-t)_+^3",
+  "zero_set_positive_points": 200
+ },
+ "C5": {
+  "all_rejected": true,
+  "points_beta_gt_2_chi_le_0": 400
+ },
+ "C6": {
+  "bound_4_4_points": 300,
+  "phi_RR_reduction": true,
+  "points_a": 55,
+  "range": "[0, 1/16]"
+ },
+ "C7": {
+  "Lambda": [
+   "128/105",
+   "-2888/2835",
+   "-907/2835"
+  ],
+  "Lambda_float_12dp": -1.329047593991,
+  "even_series_first_terms": [
+   "-14/27",
+   "-2/27"
+  ],
+  "h72_10dp": -10.1440440225,
+  "quadrature_agrees_1e-12": true
+ },
+ "C8": {
+  "E_absB_7/2_quadrature": true,
+  "E_gamma6": "120",
+  "E_gamma6_t2": "576 k^2",
+  "H_k2": "12/25",
+  "h4": "728/25",
+  "h72_constant": "(216/25) sqrt6 Gamma(9/4) Lambda / pi",
+  "k4_constants": [
+   "32256",
+   "53248"
+  ]
+ },
+ "C9": {
+  "S8_agree": 16,
+  "S8_at_origin_on_Delta": 5,
+  "S8_cases": 16,
+  "section5_examples": true,
+  "witness_elder": true
+ },
+ "controls": {
+  "C1_lemma1_identification": true,
+  "C2_theorem_A": true,
+  "C3_corollary_A1_chi0_zero": true,
+  "C4_corollary_A2": true,
+  "C5_corollary_A4": true,
+  "C6_lemma_B2_Phi": true,
+  "C7_lemma_B1_Lambda_h72": true,
+  "C8_theorem_B_bookkeeping": true,
+  "C9_fixed_points": true
+ },
+ "object": "CL-SOFT-CLOSED-FORM-20261002-v1.2",
+ "scientific_effect": "NONE"
+}
diff --git a/frontiers/soft_closed_form_20261002/SOURCES.json b/frontiers/soft_closed_form_20261002/SOURCES.json
new file mode 100644
index 000000000..830ff9d98
--- /dev/null
+++ b/frontiers/soft_closed_form_20261002/SOURCES.json
@@ -0,0 +1,696 @@
+{
+ "schema": 1,
+ "scientific_effect": "NONE",
+ "object": "CL-SOFT-CLOSED-FORM-20261002-v1.2",
+ "supersedes": {
+  "object": "CL-SOFT-CLOSED-FORM-20261002-v1.1",
+  "head": "446ea03d555968557136e9f7f569d6c56359bd76",
+  "proof_blob": "e0aff5ad5bb757eb759b64e5ba746e8491250391"
+ },
+ "kind": "author-side proof candidate, conditional on the merged #170 Theorem E(1) and [CUB] Theorem C (v1.2: applies Slice D (OA-244-D-01 the emitted object, D-02 the C5 branch description, D-03 the floating-point labels); rebinds #242 v1.5 and #243 v1.5; Remark A.1' cites OpenAI Codex's reviewed lemma on the whole curve Delta (I = (20/3) c'^3 there, Theorem A's formula with psi_e = 3c'), checked exactly in C3; v1.1: applies the nonauthor findings OA-244-A-01 (Cardano wording), B-01 (a direct proof on the fibre t = 3/4, chi0 = 0, which lies on Delta; the Slice B reviewer's argument; also automated finding 4167121706), B-02 (a range in Corollary A.3), C-01 and C-02 (wording in Lemmas B.1-B.2), and the automated workflow finding 4167121714; rebinds #242 v1.3, whose consumed sections 0-3 are byte-identical): Theorem A (the elder test of #242's fold-scale soft model in closed form, psi >= 2c' and (chi0 + 8 - 12t)^2 <= 16 (psi - 2c')^2 (psi + c'); the rejected set (1/psi_e, 1/|c'|) and I = |c'| delta^2 + delta^3/3 with explicit psi_e); Corollaries A.1-A.4 (chi0 = 0: t* = 2/3, elementary I(t, 0), the Catalan series; I(1, chi0) = (chi0 - 4)^2/48; the zero set t >= 1, chi0 = 12t - 8; the kink; exact asymptotics; beta > 2, chi <= 0 rejected); Lemma 1 (#243 FL.7(i)-(iii) in #242 normalization); Theorem B (H(k) = 1 + (12/25)k^2 + h_{7/2} k^(7/2) + h_4 k^4 + o(k^4) with h_{7/2} = 16 Gamma(9/4)(1728 sqrt6 - 4332 sqrt2 - 2721)/(2625 pi) and h_4 = 728/25, the k^4 coefficient derived by the referee)",
+ "author": "Anthropic Claude",
+ "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU",
+ "read_at": {
+  "branch_base": "2d8616ef1b45c4d5bb0970dcc20453bb4126114d"
+ },
+ "consumed": [
+  {
+   "path": "frontiers/local_elder_geometry_20260930/PROOF.md",
+   "bytes": 39722,
+   "sha256": "f68038be79b46124b0f9b31205aa6e3682b34b6f5ef81f4a5697ae81f07cc46b",
+   "git_blob": "ef2aa57959ea9f721bbf2316ce94cf616c1c9113",
+   "tag": "170",
+   "use": "Math- #170 (merged author-side candidate, OpenAI, at its stated conditional scope): section 2 (the typed cubic P_theta, the shear quantities B and D, the null sets Sigma_k and Delta_k, C(P) and h_*(P)) and Theorem E(1) (the maximin connection level of M is h_*(P)); consumed in Lemma 1(iii); section 3 (the critical-chord bound d_P(M) >= h_*(P), valid for every typed cubic), consumed on Delta in Corollary A.2"
+  },
+  {
+   "path": "frontiers/planar_cubic_cluster_20260929/PROOF.md",
+   "bytes": 19889,
+   "sha256": "117e9299a71e6139270266889eb772ed97518e402d9af029bbdb67caf9d4a0f0",
+   "git_blob": "bb446d08db8a944537a743ad550b88c1c2ad5758",
+   "tag": "CUB",
+   "use": "[CUB] (merged author-side candidate, OpenAI, at its stated conditional scope): section 2 (C1)-(C6), Theorem C (the exact classifier: n = 0 iff s <= B and D^2 <= T, including Delta_k), and the height identities (C8)-(C11) with the B = 0 paragraph (off Sigma_k only the pins sit at the boundary heights; also used in the proof of Lemma S); consumed in Lemma 1(iii), Theorem A and, on Delta, Corollary A.2"
+  }
+ ],
+ "consumed_unmerged": [
+  {
+   "path": "frontiers/soft_rejected_pairs_20261002/PROOF.md",
+   "bytes": 91967,
+   "sha256": "ee2930c1434bb765d11da0690a2abf3ab330d544ce7ede1ae076a4c29e206c75",
+   "git_blob": "271412dbc96a29590f5f805258e15c9e335cb430",
+   "tag": "242",
+   "use": "Math- #242 (open; v1.5, whose sections 0-3 are byte-identical to v1.4, v1.3 and v1.2 blob ad4beb84, which Slices A-C of this packet read): (2.2)-(2.4) (normalization, the model (0.1), typing), the elder rule (S kills M in the superlevel filtration), (2.5) (the rejected set and I), Proposition 4 (the definition of H and the jet law), (4.2) (I~ and R_{2/3}), sections 2, 3 and 5 (the values compared); Lemma 2 is cited for the rule (Step 1 of its proof); Lemma 3 is compared, not consumed (the finiteness in section 4 uses (2.8) here)",
+   "head": "ee56652e1b30f2bfbb476da269fab15eb24cecba",
+   "pr": "Math- #242"
+  }
+ ],
+ "cited_only": [],
+ "cited_unmerged": [
+  {
+   "path": "frontiers/soft_fold_limit_20261002/PROOF.md",
+   "bytes": 78874,
+   "sha256": "f972f46d6b7348a4ff5d2eea022694364895a5273265818533dd01204b4c06a0",
+   "git_blob": "6502cf7ba2edee47761e40308c15b7563b06d1f8",
+   "tag": "243",
+   "use": "Math- #243 (open; v1.5): Proposition FL.7 (the identification of #242's model with #170's cubic), re-derived here as Lemma 1 in #242's normalization so that this packet does not consume #243; the v1.1 referee's note on the scanner near X = 1/2 (section 5 there)",
+   "head": "3a188bef39f5eca6fbb7c0cc43be86a52140895c",
+   "pr": "Math- #243"
+  }
+ ],
+ "cited_external": [
+  {
+   "ref": "Math- #242 pullrequestreview-5390667993",
+   "by": "OpenAI Codex (Slice C)",
+   "use": "section 5: H(k) = 1 + (12/25)k^2 + O(k^(7/2)); finding OA-242-C-01 (a sharp fractional term would need the gamma ~ sqrt(k) transition and a nonzero coefficient), answered by Theorem B at its conditional scope"
+  },
+  {
+   "ref": "Math- #242 pullrequestreview-5391986303",
+   "by": "OpenAI Codex (v1.2 complementary review)",
+   "use": "section 3 (D.1, root-authored): the direct model-integral identity F = k A_* a_fail in every fixed d, using the same classifier identity"
+  },
+  {
+   "ref": "Math- #242 issuecomment-5952577050",
+   "by": "OpenAI Codex (v1.2 readback)",
+   "use": "a direct finite-path proof that beta > 2, chi <= 0 is rejected (compared with Corollary A.4)"
+  },
+  {
+   "ref": "Math- #242 issuecomment-5953336662",
+   "by": "Anthropic Claude (author of #242)",
+   "use": "the author disclosure of the scanner artifact in #242 section 5"
+  },
+  {
+   "ref": "Math- #244 pullrequestreview-5393778724",
+   "by": "OpenAI Codex (Slice B of this packet)",
+   "use": "the direct proof on the fibre t = 3/4, chi0 = 0 (OA-244-B-01), inserted as the last item of the proof of Corollary A.1 and checked exactly in C3"
+  },
+  {
+   "ref": "Math- #244 issuecomment-5957328502",
+   "by": "OpenAI Codex (contributor lane; author-side lemma)",
+   "use": "Remark A.1' (v1.2): the maximin identity d_P(M) = k max(h(rho), -1) on every typed point of Delta, hence the elder switch at psi = 3c' and I = (20/3) c'^3 on Delta; cited, not re-proved; its identities are checked exactly in C3",
+   "review": "Math- #244 issuecomment-5957356693 (separate read-only OpenAI reviewer discriminant_extension_review: ACCEPT at the deterministic polynomial scope; organizational independence 0)",
+   "interface": "Math- #244 issuecomment-5957339141 (uses only [CUB] (C3)-(C4), not #170 Theorem E(1) or [CUB] Theorem C)"
+  }
+ ],
+ "nonauthor_reviews": [
+  {
+   "slice": "A (sections 1-2)",
+   "review": "pullrequestreview-5393530365",
+   "at": "1781c0f",
+   "verdict": "ACCEPT WITH FIXES",
+   "findings": [
+    "OA-244-A-01 (NIT)"
+   ],
+   "applied_in": "v1.1",
+   "reviewer": "OpenAI Codex (delegated AI review; same GitHub account; organizational independence 0; Dylan personal reading pending)"
+  },
+  {
+   "slice": "B (section 3)",
+   "review": "pullrequestreview-5393778724",
+   "at": "1781c0f",
+   "verdict": "ACCEPT WITH FIXES",
+   "findings": [
+    "OA-244-B-01 (MINOR)",
+    "OA-244-B-02 (MINOR)"
+   ],
+   "applied_in": "v1.1",
+   "reviewer": "OpenAI Codex (delegated AI review; same GitHub account; organizational independence 0; Dylan personal reading pending)"
+  },
+  {
+   "slice": "C (section 4)",
+   "review": "pullrequestreview-5393825372",
+   "at": "1781c0f",
+   "verdict": "ACCEPT WITH FIXES",
+   "findings": [
+    "OA-244-C-01 (MINOR)",
+    "OA-244-C-02 (NIT)"
+   ],
+   "applied_in": "v1.1",
+   "reviewer": "OpenAI Codex (delegated AI review; same GitHub account; organizational independence 0; Dylan personal reading pending)"
+  },
+  {
+   "slice": "automated (chatgpt-codex-connector)",
+   "review": "pullrequestreview-5393535561",
+   "at": "1781c0f",
+   "verdict": "two P2 suggestions",
+   "findings": [
+    "4167121706 (the t = 3/4 fibre; = OA-244-B-01)",
+    "4167121714 (workflow: a merged dependency must be present in the tree)"
+   ],
+   "applied_in": "v1.1",
+   "reviewer": "OpenAI Codex (delegated AI review; same GitHub account; organizational independence 0; Dylan personal reading pending)"
+  },
+  {
+   "slice": "A/B affected-delta readback of v1.1",
+   "review": "pullrequestreview-5394322266",
+   "at": "446ea03",
+   "verdict": "A-01 and B-02 resolved; B-01 incorporated with its algebra verified (contributor-side verification for B-01)",
+   "findings": [],
+   "reviewer": "OpenAI Codex (delegated AI review; same GitHub account; organizational independence 0; Dylan personal reading pending)"
+  },
+  {
+   "slice": "C affected-delta readback of v1.1",
+   "review": "pullrequestreview-5394321246",
+   "at": "446ea03",
+   "verdict": "PASS_TECHNICAL_SCOPED (C-01, C-02 resolved; the consumed #242 sections 0-3 block unchanged)",
+   "findings": [],
+   "reviewer": "OpenAI Codex (delegated AI review; same GitHub account; organizational independence 0; Dylan personal reading pending)"
+  },
+  {
+   "slice": "D (sections 5-7 and the 4167121714 workflow repair)",
+   "review": "pullrequestreview-5394484567",
+   "at": "446ea03",
+   "verdict": "ACCEPT WITH FIXES",
+   "findings": [
+    "OA-244-D-01 (NIT)",
+    "OA-244-D-02 (MINOR)",
+    "OA-244-D-03 (NIT)"
+   ],
+   "applied_in": "v1.2",
+   "evidence": [
+    "issuecomment-5957056855 (independent numerical sanity, uncertified)",
+    "issuecomment-5957180884 (workflow fixtures)"
+   ],
+   "reviewer": "OpenAI Codex (delegated AI review; same GitHub account; organizational independence 0; Dylan personal reading pending)"
+  }
+ ],
+ "mutants": {
+  "M1": "C1",
+  "M2": "C2",
+  "M3": "C3",
+  "M4": "C4",
+  "M5": "C5",
+  "M6": "C6",
+  "M7": "C7",
+  "M8": "C8",
+  "M9": "C9"
+ },
+ "replayed": [
+  "closed_form_check.py"
+ ],
+ "referee": {
+  "kind": "one clean-context same-family referee (an Anthropic Claude subagent) before submission",
+  "verdict": "ACCEPT WITH FIXES, no BLOCKING or MAJOR finding: 6 MINOR (the domain of the Catalan series (3.4); statements on Delta, now proved separately with the referee's arguments; the attribution of the I~ change; the accuracy of the H0 row; the exploration archive; vacuous or mislabelled checker items and CI mutant isolation) and 10 NIT findings, all applied; the referee also derived h4 = 728/25 (now in Theorem B with proof), the (17/2) t^2 asymptotic term, and the decomposition of #242's I~ error",
+  "report": "project archive V2_2/frontiers_soft_closed_form_20261002/REFEREE_CF.md",
+  "sha256": "f31dfe06ccb2da8dec893037f072ba630b7458bd01fe92b60c7c051cf55e6fe4",
+  "bytes": 28900,
+  "independent_checks": "symbolic re-derivation of Lemma 1, Theorem A and the corollaries; (2.6) against numpy.roots at 200,000 points; Lambda and h_{7/2} four ways; a direct grid maximin at 2,800 points (400 on Delta) using neither #170 nor [CUB]; an independent quadrature of H reproducing the section 5 H row; checker modes and mutant isolation",
+  "scripts": "project archive V2_2/frontiers_soft_closed_form_20261002/referee_checks/",
+  "limits": "same provider and same GitHub account as the author: organizational-independence credit 0; not a nonauthor review"
+ },
+ "exploration": "project archive V2_2/frontiers_soft_closed_form_20261002/exploration/ (numpy, scipy, mpmath, sympy; not part of the repository)",
+ "delivered_under": "explicit owner instructions of Dylan Roy in claude.ai session session_01NMeKEismAyeqgdB4sy2NJU, given after OWNER_STOP (2026-09-27): 2026-09-30 \"Continue to Work on closing as many mathematical items as possible while working with and supporting the other models in the GitHub. Also advance the mathematics in every place that's justified based on what we currently know\", followed by \"Continue\"; standing: \"Any request or permissions are preapproved in advance by me Dylan Roy\", pull requests only, never self-merge, no register/GRAPH/STATUS/lemma_closed/prize/premise edits, OWNER_STOP.md untouched. Nothing is merged by its author.",
+ "files": [
+  {
+   "path": "PROOF.md",
+   "bytes": 58898,
+   "sha256": "dd9b436a58d5d58f706ca59ddcf3eb31519866ea9e0a854e168036a8c21e1eaf"
+  },
+  {
+   "path": "README.md",
+   "bytes": 9991,
+   "sha256": "209ee7ed7399cf0b3a78ec72f044eca277fac88c2cdaf6e43fd15470f34a4b00"
+  },
+  {
+   "path": "closed_form_check.py",
+   "bytes": 41881,
+   "sha256": "8599c3fb6a5605e8d893e0d0c067c994ce32911d75164cc698d790a5b049999f"
+  },
+  {
+   "path": "RESULTS.json",
+   "bytes": 2210,
+   "sha256": "7f730556750d43b397f3047ef2392b8359f4016a3ae9740405cd0468b09fb5b5"
+  }
+ ],
+ "exploration_manifest": {
+  "location": "claude.ai project archive V2_2/frontiers_soft_closed_form_20261002/ (and the local archive zip); not part of the repository",
+  "files": [
+   {
+    "path": "exploration/Hcf.py",
+    "bytes": 2651,
+    "sha256": "36787ccaf7dbd42ffcf21b4c138e2266aeb6e47a0e3f5b81553782124841ad96"
+   },
+   {
+    "path": "exploration/Hcf_grid.log",
+    "bytes": 465,
+    "sha256": "b42481ae7c05551d0b7ee815ad7ab0f08ac337f44bf564a32f1a5c1b0f7852a1"
+   },
+   {
+    "path": "exploration/Hcf_grid_nochi_v2.log",
+    "bytes": 465,
+    "sha256": "58dac2db3aa20d2f93eb5519f79448f27a852c071b690e4fdd339deffe1efe83"
+   },
+   {
+    "path": "exploration/Hsmall.log",
+    "bytes": 735,
+    "sha256": "539a8f413a71a482bcffa67ea758be4e8ede1944e610ee76c492898c8e61e19d"
+   },
+   {
+    "path": "exploration/Hsmall.py",
+    "bytes": 339,
+    "sha256": "f22c71bf1b54e469078cec6ac65266bae593b20ed6097fc915d05cc33cb54415"
+   },
+   {
+    "path": "exploration/Hsmall2.log",
+    "bytes": 258,
+    "sha256": "c9b0deff45c408e247835f63f826a38eee542e9cacf5a9c2e90c6d09d2ca36ef"
+   },
+   {
+    "path": "exploration/Hsmall2.py",
+    "bytes": 387,
+    "sha256": "c1bd7c9d75d54a94cca7a7021a947903e59b1c484e5e074a423ce62673d22169"
+   },
+   {
+    "path": "exploration/Itilde.py",
+    "bytes": 1306,
+    "sha256": "86f7bb01ceaa534550ab01f53ee2c7a42f11cc1202175300460e13e758f925be"
+   },
+   {
+    "path": "exploration/Itilde_16_60.log",
+    "bytes": 258,
+    "sha256": "9703c947dbf2e027715f58a937ee4ed102bcb50bbe542cd58b53b3f26b3a222d"
+   },
+   {
+    "path": "exploration/Itilde_24_80.log",
+    "bytes": 258,
+    "sha256": "545bcf4a273236cce107daef85f6f81fcf2c698673f51c510a30676be5db678f"
+   },
+   {
+    "path": "exploration/Itilde_headfix.log",
+    "bytes": 480,
+    "sha256": "84fa0caa234243d9a780613c94de06a592bfa8f5d2c91f0ce696641f524dbbe4"
+   },
+   {
+    "path": "exploration/Itilde_headfix.py",
+    "bytes": 778,
+    "sha256": "ee003377068c55ac8db454801b9d62ef99401f9b089e78367fbaa534373f4f46"
+   },
+   {
+    "path": "exploration/Itilde_n16_q60.npz",
+    "bytes": 4948,
+    "sha256": "42769f6a733f9f262429e905afe7ca1a60eea33c90b473a9b0f7833e94dfb087"
+   },
+   {
+    "path": "exploration/Itilde_n24_q80.npz",
+    "bytes": 7060,
+    "sha256": "b03653feea432a96fd431fe4894dcf1b66e65abc160e07fb4509d75d57a43ce5"
+   },
+   {
+    "path": "exploration/README.md",
+    "bytes": 7067,
+    "sha256": "48e611800887f12d6515c76f420de547e6920e60327349badd1fd7cbd3de3637"
+   },
+   {
+    "path": "exploration/antider.py",
+    "bytes": 449,
+    "sha256": "7e936b1a2504774ac5587c8fa4d027df7df4444455640ee0da678461f54caaa8"
+   },
+   {
+    "path": "exploration/antider2.py",
+    "bytes": 1116,
+    "sha256": "28a0fe1e50ec497e121508d7492157dda5adb858493b94861feaaaead5e1726c"
+   },
+   {
+    "path": "exploration/b01_check.log",
+    "bytes": 442,
+    "sha256": "c3af469638521cf21c00c7f322a42f17a08aa696014606cf7538f776adecfa36"
+   },
+   {
+    "path": "exploration/b01_check.py",
+    "bytes": 2463,
+    "sha256": "c845dcdfbf03007642ad31b236622f29c252762a6ee19fcdc56bef88c7f2105d"
+   },
+   {
+    "path": "exploration/cf.py",
+    "bytes": 1784,
+    "sha256": "5861010443118e0407fa78ba30e8ae9eaeb044a6fe1676ab4db02bb6be8f36af"
+   },
+   {
+    "path": "exploration/check_fix.py",
+    "bytes": 1732,
+    "sha256": "42cb2967cb8c043e3c2864ad7f19c0fabefab15d4e33b150ba69cd9eb1359160"
+   },
+   {
+    "path": "exploration/chk11.log",
+    "bytes": 234,
+    "sha256": "ec915a6f66aaa2e0142ba188862762fb5b4611ea826b049427b56b9314e05be8"
+   },
+   {
+    "path": "exploration/chk12.log",
+    "bytes": 516,
+    "sha256": "f51864e66327558bdb58bac7c9c8dd121e495e12ed6ffc30e7e56f129c68db39"
+   },
+   {
+    "path": "exploration/claims.log",
+    "bytes": 1506,
+    "sha256": "78cbeaf4b0e181a11e2af3ddcaab1bde361ba1348e6a5ca92b0cb668df302a28"
+   },
+   {
+    "path": "exploration/claims.py",
+    "bytes": 3215,
+    "sha256": "16ee526b08f84bf7b2ac0487ea324e9d55f8b1205f7e726f33a534a7df96a0fa"
+   },
+   {
+    "path": "exploration/classify97.json",
+    "bytes": 18503,
+    "sha256": "fbe9616640c8c9b9557aaf7fb72d5befd31526b60227cd0e579970e9f1244384"
+   },
+   {
+    "path": "exploration/classify97.log",
+    "bytes": 74,
+    "sha256": "c824c7890f9ebba442b088cf92a27e0b4df377c6b60ca955d1496bcd539f7ae6"
+   },
+   {
+    "path": "exploration/classify97.py",
+    "bytes": 1259,
+    "sha256": "01158334494db46f98090dafa9929d119d0ba6fe0d8f79efab8a902376bed0d8"
+   },
+   {
+    "path": "exploration/dec1d_fix.py",
+    "bytes": 2554,
+    "sha256": "d947845c0b26917c16fa986089be87f04814671cbcd36c321cbbce664129ae2d"
+   },
+   {
+    "path": "exploration/dec_mp.log",
+    "bytes": 419,
+    "sha256": "510f62f99cc42ac62486824ed61ae96bbf23877043ade7939cd29505d806adcc"
+   },
+   {
+    "path": "exploration/dec_mp.py",
+    "bytes": 3121,
+    "sha256": "810b3c2e8cd3f46e68eb5f79ab6c86ac4c2a57c991ea524f6af2d1c522ac75de"
+   },
+   {
+    "path": "exploration/diag.py",
+    "bytes": 2032,
+    "sha256": "94e4f5da0c5348fade5e14c5e2f3aa711c34dc18dfa0b438e97f195d88d8d088"
+   },
+   {
+    "path": "exploration/disputes.py",
+    "bytes": 1226,
+    "sha256": "1abb1b9a85e43657f684b34e4d116d9a406a8056209c4a8ba38de011342a4654"
+   },
+   {
+    "path": "exploration/g6i.py",
+    "bytes": 2261,
+    "sha256": "ec81a1631304f2dc17b254a61452a46f012e22797aedccc4d00fba20537ce1c3"
+   },
+   {
+    "path": "exploration/h72b.log",
+    "bytes": 270,
+    "sha256": "8c710bc9be99ce853723d7f027e7b53f534860b4a722d6c3bd629069cc2105c0"
+   },
+   {
+    "path": "exploration/h72b.py",
+    "bytes": 1138,
+    "sha256": "263a645607d232120dde628993e3f0fbf5cadd9cb513391e3a1c9cb62a17de5d"
+   },
+   {
+    "path": "exploration/h72s.py",
+    "bytes": 922,
+    "sha256": "daefef4724a53d1c7b3f76e6febf6d9747d59865061a9604e3ccfbd7320e91a4"
+   },
+   {
+    "path": "exploration/lam_exact2.py",
+    "bytes": 2680,
+    "sha256": "4fa4617bfaa40ea9d64a032ed176e4968447a9a6ae0f742204121d82cfac4a78"
+   },
+   {
+    "path": "exploration/lam_exact3.py",
+    "bytes": 1935,
+    "sha256": "5f880dc97361aec980377b3170c27738414a00511e57aa8e0ed602b30a1d7600"
+   },
+   {
+    "path": "exploration/other.py",
+    "bytes": 1039,
+    "sha256": "2ed8bdbfbeb52726a5c05fc9ec299b28571e3f631597c585856e430641226b4f"
+   },
+   {
+    "path": "exploration/tri.py",
+    "bytes": 1043,
+    "sha256": "3a0c1521a58980d943a75dc33f7a4bd56d4fbab752cb3a078d5cce3a68df46ef"
+   },
+   {
+    "path": "exploration/validate_cf.log",
+    "bytes": 1149,
+    "sha256": "55df2e8c1565f94678d7ed9c3e54c50dcd67f24f13b53f2db0d4c937340ec848"
+   },
+   {
+    "path": "exploration/validate_cf.py",
+    "bytes": 1287,
+    "sha256": "b33e9dae8909165b34c0ebbdc7fbb2f21b2771e7e43c42f54d70c78d196dcd34"
+   },
+   {
+    "path": "referee_checks/AB_split.py",
+    "bytes": 996,
+    "sha256": "074b95ca328ff5436f6e863375825bd37f0efdaa1e4268ba67c26a6db75d6727"
+   },
+   {
+    "path": "referee_checks/H0_check.py",
+    "bytes": 1289,
+    "sha256": "34b78d526a908ea5bbc268147a3102f208ab54a5bc8c881a45882476f5f513da"
+   },
+   {
+    "path": "referee_checks/H0_row.py",
+    "bytes": 519,
+    "sha256": "0b50b12dcd9e17f48f04136acb83276d7d83f2e12046b03726df6573fbbe57e4"
+   },
+   {
+    "path": "referee_checks/H0_values.json",
+    "bytes": 264,
+    "sha256": "5f9754356de9d95196a63226b258010e1183a123b05e4abf11d7293f763da498"
+   },
+   {
+    "path": "referee_checks/H0grid.json",
+    "bytes": 10911,
+    "sha256": "45e477e6f537b3de41f8763ef1cd49692da7a30cb5bb6d3aaa66a002b284e14d"
+   },
+   {
+    "path": "referee_checks/H0grid.py",
+    "bytes": 254,
+    "sha256": "28c8ebea2836df260f6eeb83a45e0649ce241f941d86cece5c264fa9f7a5b944"
+   },
+   {
+    "path": "referee_checks/H_dense3.json",
+    "bytes": 5488,
+    "sha256": "13986faeee2251e41d969001d3261a9b84648bc58b87d0ca47b5065c989b4b4b"
+   },
+   {
+    "path": "referee_checks/H_direct.py",
+    "bytes": 2149,
+    "sha256": "4a3af568dc15c0e0e8ce8119918a7c8617f2cdacb0d1d38bd017d721f69d5206"
+   },
+   {
+    "path": "referee_checks/H_table.py",
+    "bytes": 1231,
+    "sha256": "36dd60c4ef8c02a170cea3d739fdfd5cbcd1807a7cc928abc70c5927c219ac8e"
+   },
+   {
+    "path": "referee_checks/Itilde2.py",
+    "bytes": 3753,
+    "sha256": "1bf3b5fbd11e75d93ca2169662501ec5140a92f90dc8e83745ae58f2e2ca5e34"
+   },
+   {
+    "path": "referee_checks/J_check.py",
+    "bytes": 1092,
+    "sha256": "fb230d89368e6e263a56d22541c54b148413ffe1a8f4d8e6a90ff4b74fb0bb9b"
+   },
+   {
+    "path": "referee_checks/K_direct.py",
+    "bytes": 2539,
+    "sha256": "3138179c4f263d0031f6e90a40d2ad21138561e9aa0b6c75c70819770ff90e5b"
+   },
+   {
+    "path": "referee_checks/K_direct2.py",
+    "bytes": 1291,
+    "sha256": "e685d54568e223d8ac4a6378f2b60a10e4224499fe93b26aa5730857d8c486de"
+   },
+   {
+    "path": "referee_checks/asym.py",
+    "bytes": 1508,
+    "sha256": "c49107976397a7b5b50c79eaeed8f8d586e8f4b18ad5394fbffcc16f7986d17d"
+   },
+   {
+    "path": "referee_checks/err_O.txt",
+    "bytes": 0,
+    "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+   },
+   {
+    "path": "referee_checks/err_plain.txt",
+    "bytes": 0,
+    "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+   },
+   {
+    "path": "referee_checks/examples5.py",
+    "bytes": 420,
+    "sha256": "d450a6dbee15cee620ea08873f2a07a03bb7ea7fc781c2c3d485824dc8b9311e"
+   },
+   {
+    "path": "referee_checks/grid_analyze.py",
+    "bytes": 2252,
+    "sha256": "1f3495641870098c0b9b0537a528a0daa46bf786feae2c7105cbbf67849b8f5b"
+   },
+   {
+    "path": "referee_checks/grid_beta2.json",
+    "bytes": 229768,
+    "sha256": "d00b6bbb6930ebdf4d26987c479d8e36e2e445d639528a7507de66b6b9d6f8f2"
+   },
+   {
+    "path": "referee_checks/grid_broad.json",
+    "bytes": 230909,
+    "sha256": "4497f1b2313ca818aec9f7cc85a2f50a249819d01f40b4b7ffcb284973e521d1"
+   },
+   {
+    "path": "referee_checks/grid_delta.json",
+    "bytes": 116798,
+    "sha256": "50de739b12d77c7d98cfcd489eeda8eb1bbf0094ac238998c5e6d034a1953591"
+   },
+   {
+    "path": "referee_checks/grid_gauss.json",
+    "bytes": 232114,
+    "sha256": "5892766c09bbf272d9afb5639c2cadef2e6a35649bc4495a27860729ebbb8387"
+   },
+   {
+    "path": "referee_checks/grid_maximin.py",
+    "bytes": 7060,
+    "sha256": "b26ca4bc22615d8051eebd537b8c11220e471706aec3442e66ff32e10fcd9412"
+   },
+   {
+    "path": "referee_checks/lemmaB.py",
+    "bytes": 4627,
+    "sha256": "e985f705bfdbecb5679fbe872e4b6d761634e81401496414d5fd9d27bc8a6503"
+   },
+   {
+    "path": "referee_checks/lemmaB2.py",
+    "bytes": 3878,
+    "sha256": "c3e50e4013f9b9946c926fad94a3e2ac7460cf769bc671b922034f20039bf877"
+   },
+   {
+    "path": "referee_checks/log_H0grid.txt",
+    "bytes": 9,
+    "sha256": "6a1f3fb2ea206bfca05a9c4a0c31b46fa1d50201b4af66df9a58bda48857e41f"
+   },
+   {
+    "path": "referee_checks/log_Hconv48a.txt",
+    "bytes": 88,
+    "sha256": "703fb61e95f90943a1bee4881841a3bcfacc41c30145c5b99f39c7bce11dd9f0"
+   },
+   {
+    "path": "referee_checks/log_Hconv48b.txt",
+    "bytes": 85,
+    "sha256": "00f0066e8cbb1571c100ba0a57307e183250e9cbb04129f1d8decf45c37540a9"
+   },
+   {
+    "path": "referee_checks/log_Hfill1.txt",
+    "bytes": 610,
+    "sha256": "ce94f83bb30bbf8699b5102edf6e4e1ebbb081efcf12dade0b144ce151d276cd"
+   },
+   {
+    "path": "referee_checks/log_Hfill2.txt",
+    "bytes": 714,
+    "sha256": "786f633f985a652461ae3938601b24ce6ebd9436d4e779a3508c0e8f185f4680"
+   },
+   {
+    "path": "referee_checks/log_Hfill3.txt",
+    "bytes": 266,
+    "sha256": "521dabedd56dd08aff463993aa8f9bf33bd9c2c258ecc6c107731376d8dab588"
+   },
+   {
+    "path": "referee_checks/log_Hfill4.txt",
+    "bytes": 263,
+    "sha256": "5e8dadc2e1c395c1fb9e2e1248b44d78b4778dc312adb6e3a439c28cfb234eb8"
+   },
+   {
+    "path": "referee_checks/log_Hsmall32.txt",
+    "bytes": 434,
+    "sha256": "62d4c2559320f655e032809a856bde4ef2257fa1b852a60ab7e907c571523c49"
+   },
+   {
+    "path": "referee_checks/log_Htable32.txt",
+    "bytes": 695,
+    "sha256": "d0140471407ee62b49650f519e47d3ddfdc8913a55bb526cedf38d875b1be2b5"
+   },
+   {
+    "path": "referee_checks/log_beta2.txt",
+    "bytes": 15,
+    "sha256": "da9042b34c35633077c65a51c9a48b84ea4e0468f4821a321964d932a6a15891"
+   },
+   {
+    "path": "referee_checks/log_broad.txt",
+    "bytes": 15,
+    "sha256": "3500b5f36d1b92e0237ea50228fa8def650eea7f80f339f75f1330edee18fd0b"
+   },
+   {
+    "path": "referee_checks/log_delta.txt",
+    "bytes": 15,
+    "sha256": "43f71f8e110f15d83292f5f60c2e335d8053173b10c340e0d9887d3d324bb6d5"
+   },
+   {
+    "path": "referee_checks/log_gauss.txt",
+    "bytes": 15,
+    "sha256": "a5b347f3130978d9e945375ad66068011a7e1c5d828f5c3d849ee24d7cb13cb5"
+   },
+   {
+    "path": "referee_checks/out_O.json",
+    "bytes": 1822,
+    "sha256": "a63e5106170dc2eed34f8a79d6c4a590664a50f6d720a9a125d977c3d084e5ba"
+   },
+   {
+    "path": "referee_checks/out_plain.json",
+    "bytes": 1822,
+    "sha256": "a63e5106170dc2eed34f8a79d6c4a590664a50f6d720a9a125d977c3d084e5ba"
+   },
+   {
+    "path": "referee_checks/outliers.py",
+    "bytes": 1887,
+    "sha256": "67d7f6f75b46af7e62933315b03f76e8b92141b3264812cd22cacd2fd60c2a41"
+   },
+   {
+    "path": "referee_checks/phicore.py",
+    "bytes": 1538,
+    "sha256": "8ee9c185e2363af045cdfff8cd259697cdc029de8b4b7e87d27eb86b9649de3c"
+   },
+   {
+    "path": "referee_checks/roots_check.py",
+    "bytes": 1743,
+    "sha256": "ad70fcce9da318bdf9969e8a9a26c97eedf32bba53e0701f8754da23a5d1defd"
+   },
+   {
+    "path": "referee_checks/sym_algebra.py",
+    "bytes": 5367,
+    "sha256": "d9d877348b3c2d82a09d3c8b4909145caa5d613b51a103ba4a00e2383a1cb067"
+   },
+   {
+    "path": "REFEREE_CF.md",
+    "bytes": 28900,
+    "sha256": "f31dfe06ccb2da8dec893037f072ba630b7458bd01fe92b60c7c051cf55e6fe4"
+   },
+   {
+    "path": "PROOF_v1_preref.md",
+    "bytes": 38646,
+    "sha256": "3ed9317c474721e49414bcc2c840946396e82b581e90fa78cf734d46ca013848"
+   }
+  ]
+ },
+ "amendments": [
+  {
+   "label": "v1.2",
+   "files_changed": [
+    "PROOF.md",
+    "README.md",
+    "closed_form_check.py",
+    "RESULTS.json",
+    "SOURCES.json"
+   ],
+   "findings": [
+    "OA-244-D-01",
+    "OA-244-D-02",
+    "OA-244-D-03"
+   ],
+   "also": [
+    "rebinds #242 v1.5 and #243 v1.5",
+    "Remark A.1' (cited full-Delta lemma, checked in C3)"
+   ],
+   "results_change": "object, and the new C3.Delta_curve entry",
+   "unchanged": "the statements and proofs of Lemma 1, Theorems A and B, Corollaries A.1-A.4 and Lemmas B.1-B.2; the workflow"
+  }
+ ]
+}
diff --git a/frontiers/soft_closed_form_20261002/closed_form_check.py b/frontiers/soft_closed_form_20261002/closed_form_check.py
new file mode 100644
index 000000000..4050199c7
--- /dev/null
+++ b/frontiers/soft_closed_form_20261002/closed_form_check.py
@@ -0,0 +1,909 @@
+#!/usr/bin/env python3
+"""Exact controls for CL-SOFT-CLOSED-FORM-20261002-v1.2 (Theorem A, Corollaries A.1-A.4, Lemmas B.1-B.2, Theorem B;
+PROOF.md).
+
+Standard library only. Exact rationals, except where a control says floating point (v1.2, OA-244-D-03, the complete list):
+C2 (the explicit roots (2.6) against bisection), C4 (I(1, chi0) with psi_e found by bisection, and the positivity of I off
+its zero set by bisection), C6 (the bound (4.4) at random points), C7 (a Gauss-Legendre quadrature of (4.3)), C8 (the
+quadratures for E|B|^(7/2) and for the integral of (p(w) - p(0))/w^2) and C9 (#242's decimal S8 cases and the section 5
+examples, evaluated as Python floats). Everything else is exact. Output: RESULTS.json (sorted keys), byte-identical under -O.
+Usage:
+    python3 -B -S closed_form_check.py                 # exit 0, prints RESULTS.json
+    python3 -B -S closed_form_check.py --mutant M3     # exit 1 (only its control fails; M1..M9)
+    unknown mutant label                               -> exit 2
+
+Notation (PROOF (0.2)): psi = 1/phi, c' = 1 - t (written cp), R = chi0 + 8 - 12 t, sigma = R/8,
+g(psi) = 16 (psi - 2 cp)^2 (psi + cp).
+
+Controls
+  C1  Lemma 1: G(X, z) = P_theta(X, 24 phi z)/(24 phi) as a polynomial identity in (X, z) at random rational (phi, t, chi0),
+      theta = (-1/(24 phi), 1, t/12, chi0/576), k = 1; [CUB]'s B = -cp/12, D = R/1152, s = -psi/24; (2.3)-(2.4) exactly;
+      typing s < -|B|/2 iff psi > |cp|
+  C2  Theorem A: g' = 48 psi (psi - 2 cp) and g(c' + y)/16 = (y - cp)^2 (y + 2 cp) = y^3 - 3 cp^2 y + 2 cp^3 as polynomial
+      identities; g(psi0) = 0; the discriminant -(4p^3 + 27q^2) = 432 sigma^2 (cp^3 - sigma^2); (2.6) against bisection in
+      floating point on 600 points (both branches, cp = 0, sigma = 0), with psi_e >= psi0
+  C3  Corollary A.1: (3.1) as a polynomial identity in (psi, t); (3.3) from (2.5) at rational S (t = 3(1 - S^2)/4); the
+      ordering psi_+ >= t iff t <= 2/3; the values 20/3, 4/81, 1/3; the slopes -13/9, 5/9 and 1; strict monotonicity on a
+      rational grid; the Catalan series (3.4) and the series of I(t, 0) to order 12 (exact power series); v1.1, the fibre
+      t = 3/4, chi0 = 0 on Delta (OA-244-B-01): sigma^2 = cp^3, and at eight rational psi > 1/4 the completed square
+      24 phi G = F(v) - (psi/48)(Z - m(v))^2 (Z = 24 phi z, v = X + Z/8) as a polynomial identity in (v, Z), F', h_Y and
+      h_Y + 1, F(-1/2) = 0, F(1/2) = -1, the critical point Y with G(Y) = h_Y psi/24, the Hessian determinants at M, S, Y,
+      the sign of h_Y + 1; I(3/4, 0) = 5/48; v1.2, the whole curve Delta (the cited lemma, Math- #244 comment 5957328502):
+      at c' = sq^2 for sq in {1/3, 1/2, 1, 3/2}, both signs of sigma = -eps sq^3 and four typed psi each, the completed
+      square P = f_rho(v) + (s/2)(Z - m(v))^2 (rho = c'/psi, v = X + (1/12 + q)Z, q = eps sq/12) as a polynomial identity,
+      f_rho', h(rho) and h(rho) + 1, f_rho'' at v = -1/2, 1/2, -1/(2 rho), the extra saddle Y with G(Y) = h(rho) psi/24, the
+      switch at psi = 3c', and psi_e = 3c' with Phi(c', R) = (20/3) c'^3; at c' = 0, (t, chi0) = (1, 4), every typed psi is
+      elder
+  C4  Corollary A.2: I(1, chi0) = (chi0 - 4)^2/48; the minimum (4/3) cp^3 (cp > 0) and the zero set (cp <= 0) at R = 0;
+      the identity (2.7) as a polynomial identity in (cp, y) given the cubic for y
+  C5  Corollary A.4: g(t) = 16 (3t - 2)^2 when cp = 1 - t, and on 400 rational typed points with beta > 2, chi0 <= 0 the
+      test (A) fails
+  C6  Lemma B.2: (a) the derivative formula at rational points with rational square roots; (b) the reduction of
+      d^2 Phi/dR^2 to (3p^3 + 2cp p^2 + cp^2 p + 2cp^3)/(72 p^3) as a polynomial identity in (rho, cp); the range [0, 1/16]
+      and the monotonicity of 2x + x^2 + 2x^3; (c) the jump kappa = (3cp)^(3/2)/6 at rational squares; (d) the bound (4.4)
+      at 300 random points (floating point)
+  C7  Lemma B.1(b): F_-' and F_+' as polynomial identities after multiplying by tau^(9/2) S; the exact assembly of Lambda
+      in Q(sqrt3, sqrt6) = 128/105 - (2888 sqrt3 + 907 sqrt6)/2835; a floating-point evaluation of (4.3) (exact series near 0,
+      Gauss-Legendre elsewhere) within 1e-12; the two forms of h_{7/2} in (4.2) agree exactly in Q(sqrt2, sqrt6), and
+      h_{7/2} = -10.1440440225148...
+  C8  Theorem B's bookkeeping: E[gamma^6] = 120, E[gamma^6 t^2] = 576 k^2, 800 + 9984 k^2, 312/25 - 12 = 12/25, the
+      constants 62208 and 27648 sqrt6/3200 = (216/25) sqrt6, E|B|^q = 2^q Gamma((q+1)/2)/sqrt(pi) at q = 2, 4 (exact), and the
+      exponents 7/2, 4, 14/3, 25/6
+  C9  Fixed points: #242's exact (D') witness (3/2, 8/3, 20/3) is elder; (0, 0) has psi_e = 3, I = 20/3; #242's 16 control-S8
+      decisions; the PROOF section 5 examples
+"""
+import json
+import math
+import sys
+from fractions import Fraction as Fr
+
+MUTANTS = ('M1', 'M2', 'M3', 'M4', 'M5', 'M6', 'M7', 'M8', 'M9')
+MUT = None
+H = Fr(1, 2)
+
+
+class LCG:
+    def __init__(self, seed):
+        self.s = seed % (2 ** 61 - 1)
+
+    def nxt(self):
+        self.s = (self.s * 437799614237992725 + 1) % (2 ** 61 - 1)
+        return self.s
+
+    def rat(self, num, den, nonzero=False):
+        while True:
+            x = Fr(self.nxt() % (2 * num + 1) - num, 1 + self.nxt() % den)
+            if x != 0 or not nonzero:
+                return x
+
+
+# --------------------------------------------------------------------------------- sparse polynomials over Q
+class P:
+    """Polynomial in NV variables: dict exponent-tuple -> Fraction."""
+    NV = 4
+
+    def __init__(self, terms=None):
+        self.t = {}
+        for k, v in (terms or {}).items():
+            if v != 0:
+                self.t[k] = Fr(v)
+
+    @classmethod
+    def const(cls, c):
+        return cls({(0,) * cls.NV: c})
+
+    @classmethod
+    def var(cls, i):
+        e = [0] * cls.NV
+        e[i] = 1
+        return cls({tuple(e): 1})
+
+    def __add__(self, o):
+        o = o if isinstance(o, P) else P.const(o)
+        r = dict(self.t)
+        for k, v in o.t.items():
+            r[k] = r.get(k, 0) + v
+        return P(r)
+
+    __radd__ = __add__
+
+    def __neg__(self):
+        return P({k: -v for k, v in self.t.items()})
+
+    def __sub__(self, o):
+        return self + (-(o if isinstance(o, P) else P.const(o)))
+
+    def __rsub__(self, o):
+        return P.const(o) - self
+
+    def __mul__(self, o):
+        o = o if isinstance(o, P) else P.const(o)
+        r = {}
+        for k1, v1 in self.t.items():
+            for k2, v2 in o.t.items():
+                k = tuple(a + b for a, b in zip(k1, k2))
+                r[k] = r.get(k, 0) + v1 * v2
+        return P(r)
+
+    __rmul__ = __mul__
+
+    def __pow__(self, n):
+        r = P.const(1)
+        for _ in range(n):
+            r = r * self
+        return r
+
+    def is_zero(self):
+        return not self.t
+
+    def diff(self, i):
+        r = {}
+        for k, v in self.t.items():
+            if k[i]:
+                e = list(k)
+                e[i] -= 1
+                r[tuple(e)] = r.get(tuple(e), 0) + v * k[i]
+        return P(r)
+
+    def subs(self, i, val):
+        """substitute variable i by the polynomial val"""
+        r = P()
+        for k, v in self.t.items():
+            e = list(k)
+            n = e[i]
+            e[i] = 0
+            r = r + P({tuple(e): v}) * (val ** n)
+        return r
+
+
+V0, V1, V2, V3 = (P.var(i) for i in range(4))
+
+
+# --------------------------------------------------------------------------------- the closed form (PROOF Theorem A)
+def g_of(psi, cp, c16=16):
+    return c16 * (psi - 2 * cp) ** 2 * (psi + cp)
+
+
+def elder_test(psi, cp, R):
+    """(A): exact if the inputs are exact"""
+    return psi >= 2 * cp and R * R <= g_of(psi, cp)
+
+
+def psi_e_bisect(cp, R):
+    lo = max(2 * cp, -cp)
+    hi = lo + 1.0
+    while g_of(hi, cp) < R * R:
+        hi = lo + 2 * (hi - lo)
+    for _ in range(200):
+        m = 0.5 * (lo + hi)
+        if g_of(m, cp) < R * R:
+            lo = m
+        else:
+            hi = m
+    return 0.5 * (lo + hi)
+
+
+def psi_e_formula(cp, R, mutate=False):
+    s = R / 8.0
+    if cp > 0 and s * s <= cp ** 3:
+        return cp + 2 * cp * math.cos(2.0 / 3.0 * math.acos(min(1.0, abs(s) / cp ** 1.5)))
+    A = abs(s) + math.sqrt(s * s - cp ** 3)
+    if A == 0:
+        return cp
+    a23 = A ** (2.0 / 3.0)
+    return cp + a23 + (-1 if mutate else 1) * cp * cp / a23
+
+
+def Phi_float(cp, R):
+    d = psi_e_bisect(cp, R) - abs(cp)
+    return abs(cp) * d * d + d ** 3 / 3
+
+
+# ======================================================================================= C1: Lemma 1
+def control_C1():
+    rng = LCG(4101)
+    ok = True
+    X, Z = V0, V1
+    n_id = 0
+    for _ in range(30):
+        phi = abs(rng.rat(40, 17, True))
+        t = rng.rat(60, 13)
+        x0 = rng.rat(200, 7)
+        beta, chi = 2 * t * phi, x0 * phi * phi
+        G = (2 * (X + H) ** 2 * (X - 1) * Fr(1, 24) * (1 / phi) + H * (X * X - Fr(1, 4)) * Z - H * (1 - beta * X) * Z * Z
+             + Fr(chi, 6) * Z ** 3)
+        s, a, bp, c = -1 / (24 * phi), Fr(1), t / 12, x0 / 576
+        Zs = 24 * phi * Z
+        Pth = (2 * X ** 3 - Fr(3, 2) * X - H + s * Zs * Zs * H + (a * H) * (X * X - Fr(1, 4)) * Zs + (bp * H) * X * Zs * Zs
+               + Fr(1, 6) * c * Zs ** 3)
+        ok &= (G - Pth * (1 / (24 * phi))).is_zero()
+        n_id += 1
+        # [CUB] (C2), (C5)
+        psi, cp, R = 1 / phi, 1 - t, x0 + 8 - 12 * t
+        B = bp - a * a / 12
+        D = (c - a * bp / 4 + a ** 3 / 72) / 2
+        ok &= B == -cp / 12 and D == R / 1152 and s == -psi / 24
+        T = -(s - B) ** 2 * (B + 2 * s) / 12
+        c16 = 15 if MUT == 'M1' else 16
+        ok &= T == (psi - 2 * cp) ** 2 * (psi + cp) / 82944
+        ok &= 1327104 * (T - D * D) == g_of(psi, cp, c16) - R * R
+        ok &= 12 * D * D + B ** 3 == (R * R - 64 * cp ** 3) / 110592
+        ok &= 12 * D * D + (s - B) ** 2 * (B + 2 * s) == (R * R - g_of(psi, cp, c16)) / 110592
+        ok &= (s < -abs(B) / 2) == (psi > abs(cp))
+        ok &= (s <= B) == (psi >= 2 * cp)
+    # typing at boundary values
+    for cp in (Fr(1, 3), Fr(-2, 5), Fr(0)):
+        for psi in (abs(cp), abs(cp) + Fr(1, 1000), 2 * cp if cp > 0 else abs(cp) + 1):
+            s, B = -psi / 24, -cp / 12
+            ok &= (s < -abs(B) / 2) == (psi > abs(cp))
+    return ok, {'identities_G_eq_P': n_id, 'CUB_B': '-cp/12', 'CUB_D': 'R/1152', 'CUB_T': '(psi-2cp)^2(psi+cp)/82944',
+                'Delta_1': 'sigma^2 = cp^3', 'Sigma_1': 'R^2 = g(psi)'}
+
+
+# ======================================================================================= C2: Theorem A
+def control_C2():
+    ok = True
+    psi, cp, y, sg = V0, V1, V2, V3
+    g = 16 * (psi - 2 * cp) ** 2 * (psi + cp)
+    ok &= (g.diff(0) - 48 * psi * (psi - 2 * cp)).is_zero()
+    gy = g.subs(0, cp + y)
+    ok &= (gy - 16 * ((y - cp) ** 2 * (y + 2 * cp))).is_zero()
+    ok &= (gy - 16 * (y ** 3 - 3 * cp * cp * y + 2 * cp ** 3)).is_zero()
+    p, q = -3 * cp * cp, 2 * cp ** 3 - 4 * sg * sg
+    ok &= ((-(4 * p ** 3 + 27 * q * q)) - 432 * sg * sg * (cp ** 3 - sg * sg)).is_zero()
+    for c in (Fr(2, 7), Fr(-3, 4), Fr(0)):
+        ok &= g_of(max(2 * c, -c), c) == 0
+    # explicit roots against bisection (floating point)
+    rng = LCG(4202)
+    worst = 0.0
+    n = 0
+    branches = {'trig': 0, 'cardano': 0}
+    pts = [(0.0, 0.0), (0.0, 3.0), (0.0, -5.0), (-2.0, 0.0), (1.0, 8.0), (0.5, 0.0), (0.5, 2.8284271247461903)]
+    while len(pts) < 600:
+        cpv = float(rng.rat(300, 11))
+        Rv = float(rng.rat(2000, 9))
+        pts.append((cpv, Rv))
+    for (cpv, Rv) in pts:
+        a = psi_e_formula(cpv, Rv, mutate=(MUT == 'M2'))
+        b = psi_e_bisect(cpv, Rv)
+        worst = max(worst, abs(a - b) / max(1.0, abs(b)))
+        p0 = max(2 * cpv, -cpv)
+        ok &= a >= p0 - 1e-9 * max(1.0, abs(p0))
+        # Remark 4 / (2.8): psi_e <= psi0 + (R^2/16)^(1/3) and Phi <= (16/3)|cp|^3 + R^2/3
+        ok &= b <= p0 + (Rv * Rv / 16) ** (1.0 / 3.0) + 1e-9 * max(1.0, b)
+        dd = b - abs(cpv)
+        ok &= abs(cpv) * dd * dd + dd ** 3 / 3 <= (16.0 / 3.0) * abs(cpv) ** 3 + Rv * Rv / 3 + 1e-9 * (1 + Rv * Rv)
+        branches['trig' if (cpv > 0 and (Rv / 8) ** 2 <= cpv ** 3) else 'cardano'] += 1
+        n += 1
+    ok &= worst < 1e-9
+    # g >= 16 (psi - psi0)^3 on [psi0, inf): both factors dominate psi - psi0 (exact, random rationals)
+    rng2 = LCG(4203)
+    for _ in range(200):
+        c = rng2.rat(40, 7)
+        p0 = max(2 * c, -c)
+        ps = p0 + abs(rng2.rat(60, 7))
+        ok &= g_of(ps, c) >= 16 * (ps - p0) ** 3
+    return ok, {'points': n, 'branches': branches, 'max_rel_dev_formula_vs_bisection_lt_1e-9': worst < 1e-9,
+                'bound_2_8': '(16/3)|cp|^3 + R^2/3'}
+
+
+# ======================================================================================= C3: Corollary A.1
+def catalan(m):
+    return math.comb(2 * m, m) // (m + 1)
+
+
+def sqrt_series(coef_lin, order):
+    """exact power series of sqrt(1 + coef_lin*x) to x^order"""
+    out = []
+    for n in range(order + 1):
+        b = Fr(1)
+        for j in range(n):
+            b *= (H - j)
+        b /= math.factorial(n)
+        out.append(b * coef_lin ** n)
+    return out
+
+
+def ser_mul(a, b, order):
+    return [sum(a[i] * b[n - i] for i in range(n + 1)) for n in range(order + 1)]
+
+
+def I0_exact_at_S(S):
+    """I(t, 0) at t = 3(1 - S^2)/4 with S >= 0 rational (t <= 3/4); returns (t, I) from (3.3)/(3.2)"""
+    t = Fr(3, 4) * (1 - S * S)
+    if t <= Fr(2, 3):
+        cp = 1 - t
+        d = H - t + Fr(3, 2) * S
+        return t, cp * d * d + d ** 3 / 3
+    return t, None
+
+
+def ev1v(poly, i, val):
+    """evaluate a polynomial in the single variable i at a rational"""
+    return sum(c * val ** k[i] for k, c in poly.t.items())
+
+
+def ev2v(poly, x0, z0):
+    """evaluate a polynomial in V0, V1 at (x0, z0)"""
+    return sum(c * x0 ** k[0] * z0 ** k[1] for k, c in poly.t.items())
+
+
+def fibre_34(psi):
+    """OA-244-B-01: the fibre t = 3/4, chi0 = 0 (on Delta for every typed phi) at a rational psi > 1/4 (PROOF section 3)"""
+    ok = True
+    X, z = V0, V1
+    phi = 1 / psi
+    beta = 2 * Fr(3, 4) * phi
+    G = 2 * (X + H) ** 2 * (X - 1) * Fr(1, 24) * psi + H * (X * X - Fr(1, 4)) * z - H * (1 - beta * X) * z * z
+    v, Zv = V2, V3
+    Pp = (G * (24 * phi)).subs(1, Zv * (psi / 24)).subs(0, v - Zv * Fr(1, 8))
+    m = Fr(3, 2) / psi * (1 - 4 * v * v)
+    F = 2 * v ** 3 - Fr(3, 2) * v - H + Fr(3, 64) / psi * (1 - 4 * v * v) ** 2
+    ok &= (Pp - (F - psi / 48 * (Zv - m) ** 2)).is_zero()
+    ok &= (F.diff(2) - (3 / psi) * (v * v - Fr(1, 4)) * (v + 2 * psi)).is_zero()
+    hY = ev1v(F, 2, -2 * psi)
+    ok &= hY == -(4 * psi - 1) ** 3 * (4 * psi + 3) / (64 * psi)
+    ok &= hY + 1 == -(4 * psi - 3) * (4 * psi + 1) ** 3 / (64 * psi)
+    ok &= ev1v(F, 2, -H) == 0 and ev1v(F, 2, H) == -1
+    xY, zY = psi - Fr(3, 16) / psi, Fr(1, 16) - psi * psi
+    ok &= ev2v(G.diff(0), xY, zY) == 0 and ev2v(G.diff(1), xY, zY) == 0
+    ok &= ev2v(G, xY, zY) == hY * psi / 24
+    ok &= ev2v(G, -H, Fr(0)) == 0 and ev2v(G, H, Fr(0)) == -psi / 24
+    Gxx, Gxz, Gzz = G.diff(0).diff(0), G.diff(0).diff(1), G.diff(1).diff(1)
+    det = lambda x0, z0: ev2v(Gxx, x0, z0) * ev2v(Gzz, x0, z0) - ev2v(Gxz, x0, z0) ** 2
+    ok &= det(-H, Fr(0)) == (4 * psi - 1) / 16 and det(H, Fr(0)) == -(4 * psi + 1) / 16
+    ok &= det(xY, zY) == (1 - 16 * psi * psi) / 32
+    ok &= ((hY + 1 > 0) == (psi < Fr(3, 4))) and ((hY + 1 == 0) == (psi == Fr(3, 4)))
+    return ok
+
+
+def delta_fibre(sq, eps, psi):
+    """v1.2: the whole curve Delta (cited lemma, Math- #244 comment 5957328502, nonauthor ACCEPT 5957356693): c' = sq^2 > 0,
+    sigma = -eps sq^3 (so R^2 = 64 c'^3), at a rational typed psi > c' (PROOF section 3, Remark A.1')"""
+    ok = True
+    cp = sq * sq
+    t = 1 - cp
+    R = -8 * eps * sq ** 3
+    chi0 = R - 8 + 12 * t
+    phi = 1 / psi
+    beta, chi = 2 * t * phi, chi0 * phi * phi
+    X, z = V0, V1
+    G = (2 * (X + H) ** 2 * (X - 1) * Fr(1, 24) * psi + H * (X * X - Fr(1, 4)) * z - H * (1 - beta * X) * z * z
+         + Fr(1, 6) * chi * z ** 3)
+    q = eps * sq / 12
+    rho = cp / psi
+    s = -psi / 24
+    v, Zv = V2, V3
+    Pp = (G * (24 * phi)).subs(1, Zv * (psi / 24)).subs(0, v - Zv * (Fr(1, 12) + q))
+    m = (6 * q / s) * (v * v - Fr(1, 4))
+    f = 2 * v ** 3 - Fr(3, 2) * v - H + 3 * rho * (v * v - Fr(1, 4)) ** 2
+    ok &= (Pp - (f + (s / 2) * (Zv - m) ** 2)).is_zero()
+    ok &= (f.diff(2) - 6 * (v * v - Fr(1, 4)) * (1 + 2 * rho * v)).is_zero()
+    vY = -1 / (2 * rho)
+    h = ev1v(f, 2, vY)
+    ok &= h == -(1 - rho) ** 3 * (1 + 3 * rho) / (16 * rho ** 3)
+    ok &= h + 1 == -(1 - 3 * rho) * (1 + rho) ** 3 / (16 * rho ** 3)
+    ok &= ev1v(f, 2, -H) == 0 and ev1v(f, 2, H) == -1
+    f2 = f.diff(2).diff(2)
+    ok &= ev1v(f2, 2, -H) == -6 * (1 - rho) and ev1v(f2, 2, H) == 6 * (1 + rho)
+    ok &= ev1v(f2, 2, vY) == 3 * (1 - rho * rho) / rho
+    ZY = ev1v(m, 2, vY)
+    xY, zY = vY - (Fr(1, 12) + q) * ZY, ZY * psi / 24
+    ok &= ev2v(G.diff(0), xY, zY) == 0 and ev2v(G.diff(1), xY, zY) == 0
+    ok &= ev2v(G, xY, zY) == h * psi / 24
+    ok &= ((h + 1 > 0) == (psi < 3 * cp)) and ((h + 1 == 0) == (psi == 3 * cp))
+    ok &= R * R == 64 * cp ** 3 and g_of(3 * cp, cp) == R * R and elder_test(3 * cp, cp, R)
+    dl = 2 * cp
+    ok &= cp * dl * dl + dl ** 3 / 3 == Fr(20, 3) * cp ** 3
+    return ok
+
+
+def control_C3():
+    ok = True
+    psi, t = V0, V1
+    cp = 1 - t
+    lhs = (psi - 2 * cp) ** 2 * (psi + cp) - (2 - 3 * t) ** 2
+    rhs = (psi - t) * (psi * psi + (4 * t - 3) * psi + 4 * t * t - 3 * t)
+    ok &= (lhs - rhs).is_zero()
+    # (3.3) on t <= 2/3 from (2.5), at rational S
+    n33 = 0
+    for k in range(1, 61):
+        S = Fr(k, 20)                        # S in (0, 3]; t = 3(1 - S^2)/4 in [-6, 3/4)
+        tt = Fr(3, 4) * (1 - S * S)
+        if tt > Fr(2, 3):
+            # psi_+ < t on (2/3, 3/4]
+            ok &= Fr(3, 2) - 2 * tt + Fr(3, 2) * S < tt
+            continue
+        ok &= Fr(3, 2) - 2 * tt + Fr(3, 2) * S >= tt          # psi_+ >= t
+        _, I = I0_exact_at_S(S)
+        form = (Fr(11, 3) - Fr(21, 2) * tt + Fr(17, 2) * tt ** 2 - Fr(4, 3) * tt ** 3
+                + Fr(3, 2) * (1 - tt) * (2 - 3 * tt) * S)
+        ok &= I == form
+        n33 += 1
+    # the values and slopes
+    _, I00 = I0_exact_at_S(Fr(1))
+    ok &= I00 == Fr(20, 3)
+    _, I23 = I0_exact_at_S(Fr(1, 3))
+    mid = lambda u: (2 * u - 1) ** 2 * (2 - u) / 3
+    ok &= I23 == Fr(4, 81) == mid(Fr(2, 3))
+    ok &= mid(Fr(1)) == Fr(1, 3) == Fr(1) - Fr(2, 3)
+    # I0' = -delta [2 psi_e + (psi_e + cp)/S] against the exact derivative of (3.3) at rational S (t <= 2/3):
+    #   d/dt [P0 + P1 S] = P0' + P1' S + P1 S',  S' = -(2/3)/S
+    nder = 0
+    for k in range(7, 61):
+        S = Fr(k, 20)
+        tt = Fr(3, 4) * (1 - S * S)
+        if tt > Fr(2, 3):
+            continue
+        P0p = Fr(-21, 2) + 17 * tt - 4 * tt * tt
+        P1 = Fr(3, 2) * (1 - tt) * (2 - 3 * tt)
+        P1p = Fr(3, 2) * (-(2 - 3 * tt) - 3 * (1 - tt))
+        exact = P0p + P1p * S + P1 * (Fr(-2, 3) / S)
+        d, pe, c_ = H - tt + Fr(3, 2) * S, Fr(3, 2) - 2 * tt + Fr(3, 2) * S, 1 - tt
+        ok &= exact == -d * (2 * pe + (pe + c_) / S) and exact < 0
+        nder += 1
+    d, pe, c_, S = Fr(1, 3), Fr(2, 3), Fr(1, 3), Fr(1, 3)
+    ok &= -d * (2 * pe + (pe + c_) / S) == Fr(-13, 9)
+    dmid = lambda u: (2 * u - 1) * (3 - 2 * u)
+    ok &= dmid(Fr(2, 3)) == Fr(5, 9) and dmid(Fr(1)) == 1
+    # derivatives of the middle piece; C^2 but not C^3 at t = 1 (the right piece t - 2/3 has I'' = I''' = 0)
+    u = V1
+    midp = (2 * u - 1) ** 2 * (2 - u) * Fr(1, 3)
+    ok &= (midp.diff(1) - (2 * u - 1) * (3 - 2 * u)).is_zero()
+    ev1 = lambda poly: sum(v * Fr(1) ** k[1] for k, v in poly.t.items())
+    ok &= ev1(midp.diff(1).diff(1)) == 0 and ev1(midp.diff(1).diff(1).diff(1)) == -8
+    # strict monotonicity on a rational grid: decreasing for t <= 2/3, increasing on [2/3, 1] and beyond
+    vals = []
+    for k in range(60, 6, -1):
+        S = Fr(k, 20)
+        tt, I = I0_exact_at_S(S)
+        if I is not None:
+            vals.append((tt, I))
+    vals.sort()
+    ok &= all(vals[i][1] > vals[i + 1][1] for i in range(len(vals) - 1))
+    grid = [Fr(2, 3) + Fr(j, 90) for j in range(31)]
+    mids = [mid(x) for x in grid]
+    ok &= all(mids[i] < mids[i + 1] for i in range(len(mids) - 1))
+    # the Catalan series of psi_e(t, 0) = 3/2 - 2t + (3/2) sqrt(1 - 4t/3), and the series of I(t, 0)
+    N = 12
+    sq = sqrt_series(Fr(-4, 3), N)
+    pe_ser = [Fr(3, 2) * c for c in sq]
+    pe_ser[0] += Fr(3, 2)
+    pe_ser[1] += -2
+    cat_ser = [Fr(3), Fr(-3)] + [Fr(-(catalan(m) + (1 if (MUT == 'M3' and m == 3) else 0)), 3 ** m) for m in range(1, N)]
+    ok &= pe_ser == cat_ser
+    # the quadratic factor vanishes as a power series: psi^2 + (4t - 3) psi + 4t^2 - 3t
+    sq_pe = ser_mul(pe_ser, pe_ser, N)
+    lin = [Fr(0)] * (N + 1)
+    for n in range(N + 1):
+        lin[n] += -3 * pe_ser[n] + (4 * pe_ser[n - 1] if n >= 1 else 0)
+    quad = [sq_pe[n] + lin[n] + (-3 if n == 1 else 0) + (4 if n == 2 else 0) for n in range(N + 1)]
+    ok &= all(q == 0 for q in quad)
+    # I(t, 0) series: cp = 1 - t, delta = psi_e - cp
+    cp_ser = [Fr(1), Fr(-1)] + [Fr(0)] * (N - 1)
+    dl = [a - b for a, b in zip(pe_ser, cp_ser)]
+    d2 = ser_mul(dl, dl, N)
+    I_ser = [a + b / 3 for a, b in zip(ser_mul(cp_ser, d2, N), ser_mul(d2, dl, N))]
+    ok &= I_ser[:6] == [Fr(20, 3), Fr(-20), Fr(52, 3), Fr(-28, 9), Fr(-7, 27), Fr(-7, 81)]
+    # phi_e = 1/psi_e = 1/3 + t/3 + 10 t^2/27 + ...
+    inv = [Fr(1, 3)]
+    for n in range(1, 4):
+        inv.append(-sum(pe_ser[i] * inv[n - i] for i in range(1, n + 1)) / pe_ser[0])
+    ok &= inv[:3] == [Fr(1, 3), Fr(1, 3), Fr(10, 27)]
+    # v1.1, OA-244-B-01: the fibre t = 3/4, chi0 = 0
+    cp34, R34 = Fr(1, 4), Fr(8) - 12 * Fr(3, 4)
+    ok &= (R34 / 8) ** 2 == cp34 ** 3
+    psis = (Fr(3, 10), Fr(1, 2), Fr(2, 3), Fr(3, 4), Fr(4, 5), Fr(1), Fr(2), Fr(7))
+    for ps in psis:
+        ok &= fibre_34(ps)
+    I34 = (Fr(27, 64) - Fr(1, 64)) / 3 - (Fr(3, 4) - Fr(1, 4)) / 16
+    ok &= I34 == Fr(5, 48) == mid(Fr(3, 4))
+    # v1.2: the whole curve Delta (cited lemma 5957328502); the fibre t = 3/4 is sq = 1/2, eps = 1
+    n_delta = 0
+    for sq in (Fr(1, 3), Fr(1, 2), Fr(1), Fr(3, 2)):
+        cpd = sq * sq
+        for eps in (1, -1):
+            for ps in (cpd * Fr(8, 7), 2 * cpd, 3 * cpd, 4 * cpd):
+                ok &= delta_fibre(sq, eps, ps)
+                n_delta += 1
+    ok &= (Fr(20, 3) * (Fr(1, 4)) ** 3 == I34) and (Fr(20, 3) == I00)
+    ok &= all(elder_test(ps, Fr(0), Fr(0)) for ps in (Fr(1, 5), Fr(1), Fr(7)))     # c' = 0: (t, chi0) = (1, 4), I = 0
+    return ok, {'identity_3_1': True, 'points_3_3': n33, 'points_derivative': nder, 't_star': '2/3', 'I(0,0)': str(I00), 'I(2/3,0)': str(I23),
+                'fibre_3/4': {'psi_points': len(psis), 'I(3/4,0)': str(I34), 'tie_at_psi': '3/4'},
+                'Delta_curve': {'points': n_delta, 'I_on_Delta': "(20/3) c'^3", 'switch_at_psi': "3c'"},
+                'slopes_at_2/3': ['-13/9', '5/9'], 'catalan_terms': N, 'I_series': [str(x) for x in I_ser[:6]],
+                'phi_e_series': [str(x) for x in inv[:3]]}
+
+
+# ======================================================================================= C4: Corollary A.2
+def control_C4():
+    ok = True
+    rng = LCG(4404)
+    den = 47 if MUT == 'M4' else 48
+    psi = V0
+    ok &= (16 * (psi - 0) ** 2 * (psi + 0) - 16 * psi ** 3).is_zero()          # g_0(psi) = 16 psi^3
+    for _ in range(40):
+        x0 = rng.rat(400, 9)
+        R = float(x0 - 4)                # t = 1, cp = 0
+        pe = psi_e_bisect(0.0, R)        # found independently
+        I1 = pe ** 3 / 3
+        ok &= abs(I1 - float((x0 - 4) ** 2) / den) <= 1e-9 * (1 + I1)
+    for _ in range(40):
+        c = rng.rat(50, 7, True)
+        pe = max(2 * c, -c)              # R = 0: psi_e = psi0
+        ok &= g_of(pe, c) == 0
+        d = pe - abs(c)
+        I = abs(c) * d * d + d ** 3 / 3
+        ok &= I == (Fr(4, 3) * c ** 3 if c > 0 else 0)
+        if c > 0:                        # the rejected strip (c', 2c') alone carries (4/3) c'^3 (used on Delta)
+            ok &= (8 * c ** 3 / 3 - c * c * 2 * c) - (c ** 3 / 3 - c ** 3) == Fr(4, 3) * c ** 3
+    # the zero set, both directions: I = 0 on {t > 1, chi0 = 12t - 8}; I > 0 off it (floating point, bisection)
+    nz = 0
+    for _ in range(200):
+        tt = float(rng.rat(300, 11))
+        x0 = float(rng.rat(300, 7))
+        if tt > 1 and abs(x0 + 8 - 12 * tt) < 1e-9:
+            continue
+        cpv, Rv = 1 - tt, x0 + 8 - 12 * tt
+        dd = psi_e_bisect(cpv, Rv) - abs(cpv)
+        ok &= abs(cpv) * dd * dd + dd ** 3 / 3 > 0
+        nz += 1
+    for _ in range(20):
+        tt = 1 + abs(rng.rat(300, 11, True))
+        c = 1 - tt
+        ok &= g_of(-c, c) == 0 and (lambda d: abs(c) * d * d + d ** 3 / 3)(-c - abs(c)) == 0
+    # (2.7): with R^2 := 16 (y^3 - 3cp^2 y + 2cp^3) and psi_e = cp + y,
+    #   psi_e^3/3 - cp^2 psi_e  ==  R^2/48 + cp y (y + cp) - (4/3) cp^3       (the (2/3)|cp|^3 terms agree on both sides)
+    cp, y = V0, V1
+    R2 = 16 * (y ** 3 - 3 * cp * cp * y + 2 * cp ** 3)
+    lhs = (cp + y) ** 3 * Fr(1, 3) - cp * cp * (cp + y)
+    rhs = R2 * Fr(1, 48) + cp * y * (y + cp) - Fr(4, 3) * cp ** 3
+    ok &= (lhs - rhs).is_zero()
+    # and the equivalence of (2.5) with psi_e^3/3 - cp^2 psi_e + (2/3)|cp|^3:  |cp| d^2 + d^3/3, d = psi_e - |cp|
+    for _ in range(30):
+        c = rng.rat(30, 7)
+        pe = abs(c) + abs(rng.rat(30, 7))
+        d = pe - abs(c)
+        ok &= abs(c) * d * d + d ** 3 / 3 == pe ** 3 / 3 - c * c * pe + Fr(2, 3) * abs(c) ** 3
+    return ok, {'I(1,chi0)': '(chi0 - 4)^2/48', 'min_over_chi0': '(4/3)(1-t)_+^3', 'identity_2_7': True,
+                'zero_set_positive_points': nz}
+
+
+# ======================================================================================= C5: Corollary A.4
+def control_C5():
+    ok = True
+    t = V0
+    ok &= (16 * (t - 2 * (1 - t)) ** 2 * (t + (1 - t)) - 16 * (3 * t - 2) ** 2).is_zero()
+    rng = LCG(4505)
+    n = 0
+    while n < 400:
+        tt = rng.rat(400, 13)
+        x0 = -abs(rng.rat(300, 11))
+        if MUT == 'M5':
+            x0 = abs(x0) + 40
+        cp = 1 - tt
+        if tt <= 0:
+            continue
+        # typed with beta > 2: |cp| < psi < t
+        lo, hi = abs(cp), tt
+        if not lo < hi:
+            continue
+        psi = lo + (hi - lo) * Fr(1 + rng.nxt() % 998, 1000)
+        R = x0 + 8 - 12 * tt
+        if tt >= Fr(2, 3):
+            ok &= g_of(tt, cp) == 16 * (3 * tt - 2) ** 2
+            ok &= R * R >= g_of(tt, cp) and (psi < max(2 * cp, -cp) or g_of(psi, cp) < g_of(tt, cp))
+        else:
+            ok &= psi < 2 * cp
+        ok &= not elder_test(psi, cp, R)
+        n += 1
+    return ok, {'points_beta_gt_2_chi_le_0': n, 'all_rejected': ok}
+
+
+# ======================================================================================= C6: Lemma B.2
+def control_C6():
+    ok = True
+    # (a) at rational points with rho + 3cp = q^2: R = 4 rho q, psi_e = rho + 2cp;
+    #     dPhi/dR = (psi_e^2 - cp^2) * 2R / g'(psi_e)  ==  (rho + cp) q^3 / (6 (rho + 2 cp))
+    rng = LCG(4606)
+    na = 0
+    for _ in range(60):
+        cp = rng.rat(20, 7)
+        q = abs(rng.rat(20, 5, True))
+        rho = q * q - 3 * cp
+        if rho <= 0 or rho + 2 * cp <= 0:
+            continue
+        R = 4 * rho * q
+        pe = rho + 2 * cp
+        ok &= g_of(pe, cp) == R * R
+        gp = 48 * pe * (pe - 2 * cp)
+        ok &= (pe * pe - cp * cp) * 2 * R / gp == (rho + cp) * q ** 3 / (6 * (rho + 2 * cp))
+        na += 1
+    # (b) d2Phi/dR2 = F'(rho) sqrt(rho+3cp)/(6p), with F = (rho+cp)(rho+3cp)^(3/2)/(6p), p = rho + 2cp:
+    #     = [(rho+3cp)^2 + (3/2)(rho+cp)(rho+3cp)]/(36 p^2) - (rho+cp)(rho+3cp)^2/(36 p^3)
+    rho, cp = V0, V1
+    p = rho + 2 * cp
+    cub = 2 if MUT != 'M6' else 3
+    lhs = 2 * ((rho + 3 * cp) ** 2 + Fr(3, 2) * (rho + cp) * (rho + 3 * cp)) * p - 2 * (rho + cp) * (rho + 3 * cp) ** 2
+    rhs = 3 * p ** 3 + 2 * cp * p * p + cp * cp * p + cub * cp ** 3
+    ok &= (lhs - rhs).is_zero()                      # both sides times 72 p^3
+    # the range: x = cp/p in [-1, 1/2]; 1/24 + (2x + x^2 + 2x^3)/72 in [0, 1/16]
+    f = lambda x: Fr(1, 24) + (2 * x + x * x + 2 * x ** 3) / 72
+    ok &= f(Fr(-1)) == 0 and f(H) == Fr(1, 16)
+    xv = V0
+    dpoly = (2 * xv + xv * xv + 2 * xv ** 3).diff(0)          # 2 + 2x + 6x^2
+    co = {k[0]: v for k, v in dpoly.t.items()}
+    ok &= co.get(1, 0) ** 2 - 4 * co.get(2, 0) * co.get(0, 0) < 0
+    ok &= f(Fr(1, 3)) == Fr(13, 243)                           # d2Phi(1, 8): psi_e = 3, x = 1/3
+    ok &= (3 * 3 ** 3 + 2 * 1 * 3 ** 2 + 1 * 3 + 2) * Fr(1, 72 * 27) == Fr(13, 243)
+    xs = [Fr(-1) + Fr(k, 40) for k in range(61)]
+    ok &= all(f(xs[i]) < f(xs[i + 1]) for i in range(len(xs) - 1))
+    # (c) the one-sided limits as exact values of F(rho) = (rho + cp)(rho + 3cp)^(3/2)/(6(rho + 2cp)) at rho0:
+    #     cp > 0: rho0 = 0, F = (3cp)^(3/2)/12 (jump 2F = kappa); cp < 0: rho0 = 3|cp|, F = 0; cp = 0: F = rho^(3/2)/6 -> 0
+    def Fexact(rho, cp, q):              # q = sqrt(rho + 3cp), rational
+        return (rho + cp) * q ** 3 / (6 * (rho + 2 * cp))
+    for qq in (Fr(1), Fr(3, 2), Fr(2, 5)):
+        c = qq * qq / 3
+        ok &= Fexact(Fr(0), c, qq) == qq ** 3 / 12 and 2 * Fexact(Fr(0), c, qq) == qq ** 3 / 6
+    for c in (Fr(-1), Fr(-2, 7)):
+        ok &= Fexact(3 * abs(c), c, Fr(0)) == 0
+    ok &= all(Fexact(Fr(1, n * n), Fr(0), Fr(1, n)) == Fr(1, 6 * n ** 3) for n in (10, 100, 1000))
+    # (d) the bound (4.4) at random points (floating point)
+    worst = -1.0
+    for _ in range(300):
+        c = float(rng.rat(30, 7))
+        r = float(rng.rat(300, 7))
+        h = float(rng.rat(300, 7))
+        d2 = 0.5 * (Phi_float(c, r + h) + Phi_float(c, r - h)) - Phi_float(c, r)
+        kap = (3 * max(c, 0.0)) ** 1.5 / 6
+        bound = h * h / 32 + (kap / 2) * abs(h) * (1.0 if abs(r) < abs(h) else 0.0)
+        scale = 1e-9 * (1 + abs(Phi_float(c, r)) + bound)
+        ok &= -scale <= d2 <= bound + scale
+        worst = max(worst, (d2 - bound) / (1 + bound))
+    return ok, {'points_a': na, 'phi_RR_reduction': True, 'range': '[0, 1/16]', 'bound_4_4_points': 300}
+
+
+# ======================================================================================= C7: Lambda and h_{7/2}
+class Q3:
+    """a + b sqrt3 + c sqrt6 with rational a, b, c"""
+
+    def __init__(self, a=0, b=0, c=0):
+        self.v = (Fr(a), Fr(b), Fr(c))
+
+    def __add__(self, o):
+        return Q3(*(x + y for x, y in zip(self.v, o.v)))
+
+    def scale(self, k):
+        return Q3(*(k * x for x in self.v))
+
+
+def poly_from(coeffs):
+    """univariate (variable 0) polynomial from a coefficient list"""
+    r = P()
+    for n, c in enumerate(coeffs):
+        r = r + P({(n, 0, 0, 0): c})
+    return r
+
+
+def gauss_legendre(n):
+    xs, ws = [], []
+    for i in range(1, n + 1):
+        x = math.cos(math.pi * (i - 0.25) / (n + 0.5))
+        for _ in range(100):
+            p0, p1 = 1.0, x
+            for k in range(2, n + 1):
+                p0, p1 = p1, ((2 * k - 1) * x * p1 - (k - 1) * p0) / k
+            dp = n * (x * p1 - p0) / (x * x - 1)
+            dx = p1 / dp
+            x -= dx
+            if abs(dx) < 1e-16:
+                break
+        xs.append(x)
+        ws.append(2 / ((1 - x * x) * dp * dp))
+    return xs, ws
+
+
+def control_C7():
+    ok = True
+    tau = V0
+    P1 = lambda u: Fr(3, 2) * (1 - u) * (2 - 3 * u)
+    # F_- = S_- Qm tau^(-7/2)/945 with S_-^2 = 1 - 4tau/3:  tau^(9/2) S_- F_-' = [ (S^2)'/2 tau Q + S^2 (tau Q' - 7/2 Q) ]/945
+    Qm = poly_from([-810, 3051, -3711, 1444])
+    Qp = poly_from([810, 3051, 3711, 1444])
+    for sgn, Q, K in ((-1, Qm, Fr(1, 945)), (1, Qp, Fr(-1, 945))):
+        S2 = 1 + sgn * Fr(4, 3) * tau
+        lhs = K * (S2.diff(0) * Fr(1, 2) * tau * Q + S2 * (tau * Q.diff(0) - Fr(7, 2) * Q))
+        p1 = Fr(3, 2) * (1 - tau) * (2 - 3 * tau) if sgn == -1 else Fr(3, 2) * (1 + tau) * (2 + 3 * tau)
+        ok &= (lhs - p1 * S2).is_zero()
+    # exact assembly of Lambda in Q(sqrt3, sqrt6)
+    P0 = {0: Fr(11, 3), 1: Fr(-21, 2), 2: Fr(17, 2), 3: Fr(-4, 3)}
+    T2 = {0: Fr(20, 3), 1: Fr(-20), 2: Fr(52, 3)}
+    Imid = {0: Fr(2, 3), 1: Fr(-3), 2: Fr(4), 3: Fr(-4, 3)}           # (2t - 1)^2 (2 - t)/3
+    lin = {0: Fr(-2, 3), 1: Fr(1)}
+    sub = lambda a, b: {k: a.get(k, 0) - b.get(k, 0) for k in set(a) | set(b)}
+
+    def A_at(p, where):
+        tot = Q3()
+        for n, c in p.items():
+            e = Fr(n) - Fr(7, 2)
+            v = Q3(0, 0, Fr(2, 3) ** n * Fr(27, 16)) if where == '2/3' else Q3(1)
+            tot = tot + v.scale(c / e)
+        return tot
+
+    t23 = Fr(2, 3)
+    Fm_23 = Q3(0, 0, Fr(1, 3) * (1444 * t23 ** 3 - 3711 * t23 ** 2 + 3051 * t23 - 810) / 945 * Fr(27, 16))
+    Fp_inf = Q3(0, Fr(-2888, 2835))
+    Lam = (Fm_23 + Fp_inf + A_at(sub(P0, T2), '2/3') + A_at(sub(Imid, T2), '1') + A_at(sub(Imid, T2), '2/3').scale(-1)
+           + A_at(sub(lin, T2), '1').scale(-1))
+    claim = (Fr(128, 105), Fr(-2887 if MUT == 'M7' else -2888, 2835), Fr(-907, 2835))
+    ok &= Lam.v == claim
+    lam_f = float(Lam.v[0]) + float(Lam.v[1]) * math.sqrt(3) + float(Lam.v[2]) * math.sqrt(6)
+    # floating-point evaluation of (4.3): exact even series below tau0, Gauss-Legendre above
+    N = 60
+    sm = sqrt_series(Fr(-4, 3), N)
+    sp = sqrt_series(Fr(4, 3), N)
+    P1m = [Fr(3), Fr(-15, 2), Fr(9, 2)]                     # P1(tau)
+    P1p = [Fr(3), Fr(15, 2), Fr(9, 2)]                      # P1(-tau)
+    ev = [Fr(0)] * (N + 1)
+    ev[0] += -6
+    ev[2] += Fr(-53, 3)
+    for n in range(N + 1):
+        for i, c in enumerate(P1m):
+            if n - i >= 0:
+                ev[n] += c * sm[n - i]
+        for i, c in enumerate(P1p):
+            if n - i >= 0:
+                ev[n] += c * sp[n - i]
+    ok &= all(ev[n] == 0 for n in range(4)) and ev[4] == Fr(-14, 27) and ev[6] == Fr(-2, 27)
+    tau0 = 0.2
+    head = sum(float(ev[n]) * tau0 ** (n - 3.5) / (n - 3.5) for n in range(4, N + 1))
+
+    def Ifun(u):
+        if u <= 2.0 / 3.0:
+            S = math.sqrt(1 - 4 * u / 3)
+            return 11 / 3 - 21 * u / 2 + 17 * u * u / 2 - 4 * u ** 3 / 3 + 1.5 * (1 - u) * (2 - 3 * u) * S
+        if u <= 1.0:
+            return (2 * u - 1) ** 2 * (2 - u) / 3
+        return u - 2.0 / 3.0
+
+    def Ineg(u):                                           # I(-u, 0), u > 0
+        S = math.sqrt(1 + 4 * u / 3)
+        return 11 / 3 + 21 * u / 2 + 17 * u * u / 2 + 4 * u ** 3 / 3 + 1.5 * (1 + u) * (2 + 3 * u) * S
+
+    T2f = lambda u: 20 / 3 - 20 * u + 52 / 3 * u * u
+    f = lambda u: u ** -4.5 * (Ifun(u) - T2f(u) + Ineg(u) - T2f(-u))
+    xs, ws = gauss_legendre(40)
+    body = 0.0
+    for a, b in ((tau0, 0.4), (0.4, 2.0 / 3.0), (2.0 / 3.0, 1.0)):
+        body += sum(w * f(0.5 * (b - a) * x + 0.5 * (a + b)) for x, w in zip(xs, ws)) * 0.5 * (b - a)
+    # [1, inf): tau = 1/v^2, d tau = -2 v^-3 dv
+    body += sum(w * 2 * (0.5 * x + 0.5) ** -3 * f((0.5 * x + 0.5) ** -2) for x, w in zip(xs, ws)) * 0.5
+    lam_q = head + body
+    ok &= abs(lam_q - lam_f) < 1e-12
+    # h_{7/2}: (216/25) sqrt6 Lambda == (16/2625)(1728 sqrt6 - 4332 sqrt2 - 2721) exactly, in the basis (1, sqrt2, sqrt6)
+    a, b, c = Lam.v                                       # sqrt6*(a + b sqrt3 + c sqrt6) = 6c + 3b sqrt2 + a sqrt6
+    left = (Fr(216, 25) * 6 * c, Fr(216, 25) * 3 * b, Fr(216, 25) * a)
+    right = (Fr(16, 2625) * -2721, Fr(16, 2625) * -4332, Fr(16, 2625) * 1728)
+    ok &= left == right
+    h72 = 16 * math.gamma(2.25) * (1728 * math.sqrt(6) - 4332 * math.sqrt(2) - 2721) / (2625 * math.pi)
+    ok &= abs(h72 - (-10.144044022514828)) < 1e-12
+    return ok, {'Lambda': [str(x) for x in Lam.v], 'Lambda_float_12dp': round(lam_f, 12),
+                'quadrature_agrees_1e-12': abs(lam_q - lam_f) < 1e-12, 'h72_10dp': round(h72, 10),
+                'even_series_first_terms': [str(ev[4]), str(ev[6])]}
+
+
+# ======================================================================================= C8: Theorem B bookkeeping
+def control_C8():
+    ok = True
+    # Gaussian moments of N(0, 2): E[x^2] = 2, E[x^4] = 12, E[x^6] = 120
+    m = {2: Fr(2), 4: Fr(12), 6: Fr(120)}
+    ok &= m[6] == 15 * 2 ** 3 and m[4] == 3 * 2 ** 2
+    Eg6t2 = 144 * m[2] * m[2] if MUT != 'M8' else 575
+    ok &= Eg6t2 == 576
+    ok &= m[6] * Fr(20, 3) == 800 and Fr(52, 3) * Eg6t2 == 9984
+    ok &= Fr(9984, 800) == Fr(312, 25) and Fr(312, 25) - 12 == Fr(12, 25)
+    ok &= Fr(331776 * 6, 32) == 62208 and 576 ** 2 == 331776
+    ok &= 24 ** 3 * 2 == 27648 and Fr(27648, 3200) == Fr(216, 25)       # 24^(7/2) = 24^3 sqrt24 = 27648 sqrt6
+    # E|B|^q = 2^q Gamma((q+1)/2)/sqrt(pi) for N(0, 2): q = 2 -> 2, q = 4 -> 12 (Gamma(3/2) = sqrt(pi)/2, Gamma(5/2) = 3 sqrt(pi)/4)
+    ok &= Fr(2 ** 2, 2) == m[2] and Fr(2 ** 4 * 3, 4) == m[4]
+    # exponents: gamma = sqrt(k) g gives gamma^6 d gamma = k^(7/2); the error terms
+    ok &= Fr(6, 2) + Fr(1, 2) == Fr(7, 2) and Fr(7, 2) + Fr(1, 2) == 4
+    ok &= 2 + Fr(8, 3) == Fr(14, 3) and 2 + Fr(3, 2) + Fr(2, 3) == Fr(25, 6) and Fr(25, 6) > 4
+    # E|B|^(7/2) = 2^(7/2) Gamma(9/4)/sqrt(pi) for B ~ N(0, 2), against Gauss-Legendre (floating point)
+    xs, ws = gauss_legendre(40)
+    def quad(f, a, b):
+        return sum(w * f(0.5 * (b - a) * x + 0.5 * (a + b)) for x, w in zip(xs, ws)) * 0.5 * (b - a)
+    dens = lambda x: math.exp(-x * x / 4) / math.sqrt(4 * math.pi)
+    m72 = 2 * sum(quad(lambda x: x ** 3.5 * dens(x), a, b) for a, b in ((0, 1), (1, 4), (4, 10), (10, 20), (20, 40)))
+    ok &= abs(m72 - 2 ** 3.5 * math.gamma(2.25) / math.sqrt(math.pi)) < 1e-10
+    # the k^4 constants: 64512 = (7/27) 12^4 E[B^4]; int (p(w) - p(0)) w^-2 dw = -1/2; 32256; 53248; h4 = 728/25
+    ok &= Fr(7, 27) * 12 ** 4 * m[4] == 64512
+    pw = lambda w: (math.exp(-w * w / 4) - 1) / (w * w) / math.sqrt(4 * math.pi) if w > 1e-6 else -0.25 / math.sqrt(4 * math.pi)
+    ipw = 2 * (sum(quad(pw, a, b) for a, b in ((0, 1), (1, 4), (4, 10), (10, 30), (30, 100))) - 1 / (100 * math.sqrt(4 * math.pi)))
+    ok &= abs(ipw + 0.5) < 1e-10
+    A4 = Fr(64512, 2)
+    B4 = Fr(331776, 2) * Fr(13, 243) * 6
+    ok &= A4 == 32256 and B4 == 53248
+    h4 = (A4 + B4) / 800 + 72 - 12 * Fr(312, 25)
+    ok &= h4 == Fr(728, 25)
+    ok &= Fr(7, 2) + 1 == Fr(9, 2)
+    return ok, {'E_gamma6': '120', 'E_gamma6_t2': '576 k^2', 'H_k2': '12/25', 'E_absB_7/2_quadrature': True,
+                'k4_constants': ['32256', '53248'], 'h4': str(h4), 'h72_constant': '(216/25) sqrt6 Gamma(9/4) Lambda / pi'}
+
+
+# ======================================================================================= C9: fixed points
+def control_C9():
+    ok = True
+    res = []
+    # #242's exact (D') witness (phi, beta, chi) = (3/2, 8/3, 20/3)
+    phi, beta, chi = Fr(3, 2), Fr(8, 3), Fr(20, 3)
+    t, x0 = beta / (2 * phi), chi / phi ** 2
+    psi, cp, R = 1 / phi, 1 - t, x0 + 8 - 12 * t
+    w = elder_test(psi, cp, R)
+    ok &= w == (MUT != 'M9')
+    res.append(['witness', [str(phi), str(beta), str(chi)], [str(t), str(x0)], w])
+    # (0, 0): psi_e = 3, I = 20/3
+    ok &= g_of(Fr(3), Fr(1)) == 64 == (0 + 8 - 0) ** 2
+    d = Fr(3) - 1
+    ok &= 1 * d * d + d ** 3 / 3 == Fr(20, 3)
+    # #242 control S8 (floating point, its 16 cases)
+    cases = [((0.30, 0.0, 0.0), 1), ((0.36, 0.0, 0.0), 0), ((0.3333, 0.0, 0.0), 1), ((0.3334, 0.0, 0.0), 0),
+             ((0.95, 0.0, 0.0), 0), ((0.5, 2.2, 0.0), 0), ((0.04, 0.09, 0.002), 1),
+             ((0.30, 0.0, 3.0), 0), ((0.20, 0.0, 1.0), 0), ((0.20, 0.0, 0.5), 1), ((0.05, 0.0, 0.5), 1),
+             ((0.05, 0.0, 0.85), 0), ((0.03, -0.1, 0.0), 1),
+             ((0.2401, 2.1425, 0.5536), 1), ((0.6267, 2.3645, 2.8796), 1), ((0.5, 2.2, 0.01), 0)]
+    agree = 0
+    at_origin = 0
+    for (ph, be, ch), e in cases:
+        tt, xx = be / (2 * ph), ch / ph ** 2
+        dec = int(elder_test(1 / ph, 1 - tt, xx + 8 - 12 * tt))
+        agree += dec == e
+        at_origin += (be == 0.0 and ch == 0.0)          # (t, chi0) = (0, 0) lies on Delta: Remark 2, not Theorem A
+    ok &= agree == len(cases)
+    # section 5 examples: t = 9.005434, chi0 = 193.926947
+    tt, xx = 9.005434, 193.926947
+    ex = [(0.1112, 1), (0.1124, 1), (0.1126, 0), (0.113, 0)]
+    ex_ok = all(int(elder_test(1 / ph, 1 - tt, xx + 8 - 12 * tt)) == e for ph, e in ex)
+    # example 2 (a table node): Theorem A's edge 0.0871797..., the scanner's 0.0871798 (falsely accepted there)
+    tt, xx = 11.464348642908552, -0.426511285632118
+    edge = 1 / psi_e_bisect(1 - tt, xx + 8 - 12 * tt)
+    ex2 = [(0.08717970, 1), (0.08717976, 0), (0.0871798, 0)]
+    ex_ok &= abs(edge - 0.0871797) < 1e-7 and all(int(elder_test(1 / ph, 1 - tt, xx + 8 - 12 * tt)) == e for ph, e in ex2)
+    ok &= ex_ok
+    return ok, {'witness_elder': w, 'S8_agree': agree, 'S8_cases': len(cases), 'S8_at_origin_on_Delta': at_origin,
+                'section5_examples': ex_ok}
+
+
+def main(argv):
+    global MUT
+    if len(argv) == 2 and argv[0] == '--mutant':
+        if argv[1] not in MUTANTS:
+            print('unknown mutant label', file=sys.stderr)
+            return 2
+        MUT = argv[1]
+    elif argv:
+        print('usage: closed_form_check.py [--mutant M1..M9]', file=sys.stderr)
+        return 2
+    out = {}
+    controls = {}
+    for name, fn in (('C1_lemma1_identification', control_C1), ('C2_theorem_A', control_C2),
+                     ('C3_corollary_A1_chi0_zero', control_C3), ('C4_corollary_A2', control_C4),
+                     ('C5_corollary_A4', control_C5), ('C6_lemma_B2_Phi', control_C6),
+                     ('C7_lemma_B1_Lambda_h72', control_C7), ('C8_theorem_B_bookkeeping', control_C8),
+                     ('C9_fixed_points', control_C9)):
+        ok, detail = fn()
+        controls[name] = bool(ok)
+        out[name.split('_')[0]] = detail
+    res = {'object': 'CL-SOFT-CLOSED-FORM-20261002-v1.2', 'scientific_effect': 'NONE', 'controls': controls}
+    res.update(out)
+    ok = all(controls.values())
+    if MUT is None:
+        print(json.dumps(res, indent=1, sort_keys=True))
+    else:
+        print('mutant ' + MUT + ': failing controls ' + ', '.join(sorted(k for k, v in controls.items() if not v)),
+              file=sys.stderr)
+    return 0 if ok else 1
+
+
+if __name__ == '__main__':
+    sys.exit(main(sys.argv[1:]))