WM-01: make the shared probability carriers mean the same thing

Authored build-design cascade, 2026-09-15. Exactly WM-01. The governing item requires sound shared probability/model carriers, dependent proofs and admitted witnesses bound to the repaired source, independent repair acceptance, and consistent State/Action/Outcome, model revision and numeric semantics. This document designs that work. It neither repeats the repair nor claims it has received independent acceptance.

What can go wrong even when a table sums to one?

A list containing the same outcome twice can make a sum count its probability twice. A function can assign mass to outcomes outside the support that the consumer sums. A runtime vector can use the wrong outcome ordering. A float row can pass an admission tolerance while failing exact normalization. A proof can concern yesterday's definitions while a receipt points to today's filename.

These are different failures. A valid normalization theorem does not fix a changed subject, and a content hash does not make a malformed distribution valid. WM-01 must connect mathematical laws, numeric representation, exact model identities and evidence of their actual use.

The checklist credits repair commit 480a666ad2 with duplicate-free support, zero mass outside support and nonnegative precision, with author-reported build and negative controls. Its independent acceptance receipt remains unsupplied in that checklist. This design inspected the current carrier and rejection-control source; it did not rerun Lean or inspect a new acceptance receipt. Historical credit remains bounded to its snapshot.

Eight pattern applications

K1 — Name the object and its conditioning

Pattern: aif/declare-the-conditioning.

Inventory each carrier by its input and output domains, not by the name “probability.” A transition kernel is conditioned on state and action; a predictive outcome kernel is conditioned on policy; a parameter posterior and policy prior are other objects. Record the State, Action, Policy, Outcome and model identities required by each consumer, including vertex tags, support order, revision and numerical representation.

Output: the common carrier/consumer contract. Equal vector lengths do not establish equal domains. A policy vector cannot replace an outcome distribution, and a scalar normalizer named B is not the controlled transition B. Joint-state meaning remains WM-02 work, interpretation WM-03 work and observed likelihood authority WM-04 work; their interfaces must still agree here.

K2 — Explain domain meaning before adapting a representation

Pattern: wm-prediction/meaning-before-carrier.

For every proposed conversion, explain how identities and meanings are preserved. Distinguish a permutation of the same support from a substantive change of outcome vocabulary or state factorization. Output: explicit identity mappings and unresolved domain changes.

The twelve-disposition terminal preference member is one scoped domain, not permission to force every outcome into twelve slots. Unsupported evidence vocabulary or a new joint state cannot be filled with placeholders just to satisfy the common carrier. Structural changes need reviewed consequences across dependent models and consumers.

K3 — State and exercise the repaired laws

Pattern: wm-prediction/probability-laws-with-runtime-meaning.

Pin the repaired definitions and enumerate their obligations. The inspected Lean finite-support kernel requires nonnegative mass, exact normalization, duplicate-free support and zero mass outside support. The inspected precision type enforces nonnegative values. Runtime model validation checks support membership and mass before numeric admission. Output: a law-to-constructor/consumer map, with rejecting examples targeting each obligation.

The committed Lean controls deliberately supply all fields and fail on duplicate support, hidden mass and negative precision. Preserve this discipline: rejection for a missing unrelated field does not test the intended invariant. Include valid controls too, so rejecting everything cannot pass. Scope any additional positivity, nonempty-domain or finite-numeric requirements to the actual consumer; nonnegative precision must not silently become strictly positive precision.

K4 — Separate numeric admission from exact laws

New pattern: wm-prediction/numeric-admission-is-not-exact-equality.

The inspected runtime contract admits exact ratio/integer rows only at exact sum one. Float-carried rows use a declared 1e-12M sum criterion with exact summation of represented double values; rows are not renormalized. The finite/nonnegative checks occur in distribution validation, not solely in the sum helper. Output: the reviewed relation between runtime values and formal objects, including conversions and consumer-specific limitations.

This describes existing source behavior, not a new epsilon or its independent acceptance. Passing the float gate does not establish Lean's exact normalization for the same unchanged masses. The correspondence may require a formal error statement, an explicitly authorized exact representation or another reviewed construction. Which one applies is a decision to substantiate, not a gap to bridge with silent normalization.

A bound on row sums is not automatically a bound on composed predictions, logarithms, KL risk or final ordering. Consumers involving zeros or infinities need their own defined behavior. Finite IEEE values, exact rationals and real-valued Lean kernels are not interchangeable merely because their printed decimals look alike.

K5 — Share the contract across actual consumers

Pattern: aif/shared-kernel-predictive-forward-model.

Apply this seed's principle of one authoritative law to validators, constructors and adapters. Identify where shared executable definitions prevent drift and where different representations require explicit correspondence. Output: actual call-site bindings to the same model and numeric contract.

