First authored design, 2026-09-15. This elaborates exactly WM-10. It is a reviewable design, not implementation, independent acceptance or machine completion. The existing build loop continues under claude-2; these documents do not dispatch new jobs or override recorded decisions.
All WM cascades · Checklist item · Machine-readable cascade
WM-10 must compute canonical expected free energy from the actual cascade-induced predictive joint and feed its result to choice. Neither an action/channel controller score nor an arbitrary Lean score supplies that connection. The retained canonical mathematics is conditional on its model inputs; supplying those inputs and demonstrating runtime correspondence remain necessary.
WM-10 — G evaluates whole interpreted cascades using the AIF law. OPEN: runtime implementation of this definition, independent numeric correspondence, complete real candidate family, compatible C/model, and a selection that actually consumes these scores. Receipt construction explicitly emits :cascade-g-not-computed. This is the existing worklist F13 obligation (mapped here, not retired or renumbered in the worklist). Action/channel Gaussian controller scores do not discharge this. [T,S,L] Built evidence: mathlib4 79ac55d5d0 (CascadeEFE.lean) and 2b22eeef31 (CascadeEFEPolicies.lean, rewritten GOverCascades.lean) define finite guarded transitions, horizon predictions, risk+conditional ambiguity, equivalent information-gain expression, and composition-sensitive controls. Old arbitrary Lean score is replaced by a canonical alias. Earlier audit L predates these repairs; use their own build/axiom receipts, not that older audit as proof of acceptance.
The preceding evidence is the checklist’s dated account. It has not been re-audited as a current deployment census for this design.
Pattern: wm-pattern-design/separate-design-from-use.
Bind problem, current partial construction, proposed extension, full interpreted policy and model context. Construction index k is not observation time or horizon T. Output a per-problem comparison request; a fixed authored list across all problems does not satisfy progressive construction.
Pattern: wm-pattern-design/composition-changes-the-problem.
Use WM-02 belief, WM-03 dynamics and WM-04 observation A through WM-05, preserving guards, history, overlap and order. Retain q, J and Q for each scored observation. Joint prediction must change because interpreted effects change, not because an edge label receives an arbitrary bonus.
Pattern: wm-pattern-design/partial-design-without-imaginary-completion.
Supply prediction semantics for empty and partial constructions including unfinished target outcomes. Do not borrow the completed successor’s effects, set missing terms to zero or reject solely because construction is incomplete. Missing essential inputs are typed gaps whose producers must be built; refusal is not fulfillment of partial-design scoring.
Pattern: wm-prediction/probability-laws-with-runtime-meaning.
Under the finite categorical contract, G at each observation is KL(Q || C) plus expected conditional observation entropy under q; total G sums over the declared common schedule. Derive the equivalent preference cross-entropy minus state mutual information from the same J. It is not KL risk minus information gain. Preserve positive-Q/zero-C inadmissibility and numeric correspondence.
Pattern: wm-pattern-design/same-policy-through-comparison.
For a legal proposal and its parent in the same context, calculate delta G from the actual scores. Under the current Stage-0 rule, admit the extension iff delta G is strictly negative. Equal or worse proposals do not become admissible through a nonzero-temperature draw. Retain the searched candidate family and limits; local stopping does not establish global optimality or task success.
Pattern: wm-connected-learning/observation-to-next-choice.
Connect the canonical result to the actual choice consumer with policy, model and schedule identities. Retain failed/inadmissible candidates rather than silently shrinking coverage. A logged G alongside a controller score is not G-based choice. WM-11 owns the declared choice law over the applicable admitted alternatives.
These are design input/constraint relationships; they do not assert automatic runtime firing. Each contribution constrains the next actual artifact.
| From | To | Relationship | Why |
|---|---|---|---|
| WM-10-C1 | WM-10-C2 | prerequisite | Prediction must concern the complete compared policy. |
| WM-10-C1 | WM-10-C3 | prerequisite | The parent and extension are partial construction states. |
| WM-10-C2 | WM-10-C4 | prerequisite | G is derived from this joint, not supplied as an assumption. |
| WM-10-C3 | WM-10-C4 | prerequisite | Unfinished outcomes must enter the same calculation. |
| WM-10-C4 | WM-10-C5 | prerequisite | Extension admission depends on computed delta G. |
| WM-10-C5 | WM-10-C6 | prerequisite | The choice consumer must honor the admission decision. |
| WM-10-C6 | WM-10-C1 | revision-feedback | The actual choice may expose an incomplete candidate or comparison context. |
Comparison resolver → problem/parent/delta and common context. Joint producer → per-step q/J/Q with A/B/C provenance. Canonical scorer → risk, ambiguity, total and numeric receipt. Extension gate → legality plus strict delta test. Choice adapter → actual consumer evidence. Keep invalid-model refusal separate from a legitimate worse score.
Each envelope must retain its schema, content identity, source/model revisions, task/occurrence and information boundary. Typed missing inputs remain missing; do not replace them with success-shaped defaults. Implementers may reuse existing compatible components, but must identify the real producer and consumer before crediting integration.
Evidence gathering alone may leave the handoff unusable; revising the handoff alone may transmit an unsupported claim. Their composition can change predicted resumption outcomes. A proposed extension that only duplicates the same record need not improve G. The model must produce these distinctions, rather than assign a better score because two pattern titles sound complementary.
This situation is illustrative, not a measured production result or an adopted probability table.
Distinguishing controls: Independently recompute a finite canonical example and its decomposition. Compare same-pattern different-order interactions, no-interaction under stated assumptions, non-firing versus progress, and initial/intermediate/complete designs. Reject arbitrary scores, copied final scores, unequal observation opportunities and worse-extension softmax acceptance. Use real adapter inputs for production correspondence; fixtures remain mathematics/mechanics evidence.
Do not rerun the entire machine merely to validate a local edit. Select checks for the changed invariant; retain commits, commands and results. A future qualifying run still requires every required node and connection.
WM-01 · WM-02 · WM-03 · WM-04 · WM-05 · WM-06 · WM-08 · WM-09 · WM-11 · WM-12 · WM-13 · WM-14
Open: production joint inputs, numeric correspondence and justified schedule; unresolved fuel/yield/episode proposals remain separate. The current semantics supersedes the old global A/B formula-choice framing. Metadata-only attestation twins with identical model inputs have identical G; do not promise a strict ordering without a justified model change.
The dependency links express interface constraints, not a topological build order. A producer and consumer can jointly constrain an interface without requiring that all other implementations be finished first. Use a bounded packet once its relevant semantics are settled.
The companion JSON pins the governing checklist, September rulings, current cascade-policy semantics and every applied pattern. Where the semantics source distinguishes a ruling, extrapolation or open proposal, that distinction controls. No generic finite witness is promoted to a machine instance. Existing patterns are reused within the application stated above; their other examples, thresholds and historical implementation claims are not automatically adopted.