Section 8.4's M27 entry said M27 varies which clause is chosen. It now says each
of M22-M26 presupposes that selection succeeded and M27 attacks whether
selection is permitted at all. M25 is what varies which clause is chosen; a
correct implementation rejects M27 before selecting any clause.
Section 8.6 is untouched and verified so with a zero-context diff: its sentence
appears in the staged diff only as hunk context, never as an addition or a
deletion. It says M27 was the step no mutation had reached, which is true, and
an earlier draft of amendment 4 would have rewritten it.
Contract-only, three hunks: the replaced sentence, section 9's landed status
literal, and section 9's historical marker naming amendment 4. No annex edit --
its record that the correction was open as of bff7be0 remains true. Baseline
unchanged at 43 suites, 1586 passing; this commit changes prose only.
Section 9.6's gate observed, all items: one path staged; within section 8.4's
M27 entry the old sentence absent and the replacement present exactly once;
section 8.6 unchanged under zero context; within section 9's slice the landed
literal and an amendment-4-specific marker present; diff check clean.
One nuance in the ratified gate rationale is worth recording rather than
patching, since section 9 is frozen. Item 2 argues the scope is mandatory
because a file-wide form is unsatisfiable, section 9.1 quoting the old sentence
and 9.3 the replacement. Measured: under a normalising reader -- blockquote
prefixes stripped, whitespace collapsed, which is how every guard in this
repository reads .tex -- file-wide is indeed 1 and 2, and unsatisfiable. Under
raw exact matching against the source's own line wrapping it is 0 and 1, and
would pass. Section 9.6 does not say which reader it means. The scoping is right
under either, and item 4's scope is mandatory under both, the file carrying
eleven copies of the landed literal.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
Section 8.4's M27 entry closes by saying M27 varies which clause is chosen. It
does not. M25 varies which clause is chosen -- it moves \MUST{} into the recap
and the clause moves with it, which is exactly how M25 discriminates the
last-period rule -- and a correct implementation rejects M27 before selecting
any clause at all, on the exactly-one assertion. M27 uniquely varies whether
selection is unambiguous and therefore permitted.
Section 8.6 is NOT affected and must not be touched. It says only that M27 was
the step no mutation had reached, which is true. An earlier draft of this
amendment proposed rewriting it, which would have damaged an accurate historical
statement in frozen text to repair a different sentence's error. That near-miss
is kept in the record because it is the same class as the defect being repaired.
Contract-only: touch row 7 alone. The annex needs no edit -- its record that the
correction was open as of bff7be0 remains true, and an append would add only
redundant lifecycle prose. Rewriting it would be the worse error, but that is
not what is being declined.
A prose-only replacement has no test to sign it, so section 9.6 is the observer,
and both of its slice checks exist because an unscoped form fails in opposite
directions. Scoped to section 8.4's M27 entry, the old sentence must be absent
and the replacement present exactly once -- file-wide that is unsatisfiable by a
correct execution, since section 9.1 quotes the old sentence and 9.3 quotes the
replacement. Scoped to section 9, the landed status literal and a marker naming
amendment 4 must be present -- unscoped that passes on lifecycle text section 9
never wrote, the file already carrying the same literal for the contract, for
section 6 and for section 8. Section 8.6 is verified unchanged with a
zero-context diff, on pin 11's precedent.
No behaviour, test or normative semantics changes. The prose diff is itself
observable, which is what 9.6 observes.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
Test 3 asserted phrase presence over the whole requirement block, so a referent
could leave the sentence carrying the normative force and survive in the closing
recap. Execution measured that escape and the annex recorded it; this commit
closes it by strengthening the guard rather than softening pin 4a's claim.
Test 3 now selects the normative clause -- the sentence carrying the sole
\MUST{} -- and runs all four assertions on that slice alone. Both halves of the
start rule are load-bearing and the helper's doc comment says why: last ". "
before the occurrence, falling back to just after the label only when there is
none. An unconditional fallback would return one slice spanning label to recap,
containing every needle; a period-only rule would swallow the label, which is
not a sentence.
Six mutations, six matching radii, test 3 alone in every case. Each attacks a
different layer: M22-M24 vary what the selected clause contains, M25 varies
which sentence is selected, M26 varies the fallback boundary -- starting after
the label versus widening before it -- and M27 varies whether selection is
unambiguous and therefore permitted at all. M27 is the one that reaches the
exactly-one assertion, because an assertion guarding the precondition of
selection cannot be exercised by any mutation that presupposes selection
succeeded.
Rows 4, 6, 7 and 8 only. core_spec.tex is not touched: the requirement's text
was always correct and only the guard was weak. The rung's original 38/38
matrix is preserved unchanged and amendment 3's evidence is appended beside it,
not merged into it.
One prose defect in ratified section 8.4 remains OPEN and is deliberately not
repaired here: that entry says M27 varies which clause is chosen, which M25 does
and M27 does not, since a correct implementation rejects M27 before selecting
any clause. Section 8.6 is unaffected and states something true. The annex
carries the corrected characterization and records the correction as open;
frozen text stays frozen regardless of severity, so the repair belongs to its
own amendment, which is not part of this commit.
Baseline unchanged at 43 suites, 1586 passing: amendment 3 alters an existing
test's scope and adds none.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
Execution measured that pin 4a claims more than test 3 delivers. M12's first
application deleted the ordering referent from the requirement's normative
clause and left it standing in the closing recap; test 3 stayed green, because
it asserts phrase presence over the whole requirement block. A referent can
therefore leave the sentence where it does normative work and survive anywhere
else in the block.
Two repairs were available. Softening pin 4a to promise only what block-scoped
presence delivers would have made the contract honest and the guard no better,
leaving a measured escape undetected in a rung whose subject is documentation
drifting because nothing watches it. This amendment strengthens the guard
instead, so pin 4a's claim becomes true rather than smaller.
Test 3 will select the normative clause -- the sentence carrying the sole
\MUST{} -- and run all four assertions on that slice alone. The selector took
four rounds to get right and both halves of its start rule are load-bearing:
last ". " before the occurrence, falling back after the label only when there is
none. Revision B made the fallback unconditional, which would have handed M25 a
slice spanning label to recap containing every needle; revision C restored the
rule the fallback exists for.
Six signing mutations, one per step of the selector: M22 and M23 the referents'
clause scope, M24 the locality phrase, M25 the last-period rule, M26 the
fallback anchor, M27 the exactly-one-\MUST{} assertion. M27 closes the last open
item -- an assertion specified without asking what would exercise it -- and it is
the only mutation that varies which clause is chosen rather than what the clause
contains. Each carries a complete before/after requirement block so it applies
literally.
The section is an additive override: pin 4a and section 3 are frozen and are not
rewritten, the mutations are section 8's rather than inserted into section 3's
table, and the annex's 38/38 matrix is preserved with M22-M27 evidence appended.
Execution touches rows 4, 6, 7 and 8 only; core_spec.tex is not touched, because
the requirement's text was always correct and only the guard was weak.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
Item 10 said only that "every cross-cutting structure's references resolve to
extant objects", naming no individual class, while the checker enforced a
surface spanning cross-cutting structures, structural top-level references,
meter references at every level a MeterChange appears, an attachment-internal
reference, event-internal references and the tempo map's segment anchors. The
Rust doc comment named many of those and not all. The two were incomplete in
different places, so neither could be repaired from the other; both are now
written from one table derived by reading every emitted condition in the four
functions that raise the tag -- 41 tokens, each with its resolution target and a
symbolic anchor back to the control flow that enforces it.
Two of the ledger row's own claims did not survive scoping and were corrected at
ratification rather than carried: the G3a aside is ambiguous, not false, and the
two-sided repair stands on incompleteness rather than on a falsehood.
Guarded by exact (token, target) set equality in a new testkit suite, against an
oracle validated before use. Ordering and vocabulary are separate assertions
because an out-of-vocabulary term sorts perfectly well. Duplicates are checked on
the raw extraction, which set comparison cannot see. Item 10's opening sentence
is the slice anchor as a complete literal, required to occur exactly once, so
pin 3's retention of it is machine-observed rather than asserted. t12 is narrowed
and renamed, not deleted: cargo test -p epiphany-core must still fail when the
doc block is destroyed, and testkit is another crate.
Chapter 3 gains req:time:aleatoric-reference-locality -- an aleatoric region's
ordering and bounds references must name events of that same region, a locality
rule the checker always enforced and no requirement stated. Its three count
constants were measured at execution, never predicted: 214/285/285 -> 215/286/286.
38 mutations, 38 matching radii, every one against the full workspace with
--no-fail-fast and restored by hand write-back. M3 is the single passing control:
with equality weakened to actual.is_subset(&expected), M1-B stops failing, which
is what makes exactness load-bearing rather than assumed. Two harness faults
halted the run and are recorded in the annex rather than smoothed over; the
second exposed a real weakness in the requirement guard, reported and left for
amendment 3.
Files two candidates this rung does not repair: P13-S29, the invariant-10 tag
multiplexing Chapter 3/4 failures through a public API and its Display; and
P13-S30, the repository-wide assumption that TeX is spelled exactly, whose
requirement-block branch is demonstrated by this rung's own M20.
Baseline 42 suites/1583 -> 43/1586: one new suite, three tests, none removed.
Clippy and the pinned fmt gate clean on 1.95.0; core_spec.pdf rebuilt with zero
undefined references.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
Ratifying amendment 1 discharged its prescriptions and left its prose
describing the state it was written in. Section 6 went on calling itself a
draft, its replacement "proposed", its ratification act pending, and its review
questions open -- while its own status line read RATIFIED and the hold had been
lifted at f9170b0. This does not rewrite that commit; it corrects what
ratification could not correct by itself.
Pin 11 did not cover any of it. Its landing edit reached section 6's revision
records only, so the preamble, the section and subsection lead-ins, and the
review disposition were owned by nothing -- the same shape as the defect pin 11
exists to prevent, one layer in: a document describing a state it is not in,
this time about its own amendment rather than about the rung. Ratification is
not self-applying. A frozen prescription discharges; the prose around it does
not, unless something owns it.
Applied: the preamble becomes a dated record ending the hold at f9170b0, past
tense throughout; 6.3 and 6.7 are marked ratified, with 6.7's two
ratification-act edits marked discharged and its closing paragraph put in past
tense where it had asserted the amendment was not yet ratified; 6.8 becomes a
closed review disposition, each question answered and attributed to the round
that answered it.
Pin 11's third landing edit and gate 13 are widened from "revision records" to
section 6's revision records, preamble and lifecycle records. Widened rather
than re-enumerated: listing the sentences that had gone stale would leave the
next one unowned in exactly the way this amendment repairs. Gate 13 still reads
the status line specifically and never searches the section for DRAFT, which
the revision records legitimately contain.
No implementation target is touched. core_spec.tex, invariants.rs, the ledger
and the guard file remain untouched at 01c621d; baseline unchanged at 1583
passing across 42 suites. Execution resumes at pin 3 with amendment 1's shape
unchanged.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
Execution was dispatched, began, and stopped at pin 3 before its first edit:
pin 3 required item 10 to keep an opening sentence scoped to "cross-cutting
structures" -- a defined term denoting pin 1 group A -- while gaining a nested
list spanning every group. Reported, not patched, per the frozen-pin
discipline; this is that amendment, after five review rounds.
Item 10 gains a subordinated universal deferring to explicit permission only:
"Except where the re-anchoring rules of Chapter~\ref{ch:semops} explicitly
permit transient dangling states during edits, every graph reference resolves
to an extant object." The ratified sentence is retained verbatim beneath it
with its own exception and cross-reference, so nothing normative is removed.
Three subordination forms were tried and the reasoning behind the first two was
itself defective twice. A cross-cutting-scoped exception is not shown wrong --
only unproved, since deciding it needs the exception's surface derived. A bare
"as the re-anchoring rules permit" is ambiguous: it can be read as deferring to
coverage, and coverage is not permission. The re-anchoring table does reach
group E (Cue source, Trajectory endpoint pitch), but both rows prescribe
cascade deletion or immediate replacement -- neither leaves anything dangling,
so reach establishes governance, not permission. The surface derivation is
presented for disposition, not filed: no ledger row is added, and filing in
this contract means a row.
Pin 6 gains the new anchor, an exactly-once requirement within
req:graph:score-graph-invariants, and M21 to sign it. M19 is rebuilt: it
truncates the real opening AND places one complete anchor after the nested
list, so uniqueness stays at one and does not mask the mutation, a prefix slice
passes, and the pinned complete-literal slice starts past the list and fails --
the two anchor kinds driven to opposite verdicts by one mutation.
Two edits belong to this ratification act rather than to pin 11, because the
contract was already dispatched and its top status already untrue; deferring
them would have left the document lying about its lifecycle for the whole of
execution. Both are applied here: this section's status literal, and a
clause-level replacement in the top status paragraph, pinned as Markdown source
so that the ratification date, the owner's authority and the no-count rule all
survive. Pin 11 keeps only the landed forms.
Baseline unchanged at 1583 passing across 42 suites. No pin 3 or pin 6
implementation target has been modified; execution resumes at pin 3.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
The final whole-artifact check returned zero findings. Ratified on the
authority of the repository owner. Contract status: RATIFIED, PINS FROZEN --
executed, not edited; a defect found during execution is reported as its own
amendment with its own review round. NOT YET DISPATCHED: ratification and
dispatch are separate acts and no execution has begun. The status line states
no count of the review passes, per the rule this contract adopted after its own
tallies went stale twice.
Two of the ledger row's own claims did not survive scoping, and the row is
appended -- never rewritten -- with both corrections. The doc comment's G3a
aside is ambiguous, not false: G3a's pin 6 is titled "doc-only" and 6c5e69f
wrote the aside, so "this prose" is self-referential. The row's "claims a
specification repair that never landed" reading is withdrawn, and with it the
"only artifact pointing at the gap" rationale. The two-sided repair stands on a
different footing: the normative enumeration and the doc comment are incomplete
mirrors of each other, incomplete in different places, so neither may be
repaired from the other. The surface is derived from the check bodies instead --
41 tokens, each carrying its resolution target and a symbolic code anchor.
Review scaffolding, applied earlier under a narrow authorization and committed
here because ratification is what changes its staging state: two
DISCUSSED_NOT_CITED rows in requirement_labels.rs. The citation scan reads the
filesystem rather than git, so this contract naming two not-yet-existing labels
broke the mandated green baseline for three review passes before it was
measured. The req:graph: row is permanent -- it never becomes a requirement and
survives only in M6's evidence. The req:time: row is temporary, deleted by pin 4
when the requirement lands, because at that moment its own claim ("discussed,
never cited") turns false; gate 12 checks that deletion, since a stale row is
inert and nothing else would catch it.
The rung also files two candidates it does not repair: P13-S29, the invariant-10
tag multiplexing Chapter 3/4 failures through a public API and its Display; and
P13-S30, the repository-wide assumption that TeX is spelled exactly, which
misses \label {x}, \begin {requirement}, \end {requirement} and \chapter {X}.
S30 carries four consequences with the conditions under which each is silent or
loud -- three of them silent only conditionally, two distinct panic paths, and a
full inventory of the ten known consumer sites across three files, all
test-scope.
Baseline unchanged at 1583 passing across 42 suites; clippy and the pinned
four-crate fmt gate clean on 1.95.0.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
Levi Neuwirth