This is scoped reuse: extracting a deterministic dynamics core or adding Gaussian noise is not the WM-01 task. Shared code alone does not prove the law or empirical adequacy. Avoid local epsilon changes, support repair or fallback distributions in downstream adapters. Atomic publication of a model envelope prevents mixing definitions, supports and witnesses from different revisions.

K6 — Bind proof and acceptance to the repaired subject

Pattern: wm-qualifying-run/certificate-and-world-must-meet.

Inventory each dependent theorem, constructed witness, admitted claim and runtime adapter affected by the repair. Bind claims to exact source/toolchain/import identities, actual theorem statements and assumptions, build/axiom receipts, and the precise supplied witness. Output: a dependency/admission ledger that separates author validation from independent acceptance.

Changing Holes.lean under the same path does not preserve an old subject hash. An unchanged theorem name or statement does not by itself establish validity against changed definitions. Conversely, do not declare all old results false without inspecting their dependencies. Classify each as unaffected with evidence, rebuilt and revalidated, awaiting review, or superseded. Preserve frozen source/admission rules; do not edit a pinned subject to avoid the review work.

This applies the certificate pattern to repair and correspondence claims. It does not produce the whole-machine qualifying-run certificate.

K7 — Explain what evidence the inventory could have missed

Pattern: wm-qualifying-run/complete-acquisition-universe.

Reconcile K6's ledger against a declared search universe of imports, references, admission records, runtime constructors and consumers. Retain the roots searched and unresolvable references. Output: a coverage account for the repair's impact, with unresolved candidates and ownership rather than a falsely exhaustive list.

Search hits are candidates, not proof of semantic dependence. A successful build of one module is not a census of admitted witnesses. Unavailable old logs remain unavailable; a rebuilt artifact receives new evidence and must not be presented as the missing historical receipt.

K8 — Follow the admitted model into computation

Pattern: wm-connected-learning/observation-to-next-choice.

Retain the model/carrier revision and numeric admission at the actual WM-02–05 boundaries and subsequent consumer. Demonstrate that the validated object is the one used, with rejecting controls for stale subject, swapped support, omitted field and mismatched admission. Output: correspondence receipts and, later, ordinary production-use evidence.

A well-formed test table proves neither machine-produced A/B/belief nor whole-node completion. Tests of this boundary should distinguish the repaired model from a stale or malformed substitute. They must not require every carrier change to alter a selected action: valid revisions may preserve a decision.

Composition and feedback

K1 and K2 jointly constrain K3's law map. K3 constrains K4's numerical correspondence, and both constrain K5's shared contract. K3–K5 supply the exact subjects and computations that K6 must bind to evidence. K7 checks K6 against the broader dependency universe. K5, K6 and K7 jointly constrain K8's claim of actual use.

K4 can reveal a representation that cannot satisfy the claimed law and return to K3. K7 can expose a missed consumer and return to K1/K6. K8 can reveal a local adapter repair and return to K5. These are design-review relations, not automatic migrations or permission to replace the specification.

Proposed build components

Names describe proposed responsibilities, not newly implemented modules. Retain source bytes and immutable identities, not just paths. Changed definitions or model meaning require explicit successor revisions and review; immutable old receipts stay attached to their original objects.

A concrete failure this cascade exposes

Suppose a runtime row totals slightly less than one and passes the existing float gate. K3 confirms what the exact kernel law demands. K4 refuses the unsupported statement that this row is exactly normalized as a real-valued kernel. K6 also rejects a certificate that points to a same-named witness built against the pre-repair source. These are separate issues, both visible before the model receives completion credit.

A valid support permutation presents a different case: if identities and values are permuted together under a declared mapping, it may preserve the distribution. If only values move, the prediction changes its meaning. K2 and K8 must distinguish those cases. Sorting values or discarding extra keys to make a check pass is not a valid conversion.

Build order and acceptance evidence

1. Freeze the review subject and inventory contracts (K1–K3). Record current repaired source and dependency identities. Retain exact obligations and uncertainty about acceptance. Respect existing frozen-admission policies before making any edits.
2. Review and exercise targeted controls. Rebuild the relevant modules under the recorded toolchain, inspect actual axiom dependencies and execute positive/negative controls. Rejection must identify the intended obligation. No Lean build is claimed in this authoring task.
3. Resolve numeric correspondence (K4–K5). Test exact and float cases, support permutations, extra keys, duplicates, negative/nonfinite values, zero mass and downstream boundary behavior. Verify the full validator path, not only a permissive helper. Do not extend one-step error bounds to composed consumers without evidence.
4. Reconcile proofs and admissions (K6–K7). Independently review the repair and affected claim mappings. Retain the exact acceptance receipt or explicitly mark it missing. Review new evidence as new evidence; do not manufacture historical provenance.
5. Demonstrate actual consumer binding (K8). Retain both rejecting controls and a valid path through real constructors/adapters. Later authorized production evidence must identify the model actually used. A fixture, build log or accepted repair alone does not close every carrier connection.

