What a cascade is, with real examples

30 September 2026 · Draft by Claude-1 for Joe, from work with Codex-4, Codex-6 and Claude-17

Why this post exists

On 29 and 30 September the War Machine ran twenty clicks in which the set of policies it chose among had one member. The Lean model did not object, because its definition of the policy set, cascadePolicySet (menu : List …), takes the list as an argument that nothing has to produce. Every theorem about it holds for any list, including a list of one. Joe’s word for that argument was a backdoor.

Since then a replacement has been built in pieces: read the target’s text, form cascades from the reading and from the pattern graph, score them. Along the way a question came up about pooling cascades that share a first step. Joe’s answer was that the question is premature until we can see what these cascades are, what they do and what their specification is. This post is the attempt to show that, using the seven missions for which a reading exists.

Working definitions

These are the definitions the code implements today, in plain words. A Lean version, in which the policy set can only be obtained from the construction, is reported in the next section.

What a cascade does

Selection scores each policy by imagining it carried out. The imagined execution goes in rounds. In each round, every unit whose predecessors are all done is attempted, and each attempt succeeds with that pattern’s success probability. So the arrangement decides what can happen when: a chain of three units needs at least three rounds, while three units with no ordering between them can all finish in the first. With success probability one half, three unordered units are all done after one round with probability 1/8; a chain of three, with probability 0. Codex-6 has proved these two figures in Lean for the three-unit case.

In the drawings below, each row is the earliest round in which a unit can be attempted, and roots are shaded green. Black arrows are precedes; blue dashed lines are overlap. On retractions each arrow is labelled with the kind of graph relation it came from.

Two numbers are then computed for each policy:

• F, fit to the present. How well the reading supports the cascade’s patterns for this text: a pattern 象 cited for the text is given probability 0.9 of fitting, one it rejected 0.1, one never read against the text 0.5, and F is the average surprisal of those, plus a term for how many fragments the cascade covers. The three probabilities are stated preliminary values, not measurements. Connector patterns added by a retraction were never read against the text, which is why retractions have a higher (worse) F.
• G, expected free energy. Risk plus ambiguity minus expected information gain, over the imagined rounds. Risk measures how far the imagined progress falls from what is preferred; the preference used at the moment is simply “more units done is better, and the last units done is better still”.

Lower is better for both. The selection law combines them with habit: probability proportional to exp(log E − F − γ·G).

The definitions in Lean

Codex-6 wrote three Lean files on 30 September, in mathlib4/DarkTower/WarMachine/: CascadeSpec.lean (the definitions), CascadeSpecControls.lean (attempts that must fail) and CascadeSpecExamples.lean (one real policy set, generated by a script). They build with no sorry. The definitions went through five revisions in the day, each prompted by a review or by trying a real example. Claude-1 read the definitions, the retraction contract and the controls at an intermediate revision, and the final unit and cascade structures and the header and theorem list of the generated example; the intermediate diffs of the last three revisions, and the proofs, were not read line by line, and the builds were not re-run by Claude-1.

Proved: every member is a valid cascade; members have pairwise distinct structural identities; every member contains a pattern the reading cites; an empty reading gives an empty policy set; the number of members is at most the number of alternatives cascades plus the number of overlap cascades plus k; with k = 0 the policy set is exactly the deduplicated reading cascades.

Controls that fail as they should: calling the policy-set constructor by name or with structure notation from outside the module; giving a reading a list of cascades; a cascade with a cycle, with a label outside the library, or with a unit overlapping itself; proving that a graph edge with no authored direction justifies an arrow.

One real policy set, checked. A script (futon2/scripts/wm_policy_set_to_lean.py) writes the M-distributed-proofreaders example from this page’s data into Lean: the eight fragments with their three citations, the eight graph edges its retractions use, and the three retractions as explicit five-unit cascades. Lean then establishes:

