From b3449256f978aaa5cea403dc6f7afd8ec5a4e10d Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Wed, 22 Jul 2026 09:03:39 -0400 Subject: [PATCH] P13-S5 and P13-S6: the two inherited claims were both true `epiphany-core/DECISIONS.md` had carried two Push-4a audit claims as **unverified** through two passes, with the standing note that they "should be checked, not inherited". Checked. Both are real, and both are Chapter 4 defects standing in front of Push 4b rather than inside it -- which is the point of checking before scoping, not after. **P13-S5 -- the JI prime basis is specified at two lengths.** `req:pitch:ji-vector-basis` says the built-in JI 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, `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 own octave-reduction clause does not reconcile them: it normalizes the first component to a canonical range, it does not remove it. Same family as P13-S2 and P13-I1, and cheaper -- a one-side edit once ratified. **P13-S6 -- no built-in tuning system's resolution is pinned to a versioned definition, and 14 of 20 have no definition at all.** The claim as inherited ("the named historical tunings lack exact deterministic ratio data") understates it. It is not a missing table: `TuningResolution::Function` delegates the historical temperaments to a `TuningFunctionId`, which Chapter 10 lists as an *extension point*, and no built-in is mapped to a function id nor any function id pinned. Only the six `tet-*` entries are actually specified, by `EqualTemperament`'s structural rule. The other 14 are names: three meantone variants, `werckmeister-iii`/`iv`, `vallotti`, `kirnberger-ii`/`iii`, `young-ii`, `pythagorean` (the 3:2 ratio is named, the fifth-chain construction and wolf placement are not), three `ji-static-5limit-*`, and `ji-adaptive-5limit`. Set against `req:tuning:tuning-resolution-determinism`, which requires determinism *across platforms*, two conforming implementations may each choose a different published Werckmeister III and both pass -- in a project that runs a cross-implementation conformance step. The fix pattern is already in-house and was found by looking for it: `req:pitch:spelling-algorithm` pins `SpellingAlgorithmId "default"` at version 1 to a named algorithm and errors on any other identifier. Nothing equivalent exists for tuning. Which published variant each built-in denotes is a ratification question, not an implementation one. Both are filed open in the Batch-3 ledger. Neither was needed for 4a; both are load-bearing for 4b, whose whole job is resolving a scale position to a frequency. Co-Authored-By: Claude Opus 4.8 (1M context) --- crates/epiphany-core/DECISIONS.md | 30 ++++++++++++++++++++++++++---- spec/PASS13_CANDIDATES.md | 7 ++++++- 2 files changed, 32 insertions(+), 5 deletions(-) diff --git a/crates/epiphany-core/DECISIONS.md b/crates/epiphany-core/DECISIONS.md index f043477..3075331 100644 --- a/crates/epiphany-core/DECISIONS.md +++ b/crates/epiphany-core/DECISIONS.md @@ -588,10 +588,32 @@ implementation is now an explicit part of Push 4b. Remaining blockers: P13-S1 removed the former requirement-label blocker; Chapter 4's requirements are now independently citable. -Two further claims from the Push-4a audit are **unverified** and should be -checked, not inherited: that the JI dimension convention conflicts with its own -prime-2 requirement, and that the named historical tunings lack exact -deterministic ratio data. Neither was needed for 4a, and neither was confirmed. +The two remaining Push-4a audit claims, carried here as **unverified** through +two passes, were checked on 2026-07-22. **Both are real**, and both are Chapter 4 +defects standing in front of 4b rather than inside it. Filed as P13-S5 and +P13-S6: + +- **The JI prime basis is specified at two lengths** (P13-S5). + `req:pitch:ji-vector-basis` says the built-in JI spaces order primes ascending + *starting with 2* and that `components.len()` must equal the basis size; the + built-in table calls `ji-5limit` "Two-dimensional (prime axes 3, 5)", + `ji-7limit` three-dimensional, `ji-11limit` four-dimensional — each exactly + one short, consistently, the table being octave-reduced and the requirement + full-register. Both are normative, so a 5-limit vector must be both length 2 + and length 3. The requirement's octave-reduction clause normalizes the first + component; it does not remove it. +- **No built-in tuning system's resolution is pinned** (P13-S6), and 14 of the + 20 have no definition at all — only the six `tet-*` are specified, by + `EqualTemperament`'s structural rule. `TuningResolution::Function` delegates + the historical temperaments to a `TuningFunctionId` that Chapter 10 lists as + an *extension point*; no built-in is mapped to one and none is pinned. Against + `req:tuning:tuning-resolution-determinism`, which requires determinism across + platforms, two conforming implementations may choose different published + variants of Werckmeister III and both pass. + +The original phrasing understated the second: it is not missing ratio data but +an unpinned resolution contract, and `req:pitch:spelling-algorithm`'s versioned +`SpellingAlgorithmId "default"` is the in-house pattern for fixing it. ## The Text Projection value layer (`textvalue*.rs`) diff --git a/spec/PASS13_CANDIDATES.md b/spec/PASS13_CANDIDATES.md index 20a0958..07234b1 100644 --- a/spec/PASS13_CANDIDATES.md +++ b/spec/PASS13_CANDIDATES.md @@ -47,7 +47,10 @@ Three candidates, so the pass reopens per the house rule. P13-S3 arrived as a **live incorrectness** — a Push-4a follow-up audit found that the spelling-set 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; S4 remains open. +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. | Id | One-line statement | Filed in | Status | |---|---|---|---| @@ -55,3 +58,5 @@ S1, S2, and S3 are resolved; S4 remains 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) |