Source boundaries and remaining decisions

The checklist WM-01 supplies the scope and historical repair credit. This design inspected Holes.lean, ProbabilityKernelRepairNegative.lean and machine_model.clj; their hashes and applied pattern sources are in cascade.json. It did not independently reproduce the repair build or locate a new review receipt. Model-domain changes, exact/float correspondence and affected-admission coverage remain obligations to settle rather than assumed accomplishments.

The new numeric-admission argument is a draft in the prediction sublibrary. Existing AIF patterns are referenced within scope. WM-01 remains open; this design specifies its build and validation path without claiming mathematical, runtime or whole-machine completion.

Explicit design relations

Existing AIF source snapshots

Quoted as local library references, not copied into the new sublibrary. Their other claims and examples are not adopted by this cascade.

@flexiarg aif/declare-the-conditioning
@title Declare the Conditioning (Score the Fit, Not the Form)
@keywords conditioning, situation, context, fit, EFE, curried, referent
@audience aif implementers, pattern authors, futon developers
@tone technical
@style pattern
@references [aif/currency-before-merge aif/valuation-reads-the-paperwork]

@how aif/structured-observation-vector
@see-also aif/term-to-channel-traceability
@why no matching problem dossier node (@holds-at absent; not among the twenty dossier nodes R1-R17, R20, TRACE). Negative claim per the committed check futon2 holes labs library-loop runs l3_no_dossier_check.py, receipt runs L3-no-dossier-check.edn (enumerates every aif pattern's @holds-at against the dossier node set extracted from PROBLEMS-*.md headings). Rationale not invented (L3 rationale-backfill pilot, zai-1, 2026-09-05)
@how own mechanism: Every valuation surface must declare what slice of the situation it consumed; G(candidate) is a lambda — only G(candidate | situation) is a value. (source: this pattern's ! conclusion line; L3 rationale-backfill pilot, zai-1, 2026-09-05)
! conclusion: Every valuation surface must declare what slice of the situation it consumed; G(candidate) is a lambda — only G(candidate | situation) is a value.

  + context: A stack grows multiple valuation surfaces (blend terms, wholeness, ΔG legs, field diagrams), each labelled with the same vocabulary ("EFE", "value", "score").

  + IF:
    You want valuations to be comparable, auditable, and honestly labelled.

  + HOWEVER:
    Different surfaces silently consume different slices of the world — one eats the live observation vector, another a 160-char prose scrap, a third nothing at all — so identical labels name incomparable objects, and cross-surface comparisons are apples-to-oranges without anyone having lied.

  + THEN:
    Give every valuation surface a three-axis declaration: SENSE (which formal object it claims), SELECTION-SEMANTICS (extremum / amortized sample / bound — over what menu), and CONDITIONING (what situation-slice it consumed). Render the declaration where the number is rendered. In pattern terms: Context → (Problem → Solution) — application is modus ponens; the world supplies the antecedent; score the fit, never the form alone.

  + BECAUSE:
    Canonical expected free energy is G(π; Q(s), C) — conditioned on beliefs and preferences by definition; a policy has no value in vacuo, and Alexander says the same of form and context. Surfaces that skip the declaration re-invent the mislabeling one level up.

    + evidence: M-evaluate-policies §9.6–9.7 + exhibit "conditions on" column (futon2, 2026-07-03): the atomic-action lane conditioned on the live observation vector while the cascade lane ate a title+status scrap and two native components consumed no situation at all — one arena, incomparable conditioning. E5 measured the conditioning channel: situation-enriched ψ rebuilt 11/13 cascades. The fold contract already typed circumstance as an argument; the plumbing had starved it.

  + NEXT-STEPS:
    - Add the sense × selection-semantics × conditioning triple to each EFE-labelled surface's declaration (extends the efe-referent-declaration shape).
    - Route all lanes toward ONE situation source (the structured observation vector) where feasible.

@flexiarg aif/shared-kernel-predictive-forward-model
@title Shared Kernel for the Predictive Forward Model
@sigils [⚙️/由]
@audience fulab agents, aif implementers, simulation-based-AIF designers
@tone technical
@style pattern
@holds-at R4   ;; pegged 2026-08-30 (claude-15): the catalogue paragraph numbered R4 in p4ng/sec-catalog.tex; see PREREG-war-machine §1b

@see-also aif/expected-free-energy-scorecard
@how aif/temporal-depth-beyond-greedy
@why R4 dossier problem: R4 solves the problem of evaluating an action before enacting it: the control-stage roster places **“Forward model”** in EVALUATE (`p4ng/empirics-futon/control-stages.edn:21`; control-stage numbering), and the operational criterion requires a pure `(state, action) -> next-state-distribution` which **“the agent uses to score candidate actions before taking them”** (`docs/futon-aif-completeness.md:110-114`; contract R4). (source: futon2 holes labs wm-contract PROBLEMS-r4-r5-r6-pilot.md, R4, The problem it solves; L3 rationale-backfill pilot, zai-1, 2026-09-05)
@how own mechanism: Extract the deterministic dynamics core into a pure shared kernel; have both the live step and the predictive forward model call into it. One implementation, two callers. (source: this pattern's ! conclusion line; L3 rationale-backfill pilot, zai-1, 2026-09-05)
@why problems/r4-forward-model (L14 edge-resolution; basis: holds -- the problem node's own holds-at token covers this pattern; source: receipt runs/L14-edge-resolution.edn; zai-1, 2026-09-05)
! conclusion: Extract the deterministic dynamics core into a pure shared kernel; have both the live step and the predictive forward model call into it. One implementation, two callers.

  + context: An AIF agent that scores candidate actions via Expected Free Energy needs a predictive forward model — a function that takes a candidate action and returns the predicted next-state distribution. The naive implementation maintains a separate "shadow" dynamics for the predictive call, which inevitably drifts from the live dynamics as the code evolves.

  + IF:
    You want the predictive forward model's outputs to be principled (the agent's beliefs about candidate actions match what the live dynamics would actually do under those actions), maintainable (one set of dynamics rules to update), and verifiable (a single regression-test surface that catches accidental divergence).

  + HOWEVER:
    Two implementations of the same dynamics is two implementations to maintain, two places for bugs to hide, two surfaces where the forward model's predictions can disagree with what the live step actually does. The cost of maintaining bit-equivalent shadows grows quadratically with the dynamics complexity.

  + THEN:
    Factor the live step into (a) a *pure deterministic kernel* taking explicit (state, action, seed, opts) and returning a next state, and (b) a *thin orchestration wrapper* that threads defaults and calls the kernel. The wrapper preserves the live API; the kernel becomes callable by:
      - The wrapper, in live operation.
      - The predictive forward model, for candidate scoring — typically via a second arity that admits supplied candidate actions and skips the live action-selection step.
    The predictive forward model then becomes a thin probabilistic wrapper around the same kernel: call kernel with candidate, add Gaussian noise (or other principled uncertainty representation), produce next-state distribution.

  + BECAUSE:
    One implementation of the deterministic dynamics is the only place where the rules live. The kernel is what the live step does *and* what the forward model predicts. Any update to one is automatically reflected in the other. The bit-equivalence test (live-path output unchanged under refactor) is the cheapest catchnet for accidental drift.

  + NEXT-STEPS:
    - Audit the live step for impurities: I/O calls, atom mutations, time-of-day reads, side-effect emissions. The kernel must be pure; impurities belong in the wrapper.
    - Define the kernel signature with explicit (state, action, seed, opts) — no implicit context, no defaults inside the kernel itself.
    - Add a second arity for the forward-model seam: `(kernel state ext seed opts candidate-actions)` — supplied actions skip live action selection.
    - Document the RNG-consumption divergence: when candidate actions are supplied, the kernel doesn't consume action-selection RNG. The forward model's Gaussian noise wrap is the source of predictive uncertainty, not kernel RNG draws. This must be in the kernel docstring.
    - Capture a pre-refactor regression baseline. Commit it (e.g. as a CSV fixture). Automated test compares post-refactor output to baseline byte-for-byte.
    - DONE (UKRN v3 HO-03, 2026-05-14): step-kernel extracted to notebooks/ukrn_v3_kernel.clj:159-193; engagement-step reduced to 8-line wrapper at notebooks/ukrn_v2_engagement.clj:51-58; bit-equivalence regression fixture at test/fixtures/ho03_v11_headline_trajectory_baseline.csv. Evidence: handoffs/v3_runner/validation_HO-03.md.
    - DONE (UKRN v3 HO-04, 2026-05-14): predict-engagement-step at notebooks/ukrn_v3_forward.clj:122-149 wraps step-kernel 5-arity with Gaussian noise propagation; smoke output shows threshold-proximity behaviour discriminates candidates correctly. Evidence: handoffs/v3_runner/validation_HO-04.md.
    - Practice: keep the kernel and the forward model in separate namespaces. The kernel is the deterministic shared core; the forward model is the probabilistic wrapper. Separation makes the call surface for downstream EFE consumers clear.

Download the source-pinned cascade JSON · WM-05 cascade