• the reading yields one cascade in each mode, each of three units and two ordering edges, and they are one structure;
• each retraction contains every cited pattern that has an edge in the graph, and every one of its overlaps comes from a graph edge with no authored direction;
• the policy set has four members: the reading cascade and three distinct retractions, as the code reports.

Three planted errors make the build fail, as they should: deleting a citation from the data; turning a retraction’s overlap into an arrow while its graph edge has no authored direction; adding a unit whose pattern is outside the library. Two of the theorems (the two counts after duplicates are removed) are checked by compiled evaluation, native_decide, which rests on an additional soundness axiom of the Lean compiler; the rest use only the standard axioms. The exported data has no edge weights, so the generated graph gives every edge weight 1; no theorem here depends on weight.

What trying the real example found. Three defects in the definitions, none of which a fixture had shown: the first version let a reading carry its own list of cascades, which was the old free list one level down; the second could not express a retraction at all, because it required every unit to have a fragment; the third removed duplicates by comparing more than the code compares. And one fact about the code: its “reported” cascade counts are inflated by annotations (see below).

What the Lean does not say. The retraction computation itself is not defined; it enters as a named function under the contract above, sourced to pattern_retraction.clj, and the example checks three of its outputs against that contract, not the computation. Nothing requires a policy set to have more than one member; a run whose policy sets are degenerate is caught by the run-facts check and the alert, not by this module. Nothing says the fragments are the operator’s own words. And none of this is connected to selection: G, F and the choice among policies are specified elsewhere and still refer to the old definition.

Examples

Seven policy sets were produced by the same code from the same pinned graph. Six are from real text: three are shown in full and three are folded. The seventh is not a valid example and is set apart below.

M-distributed-proofreaders

A short HEAD in the operator’s voice. 象 cited three patterns across its fragments, giving one reading cascade, and the graph gives three retractions around them. This is the policy set that has been written out in Lean and checked against the definitions: four members.

Source: futon6/holes/missions/M-distributed-proofreaders.md, head-section, 586 characters.

## HEAD

The "killer idea" (golden-walk-ledger.md §THE KILLER IDEA), made operational:
mine the math corpus **structure-first** — concepts are the index, papers are
occurrence sites — and run a **Distributed-Proofreaders** loop over it:
mine → measure loss → fix the worst class → re-mine, anytime, never perfect.
Named for the volunteer book-digitisation model: systematic per-type passes,
each pass clearing one defect class, quality a property of the revision
process rather than any single snapshot (the Moran-1971 *because*-clause
lesson, futon5a/essays/moran-1971-agent-cascades).

Policy set: 4 structurally distinct policies (15 reported before duplicates are removed; see the note on reported counts below). Counted failures: none.

Policy 1: read from the text, one pattern per fragment

3 units over 3 distinct patterns; 2 precedes edges (black arrows); 0 overlap relations (blue dashed); 1 root.

Policy 2: cut from the pattern graph around the reading’s patterns

5 units over 5 distinct patterns; 0 precedes edges (black arrows); 4 overlap relations (blue dashed); 5 roots.

Policy 3: cut from the pattern graph around the reading’s patterns

5 units over 5 distinct patterns; 0 precedes edges (black arrows); 4 overlap relations (blue dashed); 5 roots.

Policy 4: cut from the pattern graph around the reading’s patterns

5 units over 5 distinct patterns; 0 precedes edges (black arrows); 4 overlap relations (blue dashed); 5 roots.

M-essays-diachronic-model

A short opening paragraph. One of the two cited patterns has no edges in the pattern graph, so it cannot seed a retraction; the retraction that remains is a single pattern.

Source: futon4/holes/missions/M-essays-diachronic-model.md, opening-before-first-section, 317 characters.

# Mission: Essays Diachronic Model — Golden/Live Dataset Discipline and XTDB Lifecycle Semantics

**Date:** 2026-05-14
**Status:** OPEN — specified; implementation not yet started (previous status: specified, implementation pending)
**Parent mission:** `M-essays-edit-cycle.md`
**Owner:** futon4 / WebArxana / futon1a

