neuwirth
/
epiphany
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Pass 13: five ledger movements, one of them a repair to the ledger itself 

S5 and S6 close, which closes the spec half of Push 4b: the JI basis is
full-register (a JiVector is an absolute position -- without the prime-2
exponent, ji-5limit cannot tell C4 from C5), and all twenty tuning systems now
carry constructions rather than names.

S7 is filed retroactively. Its id was minted in PLAN_PUSH4B_TUNING.md marked
"new; file it", ratified as that plan's Ruling C, and implemented in Wave 1a --
but it never entered this ledger, so an id lived outside the index whose whole
job is to be the index. The candidate itself: the specification required every
score to *define* a pitch space, and the data model gives a score no way to do
it. Both "define"s are now "select".

S8 is new and was measured, not argued. TempoShape::Constant legalizes
end_tempo as None *or* equal to start_tempo -- two spellings of one musical
fact -- and TempoSegment encodes the field positionally into canonical state.
Encoding both forms of an otherwise identical score gives 336 bytes and 363.
Nothing normalizes; invariants.rs merely permits both. Everywhere else this
project looked at redundant encodings it ruled the other way: NFC for text, a
total order for collections. Tempo got no equivalent, so two musically
identical scores hash differently. Found sideways -- the branch is untested,
which is why the map_or rewrite could not be mutation-verified there.

S9 is the pattern behind three failures in one day: the citation checker
proves cited-to-defined and never cited-to-relevant, so a citation that
resolves cleanly while supporting nothing passes a fully green gate. An agent
justified "resolved layout is non-canonical" with a requirement about f32; a
dispatch contract of mine put KeySignature in Chapter 10 when the Score Graph
is Chapter 5. And S4 is itself an instance, which is what turned this from
incident into candidate.

The asymmetry is the dangerous part and is recorded with it: a dangling
citation is loud, a wrong one is silent, so repairing the loud kind without
reading the target converts a caught defect into an uncaught one. That is
exactly how S4 happened.

Every line citation in the new entries was re-read against its target before
filing, S9's own discipline applied to S9.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
Levi Neuwirth 2026-07-22 15:24:43 -04:00
parent a421b95edf
commit 600cc31be4
1 changed files with 17 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
spec/PASS13_CANDIDATES.md
View File

