P13-S19: what a partial measure actually costs

Filed as a deferral -- pickups unmodelled -- it is closer to a live defect, and
the tree already held the proof. m35 placed a first measure at offset 0 and its
successor half a whole note later under a whole-note signature and asserted
invariant 20 fires. That is a pickup. The test has been labelled "wrong distance"
since packet 2. create_measure applies the same rule as a refusal, now observed
end to end rather than cited: the successor comes back NoOp with
MeasureMeterMismatch. Authoring a pickup does not leave it unmodelled; it makes
the rest of the instance unauthorable.

Both refusals carry the same reason code, so the fixture is the only thing
separating them. Pickup and successor both declare None, which keeps clause 2
from running on either side and makes the observed refusal provably clause 3's.
The pickup's own mint is asserted Applied before the successor's NoOp, because a
fixture whose operations never execute produces a non-Applied result
indistinguishable from a refusal.

The exemption is narrower than every document said. A first measure escapes only
the predecessor-dependent checks -- invariant 20's boundary clause, and
create_measure's clauses 1 and 3 -- plus agreement when it declares None or a
matching signature, and only when its other preconditions hold. It can still be
refused for a dead parent or an unresolving anchor referent, and invariant 10 can
still flag it. Seven surfaces carried the loose form; one had hardened into
falsehood, claiming all three clauses are vacuous for a first measure when
clause 2 has no predecessor dependency at all.

core/DECISIONS.md is deliberately untouched. It already said "never flagged by
the boundary clause" -- the one site that drew the distinction correctly -- and
an earlier contract draft listed it as defective by matching the phrase without
reading its qualifier. The corrected ops entry now quotes that qualifier, and a
positive gate check protects it.

A mid-score partial enters successfully and its successor fails, so the scope is
boundaries following any partial measure, not partial measures. The root cause is
a missing quantity rather than a missing exemption: both rules compare the
start-to-start distance against the governing signature's full measure_duration
when it actually equals the predecessor's own content duration. Introducing that
quantity is a semantic rung; this one stops at its edge, with both function
bodies byte-identical.

P13-S24 is filed for the Chapter 3 splitter deferral, which shares the missing
partial-duration concept and is otherwise independent.

Executed against spec/CONTRACT_P13S19_PARTIAL.md, four mutations.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QjsEnYhm1gPpf6ii2iFxFV

crates/epiphany-core/src/graph.rs