Policy set: 2 structurally distinct policies (9 reported before duplicates are removed; see the note on reported counts below). Counted failures: isolated-seed (sidecar/fact-lifecycle-event-types).

Policy 1: read from the text, one pattern per fragment

2 units over 2 distinct patterns; 1 precedes edge (black arrows); 0 overlap relations (blue dashed); 1 root.

Policy 2: cut from the pattern graph around the reading’s patterns

1 units over 1 distinct patterns; 0 precedes edges (black arrows); 0 overlap relations (blue dashed); 1 root.

M-self-documenting-stack

A longer opening. This is the target the joint run chose on 30 September, through its three retractions. Look at how the three differ.

Source: futon7/holes/M-self-documenting-stack.md, opening-before-first-section, 2078 characters.

# Mission: M-self-documenting-stack

> **Naming history (Joe 2026-05-20)**: started life narrowly as `M-autonomous-doc-maintenance` (single-axis: doc-freshness). IDENTIFY-time mission survey revealed a parallel gap — *mission discoverability* — that the same apparatus naturally serves; both are aspects of the same broader goal ("I want the futon stack to be *deeply* self-documenting"). File renamed to `M-self-documenting-stack` to reflect the actual scope. POC scope (LC1 only) ratified by Joe same-day; Deliverables A + B and the chain-link applications #3-#7 are explicit follow-on missions, not extensions of this one.

**Status:** OPEN — INSTANTIATE (recovery pass 2026-05-21). **POC scope: LC1 (Deliverable C — mission-discoverability surface) only.** LC1 code/tests/build are now recovered after review; manual browser walk-through + DOCUMENT pass remain before closure. A + B + chain-link applications #3-#7 are follow-on missions inheriting this mission's shape-naming + protocol-family framing.
**Owner:** codex-5 (LC1 recovery + closure pass 2026-05-21); claude-2 (framing-author; original LC1 author)
**Co-owners (for follow-ons, not this POC):** claude-4 (VSATARCS-side; peripheral wrapping when A becomes a follow-on); claude-1 or claude-13 (futon3c-side; peripheral-spec compliance for A); WM-side ownership for B
**Driver:** Joe (operator; framing-extender; POC-close-decider)
**Authors:** claude-2 IDENTIFY draft 2026-05-20, following M-vsatarcs-writer Option B live cycle which proved the per-cycle apparatus works but exposed the gap to autonomy. Joe-driven extension same-day to absorb mission-discoverability per his felt need ("a search box where I could start typing 'self documenting stack' and get a summary of the relevant missions"). Joe scoping decision 2026-05-20: ship LC1 as POC; follow-on missions inherit the framing; mission closes as POC when LC1 ready. codex-5 recovery pass 2026-05-21 after external review surfaced LC1 blockers/gaps (broken embedding helper, missing warm corpus, per-request JVM shell-out, missing D11/D12/DL1 closures).

Policy set: 4 structurally distinct policies (5 reported before duplicates are removed; see the note on reported counts below). Counted failures: isolated-seed (coordination/intent-to-mission-binding).

Policy 1: read from the text, one pattern per fragment

9 units over 5 distinct patterns; 8 precedes edges (black arrows); 0 overlap relations (blue dashed); 1 root.

Policy 2: cut from the pattern graph around the reading’s patterns

5 units over 5 distinct patterns; 0 precedes edges (black arrows); 4 overlap relations (blue dashed); 5 roots.

Policy 3: cut from the pattern graph around the reading’s patterns

5 units over 5 distinct patterns; 0 precedes edges (black arrows); 4 overlap relations (blue dashed); 5 roots.

Policy 4: cut from the pattern graph around the reading’s patterns

5 units over 5 distinct patterns; 0 precedes edges (black arrows); 4 overlap relations (blue dashed); 5 roots.

The other three