@ -49,8 +49,18 @@ chain introduced to make `TransposeInterval` undoable had only one writer, so
undo erased an ordinary `RespellPitch` on either side of it. It is resolved.
S1, S2, and S3 are resolved. S5 and S6 were filed 2026-07-22 by verifying the
two Push-4a audit claims that `epiphany-core/DECISIONS.md` had carried as
**unverified** through two passes; both are real, and both are Chapter 4
defects standing in front of Push 4b. S4, S5, and S6 remain open.
**unverified** through two passes; both were real, and both were Chapter 4
defects standing in front of Push 4b. Both are now resolved, closing the spec
half of Push 4b.
**Filed 2026-07-22, second round.** S7 is a **bookkeeping repair**: the id was
minted in `spec/PLAN_PUSH4B_TUNING.md` ("new; file it"), ratified as that plan's
Ruling C, and implemented — but never entered this ledger, so an id existed
outside the index that is supposed to be the index. S8 and S9 are new. S9 is
the third instance of one pattern in a single day and, notably, **S4 is itself
an instance of it**, which is what moved it from incident to candidate.
S4, S8, and S9 are open — three, so the pass stays open.
| Id | One-line statement | Filed in | Status |
|---|---|---|---|
@ -58,5 +68,8 @@ defects standing in front of Push 4b. S4, S5, and S6 remain open.
| P13-S2 | `cmn-24` was declared in the built-in pitch-space table as CMN with quarter-tone accidentals while `PitchSpacePosition::Cmn.alteration`, transposition, and `CmnChromatic` were all specified in fixed semitones. The specification now denominates both CMN alteration sites and interval chromatic steps in the enclosing space's chromatic layer, with `cmn-24`'s map fixed explicitly. Until Push 4b provides structural registry resolution, the core fails closed outside provable built-in `cmn-12` instead of applying guessed 12-chromatic arithmetic | `spec/PLAN_P13S2_CMN24.md`; `crates/epiphany-core/DECISIONS.md` | **resolved** (schema and wire layout unchanged; `PitchSpaceUnavailable` maps to existing `PitchSpaceMismatch` 6; Operation Catalog 0.9.0; registry-backed generalization remains a Push 4b implementation blocker) |
| P13-S3 | The `engraved_spelling_chain` introduced with `TransposeInterval`'s undo had a **single writer**. `RespellPitch` mutates the same graph attachments but recorded only on `respell_chain`, so (a) undoing a transposed transaction after a prior respell restored the pitch and **erased the respell**, and (b) a respell landing canonically *after* the transaction was invisible to the chain, so a `StrictInverse` undo reported `Applied` and **wiped the newer authoring** instead of refusing as superseded. A `BestEffort` undo could also restore the pre-transpose pitch while leaving a spelling authored against the transposed one | `crates/epiphany-ops/DECISIONS.md` (P13-S3) | **resolved** (both operations now record on the shared key; pitch value + spelling set undo as one unit; new `req:opcat:spelling-set-chain`. The chain stays *physically* separate from `respell_chain`, which is `RespellPitch`'s LWW conflict state — folding transposes in would make a concurrent respell conflict with a transpose and move the canonical bytes of every existing history) |
| P13-S4 | **No labelled requirement governs vertical-band *heights*.** Pass 12 twice recorded a behavioural fix to the inter-staff solve — realizing an `InterStaffGap` band's declared `preferred_height` rather than a constructor default — and both times cited `req:layoutir:vertical-bands`, which never existed. The two real band requirements (`req:layoutir:primitive-band-ownership`, `req:layoutir:resolved-band-ownership`) govern *ownership*: which band a primitive belongs to, and that a resolved primitive retains it. Nothing states what a band's height means or that the solver must realize it, so the shipped behaviour is unspecified and the log invented a name for the gap | this file | **open** (found in P13-S1 review: an agent 'corrected' the dangling citations to the two ownership requirements, which replaced a visibly broken pointer with a silently wrong one) |
| P13-S5 | **The JI prime basis is specified at two lengths.** `req:pitch:ji-vector-basis` states that the built-in JI pitch spaces "order primes ascending **starting with 2**" and that `components.len()` MUST equal the basis size; the built-in pitch-space table calls `ji-5limit` "Two-dimensional (prime axes 3, 5)", `ji-7limit` three-dimensional and `ji-11limit` four-dimensional — each **exactly one short**, consistently, because the table is octave-reduced and the requirement is full-register. `req:tuning:builtin-tuning-catalog` makes the table normative, so a 5-limit vector is required to be both length 2 and length 3. The requirement's octave-reduction clause does not reconcile them: it *normalizes* the first component to a canonical range, it does not remove it | this file (verified 2026-07-22 against `core_spec.tex:1005-1008` and `:3496-3501`) | **open** (one-side edit once ratified: either the table gains prime 2 and the dimensions become 3/4/5, or the requirement declares the built-in JI spaces octave-reduced with 2 outside the basis — which then needs `JiLattice.generators` and `req:pitch:ji-vector-basis`'s ratio formula to agree) |
| P13-S6 | **No built-in tuning system's resolution is pinned to a versioned definition, and 14 of 20 have no definition at all.** `req:tuning:builtin-tuning-catalog` makes all 20 identifiers MUST-resolve with normative semantics, but only the six `tet-*` entries are actually specified — by `TuningResolution::EqualTemperament`'s structural rule. The other 14 are names: 3 meantone variants, `werckmeister-iii`/`iv`, `vallotti`, `kirnberger-ii`/`iii`, `young-ii`, `pythagorean` (the 3:2 ratio is named but not the fifth-chain construction or wolf placement), 3 `ji-static-5limit-*`, and `ji-adaptive-5limit`. `TuningResolution::Function` delegates them to a `TuningFunctionId`, which Chapter 10 lists as an **extension point**; no built-in is mapped to a function id and no function id is pinned. Against `req:tuning:tuning-resolution-determinism` — determinism MUST hold *across platforms* — two conforming implementations may each choose a different published Werckmeister III and both pass | this file (verified 2026-07-22 against `core_spec.tex:3246-3261`, `:3291`, `:3526-3546`, `:13271`) | **open** (the in-house fix pattern exists: `req:pitch:spelling-algorithm` pins `SpellingAlgorithmId "default"` at version 1 to a named algorithm and errors on any other identifier. Which published variant each built-in denotes is a ratification question, not an implementation one) |
| P13-S5 | **The JI prime basis is specified at two lengths.** `req:pitch:ji-vector-basis` states that the built-in JI pitch spaces "order primes ascending **starting with 2**" and that `components.len()` MUST equal the basis size; the built-in pitch-space table calls `ji-5limit` "Two-dimensional (prime axes 3, 5)", `ji-7limit` three-dimensional and `ji-11limit` four-dimensional — each **exactly one short**, consistently, because the table is octave-reduced and the requirement is full-register. `req:tuning:builtin-tuning-catalog` makes the table normative, so a 5-limit vector is required to be both length 2 and length 3. The requirement's octave-reduction clause does not reconcile them: it *normalizes* the first component to a canonical range, it does not remove it | this file (verified 2026-07-22 against `core_spec.tex:1005-1008` and `:3496-3501`) | **resolved** (Push 4b Wave 1a, 5dcaa58: ratified **full register**. The three table rows gain prime 2 and become three-, four- and five-dimensional; `req:pitch:ji-vector-basis` is untouched, being the side that was already correct. A `JiVector` is an absolute *position*: without the prime-2 exponent, `ji-5limit` cannot distinguish C4 from C5) |
| P13-S6 | **No built-in tuning system's resolution is pinned to a versioned definition, and 14 of 20 have no definition at all.** `req:tuning:builtin-tuning-catalog` makes all 20 identifiers MUST-resolve with normative semantics, but only the six `tet-*` entries are actually specified — by `TuningResolution::EqualTemperament`'s structural rule. The other 14 are names: 3 meantone variants, `werckmeister-iii`/`iv`, `vallotti`, `kirnberger-ii`/`iii`, `young-ii`, `pythagorean` (the 3:2 ratio is named but not the fifth-chain construction or wolf placement), 3 `ji-static-5limit-*`, and `ji-adaptive-5limit`. `TuningResolution::Function` delegates them to a `TuningFunctionId`, which Chapter 10 lists as an **extension point**; no built-in is mapped to a function id and no function id is pinned. Against `req:tuning:tuning-resolution-determinism` — determinism MUST hold *across platforms* — two conforming implementations may each choose a different published Werckmeister III and both pass | `spec/DRAFT_P13S6_TEMPERAMENTS.md`; `spec/CONTRACT_P13S6_TEMPERAMENTS.md`; `spec/CONTRACT_P13S6_PROMOTION.md` | **resolved** (5e465a1: all 20 pinned by construction, not by cents table. The ten temperaments carry which fifths are tempered by what fraction of **which** comma, wolf placement where the name does not force it, exact ratios, and a closure sum that makes the section self-verifying. The static 5-limit systems are the lattice block $\{3^a5^b \mid a\in[-1,2], b\in[-1,1]\}$ — a 4×3 rectangle filling all twelve chromatic positions with nothing discarded — at three anchors, `req:tuning:ji-static-construction`. `ji-adaptive-5limit` is `"default-v1"`, the key-anchored static scale, with the anchor pinned to a staff and a moment (`req:tuning:adaptive-default-version`, `req:tuning:adaptive-anchor-derivation`). **Sourcing alone was insufficient**: a first draft produced two arithmetically impossible temperaments and one false ambiguity, every one properly cited, and only the closure invariant caught them — the contract gained a permanent "check the arithmetic, not just the source" section as a result) |
| P13-S7 | **`ScalePosition` referenced a score pitch-space registry that does not exist.** The listing comment said the space "References an entry in **the score's pitch-space registry**", and `req:pitch:default-pitch-space` said every score MUST **define** at least one pitch space and MAY define more. No such registry exists anywhere: `Score` has thirteen fields and none is one, and `ScoreTuningContext` carries ids plus accidental extensions — never space or system definitions. So the specification required an act (defining a pitch space) that the data model gives a score no way to perform | `spec/PLAN_PUSH4B_TUNING.md` (Ruling C); `spec/CONTRACT_PUSH4B_SPEC1.md` | **resolved** (Wave 1a, 5dcaa58: ratified **the catalog is closed**. Both "define"s become *select*, from the built-in catalog; the `ScalePosition` comment names the built-in catalog; score-local definition is deferred to a later schema major, because the Chapter 4 type surface has never had a consumer and `req:binfmt:frozen-layout` would freeze it permanently on first encode. **No struct gained a registry field — that was the point of the ruling.** Filed here retroactively: the id was minted in the plan, ratified, and implemented without ever entering this ledger) |
| P13-S8 | **Canonical state admits two encodings of one musical fact, and nothing normalizes them.** `TempoShape::Constant` (`core_spec.tex:2230`) says `end_tempo` MUST be `None` **or** equal to `start_tempo` — explicitly legalizing two spellings of an identical constant-tempo segment. `TempoSegment` encodes `end_tempo` positionally through `struct_codec!` (`codec.rs:1510`) and `TempoMap` is canonical state on `Score` (`graph.rs:1685`, `codec.rs:1517`), so the two forms produce different canonical bytes: **measured at 336 vs 363 for otherwise identical scores.** `invariants.rs:1335` merely permits both; no normalization runs anywhere. The project has ruled the other way everywhere else it looked — `req:determinism:unicode-canonicalization` applies NFC precisely so that "two texts whose NFC byte representations are equal are canonically equal", and `req:determinism:canonical-collection-order` pins iteration to a total order — but tempo has no equivalent, so two musically identical scores hash differently | this file (measured 2026-07-22 by encoding both forms) | **open** (ratification: normalize on encode to one form — `None` is the smaller and the one every generator already emits — or state that both are canonical and accept divergent hashes for identical music. Found sideways: the branch is also **untested**, since flipping `is_none_or` to `is_some_and` at `invariants.rs:1335` kills no test, so nothing in the suite constructs a `Constant` segment with `end_tempo: None`) |
| P13-S9 | **The citation checker enforces cited→defined, never cited→relevant.** `requirement_labels.rs` proves every `req:*` string in the repo resolves to a real label and nothing further, so a citation that resolves cleanly but does not support the sentence it is attached to is invisible to a fully green gate. Three instances in one day: a Push-4b spec agent justified "resolved layout is non-canonical" with `req:layoutir:staff-space-coordinates`, which mandates staff-space units and `f32` and says nothing about canonicality; a dispatch contract asserted "Chapter 10 defines `KeySignature`" when the Score Graph is Chapter 5 (caught only because the agent used `\ref{ch:graph}` and reported the discrepancy rather than hardcoding either number); and **P13-S4 is itself an instance** — an agent "corrected" two dangling citations to the ownership requirements, replacing a visibly broken pointer with a silently wrong one | this file | **open** (relevance is not mechanically checkable, so the ratification is *what discipline replaces a check*: e.g. requiring the quoted sentence alongside any newly-added citation so review compares text to text, or treating agent-authored citations as unverified until a human reads the cited requirement. Note the asymmetry that makes this dangerous — the broken-pointer case is loud and the wrong-pointer case is silent, so **fixing the loud one without reading the target converts a caught defect into an uncaught one**) |