fold(B3): contracts / ONT / PVL / docs onto main — replaces #4317

[noahgift]

Replaces #4317 (cop ruling 2026-09-25 16:15Z: no main-merges into a PR; a fresh branch from main instead).

One squashed commit on main a5efa14 carrying fold/b3-contracts-ont-docs @88885740d (263 commits, 63 merges). Conflicts with the B4 fold (#4312) were resolved to B3, which is a superset: 22 lint gates, NAMED_GATES [&str;14], sigma ReservedEntityType beside VocabularyMalformed. roadmap.yaml was re-aggregated, and census + README counts were regenerated with the pv built from this tree. Local results: fmt clean; aprender-contracts --lib 2001 passed; ont6_lint_verdict 7 passed; roadmap-fragment and readme-claims guards PASS. #4317's original body follows.

Emergency fold B3 (contracts / ONT / docs), operator 2026-09-24: "We FIRST RIGHT NOW, emergency merge all 80 into 4 batches., the enforce 10 max rule going forward."

Folded sources (each merged --no-ff, history kept)

• folds fix(orchestrate): resolve_project_root's fallback test no longer reads the host's /tmp (#4191) #4204: fix(orchestrate): resolve_project_root's fallback test no longer reads the host's /tmp (aprender-orchestrate: test_resolve_project_root_nonexistent_falls_back is host-dependent (stray /tmp/Cargo.toml) #4191)
• folds fix(contracts): lint tests read the shared /tmp as their project root — nest each corpus (#4207) #4227: fix(contracts): lint tests read the shared /tmp as their project root — nest each corpus (aprender-contracts lint::tests::lint_empty_dir fails on pristine main aa7c6ef03 (report.passed, mod_tests.rs:32), likely env-dependent #4207)
• folds fix(guard): guard_tree.sh — 0 executed checks or a lost plan fails, never '0 checks, 0 failed' exit 0 (#4108) #4121: fix(guard): guard_tree.sh — 0 executed checks or a lost plan fails, never '0 checks, 0 failed' exit 0 (guard_tree.sh: vacuous PASS — lost scratch dir → '0 checks, 0 failed', exit 0; make gate green on nothing #4108)
• folds ci(#4102): a run's target dir is deleted by its LAST job out (flock-guarded, always()); by-kind size split measured #4150: ci(ci: a single #4046 shard left 64G of target on gx10 — delete the job's own run target on exit, then pick a size lever by measured kind #4102): a run's target dir is deleted by its LAST job out (flock-guarded, always()); by-kind size split measured
• folds ci: fold pushes to release/** run guard-tree + guard-cargo, and only them (#4112) #4163: ci: fold pushes to release/** run guard-tree + guard-cargo, and only them (ci.yml guards never run on PRs into release/** (or on fold pushes), so batch folds skip guard-cargo/guard-tree until the integration PR #4112)
• folds ci(workspace-test): shards wait on guard-tree, so a RED guard stops burning shard runner time (#3177) #4196: ci(workspace-test): shards wait on guard-tree, so a RED guard stops burning shard runner time (A merge group whose guard-tree is RED still burns ~2 h of intel workspace-test time before gate reports it #3177)
• folds fix(release): the milestone cut blocks on must-carry issues only; the autopilot carries the rest before the tag (#3459) #4177: fix(release): the milestone cut blocks on must-carry issues only; the autopilot carries the rest before the tag (release train: move the release autopilot's tag path into the repo — tag step calls scripts/check_milestone_cut.sh and cannot be reached without it #3459)
• folds feat(contracts): ONE shared in-tree helper — skip by name out of tree, FAIL in tree; contracts a versioned dev-dep (#4175) #4183: feat(contracts): ONE shared in-tree helper — skip by name out of tree, FAIL in tree; contracts a versioned dev-dep (clean-room B2: packaged-tarball test gate, all crates #4175)
• folds PVL-001 EV-6c pt1: kani_assume.rs per-file kani::assume token count (use-import refused, fails closed) + rises + Baseline check; 14 tests; proc-macro2 dep; DELETE dead tests_12b.rs. NO CLI flag, baseline, Makefile, workflow #4216: PVL-001 EV-6c pt1: kani_assume.rs per-file kani::assume token count (use-import refused, fails closed) + rises + Baseline check; 14 tests; proc-macro2 dep; DELETE dead tests_12b.rs. NO CLI flag, baseline, Makefile, workflow
• folds PVL-3: one definition of L4/L5 (PVL-001 EV-3, PMAT-4081) #4092: PVL-3: one definition of L4/L5 (PVL-001 EV-3, PMAT-4081)
• folds PVL-2: proof-status resolves bindings; ghost binding is a reject (PVL-001 EV-2, PMAT-4080) #4095: PVL-2: proof-status resolves bindings; ghost binding is a reject (PVL-001 EV-2, PMAT-4080)
• folds PVL-001 EV-10: pv obligations [ROOT] --gate (commands/obligations.rs, cli/lib/mod wiring) = pv-obligation-gate.py; 11 golden tests, fixtures, ci fragment 460; tree_reader registry +2, surface_audit pv cites +11 lines. NO ci.yml/Makefile/pmat edit #4230: PVL-001 EV-10: pv obligations [ROOT] --gate (commands/obligations.rs, cli/lib/mod wiring) = pv-obligation-gate.py; 11 golden tests, fixtures, ci fragment 460; tree_reader registry +2, surface_audit pv cites +11 lines. NO ci.yml/Makefile/pmat edit
• folds ONT-2c: in-house OWL 2 EL writer; told-closure TBox, advisory; ELK + horned-owl oracle out of gate (#4071) #4136: ONT-2c: in-house OWL 2 EL writer; told-closure TBox, advisory; ELK + horned-owl oracle out of gate (ONT-2c: in-house OWL 2 EL writer; TBox check via the oracle, advisory #4071)
• folds ONT-5: relation consistency — Horn witness, pv-sat, ont-consistency gate (computed, not armed) (Refs PMAT-4074) #4248: ONT-5: relation consistency — Horn witness, pv-sat, ont-consistency gate (computed, not armed) (Refs PMAT-4074)
• folds PVL-001 EV-5a: pin Mathlib, scoped Lean warning gate, orphan allowlist (#4122) #4205: PVL-001 EV-5a: pin Mathlib, scoped Lean warning gate, orphan allowlist (PVL-001 EV-5a: pin Mathlib, scoped Lean warning gate, orphan allowlist #4122)
• folds ONT-4d: subsumption in Σ; shapes inherit down the hierarchy (#4070) #4137: ONT-4d: subsumption in Σ; shapes inherit down the hierarchy (ONT-4d: subsumption in Σ; shapes inherit down the hierarchy #4070)
• folds [stacked on #4248/#4137] ONT-4e: requires/ensures as first-class; Liskov rule on refines, witness-checked #4301: [stacked on ONT-5: relation consistency — Horn witness, pv-sat, ont-consistency gate (computed, not armed) (Refs PMAT-4074) #4248/ONT-4d: subsumption in Σ; shapes inherit down the hierarchy (#4070) #4137] ONT-4e: requires/ensures as first-class; Liskov rule on refines, witness-checked
• folds PVL-001 EV-6a: pv discharge check — axiom subset pins, escape allowlist (#4139) #4289: PVL-001 EV-6a: pv discharge check — axiom subset pins, escape allowlist (PVL-001 EV-6a: pv discharge check — axiom subset pins; compiler-escape allowlist #4139)
• folds PMAT-3997: DEBT-RATCHET-001 — step-1 quorum research plan for the 0.70→0.74 debt ratchet (#3997) #4003: PMAT-3997: DEBT-RATCHET-001 — step-1 quorum research plan for the 0.70→0.74 debt ratchet (EPIC S3 standing: Debt Ratchet #3997)
• folds PMAT-4002: EPIC 0.75 CRUX fine-tune/distill — plan with measured baselines + decision quorum (#4002) #4009: PMAT-4002: EPIC 0.75 CRUX fine-tune/distill — plan with measured baselines + decision quorum (EPIC E8 0.75: CRUX Fine-Tune/Distill #4002)
• folds PMAT-3994: EPIC 0.71 Don't Leave Behind + MoE — plan with measured baselines + decision quorum (#3994) #4011: PMAT-3994: EPIC 0.71 Don't Leave Behind + MoE — plan with measured baselines + decision quorum (EPIC E3 0.71: Don't Leave Behind #3994)
• folds PMAT-4000: EPIC 0.72 Agent Ready — plan with measured baselines + decision quorum (#4000) #4012: PMAT-4000: EPIC 0.72 Agent Ready — plan with measured baselines + decision quorum (EPIC E5 0.72: Agent Ready #4000)
• folds PMAT-3999: EPIC 0.73 llama.cpp Parity — plan with measured baselines + decision quorum (#3999) #4013: PMAT-3999: EPIC 0.73 llama.cpp Parity — plan with measured baselines + decision quorum (EPIC E6 0.73: llama.cpp Parity #3999)
• folds PMAT-4001: EPIC 0.74 Any Model — plan with measured baselines + decision quorum (#4001) #4014: PMAT-4001: EPIC 0.74 Any Model — plan with measured baselines + decision quorum (EPIC E7 0.74: Any Model #4001)
• folds PVL-7b: the comparator — each solution closes exactly its pinned Challenge statement (#4201) #4237: PVL-7b: the comparator — each solution closes exactly its pinned Challenge statement (PVL-001 EV-7b — PVL-7b: comparator — the solution closes exactly the pinned statement #4201)
• folds EV-8a (#4202): pv discharge run writes discharge-summary.json; proved-is-derived armed #4281: EV-8a (PVL-001 EV-8a — PVL-8a: pv discharge run — one summary the tree can carry #4202): pv discharge run writes discharge-summary.json; proved-is-derived armed

Closes #4191
Closes #4207
Closes #4108
Closes #4112
Closes #3177
Closes #4081
Closes #4080
Closes #4198
Closes #4071
Closes #4074
Closes #4122
Closes #4075
Refs #4102
Refs #4175
Refs #4070
Refs #4139
Refs #3997
Refs #4002
Refs #3994
Refs #4000
Refs #3999
Refs #4001
Refs #4201
Refs #4202

Parked (branch kept; re-enters via the next like-batch)

• feat(release): serve-parity gate verdict + release receipt check (#4218 PR1) #4243 feat/4218-serve-parity-gate: red on its own CI (guard-tree, guard-cargo, workspace-test), and its contract raises unanchored_but_bindable from 297 to 298. The fold was reverted out of the batch.
• PMAT-4029: vLLM CRUX driver sizes max_model_len to context + the loading group's largest budget #4093, chore: 0.69.1 follow-up — preflight tooling (f5), crux-smoke meta skip, apr capability chapter #4115, docs(readme): 0.69.1 post-release — certification scope + published-binary cookbook receipts #4119, PMAT-4039: the ladder measures its cells in one planned order — CRUX-certified first, then largest first #4123, feat(crux): reference cache + source-weight engine batching (#4036) #4171, fix(crux): greedy cell stops llama-server through the teardown trap; failed teardown → every row RED (#4209) #4217, test(crux): inline-kill case table pins kill -TERM / kill -9 (#4225) #4226: these are based on chore/0.69.1-merge-back, which is 678 commits ahead of main (its PR chore: 0.69.1 merge-back — release/0.69.1-batch-2 + rc/0.69.1-x (X2) into main #4046 is closed). They touch CRUX files that do not exist on main (scripts/crux_vllm/*, scripts/lib/crux_cells_*, the README "Verified this release" section), so they cannot fold without the merge-back itself.

Batch resolution

• lint gates are the union of ONT-2c tbox, ONT-5 ont-consistency, ONT-4e refines, ONT-7 valid-under, EV-11 theorem-pairing/depends-on-present, EV-8a proved-is-derived and EV-7a challenge-fresh. Full run: 19 gates. Numbering: 13 valid-under, 14–16 ratchets, 17 challenge-fresh, 18 ont-consistency, 19 refines (renumbered from 17/18). NAMED_GATES has 11 entries.
• contract_walk exit-1 errors: ObligationsRejected + GateRejected + DischargeRejected (all three kept).
• ci.yml workspace-test: needs: [guard-tree, workspace-test-shard] (ci(workspace-test): shards wait on guard-tree, so a RED guard stops burning shard runner time (#3177) #4196) plus the release-push skip from ci.yml guards never run on PRs into release/** (or on fold pushes), so batch folds skip guard-cargo/guard-tree until the integration PR #4112.
• Generated set: regenerated once (batch_fold.sh --regen), plus the pv-sat witness (make contracts) and tree_reader_tests.txt --update. There are 54 stale cli.rs:N rows in surface_audit.csv, each re-derived from its Commands::<Variant>.

Local evidence (on this head)

• make contracts: rc 0; aprender-contracts lib 1904 passed.
• cargo test -p aprender-contracts-cli: rc 0. cargo clippy -p aprender-contracts -p aprender-contracts-cli --all-targets -D warnings: rc 0.
• cargo fmt --all --check 0 · cargo deny check advisories 0.
• Guards rc 0: check_ont_ratchet, check_roadmap_sorted, check_tree_reader_tests, check_dogfood_coverage, check_readme_claims.

Workflow change: #4150, #4163 and #4196 edit .github/workflows/, so this batch needs a 3/3 quorum and the cop merges it.

keep-open: #3994 #3997 #3999 #4000 #4001 #4002 (epics, Refs only)
ont-delta: resolves ONT-2c + ONT-4d + ONT-4e + ONT-5 land together; the PVL-001 EV-2/3/5a/6a/6c/7b/8a/10/11 gates land.

Folded: #3142 PVL-F7 advisory con-leche nightly (9ef6d39, merge of fd06d80)

• New .github/workflows/conleche-nightly.yml (advisory, cron + dispatch, clean-room pool, no runner-host or secret changes) + crates/aprender-contracts-staging/lean/conleche.sh.
• Quorum 3/3 PASS, degraded: same-family (agy void twice on isolation): /mnt/nvme-raid0/tmp/pvl-a-q3142/VERDICT.md. Evidence: /mnt/nvme-raid0/tmp/pvl-a-3142/EVIDENCE.md (3 runs, 402163 decls accepted).
• Refs PVL-F7: con-leche nightly independent re-check, advisory #3142. Also: this fold carries PVL-001 EV-6b — PVL-6b: leanchecker re-check inside discharge check #4199's branch (ff44809 is an ancestor).

Fixes #4199

🤖 Generated with Claude Code

Closes #4238
Closes #4355 #4357 #4358 #4359

🤖 Generated with Claude Code

• ONT-3a (aprender-ea, fe8c9df): bindings gate emits the spec probe fields pc_extract/unresolved + RED tests (pub(super), wrong module, missing ticket); probe PASS on repo corpus
  Closes ONT-3a: extract:code — bindings resolve fail-closed across the workspace, via syn #4072

[noahgift]

Quorum receipt (degraded: same-family; author claude-opus-5-5; lanes claude-sonnet-5 + claude-haiku-4-5, headless plan mode, read-only whitelist) @ cf038d3. Scope: the resolutions vs #4317's head 8888574 (sigma.rs union, B3-superset files, README/census regen). Main's B4 content was already reviewed in #4312. sonnet PASS: NAMED_GATES 5→14 keeps valid-under, gate assert 13→22, the ratchet generalizes main's allowlist, README 1851 == census n_files. Its one asserted finding (no local build) is covered by the author's measured cargo test -p aprender-contracts --lib: 2001 passed. haiku PASS, 0 findings.

[github-actions]

§13.11 rung 1 — quorum shadow verdict

S13-SHADOW pr=4431 head=ebf21c83d4948d6eb8785d31667dcd76844ff22e verdict=REFUSE class=Q1 arm_rc=1

Shadow mode: this records a verdict and merges nothing. A refusal
to arm is not a block (§13 adds zero rows to §7) — the pull request is
exactly as green as it was.

[noahgift]

Pre-merge finding: ONT-3a's spec probe will stay false after this merges, because the bindings report emits pc_resolver/ghosts and the probe reads pc_extract/unresolved. Details: #4454. Rows 2c, 4e, 5 and 9 are clean at ae1887d except for merged.

🤖 Generated with Claude Code