@@ -596,7 +596,15 @@ impl Voice {
 /// comparison or delta they need is not computable (contract pin 7): this is
 /// deliberate, not a safety property, because base-ingested data may predate
 /// the rule. Pickup/anacrusis (a partial first measure) is deferred
-/// (P13-S19) and is never refused or flagged by this rung.
+/// (P13-S19): a first measure skips only the predecessor-dependent checks
+/// — invariant 20's boundary clause and `create_measure`'s clauses 1 and 3
+/// — plus the agreement check when it declares `None` or a matching
+/// signature; it can still be refused for other reasons (a dead parent, an
+/// unresolving referent). Its own successor is unaffected by any of this:
+/// the successor is measured against the governing signature's full
+/// `measure_duration()` regardless, and is refused (`MeasureMeterMismatch`)
+/// and flagged by invariant 20 when the pickup's actual length is shorter
+/// than a full bar.
 #[derive(Clone, PartialEq, Eq, Debug)]
 pub struct Measure {
     pub id: MeasureId,

crates/epiphany-core/src/invariants.rs

@@ -108,8 +108,12 @@ pub enum GraphInvariant {
     ///     comparable relation or pin 6b's musical delta cannot decide the
     ///     comparison (base-ingested data may predate the rule); this is
     ///     deliberate abstention, not a soundness gap (pin 7). A
-    ///     pickup/anacrusis first measure has no predecessor and is never
+    ///     pickup/anacrusis first measure has no predecessor for the
-    ///     flagged (P13-S19, deferred).
+    ///     boundary clause, which is vacuous for it; the agreement clause
+    ///     has no such exemption and still applies. Its successor is
+    ///     measured against the governing signature's full
+    ///     `measure_duration()` and can be refused and flagged (P13-S19,
+    ///     deferred).
     MeasureMeterConsistency,
 }
 
@@ -4756,15 +4760,34 @@ mod g3b_measure20_tests {
         );
     }
 
-    /// M35: removing the boundary clause must let this go undetected. Both
+    /// M35: this IS the pickup/anacrusis demonstration (spec/CONTRACT_P13S19_
+    /// PARTIAL.md pin 1). `m0` is a first measure occupying only half a bar
+    /// -- a pickup -- and by itself is flagged by neither clause: it has no
+    /// predecessor, so the boundary clause is vacuous, and it avoids the
+    /// agreement clause here by declaring `None` (not by any first-measure
+    /// exemption -- there is none). `m1` is its successor, comparable and
+    /// correctly ordered, but only HALF a `measure_duration` away -- the
+    /// pickup's own actual length, not the governing signature's full bar.
+    /// Removing the boundary clause must let THAT go undetected. Both
     /// measures avoid the agreement clause (`None`) so only boundary can
     /// fire.
     #[test]
-    fn m35_boundary_flags_wrong_distance() {
+    fn m35_pickup_successor_boundary_flags_wrong_distance() {
         let replica = ReplicaId(7);
         let (active, ts_active) = sig(replica, 1);
         let region = probe_region_id();
         let m0 = measure_at(MeasureId::new(replica, 10), region, 0, None);
+
+        // The pickup by itself: a first measure has no predecessor, so the
+        // boundary clause is vacuous for it, and `None` separately avoids
+        // the agreement clause -- neither is an exemption granted TO the
+        // agreement clause itself (pin 1).
+        let (lone, _) = score_with(Some(active), vec![ts_active.clone()], vec![m0.clone()]);
+        assert!(
+            !fires(&lone, GraphInvariant::MeasureMeterConsistency),
+            "the pickup by itself, first measure, no predecessor, must not be flagged"
+        );
+
         // Half a whole note later — not a full measure_duration away.
         let m1 = Measure {
             id: MeasureId::new(replica, 11),
@@ -4855,20 +4878,26 @@ mod g3b_measure20_tests {
         );
     }
 
-    /// M38: a pickup (partial) first measure must never be flagged -- it
+    /// M38: a pickup (partial) first measure declaring no time signature
-    /// has no predecessor, so the boundary clause is vacuous for it.
+    /// must never be flagged BY THE BOUNDARY CLAUSE -- it has no
+    /// predecessor, so that clause is vacuous for it. This is narrower than
+    /// "never flagged" in general: the agreement clause is not
+    /// predecessor-dependent and would apply to this same measure if it
+    /// declared a disagreeing signature instead of `None` (spec/CONTRACT_
+    /// P13S19_PARTIAL.md pin 1) -- this fixture's `None` avoids agreement
+    /// separately, not as a consequence of being a first measure.
     ///
     /// **On the mutation's failure mode:** the M38 mutation (removing the
     /// `if i == 0 { continue; }` guard in `check_measure_meter_consistency`)
     /// is observed as an `attempt to subtract with overflow` PANIC, not a
     /// wrong-flag assertion failure. This is expected and still a valid red
     /// signal, not a weak one: that `i == 0` guard is simultaneously the
-    /// pickup-measure exemption AND the only thing standing between `i - 1`
+    /// pickup-measure boundary-clause exemption AND the only thing standing
-    /// and a `usize` underflow, so any mutation that removes or weakens it
+    /// between `i - 1` and a `usize` underflow, so any mutation that removes
-    /// crashes before it could ever produce a wrong (but well-formed)
+    /// or weakens it crashes before it could ever produce a wrong (but
-    /// verdict to assert against.
+    /// well-formed) verdict to assert against.
     #[test]
-    fn m38_pickup_first_measure_not_flagged() {
+    fn m38_pickup_first_measure_boundary_clause_not_flagged() {
         let replica = ReplicaId(7);
         let (active, ts_active) = sig(replica, 1);
         let region = probe_region_id();
@@ -4888,7 +4917,9 @@ mod g3b_measure20_tests {
         let (score, _) = score_with(Some(active), vec![ts_active], vec![m0]);
         assert!(
             !fires(&score, GraphInvariant::MeasureMeterConsistency),
-            "a lone first (pickup) measure must never be flagged by invariant 20"
+            "a lone first (pickup) measure declaring no time signature must not be flagged \
+             by invariant 20's boundary clause -- vacuous, no predecessor (its agreement \
+             clause is separately avoided by `None`, not exempted by being first)"
         );
     }
 
@@ -4919,10 +4950,11 @@ mod g3b_measure20_tests {
     // clauses = 18 cells) plus the four non-shape-driven paths (A1, A3, B2,
     // B3) that pin 4's shapes do not themselves exercise. A2 and B1 reuse
     // `m39_unresolvable_reference_is_invariant_10_only` and
-    // `m38_pickup_first_measure_not_flagged` above respectively; S3 reuses
+    // `m38_pickup_first_measure_boundary_clause_not_flagged` above
-    // `m34_agreement_flags_disagreement` and `m35_boundary_flags_wrong_
+    // respectively; S3 reuses `m34_agreement_flags_disagreement` and
-    // distance` above (Region same id, same edge, Musical offsets is
+    // `m35_pickup_successor_boundary_flags_wrong_distance` above (Region
-    // exactly their shape). Every other cell gets a dedicated fixture below.
+    // same id, same edge, Musical offsets is exactly their shape). Every
+    // other cell gets a dedicated fixture below.
     // -------------------------------------------------------------------
 
     /// Matrix cell A1: `m.time_signature` is `None` -- inapplicable, not

crates/epiphany-ops/DECISIONS.md

@@ -2157,11 +2157,19 @@ and strictly after it (`MeasureOutOfOrder`, or `MeasureOrderUnverifiable` if
 incomparable); agreement against the effective grid's active signature
 (`MeasureMeterMismatch`); and the boundary distance from the predecessor
 equals the governing `measure_duration()` (`MeasureMeterMismatch`, or
-`MeasureOrderUnverifiable` if the delta is not computable). All three
+`MeasureOrderUnverifiable` if the delta is not computable). Clauses 1
-clauses are vacuous for an instance's first measure — no predecessor to
+(ordering) and 3 (boundary distance) are vacuous for an instance's first
-compare against — which is the pickup/anacrusis deferral filed as
+measure — no predecessor to compare against. Clause 2 (agreement) has **no**
-**P13-S19**, open by design (core `DECISIONS.md` files the invariant-side
+predecessor dependency and runs on a first measure exactly as on any other:
-mirror). `CreateMeasure` fails **closed** on every incomputable case; graph
+a pickup declaring a signature that disagrees with the governing grid is
+refused by clause 2 alone, first measure or not. And clause 3's exemption is
+narrower than "vacuous" suggests: the pickup's *own successor* is measured
+against the governing signature's full `measure_duration()`, not the
+pickup's own (shorter) length, so `create_measure` refuses that successor
+too. This is the pickup/anacrusis deferral filed as **P13-S19**, open by
+design (core `DECISIONS.md` files the invariant-side mirror, correctly
+scoped to "never flagged **by the boundary clause**" — not never flagged at
+all). `CreateMeasure` fails **closed** on every incomputable case; graph
 invariant 20 (core `DECISIONS.md`) **abstains** on the identical cases —
 deliberately opposite postures, not an inconsistency.
 

crates/epiphany-ops/src/reduce.rs

@@ -19832,6 +19832,246 @@ mod tests {
         );
     }
 
+    /// Pin 4 (spec/CONTRACT_P13S19_PARTIAL.md): a pickup's successor is
+    /// refused end-to-end, not merely read off the reducer's source. The
+    /// pickup itself — first measure of the instance, `time_signature:
+    /// None` so the agreement clause (clause 2, which is NOT
+    /// predecessor-dependent) is avoided by declaration rather than by any
+    /// first-measure exemption — mints `Applied`: clauses 1 and 3 are
+    /// vacuous for it (no predecessor). Its successor, ALSO declaring
+    /// `time_signature: None` (so its own clause 2 is out of the way and
+    /// the refusal below cannot be clause 2's), starts only HALF a
+    /// `measure_duration` after the pickup — the pickup's own actual
+    /// (unmodelled) content length, not the governing signature's full
+    /// whole-note bar — and clause 3 refuses it: `MeasureMeterMismatch`.
+    /// The governing signature's own write and the pickup's mint are both
+    /// asserted `Applied` before the refusal is asserted, so envelope
+    /// counter gaps cannot make either op silently pending and pass the
+    /// refusal off as something it isn't.
+    #[test]
+    fn g3b_create_measure_pickup_successor_refused_end_to_end() {
+        let region = RegionId::new(ReplicaId(1), 90);
+        let instance = StaffInstanceId::new(ReplicaId(1), 91);
+        let staff = StaffId::new(ReplicaId(1), 92);
+        let mut envs = g3b_region_and_instance_envs(1, region, instance, staff);
+
+        let sig_a = TimeSignatureId::new(ReplicaId(1), 93);
+        // numerator 4 -> measure_duration = 4/4 = one whole note ("a full bar").
+        let set_sig_a = prim_env(
+            1,
+            2,
+            2,
+            CausalContext::new(),
+            OperationKind::SetTimeSignature(SetTimeSignatureOp {
+                region,
+                anchor: g3b_region_anchor(region, 0),
+                time_signature: Some(crate::valuegen::time_signature(sig_a, 4)),
+            }),
+        );
+        envs.push(set_sig_a.clone());
+
+        fn measure(id: u64, start: TimeAnchor, sig: Option<TimeSignatureId>) -> Measure {
+            Measure {
+                id: MeasureId::new(ReplicaId(1), id),
+                start,
+                time_signature: sig,
+                explicit_number: None,
+                number_visibility: epiphany_core::MeasureNumberVisibility::Auto,
+            }
+        }
+
+        // The pickup: first measure, `None` (pin 4's fixture constraint —
+        // `Some` of a disagreeing signature would be refused by clause 2
+        // instead, for a reason that has nothing to do with partiality).
+        let pickup = g3b_measure_env(
+            1,
+            3,
+            3,
+            instance,
+            measure(400, g3b_region_anchor(region, 0), None),
+        );
+
+        // The successor: also `None`, so ITS clause 2 is equally out of the
+        // way. Half a whole note after the pickup — not the full bar sig_a
+        // demands.
+        let successor = g3b_measure_env(
+            1,
+            4,
+            4,
+            instance,
+            measure(
+                401,
+                TimeAnchor::Region {
+                    id: region,
+                    edge: RegionEdge::Start,
+                    offset: AnchorOffset::Musical(MusicalDuration(
+                        RationalTime::new(1, 2).unwrap(),
+                    )),
+                },
+                None,
+            ),
+        );
+
+        envs.extend([pickup.clone(), successor.clone()]);
+        let mut set = OperationSet::new();
+        set.accept_all(envs);
+        let state = set.reduce();
+
+        assert_eq!(
+            g3b_effect_of(&state, set_sig_a.id),
+            Some(OperationEffect::Applied),
+            "the governing signature must itself be applied, or the refusal below proves nothing"
+        );
+        assert_eq!(
+            g3b_effect_of(&state, pickup.id),
+            Some(OperationEffect::Applied),
+            "pin 1: the pickup itself is neither refused nor flagged — clauses 1 and 3 are \
+             vacuous for a first measure, and clause 2 is avoided here by declaring `None`, \
+             not by any first-measure exemption"
+        );
+        assert_eq!(
+            g3b_effect_of(&state, successor.id),
+            Some(OperationEffect::NoOp {
+                reason: NoOpReason::PreconditionFailedUnderReduction {
+                    reason: PreconditionFailureReason::MeasureMeterMismatch
+                }
+            }),
+            "pin 4: the pickup's successor is measured against the governing signature's FULL \
+             measure_duration (one whole note), not the pickup's own half-note actual length — \
+             clause 3 refuses it MeasureMeterMismatch, and (both sides declaring `None`) this \
+             refusal cannot be clause 2's"
+        );
+    }
+
+    /// Pin 2 (spec/CONTRACT_P13S19_PARTIAL.md): a mid-score partial measure
+    /// — index >= 1, so it has no first-measure exemption at all — enters
+    /// successfully, because the boundary check run when IT is created only
+    /// examines the distance from ITS predecessor (`m0`, a full measure),
+    /// never its own eventual length. The failure surfaces one measure
+    /// later, on `m1`'s own successor (`m2`), whose distance from `m1`
+    /// exposes `m1`'s actual (partial) length against the same governing
+    /// signature's full `measure_duration()`.
+    #[test]
+    fn g3b_create_measure_mid_score_partial_successor_refused_end_to_end() {
+        let region = RegionId::new(ReplicaId(1), 94);
+        let instance = StaffInstanceId::new(ReplicaId(1), 95);
+        let staff = StaffId::new(ReplicaId(1), 96);
+        let mut envs = g3b_region_and_instance_envs(1, region, instance, staff);
+
+        let sig_a = TimeSignatureId::new(ReplicaId(1), 97);
+        // numerator 4 -> measure_duration = 4/4 = one whole note.
+        let set_sig_a = prim_env(
+            1,
+            2,
+            2,
+            CausalContext::new(),
+            OperationKind::SetTimeSignature(SetTimeSignatureOp {
+                region,
+                anchor: g3b_region_anchor(region, 0),
+                time_signature: Some(crate::valuegen::time_signature(sig_a, 4)),
+            }),
+        );
+        envs.push(set_sig_a.clone());
+
+        fn measure(id: u64, start: TimeAnchor, sig: Option<TimeSignatureId>) -> Measure {
+            Measure {
+                id: MeasureId::new(ReplicaId(1), id),
+                start,
+                time_signature: sig,
+                explicit_number: None,
+                number_visibility: epiphany_core::MeasureNumberVisibility::Auto,
+            }
+        }
+
+        // m0: an ordinary, FULL first measure — not itself a pickup, so
+        // this scenario cannot be mistaken for pin 4's first-measure case.
+        let m0 = g3b_measure_env(
+            1,
+            3,
+            3,
+            instance,
+            measure(410, g3b_region_anchor(region, 0), None),
+        );
+
+        // m1: index 1, one full measure_duration after m0 — enters
+        // successfully. This validates m0's implied length (full), NOT
+        // m1's own eventual length; nothing examines that until m1 gets a
+        // successor of its own. m1 is the mid-score partial: it has no
+        // exemption from clauses 1/3 (it HAS a predecessor), it merely
+        // happens to satisfy them here because m0 was full.
+        let m1 = g3b_measure_env(
+            1,
+            4,
+            4,
+            instance,
+            measure(
+                411,
+                TimeAnchor::Region {
+                    id: region,
+                    edge: RegionEdge::Start,
+                    offset: AnchorOffset::Musical(MusicalDuration(RationalTime::from_int(1))),
+                },
+                None,
+            ),
+        );
+
+        // m2: m1's successor, only HALF a measure_duration after m1 — m1's
+        // own actual (partial) length, not sig_a's full bar. This is where
+        // the partial duration surfaces, on the measure AFTER the partial
+        // one, exactly as pin 2 describes.
+        let m2 = g3b_measure_env(
+            1,
+            5,
+            5,
+            instance,
+            measure(
+                412,
+                TimeAnchor::Region {
+                    id: region,
+                    edge: RegionEdge::Start,
+                    offset: AnchorOffset::Musical(MusicalDuration(
+                        RationalTime::new(3, 2).unwrap(),
+                    )),
+                },
+                None,
+            ),
+        );
+
+        envs.extend([m0.clone(), m1.clone(), m2.clone()]);
+        let mut set = OperationSet::new();
+        set.accept_all(envs);
+        let state = set.reduce();
+
+        assert_eq!(
+            g3b_effect_of(&state, set_sig_a.id),
+            Some(OperationEffect::Applied),
+            "the governing signature must itself be applied, or nothing below proves anything"
+        );
+        assert_eq!(
+            g3b_effect_of(&state, m0.id),
+            Some(OperationEffect::Applied),
+            "m0: an ordinary full first measure"
+        );
+        assert_eq!(
+            g3b_effect_of(&state, m1.id),
+            Some(OperationEffect::Applied),
+            "pin 2: a mid-score partial measure enters successfully — its creation only checks \
+             the distance from ITS predecessor (m0, full), never its own eventual length"
+        );
+        assert_eq!(
+            g3b_effect_of(&state, m2.id),
+            Some(OperationEffect::NoOp {
+                reason: NoOpReason::PreconditionFailedUnderReduction {
+                    reason: PreconditionFailureReason::MeasureMeterMismatch
+                }
+            }),
+            "pin 2: m1's successor is what exposes the partial duration — measured against the \
+             governing signature's full measure_duration, not m1's own half-note actual length. \
+             m1 has NO first-measure exemption (index 1, it HAS a predecessor); it simply \
+             satisfied clause 3 because m0 happened to be full"
+        );
+    }
+
     /// Repair 2 (spec/CONTRACT_GENESIS_G3B_MEASURE.md pin 6c case 1 / pin 7):
     /// creating a measure against a WHOLLY EMPTY effective grid — no
     /// `local_metric_grid`, no region `default_metric_grid`, and no

spec/CONTRACT_P13S19_PARTIAL.md

@@ -1,6 +1,6 @@
 # Contract — P13-S19: what a partial measure actually costs
 
-**Status:** DRAFT.
+**Status:** RATIFIED.
 
 **Rung type:** correction and observation. **No behaviour change.** Not one
 graph's invariant-20 verdict may move, and not one operation's effect may
@@ -13,7 +13,8 @@ change. The rung makes the tree say what it already does.
 Read out of the working tree at `339269b`, not recalled.
 
 1. **An existing test is already the pickup demonstration.**
-   `m35_boundary_flags_wrong_distance` (`invariants.rs`) places `m0` at region
+   `m35_boundary_flags_wrong_distance` (`invariants.rs`, renamed by this rung
+   to `m35_pickup_successor_boundary_flags_wrong_distance`) places `m0` at region
    start offset `0` and `m1` at offset `Musical(1/2)`, under a signature whose
    `measure_duration()` is a **whole** (`sig()`, `:4597`), and asserts invariant
    20 **fires**. That is a first measure occupying half a bar followed by its
@@ -41,7 +42,7 @@ Read out of the working tree at `339269b`, not recalled.
    | c | `spec/operation_catalog.tex:1678` | "never refused or flagged on this account" |
    | d | `spec/core_spec.tex:6632`–`:6633` | "has no predecessor and is never flagged" |
    | e | `crates/epiphany-core/src/invariants.rs:111`–`:112` | the **public doc comment** on `GraphInvariant::MeasureMeterConsistency`, same form |
-   | f | `m38_pickup_first_measure_not_flagged` | its **name**, its comment, and its assertion message ("must never be flagged by invariant 20") |
+   | f | `m38_pickup_first_measure_not_flagged` (renamed by this rung to `m38_pickup_first_measure_boundary_clause_not_flagged`) | its **name**, its comment, and its assertion message ("must never be flagged by invariant 20") |
    | g | `crates/epiphany-ops/DECISIONS.md:2161` | **"All three clauses are vacuous for an instance's first measure — no predecessor to compare against."** This is not understatement, it is **false**: clause 2 has no predecessor dependency and runs |
 
    Rows **d, e, f** were **absent from the ratified scope**, which named the

spec/PASS13_CANDIDATES.md

@@ -96,7 +96,8 @@ visible — a value with a wire form and no canonical carrier to reach it.)
 | P13-S16 | **`StaffGroup.members` and `Staff.group` may disagree in both directions, and nothing detects it.** The two fields encode the same relation twice. `Staff.group` (`core_spec.tex:5578`, `graph.rs:819`) names the group a staff belongs to; `StaffGroup.members` (`core_spec.tex:4231`, `graph.rs:1614`) lists the staves in a group. **The specification declares both and states neither an authority nor an agreement requirement.** Graph invariant 10 checks that each side *resolves* — a staff's group is declared (`invariants.rs:1126`), a group's members are declared (`:1135`) — and never that the two agree, so **both stale forms pass every check in the tree**: a *missing* member (`s.group == Some(g)` while `g.members` omits `s`) and a *spurious* member (`g.members` contains `s` while `s.group` is `None` or names a different group). Genesis G3a ruled `Staff.group` the sole authority and `StaffGroup.members` a non-authoritative denormalized projection (`spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1, disposition B, ratified 2026-07-29) — a normative semantic ruling that makes the disagreement *defined* rather than merely undetected, but does not make it *impossible*: G3a stores the projection without maintaining it | `spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1 (found 2026-07-29 during G3a contract review; the authorship cycle is what surfaced it — with mints only, no authoring order produces an agreeing pair, since `CreateStaff` requires its group live at `reduce.rs:4117` and `CreateStaffGroup` requires its members live) | **open.** Deliberately no code change in G3a. The fix is disposition **A**: maintain the projection under reduction — `create_staff` with `group: Some(g)` appends to `g.members` — plus a candidate **graph invariant 21** enforcing agreement in both directions, and a decision on whether a re-carried `CreateStaffGroup` compares against its *carried* `members` (empty) or the current derived state. **Consumers must read `Staff.group`, never `StaffGroup.members`, for membership** until that lands. Sequence it after G3b so an invariant append is not competing with G3b's invariant 20 |
 | P13-S17 | **Binary Format revision history omitted genesis tranche G2b entirely, including the accept-set raise it performed.** `spec/binary_format.tex`'s Revision History chapter ran G2a 0.12.0 straight to G-minor 0.13.0 to G3a 0.14.0, with no row anywhere recording G2b (`spec/CONTRACT_GENESIS_G2B_TUNING.md`, kind/tag 34, `SetTuningContext`) — even though `OperationEnvelopeBlock`'s accept-set raise 2→3, the first accept-set move since genesis tranche G2a explicitly recorded staying at 2, reached the normative tables (the per-chunk-role accept-set prose at `binary_format.tex:2353`–`:2363`, which names the `OperationEnvelopeBlock` role's maximum as 3 "as of genesis tranche G2b", and the `OperationKind` minor-additive bullet at `:2395`–`:2418`, which records "genesis tranche G2b took 34 (`SetTuningContext`)") and never the history. G2b's own contract touch table row 27 required "version, Revision History row" among the four-document ritual, and the rung was signed off without it — the gate did not catch a documentation MUST because nothing tests the revision history | `spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` §0 (found 2026-07-29 during the G3a undo-repair contract review, verified against the working tree: `binary_format.tex:3599`, `:3628`, `:3643` before this rung's edit) | **RESOLVED in this same commit.** The chronology is restored: G2b lands as its own 0.14.0 row between G-minor and G3a, and G3a renumbers to 0.15.0 (`spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` Packet B, pins B2–B3). A new scoped guard in `epiphany-testkit` makes the omission recurrence-detectable — a distinct principal marker per standalone-row rung (G2a, G-minor, G2b, G3a — G1 is deliberately unguarded, having no standalone row of its own), strictly ordered, with G2b's content anchored within its own row segment — so the entry is filed and closed by the same packet that finds it, unlike **P13-S15** and **P13-S16**, which stay open because their fixes are sequenced to later rungs |
 | P13-S18 | **Graph invariant 20's agreement and boundary-consistency checks are partial, but only three of the checker's nine non-success paths are the real gap — not the whole checker, as first filed and over-sized.** `check_measure_meter_consistency` (`invariants.rs:2662`) has nine non-success paths across its two clauses, enumerated and classified by both its own doc comment and `spec/CONTRACT_P13S18_MATRIX.md`'s 18-cell outcome matrix (agreement: A1-A4; boundary: B1-B5). A1 (`None` declared signature) is **inapplicable** — nothing to disagree with. A3/B3 (`Governing20::None`, an empty governing candidate set) are **vacuous** (pin 6c case 1). A2/B2 (an unresolving declared or governing signature) are **delegated** to invariant 10's own resolution check (`invariants.rs:1220`ff, its per-measure and instance-local-grid arms) — verified, not merely asserted: the matrix rung's mutations M7/M8 delete each arm in turn and show the SAME condition go unreported by the ENTIRE workspace suite, not merely by invariant 20. B1 (the first measure) is the already-filed pickup/anacrusis deferral, **P13-S19**. **Exactly three paths are genuine abstention: A4 and B4 (`Governing20::Indeterminate` — the comparable relation cannot place a candidate) and B5 (a decided governing selection with no computable musical delta — order without distance).** Also corrected: the earlier **"any `Measure` *end* anchor is incomparable"** claim was wrong only in its "any" — same-id, same-position `End`<->`End` IS comparable under c2 **when its offsets compare** (`measure20_offset_order`, `:2419`, returns `None` only for `Musical` against `WallClock`); distinct-id `End` anchors genuinely are incomparable (c3 restricts to `Start`+`Zero`) and do reach A4/B4/B5; and the `resolve_anchor` `Measure` arm citation (now `:503`-`:516`, formerly miscited as `:400`ff — see the companion line-number repair to `CONTRACT_GENESIS_G3B_MEASURE.md:206`) names the missing duration machinery, not invariant 20's own execution path, which never calls `resolve_anchor`. And the `WallClock`-anchored measure start `epiphany-ops::valuegen::measure` (`ops/src/valuegen.rs:447`) actually emits does **not** uniformly abstain both clauses: against `WallClock`-anchored meter changes (c5) agreement DECIDES and only the boundary clause abstains (B5, since `measure20_musical_delta` never returns a `WallClock` delta); against `Region`-anchored meter changes both abstain (A4/B4), because `WallClock` against `Region` has no comparability arm at all | `spec/CONTRACT_P13S18_MATRIX.md` pin 8 (ratified 2026-07-31, a diagnostic and bookkeeping rung: test coverage over `check_measure_meter_consistency`'s existing nine paths plus these three ledger repairs, no behaviour change) | **open, at its true size.** A4, B4 and B5 remain real, still gated on the deferred common-timeline machinery — but the capability that closes them is now filed as **P13-S23** (below), not P11-C5: P11-C5 is a narrower re-anchoring proximity metric this entry previously over-cited as the gate; P13-S23 is the broader "place any anchor pair on a common timeline and measure musical distance" capability that actually owns A4, B4 and B5 |
-| P13-S19 | **`CreateMeasure`'s ordering and boundary-distance preconditions are vacuous for an instance's first measure, so pickup/anacrusis measures are unauthored by this rung.** Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9) makes clauses 1 and 3 of `create_measure`'s append-only discipline vacuous when there is no predecessor measure, and invariant 20's boundary clause is symmetrically exempt for a first measure (core specification, invariant 20's doc comment) — a partial first measure MUST NOT be refused or flagged by either. This is a scoped deferral, not an oversight: a pickup measure's *own* internal consistency (its declared duration against its content) is a decomposition-sum question, not a measure-to-measure boundary question, and modelling it correctly needs a notion of "partial measure" this rung does not introduce | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9 (filed 2026-07-30 during the G3b contract's own drafting) | **open, deliberately.** A pickup/anacrusis authoring story — whatever shape it takes — is later schema-fill work, sequenced after the genesis ladder closes |
+| P13-S19 | **A pickup's *successor*, not the pickup itself, is what `CreateMeasure` and invariant 20 refuse — pickup/anacrusis measures are authorable, but the rest of the instance becomes unauthorable once one exists.** Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9) makes `create_measure`'s clauses 1 (ordering) and 3 (boundary distance) vacuous for a first measure, and invariant 20's boundary clause is symmetrically exempt at `i == 0` — both for lack of a predecessor. **The agreement clause (clause 2) is not predecessor-dependent and applies to a first measure like any other**: a pickup declaring a signature that disagrees with the governing grid is itself refused (`MeasureMeterMismatch`) and flagged; only a pickup declaring `None` or a matching signature clears it, and only when its other preconditions (a live parent `StaffInstance`, resolving referents) are satisfied too. **The real defect is one measure downstream**: both rules compare `delta(prev.start, m.start)` against the *governing signature's full* `measure_duration()`, when the true distance is `prev`'s own content duration — those coincide only for full measures. A pickup's successor is therefore refused (`MeasureMeterMismatch`) by `create_measure` and flagged by invariant 20, which is what actually makes the rest of the instance unauthorable once a pickup is minted. This applies to **any** partial measure, not only a first one: a mid-score partial measure enters successfully (nothing examines its own duration when it is created), while *its* successor is refused the identical way — the failure is always attributed to the measure after the partial one. Closing this needs a per-measure duration — the "partial measure" notion this entry already names — and that is deliberately **not** introduced by the correction that reworded this entry. See also **P13-S24**, the Chapter 3 derived-notation deferral that shares this same missing concept but touches neither invariant 20 nor `CreateMeasure` | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9 (filed 2026-07-30 during the G3b contract's own drafting); corrected 2026-07-31 by `spec/CONTRACT_P13S19_PARTIAL.md`, which found the original wording true only of the pickup itself and, read as written, indistinguishable from "pickups work" | **open, deliberately.** A pickup/anacrusis authoring story — whatever shape it takes — is later schema-fill work, sequenced after the genesis ladder closes; it now depends on a per-measure duration concept, which does not yet exist |
+| P13-S24 | **The Chapter 3 integer-grid metric splitter assumes the region origin falls on a barline, deferring anacrusis/pickup handling — a second, independent site carrying the same missing partial-measure-duration concept P13-S19 names for invariant 20 and `CreateMeasure`.** `core_spec.tex:2484` (Chapter 3, derived notation) states the assumption directly; the same deferral is mirrored at `crates/epiphany-core/DECISIONS.md:340` ("region origin assumed to be a barline (anacrusis/pickup deferred)"). **Not a duplicate of P13-S19**: it predates genesis tranche G3b, lives in the derived-notation splitter rather than the graph model, and does not touch invariant 20 or `CreateMeasure` at all — a pickup measure can now be *authored* (P13-S19's corrected scope) with no effect whatsoever on this splitter's own barline assumption. The two entries are filed separately because they own different subsystems' work — merging them would conflate a graph-model rung with a derived-notation one — and both wait on the same underlying capability: a per-measure partial-duration notion neither rung introduces. See also **P13-S19** | `core_spec.tex:2484` and `crates/epiphany-core/DECISIONS.md:340` (mirrored deferral sites; filed 2026-07-31 during `spec/CONTRACT_P13S19_PARTIAL.md`'s drafting, pin 6) | **open.** No code owed by this rung — filed so the deferral is discoverable on its own terms, independent of P13-S19, with which it shares a root cause but not a subsystem |
 | P13-S20 | **`decode.rs`'s `precondition_reason` decoder stopped at discriminant 13, so `PreconditionFailureReason` 14 (`AcousticRealizationPinned`) and 15 (`TranspositionOutOfRange`), both live since Push 4a, encoded but could not decode.** A materialized effect carrying either reason failed canonical round-trip in production code, undetected because `epiphany-testkit`'s `precondition_failure_reason` generator (`generators.rs:417`, then `rng.below(14)`) never drew past 13 despite its doc comment claiming "every core and registered variant" | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` §0 / touch-table row 12a (found 2026-07-30 during the G3b contract's own drafting, verified against the working tree: `decode.rs:205`ff ended at 13, `generators.rs:417` drew `below(14)`) | **RESOLVED in this rung** (genesis tranche G3b packet 1, `e64a4b7`). `decode.rs`'s `precondition_reason` now decodes discriminants 14 through 18 (the pre-existing 14/15 hole plus G3b's own 16–18), and `generators.rs`'s `precondition_failure_reason` now draws `below(19)` with arms for all of them — the generator's doc comment claim is true again, and the decode hole this rung found already latent in the tree, not introduced by it, is closed alongside G3b's own additions |
 | P13-S21 | **The wire specification never documented `PreconditionFailureReason` 14 and 15, so the decoder hole P13-S20 repaired had no normative text to be measured against.** `binary_format.tex`'s bounded reason table (`\sectionsc{Bounded Enumerations}`) ran `\tablenums{13}` straight to G3b's `\tablenums{16}`, and Push 4a's own Revision History row recorded only `OperationKind` `\tablenums{30}` (`TransposeInterval`) while saying nothing about the two reasons it appended in the same epoch. `AcousticRealizationPinned` and `TranspositionOutOfRange` appeared **nowhere** in the document, though the Operation Catalog documented both at 0.8.0 and `effect.rs` has carried both since Push 4a. This is P13-S20's specification-side twin: the same two variants, the same silence, and the reason a decoder that stopped at 13 could sit in the tree unchallenged — a conforming implementer reading only the wire specification would have built exactly that decoder and been right | Found 2026-07-30 while verifying genesis tranche G3b packet 3b (`d58eee8`), whose touch-table row 28 scoped the reason table to discriminants 16–18 only; the executing agent correctly declined to widen scope and reported the gap instead | **RESOLVED in this rung** (the G3b pre-push repair). The bounded table gains `\tablenums{14}` and `\tablenums{15}` with their refusal conditions, and Push 4a's Revision History row is amended to record both appends in its own epoch — no version bump and no new history row, because this documents an assignment that has been normative since Push 4a rather than making one. `binary_format_history.rs` gains a bounded regression test requiring both names in the reason table **and** in Push 4a's own row segment, so neither the G3b row's prose nor the Operation Catalog's coverage can satisfy it |
 | P13-S22 | **`OperationKindTag`'s normative tag-to-byte mapping is asserted for a minority of the vocabulary; the rest is defended only incidentally, by frozen byte artifacts that cannot say what broke.** P13-S15 closed the `OperationKind` half with one table covering 0..=39. The tag half has no equivalent. **Semantic locks — a named tag bound to a literal byte — exist only for:** 24–29 (`phase3_tag_discriminants_are_golden`, `payload.rs:2728`), 34 (one assertion inside a G2b reduction test, `reduce.rs:12744`), 35–38 (`t1_g3a_kinds_and_tags_are_35_to_38_in_both_spaces`, `reduce.rs:15931`), 39 (`payload.rs:2936`); **16** (`Registered`, whose corpus row is emitted under its *variant* name at `ops/src/vectors.rs:210` and whose committed literal leads with `0x10` at `spec/vectors/decode_vectors.txt:80`, so the drift comparison binds the association); and — incidentally — 1, spelled in a comment inside a golden blob (`barrier.rs:1058`, *"len 1, DeleteEvent (tag 1)"*). **Tags 0, 2–15, 17–23, and 30–33 have no semantic lock at all.** The derived tests do not supply one: `the_tag_vocabulary_is_complete` (`payload.rs:2652`) proves **completeness, density, and round-trip** — that the payload-free discriminants are exactly `0..unknown` with no gaps and each decodes — which constrains the *shape* of the assignment, not *which tag holds which byte*, and `operation_kind_tag_vocabulary!` guarantees coverage rather than value. **What actually catches a permutation is byte-level goldens that embed the tag by accident**, and they diagnose it as a blob mismatch: three probes, three catches, none of them naming a tag (below) | this file (found 2026-07-30 while closing P13-S15, whose kind-side extension made the asymmetry visible; **the entry was rewritten the same day after its own probes falsified its first draft.** That draft claimed a permutation was invisible and named 32↔33 as the demonstration. Three permutations were then executed against the working tree at `dcb28f0` and **all three failed**, so the claim was wrong and the severity is lower than filed: 32↔33 (`SetCanvasLayoutDefaults`/`SetSpellingPrecedence`) → caught by `the_committed_corpus_matches_the_generator` (`testkit/src/vectors.rs:225`); 1↔2 (`DeleteEvent`/`ModifyEvent`) → caught by `edit_barriers_blob_bytes_are_golden` (`layout-ir/src/barrier.rs:1061`); 2↔3 (`ModifyEvent`/`RespellPitch`) → caught by the corpus again. Each mutation was restored by hand and the suite returned to 1541/0) | **open.** **Not a live incorrectness, and — corrected — not an undefended one either:** every tag discriminant is currently correct, `binary_format.tex:1548`–`:1552` carries the mapping normatively, and no probe escaped. **The gap is intent and diagnosis, not exposure.** A permutation fails as *"the committed corpus does not match the generator"* or *"blob bytes are not golden"* — artifacts that regenerate, and whose failure reads as corpus drift rather than as a moved wire discriminant. **The corpus's tag coverage is deliberate, not accidental** — `ops/src/vectors.rs:201`–`:204` emits one row per tag straight from the vocabulary and names the reason: *"A hand-picked subset is how `TransposeInterval` shipped encoding to a byte its own decoder rejected: the corpus never named it."* **But those rows lock byte→byte, not variant→byte.** Each is named `tag_{discriminant}` and carries `[discriminant]`, both derived from the value alone, so `tag_32` asserts that `0x20` round-trips — never that `SetCanvasLayoutDefaults` is 32. Every one of the 40 rows is identical under a permutation; what actually moves is their **order**, since `PAYLOAD_FREE` is declaration order. That is why the 32↔33 probe failed, and it is exactly the property `Registered`'s row has and the numbered rows do not — its row is named for the variant. **The gap is that one row's discipline is not the vocabulary's.** **Likely shape of the repair:** one table over the whole tag vocabulary asserting tag → byte directly, superseding the six scattered fragments rather than adding a seventh — a seventh band is how this got here — so that moving a tag fails by *name*. **Probe design note for whoever takes this:** do not reuse 32↔33 or 1↔2; both are now known to be caught, and a probe that fails proves the lock exists, not that it is missing. The mutation that would sign this rung is the **inverse**: delete the proposed table and show that some permutation then passes, or show the surviving failure names no tag. **Its own rung, not a rider** |

spec/core_spec.tex

@@ -6629,8 +6629,16 @@ The score graph maintains a set of structural invariants. Implementations
       raises no violation --- wherever the comparison or the
       distance cannot be decided (base-ingested data may predate
       this rule); this is deliberate abstention, not a soundness
-      gap. A pickup/anacrusis first measure has no predecessor and
+      gap. A pickup/anacrusis first measure has no predecessor, so
-      is never flagged.
+      only the BOUNDARY clause is vacuous for it; the AGREEMENT
+      clause is not predecessor-dependent and still applies (unless
+      \texttt{time\_signature} is \texttt{None} or agrees with the
+      governing grid). Regardless of what the pickup itself
+      declares, its successor's boundary distance is measured
+      against this same governing signature's full
+      \texttt{measure\_duration()}, and IS flagged when that
+      distance is the pickup's own shorter length rather than a
+      full bar.
   \end{enumerate}
 
   Implementations \MUST{} reject graph configurations that violate any

spec/operation_catalog.tex

@@ -231,7 +231,7 @@
   {\Large\scshape\color{epiphanyslate}Operation Catalog}\\[6pt]
   {\large\itshape\color{epiphanyslate}A companion to the Core Specification}\\[14pt]
   {\color{epiphanygold}\rule{3in}{0.8pt}}\\[24pt]
-  {\normalsize\color{epiphanyink}Version 0.13.0 --- The genesis operation tranche closes: \texttt{CreateMeasure} and graph invariant 20 (G3b)}\\[4pt]
+  {\normalsize\color{epiphanyink}Version 0.14.0 --- Pickup/anacrusis: what a partial measure actually costs (P13-S19)}\\[4pt]
   {\small\color{epiphanyslate}Normative for the operation kinds it defines}
   \vfill
 \end{titlepage}
@@ -517,6 +517,31 @@ G2b left it. This closes the genesis ladder
 (\texttt{spec/PLAN\_GENESIS\_OPS.md} \S4): G1 $\rightarrow$ G2a $\rightarrow$
 G-minor $\rightarrow$ G2b $\rightarrow$ G3a $\rightarrow$ G3b.
 
+\medskip
+
+\noindent\textbf{Version 0.14.0 (P13-S19, correction and observation,
+\texttt{spec/CONTRACT\_P13S19\_PARTIAL.md}).} No payload byte changes, no
+behaviour change: \texttt{create\_measure} and graph invariant 20 are
+byte-identical to 0.13.0. Corrects this section's ordering and
+boundary-distance description above, which read as though a pickup/anacrusis
+first measure --- and everything downstream of it --- were simply exempt. A
+first measure skips only the \emph{predecessor-dependent} clauses (ordering
+and boundary distance) for lack of a predecessor, and the agreement clause
+only when it declares \texttt{None} or a signature that agrees with the
+governing grid; a disagreeing declared signature is refused
+(\texttt{MeasureMeterMismatch}) even on a first measure, since agreement is
+not predecessor-dependent. Independently of what the pickup itself declares,
+its \textbf{successor} is measured against the governing signature's full
+\texttt{measure\_duration()} regardless, and is refused
+(\texttt{MeasureMeterMismatch}) and flagged by invariant 20 whenever the
+pickup's actual length is shorter than a full bar --- which, for an authored
+pickup, it always is. The same gap applies to any partial measure at any
+position, not only a first one: a mid-score partial measure is itself
+unexamined at creation (nothing checks its own length), while \emph{its}
+successor is refused the identical way. Closing this needs a per-measure
+duration concept this rung does not introduce
+(\texttt{spec/PASS13\_CANDIDATES.md}, P13-S19, still open).
+
 % ===========================================================================
 \chapter{The Catalog Framework}
 \label{ch:framework}
@@ -1675,19 +1700,25 @@ every non-\texttt{WallClock} referent of \texttt{measure.start} (an
 \textbf{Ordering and boundary-distance preconditions (core specification
 \sectionsc{Graph Invariants}, invariant 20).} Graph-aware, against the current
 last live measure of the same instance (vacuous for an instance's first
-measure --- a pickup/anacrusis is never refused or flagged on this account):
+measure's own ordering and boundary-distance clauses, for lack of a
-the carried \texttt{start} must be \textbf{comparable} to the predecessor's
+predecessor to compare against --- but \textbf{not} for that same pickup's own
-start and \textbf{strictly after} it (else \texttt{MeasureOutOfOrder}), and,
+successor, which is checked against this same governing signature's full
-when a governing time signature is determinable, the \textbf{musical delta}
+\texttt{measure\_duration()} from the pickup's start, and refuses with
-between the two starts must equal that signature's
+\texttt{MeasureMeterMismatch} when the pickup's actual, shorter length
-\texttt{measure\_duration()} (else \texttt{MeasureMeterMismatch}). Either
+disagrees with it): the carried \texttt{start} must be \textbf{comparable} to
-comparison being \textbf{unverifiable} --- the two starts are not comparable,
+the predecessor's start and \textbf{strictly after} it (else
-or the delta is not computable --- refuses with
+\texttt{MeasureOutOfOrder}), and, when a governing time signature is
-\texttt{MeasureOrderUnverifiable} rather than silently permitting an
+determinable, the \textbf{musical delta} between the two starts must equal
-unverifiable mint. A resolving \texttt{time\_signature} that \textbf{disagrees}
+that signature's \texttt{measure\_duration()} (else
-with the effective grid's active signature at the measure's start also refuses
+\texttt{MeasureMeterMismatch}). Either comparison being \textbf{unverifiable}
-with \texttt{MeasureMeterMismatch}; \texttt{time\_signature: None} skips only
+--- the two starts are not comparable, or the delta is not computable ---
-this agreement check, not the boundary-distance check above.
+refuses with \texttt{MeasureOrderUnverifiable} rather than silently permitting
+an unverifiable mint. A resolving \texttt{time\_signature} that
+\textbf{disagrees} with the effective grid's active signature at the
+measure's start also refuses with \texttt{MeasureMeterMismatch} --- this
+agreement check is \textbf{not} predecessor-dependent and applies to a first
+measure like any other; \texttt{time\_signature: None} skips only this
+agreement check, not the boundary-distance check above.
 
 \textbf{The effective grid} is \texttt{StaffInstance.local\_metric\_grid} when
 present, else the enclosing region's default metric grid, reconstructed from