[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.72: 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.73: Train What You Serve  #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: Runs Everywhere #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
• ports PVL-001 EV-6c — PVL-6c: Kani assume baseline #4197 part 2 (aprender-0d, c901a32): pv discharge check --kani + contracts/kani-assume-baseline.json + ci fragment 463

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
Refs #4197

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

Conflict resolution

Untangle (cop ANDON, 2026-09-27): git merge origin/main @aca6f2d7f6 → merge 1596517, regen b9de7de. No force-push.

file:hunk	side kept	why
Makefile:contracts: recipe	union	main's || exit per step + this branch's pv-sat witness lines; both needed
scripts/claim_literal_baseline.txt	union	shrink-only baseline; check_no_claim_literals.sh PASS, did not grow
scripts/check_ont_ratchet.sh:local decl	ours	cosmetic ordering
scripts/check_ont_ratchet.sh:top_line=	ours	keeps || return 2 (multi-line foreign key refused, not dropped)
scripts/check_ont_ratchet.sh:JSON emit order	ours	merged lint-baseline.json lists top keys before readme/claude_md; ratchet PASS, self-test 34/34
scripts/check_ont_ratchet.sh:mode	main	100755
README.md:Quick Start	union	main's installer paragraph; fences kept ```text (PV-ONT-012: bash fences are verified claims)
README.md:Workspace crates	regen	cargo metadata --no-deps on the merged tree = 82
README.md:CONTRACT_COUNT	regen	readme_sync.sh --write → 1855 (census fresh)
docs/roadmaps/roadmap.yaml	regen	roadmap_fragments.py aggregate --write

Local: cargo check --workspace ✅ · --test readme_contract 16/16 ✅ · ont-ratchet ✅ · readme-claims ✅. Owner re-quorums.

[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=bd124f8c0fd6baf9d43175dd51e54cf91d8d6c44 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

[noahgift]

quorum-review (AD-04): three PASS — agreed (auto_merge: checked=true was_armed=false disarmed=false)

{
 "ticket": "PMAT-4431",
 "head": "0cce84279ec08677b8a26cf8d8d1c18c90424189",
 "width": 3,
 "executor": "agy",
 "agreed": true,
 "auto_merge": {
  "checked": true,
  "was_armed": false,
  "disarmed": false,
  "note": "auto-merge not armed"
 },
 "lanes": [
  {
   "lane": 1,
   "verdict": "PASS",
   "findings": 6
  },
  {
   "lane": 2,
   "verdict": "PASS",
   "findings": 0
  },
  {
   "lane": 3,
   "verdict": "PASS",
   "findings": 0
  }
 ]
}

[noahgift]

quorum-review (AD-04): three PASS — agreed (auto_merge: checked=true was_armed=true disarmed=true)

{
 "ticket": "PMAT-4431",
 "head": "7a8088d9a7ab39e1fecc9d6fab91994f9365e337",
 "width": 3,
 "executor": "agy",
 "agreed": true,
 "auto_merge": {
  "checked": true,
  "was_armed": true,
  "disarmed": true,
  "note": "auto-merge was armed from an earlier round; disarmed before lanes launched"
 },
 "lanes": [
  {
   "lane": 1,
   "verdict": "PASS",
   "findings": 0
  },
  {
   "lane": 2,
   "verdict": "PASS",
   "findings": 0
  },
  {
   "lane": 3,
   "verdict": "PASS",
   "findings": 0
  }
 ]
}

[noahgift]

quorum-review (AD-04): NOT agreed (auto_merge: checked=true was_armed=false disarmed=false)

{
 "ticket": "PMAT-4431",
 "head": "76d6f4886b775d07d5d8d7acdec976563e7d3aeb",
 "width": 3,
 "executor": "agy",
 "agreed": false,
 "auto_merge": {
  "checked": true,
  "was_armed": false,
  "disarmed": false,
  "note": "auto-merge not armed"
 },
 "lanes": [
  {
   "lane": 1,
   "verdict": "PASS",
   "findings": 0
  },
  {
   "lane": 2,
   "verdict": "PASS",
   "findings": 0
  },
  {
   "lane": 3,
   "verdict": "NO-VERDICT",
   "findings": 0
  }
 ]
}

[noahgift]

quorum-review (AD-04): three PASS — agreed (auto_merge: checked=true was_armed=false disarmed=false)

{
 "ticket": "PMAT-4431",
 "head": "76d6f4886b775d07d5d8d7acdec976563e7d3aeb",
 "width": 3,
 "executor": "agy",
 "agreed": true,
 "auto_merge": {
  "checked": true,
  "was_armed": false,
  "disarmed": false,
  "note": "auto-merge not armed"
 },
 "lanes": [
  {
   "lane": 1,
   "verdict": "PASS",
   "findings": 1
  },
  {
   "lane": 2,
   "verdict": "PASS",
   "findings": 0
  },
  {
   "lane": 3,
   "verdict": "PASS",
   "findings": 0
  }
 ]
}

[noahgift]

Closed to bring open PRs under the cap of 10 (18 open). The branch is kept (not deleted), and so is its head. Reopen this PR, or re-cut it from the branch as a PR of at most 4 rows, after the 0.70.0 FINAL, when merge-main is allowed again.

Why it was not landed or folded: the required checks gate and workspace-test are red at this head. The PR is behind or conflicting with main, and no bulk merge-main is allowed before FINAL. No legal fold target exists (PRCAP plan, 22:15Z).

Head bd124f8c0f on fold/b3-onto-main. It is largely superseded by #4502 → #4587 (PR-1) + #4588 (PR-2):

• 558 of its 731 changed files are byte-identical in batch/ont-10.
• The ONT-4c rows (entity_type_target_class) are in PR-1 and PR-2.

Residue NOT carried anywhere, so it must be re-cut from the branch after FINAL. These 28 files exist in neither main, PR-1 nor PR-2:

• PVL-001 EV-6c — PVL-6c: Kani assume baseline #4197 EV-6c part 2: crates/aprender-contracts-cli/src/commands/discharge_kani.rs, contracts/kani-assume-baseline.json, tests/pvl_kani_assume.rs and fragment 464.
• contracts/cooperative-matrix-gemm-v1.yaml.
• 20+ aprender-contracts-staging/lean/Challenge/*.lean files.
• 1 witness file and the fold(B3): contracts / ONT / PVL / docs onto main — replaces #4317 #4431 review evidence.