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) <noreply@anthropic.com>

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
+The two remaining Push-4a audit claims, carried here as **unverified** through
-checked, not inherited: that the JI dimension convention conflicts with its own
+two passes, were checked on 2026-07-22. **Both are real**, and both are Chapter 4
-prime-2 requirement, and that the named historical tunings lack exact
+defects standing in front of 4b rather than inside it. Filed as P13-S5 and
-deterministic ratio data. Neither was needed for 4a, and neither was confirmed.
+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`)
 

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) |