docs(arc): reconcile the arc's records with what the units measured
Every correction here is to something I wrote earlier in this arc. Original text is preserved in place; nothing was rewritten to look right in hindsight. ADR-0264 §4.2 — CORRECTED block. I sized the eleven band ceilings from per-TERM exclusivity; `resolve_domain`'s predicate is per-PAIR, which is looser, so every ceiling was understated and one verdict was wrong: systems_software_causal is 720, not 630, i.e. reachable rather than impossible. Seven of eleven bands cannot reach 657, not eight. Downstream conclusions survive — physics·modal (480) is still impossible and philosophy_theology·modal is still the target. ADR-0264 R5 + DIVISION-OF-WORK ×2 + compile_premises docstring — the "verdict-identical" claim is exact only where the full family was READABLE. Over MAX_PREMISE_SENTENCES, full-family compilation refuses outright, so narrowing is verdict-IMPROVING there. Read literally the unqualified phrasing implies a 17-chain family keeps declining, which is backwards — the opposite of the unblock. E2 rename staleness, 4 sites: ADR-0256 (Accepted) named `gold.py::assert_corpus_sound`, which #119 deleted; the plan's E2 item and DIVISION-OF-WORK's §2 row, §4 heading and "renaming after that is strictly more work" reasoning were all still written as pending. DIVISION-OF-WORK §0b — new status table: which PR each unit is, what stacks on what, and the four things the units found that the plan did not predict. Adds the arc-close brief from ARC-CLOSE-TEMPLATE.md. Its §3 (falsified assumptions) is the section that cannot be recovered from the diff: nine entries, five of them corrections to my own claims. Records that the articulation trigger is not merely unmet but STRUCTURALLY unmeetable — the previous arc left it unrecorded, which is what kept it re-triggerable — and names four pieces of stale reasoning still in the tree, with files, since that is the class of staleness nobody greps for. [Verification]: in-worktree on canonical CPython 3.12.13 with `uv sync --locked`: smoke 569, deductive 291 — both baseline, since the only non-doc change is one docstring.
This commit is contained in:
Shay
parent
b67c703bc4
commit
923e60c136
7 changed files with 299 additions and 12 deletions
|
|
@ -26,7 +26,7 @@ Make deduction serving an earned capability gated by a committed, SHA-sealed rel
|
|||
- **Shape-band capability axis** (`generate/proof_chain/shape.py`) — a deterministic, structural classification of an argument into one of five exhaustive bands: the four propositional bands `disjunctive` / `conditional_chain` / `conditional_single` / `atomic` (assigned by `classify_deduction_shape` over the projected `(premises, query)`), plus `categorical` (Band v1b, Phase 4 — assigned directly to any syllogism projected by `to_syllogism`). Computed identically by the practice arena and the serving composer (no drift). Coarse on purpose: each band mixes entailed/refuted/unknown (or valid/invalid) gold, so a band's reliability measures decision correctness across outcomes, not just how many entailments pass through.
|
||||
- **Band v1b — production categorical decider** (`generate/proof_chain/categorical.py`) — the piece Phase 0's fork identified as missing. Serving cannot import `evals/syllogism/oracle.py` (the sealed independence oracle; INV-25), so this is a fresh production decider that lowers a categorical argument to the propositional regime (one Boolean atom per term-membership *profile*) and rides the already-verified ROBDD engine. Sound AND complete for the modern/Boolean reading; independent of the eval oracle by mechanism (ROBDD over a profile encoding vs. brute-force subset enumeration), verified by case-for-case agreement with it across the syllogism gold lane. Serving projects a syllogism via `to_syllogism` and decides it here (ENTAILED ⇒ valid; UNKNOWN/REFUTED ⇒ invalid; REFUSED ⇒ inconsistent).
|
||||
- **Deduction practice arena** (`evals/deduction_serve/practice/`) — the **second** concrete instance of the ADR-0199 arena (GSM8K math is the first). A deterministic, synthetic, indexed corpus (`gold.py`, no clock/RNG) of propositional arguments per shape-band, each with **by-construction gold** (the generating template's logical form, independent of the reader — ADR-0199 L-2). `DeductionSolver` runs the exact serving pipeline; `ConstructionGoldTether` scores the committed outcome against the by-construction gold; a misread is caught as `wrong`. Sized to the SERVE volume floor (≥657 committed for a perfect record to clear θ_SERVE=0.99; `CASES_PER_BAND=720`).
|
||||
- **Construction-time soundness check** (`gold.py::assert_corpus_sound`) — every generated case's by-construction gold is cross-checked against the **independent truth-table oracle** (`evals.deductive_logic.oracle`, INV-25 — shares no code with the ROBDD engine) before the ledger can seal. A mis-stated template gold can never silently inflate the ledger.
|
||||
- **Construction-time soundness check** (`gold.py::assert_practice_gold_sound`, renamed from `assert_corpus_sound` in #119 to resolve a collision with the curriculum lane's same-named contract check) — every generated case's by-construction gold is cross-checked against the **independent truth-table oracle** (`evals.deductive_logic.oracle`, INV-25 — shares no code with the ROBDD engine) before the ledger can seal. A mis-stated template gold can never silently inflate the ledger.
|
||||
- **Sealed, SHA-verified committed ledger** (`chat/data/deduction_serve_ledger.json`, produced by `evals/deduction_serve/practice/runner.py::seal_ledger`) — the per-band `ClassTally`, self-sealed by `content_sha256`. The engine READS it; only the sealed-practice runner WRITES it. Mirrors the estimation ledger topology exactly (`generate/determine/data/estimation_ledger.json`).
|
||||
- **Serving-side license reader** (`chat/deduction_serve_license.py::deduction_serve_license`) — loads + SHA-verifies the committed ledger and returns the `Action.SERVE` `LicenseDecision` per band under the safe **default** ceilings (θ_SERVE=0.99). A tampered ledger is rejected on load; a band absent from the ledger returns `None` (never licensed). The engine never raises its own ceiling (ADR-0175 invariant #4).
|
||||
- **Composer gate** (`chat/deduction_surface.py::deduction_grounded_surface`) — after the engine decides an in-band argument, the composer classifies its shape-band and consults the license:
|
||||
|
|
|
|||
|
|
@ -158,8 +158,19 @@ The default scope is **term incidence**: rows whose subject or object is one of
|
|||
the query's two terms. This is bounded by vocabulary degree rather than corpus
|
||||
size, keeps real neighbouring premises in the argument, and is a superset of the
|
||||
query-atom rows. If term incidence would still exceed the band's cap, narrow to
|
||||
the query-atom rows — which is verdict-identical, never an arbitrary truncation.
|
||||
The reader is never asked to refuse for size.
|
||||
the query-atom rows — never an arbitrary truncation. The reader is never asked to
|
||||
refuse for size.
|
||||
|
||||
> **Precision fix, 2026-07-26.** "Verdict-identical" is exact for every scope the
|
||||
> full family could be *read* at, and that is where the 8,520-question / zero-
|
||||
> mismatch evidence in §6 was gathered. It is **not** exact for the over-cap
|
||||
> branch: there the full family exceeds `MAX_PREMISE_SENTENCES`, so full-family
|
||||
> compilation would refuse `compiled_premises_unreadable` and answer nothing.
|
||||
> Narrowing there is verdict-**improving**, not identical — which is the entire
|
||||
> point of the unblock. The precise claim is therefore: **identical wherever the
|
||||
> full family was readable, improving where it was not.** Read literally, the
|
||||
> unqualified phrasing would lead a reader to expect a 17-chain family to keep
|
||||
> declining, which is backwards.
|
||||
|
||||
**R6 — An empty scope is UNKNOWN; only an empty family is a refusal.** Today
|
||||
`compile_premises` returning nothing means "this family has no ratified chains"
|
||||
|
|
@ -270,7 +281,38 @@ that prerequisite: query-scoped compilation removes the 16-chain ceiling, at
|
|||
which point §5.1's ≈219-relation prescription becomes achievable and its
|
||||
arithmetic becomes correct again.
|
||||
|
||||
### 4.2 Eight of eleven bands cannot reach the threshold even with unlimited authoring
|
||||
### 4.2 Seven of eleven bands cannot reach the threshold even with unlimited authoring
|
||||
|
||||
> **CORRECTED 2026-07-26, after Phase C measured this against the wired code.**
|
||||
> The original heading said *eight* of eleven and the table below understated
|
||||
> every ceiling. Both errors have one cause: I sized bands from **per-term
|
||||
> exclusivity** (a lemma taught by only one subject), while `resolve_domain`'s
|
||||
> actual predicate is **per-pair** — a question routes iff exactly one served
|
||||
> subject holds *both* terms. A lemma taught in two subjects can still appear in
|
||||
> a pair only one of them holds both halves of, so per-term exclusivity is a
|
||||
> strictly tighter bound.
|
||||
>
|
||||
> | band | stated below | measured | change |
|
||||
> |---|---:|---:|---|
|
||||
> | `curriculum_systems_software_causal` | 630 | **720** | **impossible → reachable** |
|
||||
> | `curriculum_philosophy_theology_modal` | 44,104 | 45,300 | — |
|
||||
> | `curriculum_philosophy_theology_contrast` | 22,052 | 22,650 | — |
|
||||
> | `curriculum_mathematics_logic_modal` | 420 | 480 | — |
|
||||
> | `curriculum_mathematics_logic_{sequence,contrast,evidential}` | 210 | 240 | — |
|
||||
> | `curriculum_systems_software_modal` | 420 | 480 | — |
|
||||
> | `curriculum_systems_software_sequence` | 210 | 240 | — |
|
||||
> | `curriculum_physics_{causal,modal}` | 720 / 480 | 720 / 480 | — |
|
||||
>
|
||||
> So **four** bands can reach 657, not three, and **seven** cannot, not eight.
|
||||
> Every conclusion that depends on this survives: `physics · modal` at 480 is
|
||||
> still impossible at any authoring volume, and `philosophy_theology · modal` is
|
||||
> still the defensible target by two orders of magnitude. The numbers are now
|
||||
> pinned as *measured* values in
|
||||
> `tests/test_curriculum_practice.py::BAND_ATOM_SPACE`, so this class of error
|
||||
> cannot recur silently. See
|
||||
> `docs/research/curriculum-practice-producer-2026-07-26.md` §2.
|
||||
>
|
||||
> The original text is preserved below unedited.
|
||||
|
||||
Volume is bounded by *taught vocabulary*, not by corpus size, because a question
|
||||
must have both terms in exactly one served subject's vocabulary to route at all
|
||||
|
|
|
|||
|
|
@ -0,0 +1,179 @@
|
|||
# Arc-Close Brief — Curriculum License Loop
|
||||
|
||||
**Arc:** curriculum-license-loop-2026-07 · **Closed:** 2026-07-26 · **Closing tier:** Opus 5
|
||||
**Plan of record:** `docs/plans/curriculum-license-loop-2026-07-25.md` (carries an
|
||||
`AMENDED 2026-07-25` block; §4.2 of ADR-0264 carries a `CORRECTED 2026-07-26` block)
|
||||
**ADRs minted:** ADR-0264 (the arc's only new ADR; ADR-0262 gained three forward-pointers)
|
||||
|
||||
**Nothing in this arc is merged.** Seven PRs (#119–#120 merged; #121–#125 plus the
|
||||
doc branch open) sit awaiting authorization. Read §2 before assuming any behaviour
|
||||
changed: it did not.
|
||||
|
||||
## 1. What shipped
|
||||
|
||||
| Capability | ADR | Enforcement site | Evidence |
|
||||
|---|---|---|---|
|
||||
| Query-scoped premise compilation — a >16-chain family answers again | 0264 R5–R7 | `teaching/curriculum_premises.py::compile_premises` | #120 merged; 0 verdict mismatches / 8,190 questions |
|
||||
| Volume-honesty invariant — committed volume must be DISTINCT evidence | 0264 R9 | `tests/test_volume_honesty.py`, `core/reliability_gate/evidence.py` | #117 merged; 21/25 deduction bands measured short |
|
||||
| The curriculum practice producer (the ledger's only writer) | 0262/0264 | `evals/curriculum_serve/practice/` | #121; 11 bands, wrong=0, inflation 1.0 |
|
||||
| `core proposal-queue reseal` — the `ledger_reseal` ceremony stage | 0262 | `teaching/ledger_reseal.py` | #122; refuses to grant a license without `--allow-new-licenses` |
|
||||
| Durable telemetry carries the POST-override turn event | audit-ledger R7 | `chat/runtime.py::_emit_turn_event`, `pipeline.run` | #123; I1–I8 pinned, 3 mechanisms mutation-checked |
|
||||
| Taught curriculum NEGATIVES — `polarity` is read | 0264 R1–R4/R8 | `CurriculumChain.sentence`, `validate_admissible`, `oracle.py` | #125; 22 tests, 3 rules mutation-checked |
|
||||
| `core rust build` works at all | — | `core/cli.py::_run` | #124; raised `TypeError` on every prior invocation |
|
||||
|
||||
## 2. Flag state at close
|
||||
|
||||
**No flag moved. No serving behaviour changed anywhere in this arc.**
|
||||
|
||||
| Flag | Default at close | Ratified by | Notes |
|
||||
|---|---|---|---|
|
||||
| `curriculum_serving_enabled` | **OFF** | — | unchanged; no band holds a license because no ledger is committed |
|
||||
| `deduction_serving_enabled` | **ON** | ratified 2026-07-24 | untouched. Its ledger's distinct-evidence exposure is measured and pinned, **not** repaired |
|
||||
| `identity_wave_gate` | OFF | ADR-0244/0245 | untouched |
|
||||
| `CORE_BACKEND` | `python` | — | untouched. `core_rs` importable ≠ active; verified |
|
||||
|
||||
`chat/data/curriculum_serve_ledger.json` is **deliberately absent** — see §3.1.
|
||||
|
||||
## 3. Falsified assumptions
|
||||
|
||||
| Plan assumed | Measurement showed | Evidence |
|
||||
|---|---|---|
|
||||
| "The binding constraint is ratified curriculum volume, not machinery" | Half wrong both ways. The 16-premise cap meant **no** band could earn at any volume (engineering, not content); and once fixed, the *unknown class alone* clears the floor (content is not the constraint either) | ADR-0264 §4.1; `curriculum-practice-producer-2026-07-26.md` §1 |
|
||||
| Phase 1 exits with "a real (still-unearned) ledger" | **Unreachable.** Reliability is commitment precision and a correct UNKNOWN is a commitment, so any band with ≥657 routable atoms clears θ_SERVE on non-commitments alone. A committed ledger is necessarily an earning one | #121; `conservative_floor(660,660)=0.990046` |
|
||||
| 8 of 11 bands cannot reach n=657 (`systems_software·causal` impossible at 630) | **7 of 11.** I sized bands from per-*term* exclusivity; the router's predicate is per-*pair*, which is looser. `systems_software·causal` is **720** | ADR-0264 §4.2 CORRECTED block; `BAND_ATOM_SPACE` |
|
||||
| R5 narrowing is "verdict-identical" | Identical wherever the full family was **readable**; verdict-*improving* over the cap, where full-family compilation refuses outright | ADR-0264 R5 precision note |
|
||||
| R7: the sink holds "a stale surface and a stale `trace_hash`" | `trace_hash` is **never serialized** — `chat/telemetry.py` has zero references. Only the surface half was real | #123; `test_trace_hash_is_not_in_the_wire_format_at_all` |
|
||||
| The R7 surface divergence is exercised by default | `finalize_turn_surface` is a **no-op on all 36 default-config turns probed**. It fires only under `realizer_grounded_authority` (24/84) | #123 fixture |
|
||||
| "Rerun the hash-pinned lanes under `CORE_BACKEND=rust`" measures parity | **Cannot fail.** Sabotaging every Rust kernel still yields 11/11 pins matching. Zero Rust calls in the deductive lane; exactly ONE per pipeline turn | #124; `rust-parity-measurement-2026-07-26.md` §2 |
|
||||
| Curriculum vocabulary is safe to enumerate over | `then` and `therefore` are **taught lemmas that are also the reader's control words** — 164 atoms refuse, in the Phase F target band | #121 §3 |
|
||||
|
||||
## 4. Binding constraint going into the next arc
|
||||
|
||||
**The outcome-mix ruling.** It is the single thing between a fully built license
|
||||
loop and four unearned SERVE licenses. Every mechanism now exists — producer,
|
||||
audit, reseal verb, negatives — and running `core proposal-queue reseal
|
||||
curriculum_serve --allow-new-licenses` today would license
|
||||
`philosophy_theology·{modal,contrast}`, `physics·causal` and
|
||||
`systems_software·causal` on evidence that is **99.0%–99.98% correct
|
||||
non-commitment**, which ADR-0262 §5.1 rules unacceptable and which `ClassTally`
|
||||
structurally cannot see (no verdict axis: a correct UNKNOWN is indistinguishable
|
||||
from a correct ENTAILED once tallied). Max entailed volume in any band today is
|
||||
**9**. Until mix is enforced *at the producer*, curriculum volume is not the
|
||||
constraint — the absence of a mix rule is.
|
||||
|
||||
## 5. Trigger state
|
||||
|
||||
- **Articulation depth (plan §5).** Trigger **not met, and structurally cannot
|
||||
be**: `generate/proof_chain/entail.py` decides by asking `is_tautology` on
|
||||
`(P1 ∧ … ∧ Pn) → Q`, so there are no intermediate steps to drop. The stated
|
||||
trigger describes an event that cannot occur. Recorded here because the previous
|
||||
arc left it unrecorded, which is what made it re-triggerable. The real
|
||||
deliverable remains a **feasibility study for proof-term extraction over the
|
||||
ROBDD** — not undertaken this arc, and it is a study, never a ticket.
|
||||
- **Phase F content.** Unblocked in mechanism, gated on §4's ruling. Target is
|
||||
`philosophy_theology · modal` (45,300 routable atoms), **not** `physics · modal`
|
||||
(480, impossible at any authoring volume).
|
||||
- **Phase G flag.** Not triggerable: requires an earned license, which requires §4.
|
||||
|
||||
## 6. What is NOT next, and why
|
||||
|
||||
- **Authoring `physics · modal` volume.** Ceiling 480 < 657 with every possible
|
||||
question counted. No amount of chain authoring raises it; only growing
|
||||
`en_physics_v1` would.
|
||||
- **Committing the curriculum ledger as housekeeping.** It is a ratification that
|
||||
licenses four bands (§4). #122's verb refuses by default for exactly this reason.
|
||||
- **"Repairing" the deduction ledger's distinct-evidence exposure.** SHA-sealed,
|
||||
ratified, gating a live flag. Re-sealing is Shay's. Any unit that makes
|
||||
`test_volume_honesty.py` fail has found a real signal, not a stale pin.
|
||||
- **Making Rust the default backend (plan §6B).** Its premise rests on a
|
||||
measurement that cannot fail (§3). Flipping it today changes one call per turn.
|
||||
- **Accelerating the CGA hot path before fixing the dispatch (plan §6C).** 69 call
|
||||
sites bypass `algebra.backend` entirely and every dispatch arm swallows all
|
||||
exceptions, so no lane-hash measurement can currently see whether Rust ran.
|
||||
Order: fail loudly → a test that fails when Rust is not *taken* → then route.
|
||||
- **`.metal` Cl(4,1) kernel / MLX fusion / bf16.** Explicitly refuted in prior
|
||||
arcs; unchanged.
|
||||
|
||||
## 7. Open items carried forward
|
||||
|
||||
| Item | Kind | Where it is recorded |
|
||||
|---|---|---|
|
||||
| Outcome-mix ruling (per-verdict-class volume) | **blocked on Shay** — now the binding constraint | `distinct-evidence-audit-2026-07-25.md`; #121 |
|
||||
| Band-level capability index scoring | blocked on ruling | plan §4A |
|
||||
| Discovery-yield stratification | blocked on new persisted counters | plan §4B |
|
||||
| `hash_surface` on `TurnEvent` | blocked on ruling; explicitly out of R7's scope | plan §4C; `runtime_contracts.md` |
|
||||
| Reserved-word screening (curriculum vocab vs reader grammar) | deferred; bound pinned at 2 lemmas | #121 §3 |
|
||||
| Rust dispatch fails silently; hot path bypasses it | deferred, escalated not fixed | `rust-parity-measurement-2026-07-26.md` §3 |
|
||||
| A lane case covering empty-scope→UNKNOWN (R6) | deferred — moves the `curriculum_serve_v1` pin | this brief §9 |
|
||||
| E3 ADR status vocabulary sweep (312 files) | deferred to Haiku | DIVISION-OF-WORK §5 |
|
||||
| Proof-term extraction feasibility study | untested | plan §5 |
|
||||
| `arena_queue_entry` ceremony stage | deferred (only `ledger_reseal` was built) | `teaching/ratification.py` |
|
||||
|
||||
## 8. Gates and their state at close
|
||||
|
||||
Per-branch, in-worktree, canonical **CPython 3.12.13** with `uv sync --locked`.
|
||||
Arc-start baselines: smoke 555 → **569** after Phases A+B.
|
||||
|
||||
| Gate | Command | Result at close |
|
||||
|---|---|---|
|
||||
| smoke | `uv run core test --suite smoke -q` | #121 **571** · #122 571 · #123 **591** · #124 **575** · #125 **593** |
|
||||
| deductive | `uv run core test --suite deductive -q` | #121 **310** · #122 **327** · #123 291 · #124 291 · #125 **332** |
|
||||
| lane pins | `scripts/verify_lane_shas.py` | **11/11** on every branch; no pin moved in this arc |
|
||||
| curriculum lane | `python -m evals.curriculum_serve.runner` | `n=32 correct=32 wrong=0 anti_recall=5` throughout |
|
||||
| cargo | `PYO3_PYTHON=… cargo test --offline` | **43 passed / 0 failed** |
|
||||
| sink suites | 7 files, unchanged | **80 passed** under #123 |
|
||||
|
||||
Every count is `baseline + exactly the tests that branch adds`; the arithmetic is
|
||||
in each PR body. Mutation checks were run on all five gate-bearing units.
|
||||
|
||||
## 9. Ground truth corrections for the next opener
|
||||
|
||||
**Read §3 before the plan.** The plan of record is now wrong in five places and
|
||||
carries an `AMENDED` block for four of them; ADR-0264 §4.2 carries a `CORRECTED`
|
||||
block for the fifth. Original text is preserved everywhere — nothing was rewritten
|
||||
to look right in hindsight.
|
||||
|
||||
**Two things I got wrong that are worth internalizing as patterns, not incidents.**
|
||||
|
||||
1. **I sized a question space from the wrong predicate** (per-term exclusivity vs
|
||||
per-pair routability) and shipped a table of eleven ceilings with one wrong
|
||||
verdict in it. The fix was not cleverness — it was asking the *router* instead
|
||||
of reimplementing its rule. `evals/curriculum_serve/practice/generator.py` now
|
||||
calls `resolve_domain` rather than restating routability, and the ceilings are
|
||||
pinned as measured values.
|
||||
2. **I wrote an assertion spec against a field that is not serialized.** The E1
|
||||
spec asserted a stale `trace_hash` in the durable stream; `chat/telemetry.py`
|
||||
never wrote one. Specifying assertions before reading the wire format is the
|
||||
error, and it survived until implementation because a spec has no gate.
|
||||
|
||||
**The load-bearing test-design lesson of this arc:** three separate times, the
|
||||
obvious measurement would have passed while proving nothing — the R7 fixture under
|
||||
the default config (`finalize_turn_surface` no-ops), the Rust lane parity
|
||||
(sabotage-proof), and the R8 depth check (needed an affirmative control). Each was
|
||||
caught only by asking "what would this look like if the thing I am testing were
|
||||
absent?" Ask that of every new pin. `test_the_pipeline_really_does_override_the_
|
||||
sealed_surface` and `test_e2e_an_affirmative_row_in_the_same_slot_WOULD_create_
|
||||
that_path` exist purely to keep their siblings from going vacuous, and both should
|
||||
be preserved if those files are ever refactored.
|
||||
|
||||
**Stale reasoning still in the tree, named because nobody greps for it:**
|
||||
|
||||
- `evals/curriculum_serve/practice/runner.py` docstring explains why the ledger is
|
||||
uncommitted. If the mix ruling lands and the ledger is committed, that docstring
|
||||
and `test_curriculum_ledger_is_not_committed` must be updated **together** —
|
||||
the test is deliberately written to fail loudly rather than let the file appear
|
||||
as housekeeping.
|
||||
- `teaching/ratification.py`'s module docstring still says every one of the eleven
|
||||
bands "is 24×–73× short of the entailed-bucket floor." That framing predates
|
||||
R5 and §4 above; the shortfall is real but the mechanism named for it is not.
|
||||
- `tests/test_curriculum_practice.py::test_gold_mix_has_no_refuted_class` is a
|
||||
statement about **content**, not machinery, as of #125. Polarity works; no
|
||||
negative row is committed. Phase F should update that pin deliberately when it
|
||||
authors one.
|
||||
- The R6 empty-scope path (52.7% of the question space) is guarded by exactly
|
||||
**one** test, `test_empty_scope_is_unknown_not_declined`, and **not** by the
|
||||
lane: 0 of 32 lane cases exercise it (all 12 `unknown` cases have non-empty
|
||||
scope; the 6 with `scope_size == 0` decline before scope is computed). Verified
|
||||
by mutation. Adding a lane case is a small, deliberate act that moves the
|
||||
`curriculum_serve_v1` pin — which is why it was not bolted onto a PR that
|
||||
asserts the pin is unchanged.
|
||||
|
|
@ -10,6 +10,50 @@ a memory or a chat instruction, the plan of record and `AGENTS.md` win.
|
|||
|
||||
---
|
||||
|
||||
## 0b. Status 2026-07-26 — every code unit in this arc is open as a PR
|
||||
|
||||
Superseding §0 below (kept for the reasoning, which still holds). All units are
|
||||
**open, unmerged, awaiting Shay's authorization.**
|
||||
|
||||
| unit | PR | branch | state |
|
||||
|---|---|---|---|
|
||||
| E2 rename | #119 | — | **MERGED** |
|
||||
| R5–R7 query-scoped premises | #120 | — | **MERGED** |
|
||||
| **C** practice producer | **#121** | `feat/curriculum-practice-producer` | open |
|
||||
| **D** `proposal-queue reseal` | **#122** | `feat/proposal-queue-reseal` (on #121) | open |
|
||||
| **E1** code half (audit-ledger R7) | **#123** | `feat/audit-ledger-r7` | open |
|
||||
| **parity** measurement + `core rust build` fix | **#124** | `fix/rust-build-env-and-parity-report` | open |
|
||||
| **polarity** R1–R4/R8 | **#125** | `feat/curriculum-polarity` (on #121) | open |
|
||||
| doc reconciliation + arc close | this branch | `docs/arc-reconciliation` | open |
|
||||
|
||||
Merge order: **#121 first** (#122 and #125 stack on it; retarget both to `main`
|
||||
after it lands). #123 and #124 are independent of everything. Merge-commit, not
|
||||
squash. #122 and #125 both touch `core/cli_proposal_queue.py` in different hunks.
|
||||
|
||||
Still Shay's, unchanged: **Phase F** content (`philosophy_theology · modal`),
|
||||
**Phase G** the flag, **E3** the ADR vocab sweep (Haiku), and the four open
|
||||
rulings — of which **outcome mix is now blocking rather than academic** (#121).
|
||||
|
||||
**What the units found that the plan did not predict** — all four are in the PRs
|
||||
and the research notes, listed here because a status table is where someone looks:
|
||||
|
||||
1. **A committed curriculum ledger is necessarily an EARNING ledger.** The plan's
|
||||
Phase-1 exit criterion ("a real, still-unearned ledger") is unreachable: a
|
||||
band clears θ_SERVE on correct NON-COMMITMENTS alone, so sealing licenses four
|
||||
bands on ~99% non-entailed evidence. Hence #121 ships the writer and commits
|
||||
no artifact, and #122's verb refuses to grant a license without an explicit
|
||||
flag.
|
||||
2. **§4.2's ceiling table was understated** (per-term vs per-pair routability);
|
||||
`systems_software · causal` is reachable, not impossible. Four bands can reach
|
||||
657, not three. ADR-0264 §4.2 now carries the correction.
|
||||
3. **`then` and `therefore` are taught lemmas that collide with the argument
|
||||
reader's control grammar** — 164 atoms refuse, in the Phase F target band. The
|
||||
vocabulary boundary is never screened against the reader's grammar.
|
||||
4. **The Rust lane-parity method cannot fail.** Sabotaging every Rust kernel
|
||||
still yields 11/11 lane pins matching, so §6B's premise needs re-earning.
|
||||
|
||||
---
|
||||
|
||||
## 0. Status at handoff — 2026-07-25, Opus units complete
|
||||
|
||||
The three Opus units are done and pushed. **Read the plan of record's AMENDED
|
||||
|
|
@ -35,6 +79,9 @@ remaining work different from §4 as originally written:
|
|||
building Phase C first would produce a correct instrument reporting that every
|
||||
band is at its ceiling. R5 is fully specified and verified verdict-identical
|
||||
over 8,520 questions — it is a loud unit (the physics lane pins every verdict).
|
||||
(Precisely: identical wherever the full family was READABLE, and
|
||||
verdict-*improving* over the cap, where full-family compilation refuses
|
||||
outright. See ADR-0264 R5's precision note.)
|
||||
2. **Phase F retargets to `philosophy_theology · modal`.** `physics · modal` has a
|
||||
hard ceiling of 480 against a 657 threshold. Do not author physics modal volume.
|
||||
3. **Phase C's producer must call the Phase B audit.** `AUDIT_SOURCES` in
|
||||
|
|
@ -97,7 +144,7 @@ and escalate (§6). That is not a failure — it is the mechanism working.
|
|||
| Volume-honesty invariant (tests first) | B | **Opus** ✅ | silent |
|
||||
| R7 assertion — *what* to assert | E1 | **Opus** ✅ | silent |
|
||||
| Articulation feasibility study | §6 of plan | **Opus** | silent |
|
||||
| `assert_corpus_sound` rename | E2 | **Sonnet** | loud |
|
||||
| `assert_corpus_sound` rename | E2 | **Sonnet** ✅ #119 | loud |
|
||||
| **Query-scoped premise compilation (R5–R7)** | **new, gates C/D/F** | **Sonnet** | loud |
|
||||
| Practice producer implementation | C | **Sonnet** | loud |
|
||||
| `core proposal-queue reseal` verb | D | **Sonnet** | loud |
|
||||
|
|
@ -190,6 +237,12 @@ design decision, that is the signal in §6.
|
|||
third `assert_corpus_sound` caller and renaming after that is strictly more work.
|
||||
R5–R7 second because nothing downstream can earn anything until it lands (§0).
|
||||
|
||||
> **Both landed (#119, #120), so this ordering constraint is spent.** The names are
|
||||
> now `assert_practice_gold_sound` (no args, practice gold) and
|
||||
> `assert_lane_cases_sound(domain, cases)` (lane contract); Phase C added its
|
||||
> caller after the rename, as intended. Remaining units are order-independent
|
||||
> except for the stacking recorded in §0b.
|
||||
|
||||
### R5–R7. Query-scoped premise compilation — **do this before C and D**
|
||||
|
||||
`teaching/curriculum_premises.py::compile_premises` emits *every* chain in the
|
||||
|
|
@ -210,7 +263,10 @@ family, and `read_verb_argument` refuses past `MAX_PREMISE_SENTENCES = 16`. So a
|
|||
**Why this is loud, and why it is not the ADR-0261 §5.1 premise-dropping sin.**
|
||||
Narrowing is verdict-*identical*, not merely sound: each compiled premise mints one
|
||||
independent propositional atom, so a scope containing the query atom decides the
|
||||
query exactly as the full family does. Verified over 8,520 routable questions with
|
||||
query exactly as the full family does — **wherever the full family was readable.**
|
||||
Over the cap it is verdict-*improving*: full-family compilation refuses
|
||||
`compiled_premises_unreadable` there, so the narrowed scope answers questions the
|
||||
unscoped compiler could not. That is the unblock, not a deviation from it. Verified over 8,520 routable questions with
|
||||
zero mismatches (`docs/research/curriculum-premise-scope-2026-07-25.md` probe 3).
|
||||
Gold is preserved: physics stays `entailed 14 / unknown 12 / declined 6`.
|
||||
|
||||
|
|
@ -218,8 +274,9 @@ Gold is preserved: physics stays `entailed 14 / unknown 12 / declined 6`.
|
|||
`tests/test_curriculum_serve.py`. If any verdict moves, stop — the equivalence
|
||||
argument has a hole and that is escalation §6.3.
|
||||
|
||||
### E2. `assert_corpus_sound` rename
|
||||
Two functions, one name: `evals/deduction_serve/practice/gold.py:1163` (no args,
|
||||
### E2. `assert_corpus_sound` rename — **DONE, #119**
|
||||
Renamed to `assert_practice_gold_sound` / `assert_lane_cases_sound`. Two
|
||||
functions, one name: `evals/deduction_serve/practice/gold.py:1163` (no args,
|
||||
practice corpus) and `evals/curriculum_serve/runner.py:71` (`domain, cases`, lane
|
||||
contract). Not a missing contract — a name collision, flagged in
|
||||
`BRIEF-CLOSE-assessment-verification-2026-07-25.md` §9.5. **Gate:** imports break.
|
||||
|
|
|
|||
|
|
@ -158,7 +158,9 @@ absent one.
|
|||
`docs/specs/runtime_contracts.md:448-456`). Repairs the stale surface and
|
||||
stale `trace_hash` together. Default sink is `None`, so no deployment risk.
|
||||
Independent of the `hash_surface`-on-`TurnEvent` ruling.
|
||||
- **E2 — `assert_corpus_sound` name collision.** Two functions, one name:
|
||||
- **E2 — `assert_corpus_sound` name collision.** ✅ **DONE (#119)** — now
|
||||
`assert_practice_gold_sound` (no args, practice gold) and
|
||||
`assert_lane_cases_sound(domain, cases)` (lane contract). Two functions, one name:
|
||||
`evals/deduction_serve/practice/gold.py:1163` (no args, practice corpus) vs
|
||||
`evals/curriculum_serve/runner.py:71` (`domain, cases`, lane contract). Must
|
||||
land **before** Phase C adds a third caller.
|
||||
|
|
|
|||
|
|
@ -156,7 +156,8 @@ implement without re-litigating epistemology.
|
|||
4. **Independent oracle** — per subject, a closed-world reachability
|
||||
oracle over the chain corpus (sharing no code with the serving path)
|
||||
validates every gold verdict; the lane asserts corpus soundness
|
||||
before any case runs (the `assert_corpus_sound()` pattern).
|
||||
before any case runs (the `assert_corpus_sound()` pattern — since #119 split
|
||||
into `assert_practice_gold_sound` / `assert_lane_cases_sound`).
|
||||
5. **License granularity** — bands keyed by (subject × relation family ×
|
||||
chain depth), earned in the ADR-0199 arena: θ_SERVE=0.99, n≥720,
|
||||
wrong=0, sealed + SHA-verified ledger per subject.
|
||||
|
|
|
|||
|
|
@ -227,8 +227,14 @@ def compile_premises(
|
|||
probe 3). If term incidence would still exceed the reader's
|
||||
:data:`MAX_PREMISE_SENTENCES` cap, narrow further to the **query-atom
|
||||
rows** — chains whose ``(subject, connective, obj)`` exactly match the
|
||||
query's — which stays verdict-identical for the same reason. Scope is
|
||||
never truncated arbitrarily and never refused for size.
|
||||
query's. Scope is never truncated arbitrarily and never refused for size.
|
||||
|
||||
Precisely: narrowing is verdict-**identical** wherever the full family was
|
||||
readable, and verdict-**improving** where it was not. In the over-cap branch
|
||||
full-family compilation would refuse ``compiled_premises_unreadable`` and
|
||||
answer nothing at all, so the narrowed scope answers questions the unscoped
|
||||
compiler could not — which is the unblock this exists for, not a deviation
|
||||
from it.
|
||||
|
||||
Deterministic: the same curriculum, family and query always compile to
|
||||
the same sentences in the same order, so a lane report over them is
|
||||
|
|
|
|||
Loading…
Reference in a new issue