# M-value-creation-loop — the prospective pattern cascade as build strategy

**Date:** 2026-06-16
**Status:** OPEN — IDENTIFY (minted from a live design conversation, Joe + claude-2,
in the session that built kit-intake / kit-outbox / mint 3-state consumption).
**Name:** provisional — Joe's to set (candidates: M-value-creation-loop /
M-prospective-cascade / M-generative-build-cascade).
**Owner:** TBD (Joe's call). Drafted by claude-2.

## HEAD

- **Operator-voice anchor (Joe, 2026-06-22):** *"If we do one paper end-to-end we should
  already have metrics, and those metrics should improve if we do 10 papers end to end.
  If they are not improving then we should be able to pinpoint why."* The point is **not**
  "100 papers completed."
- **What's already felt to be true:** Phase 2 is cross-paper/holistic, so the substrate
  should *compound* — a held-out paper grounds better as the corpus grows. The
  comprehension floor is already corpus-relative; G-coverage was designed to rise with
  corpus-fraction. The progress signal is a **slope**, and it should already be latent at
  n=1.
- **Anti-glibness discipline:** throughput is not progress. A pile of graphs, or "N
  papers done," hides whether the holistic claim is real. Every headline number must be
  defined at n=1, expected to rise n=1→10, and **decomposed per stage** so a flat curve
  names the culprit. A flat/falling metric is a *finding to pinpoint*, never something to
  paper over with volume (the mark5 lesson, generalized).
- **Working-economy position:** this mission **underwrites the superpod scale decision** —
  we only pay for archive-scale once the small run shows the slope is real and diagnosable.
  It is underwritten by the corrected full-pipeline contract + the already-built stages.
- **Carried-forward tensions:** (i) the S7 macro-collapse cause is still open — paper-level
  lens vs fixed-vs-data-driven vocab (mark5 D1, Diagnostic 1); (ii) the **S4 expository
  GPU run has never been exercised**; (iii) the **S6 paper-graph(B) assembler is unbuilt**;
  (iv) the embedding/macro-vocab rework is **deferred** (separate work, not this mission).
- **Provenance:** this conversation (2026-06-22→23), as the post-mortem of mark5. Intake =
  operator principle stated after reviewing the readiness docs + the mark5 results.

**Exit criterion (HEAD):** Joe recognises this as the faithful shape of "what we need next
time"; the four tensions are named, not buried.

---

# Mission: M-war-machine-aif-completion

<!-- engine: structural header, AI-written -->
**Date:** 2026-05-17
**Status:** OPEN — exit criterion #2 satisfied; HEAD-as-escrow scaffold (claude-1, PM pass for the futon-stack-as-Hyperreal-business mission cluster); awaiting Joe verbatims via simulated `eoi-engine` `eoi-inward-mission` flash. **Exit criterion source:** §0 of `~/code/futon7/holes/M-descriptive-essay-of-the-stack.md`, criterion #2.
**Bar (lifted verbatim from §0):** *"War Machine ≥ ukrn-services-simulation coherence — concretely: ~12 clojure notebooks (substrate + dynamics + engagement on v2 side; belief + kernel + forward model + EFE + trace on v3 side); test harness with regression baselines; figure-rendering pipeline; R1-R12 (or F1-F10) completeness contract satisfied. Today's War Machine is `:π-display`-only — a reading surface, no belief state, no predictive forward model, no EFE-scored action ranking. The gap is substantial — weeks of work, not hours."*
**Timebox:** estimated 3-4 weeks; final cap is Joe's call at §1.5 verbatim authoring.
**Owner:** Joe (futon7); engineering ownership undefined pending Q-CL1 (see §3.1).
**Sequencing role:** Sibling to `M-stack-essay` and `M-stack-essay-code-alignment` in the mission cluster; predecessor for `M-stack-morphogenetic-rewrite`. **Hard predecessor:** none in the cluster; outside the cluster, depends on `M-interim-director`'s arm-G work (substrate-2 already operational) and on Arms A/B/F producing live data the forward model can train on / score against.
**Cross-ref:**
- `~/code/ukrn-services-simulation/README.md` + `notebooks/ukrn_v3_*.clj` — the predecessor exemplar; the bar this mission graduates the War Machine to
- `~/code/ukrn-services-simulation/docs/aif-completeness.md` — R1-R12 contract; companion to F1-F10 below
- `~/code/futon0/docs/stack-fitness-completeness.md` — F1-F10 stack-fitness contract; the homeostat analogue of R1-R12
- `~/code/futon7/holes/M-interim-director-proxy-metric-inventory.md` §2.5 (math trajectory L1-L5), §2.6 (stack-fitness trajectory L1-L5) — these levels are this mission's *sub-deliverable map*
- `~/code/futon2/scripts/futon2/report/war_machine.clj` — current War Machine surface (2850 lines, single namespace `futon2.report.war-machine`). 13 `scan-*` projection functions; AIF observer at lines 1803–2060 (`observation-channels`, `observe`, `sense->vector`, `preferences`, `avoided-states`, `mode-prior`, `pragmatic-weights`, `compute-free-energy`, `infer-mode`); plus `evaluate-mark2-batches`, `scan-aif-heads`, `load-invariant-inventory`, `enrich-support-attack`, `judge`. **Precision on the §0 Bar quote:** "no belief state" understates current state — there is a mode-prior + mode-inference observer. The accurate baseline is: **`:π-display`-only at the policy/action layer** (no forward model `(state, action) → predicted-state`, no EFE-scored action ranking); a mode-inference observer already exists. The completion gap is forward-model + action-space + EFE-scored policy ranking + test harness + regression fixtures, not "AIF substrate from scratch."
- `~/code/futon3c/src/futon3c/portfolio/observe.clj` — 16-channel portfolio surface
- `~/code/futon3/holes/war-bulletin-9.md` — strategic context (WR-16: operationalised exploit-loops as observation channels)
- `~/code/futon4/README-rewriting.md` — typed-rewrite discipline; the WM's belief updates are operadic-by-construction (Q-SA3)

**Authors:** Joe (verbatim answers, pending); claude-1 (engine-side ordering and minimal structural connective tissue, 2026-05-17 PM scaffold).

A reading of something that is not a HEAD

Joe pointed this one out. The HEAD section of M-web-arxana-ui-improvements contains only the sentence “The mission’s live operator-shape, captured before IDENTIFY hardens it into a tractable gap statement.” That is the template’s definition of what a HEAD is; the mission has no HEAD. The request script took the section at face value, 象 cited two patterns for the definition, and the construction produced six policies from it. In the joint run of 30 September one of those six was the best-scoring single policy of all 27. The correct outcome for this target is a counted failure and an empty policy set, and since futon2 891f5601f that is what happens: the request script refuses the section without falling back to the rest of the file, the registry refuses to publish a reading of it, and the target is counted under its own failure key. It is the only mission file found with this shape. The fragments 象 cited are kept below for the record; the policy set is now empty.

## HEAD

*The mission's live operator-shape, captured before IDENTIFY hardens it into a tractable gap statement.*

What the examples show that is wrong or unsettled

1. Most retractions are unordered bags. The pattern graph is undirected except where a pattern’s own text names another. Until 30 September the scorer turned every graph edge into an arrow pointing from the alphabetically earlier pattern name to the later one; that is fixed (futon2 3a247262a): an edge with an authored direction keeps it and every other graph edge is an overlap. In the 16 retractions here, 22 of 98 edges have an authored direction. The consequence is visible in the drawings: most retractions now have no ordering at all, every unit is a root, and the imagined execution attempts all of them in the first round. G rewards that. A five-pattern bag scores 0.89 to 1.04 where the chain read from the same text scores 1.66 to 2.05. Whether five patterns can really be applied at once, and so whether this is what a cascade should be allowed to be, is not settled by anything in the model.
2. “Cited in the next turn” is treated as having no direction. Many graph edges are of kind next-in-session: one pattern was cited in a turn and the other in the following turn. That relation has an order in the evidence, but the graph stores it as undirected, so it becomes an overlap.
3. Wide cascades cannot be scored. The exact scorer enumerates every subset of the units attemptable in a round, so its cost doubles with each additional one: measured at 0.4 seconds for five, 1.6 for nine, 2.9 for ten. The three M-war-machine-aif-completion retractions allow 13 or more at once and exhausted memory. Since futon2 86822f367 an arrangement wider than nine is refused before any enumeration and counted as a failure; nothing approximate is substituted. So at present the machine cannot consider a wide cascade at all.
4. Retractions of one seed set are near-copies. For M-self-documenting-stack the three retractions differ by one connector. Claude-17 measured that asking for 6 or 10 gives 6 or 10, all at nearly the same cost, with no sign of settling. So k decides how many near-copies a target gets, and k has no stated source.
5. Most of these readings are not of a HEAD at all. When a mission file has no HEAD section, the request script reads whatever comes before the first section heading: usually a title, a status line and some framing, of unknown authorship. Of the six readings here, M-distributed-proofreaders and M-metric-harness are of a real HEAD; M-essays-diachronic-model, M-self-documenting-stack, M-war-machine-aif-completion and M-value-creation-loop are of the file’s opening. Of 199 mission targets with a file, 15 have a HEAD with content, and none of the 55 tickets does. Joe’s proposal, now being piloted, is to recover HEADs from his own recorded words in the Evidence Landscape: over the first 20 missions tried, 7 have his words commissioning the mission at or before its creation, 9 have his words about it from later, and 4 have none.
6. A definition of a HEAD was read as a HEAD. See M-web-arxana-ui-improvements above. Nothing between the mission file and the policy set checks that the text read is the operator’s own statement. The Lean definition of a reading does not require it either.
7. The “reported” counts are inflated by annotations. For each fragment where 象 also recorded patterns it rejected, the code emits the same cascade once more per rejected pattern, labelled with which one it was preferred over. The rejected pattern never enters the cascade. M-distributed-proofreaders reports twelve reading cascades; they are one structure. The Lean construction, which knows only citations, computes two (one per mode) and the same single structure after duplicates are removed. So the rejected patterns, which are the reading’s own record of what did not fit, currently change nothing about the policies.
8. Every success probability is one half, because no pattern has recorded trials. Expected information gain is therefore the same (0.31) for every policy, and habit is neutral for every policy. Differences in G come from risk and ambiguity only.
9. The preference is synthetic. “More units done is better” was written for this scorer. It is not the preference from Joe’s ruling of 22 September that the real decision scores with, nor the one derived from mission wants that the real decision records without scoring. Which of the three should score cascades is an open question for Joe.
10. Coverage. Seven readings exist. The field has 288 targets; 192 missions with a file have no reading, and 89 targets (tickets, proposals) have no file the machine knows of.
11. Not in the formal model yet. Until the Lean definitions above are complete and the real decision is changed to call the construction, the old free-list definition is still the one the running machine answers to.

Where things are

Code (futon2, all unloaded): analysis_cascade.clj, pattern_retraction.clj, target_policy_family.clj, cascade_shape_g.clj, wm/family_selection.clj. Lean (mathlib4): DarkTower/WarMachine/HeadCascadeG.lean, Proof2/CascadePolicySet.lean (the old definition). Readings: futon2/holes/labs/wm-contract/mission-head-cascades-2026-09-30/. Incident: futon2/holes/labs/wm-contract/incidents/INCIDENT-2026-09-30-one-policy-selection-repeated-refusal.md. Claude-17’s wiring check and the k measurement: futon3c/holes/excursions/E-象-spec-wiring.md.