Prose bankruptcy, dag/test slice: commentary rows become §4c annotations

dag/test/claim/algebra_carrier_roster_witness_test.dag

@@ -11,7 +11,28 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
 
 data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
 
-data carrier_alias_surface_invariant_note: String = "WHAT WENT WRONG ONCE, STATED AS A PROPERTY OF THE ROSTER RATHER THAN AS A MISSING MAP ROW. A spelling that resolves as a declared container alias is returned by resolve_method_receiver_type AS AUTHORED, and method existence is then decided by looking its CANONICAL alias spelling up in kernel_algebra_profile -- container_kind_canonical does exactly that. So a carrier that resolves as a container and whose canonical alias spelling carries no profile has a receiver the compiler admits and a method surface it cannot decide: tree.facts.lookup(node) refused on a PartialFunction receiver while the byte-identical call on Map resolved. One concept, two answers, decided by which spelling the author wrote.\n\nUnder the five hand-authored spelling maps that preceded the roster, that state was not expressible as a violated invariant at all -- it was a row nobody had written, in one of five places, and the only way to find it was for a declaration to refuse. The roster makes the two facts fields on the same spelling row, so the join below is authorable, and this witness asserts it: for every carrier that declares any container_alias_row spelling, the ASCII-least such spelling declares RowPresent method_surface. container_alias_canonical_spelling picks the first sorted key, so the ASCII-least spelling is exactly the one the lookup will land on.\n\nTHE RED IS AUTHORABLE AND IS AUTHORED HERE. carrier_missing_its_alias_surface() is a fixture carrier shaped exactly like the PartialFunction row before its repair -- alias rows declared, method surface absent -- and the same predicate returns false on it. Without that control the invariant would be permanently green over a roster that happens to satisfy it, which DESIGN.md section 4b calls a decoration rather than a wall."
+// WHAT WENT WRONG ONCE, STATED AS A PROPERTY OF THE ROSTER RATHER THAN AS A MISSING MAP ROW. A
+// spelling that resolves as a declared container alias is returned by resolve_method_receiver_type
+// AS AUTHORED, and method existence is then decided by looking its CANONICAL alias spelling up in
+// kernel_algebra_profile -- container_kind_canonical does exactly that. So a carrier that resolves
+// as a container and whose canonical alias spelling carries no profile has a receiver the compiler
+// admits and a method surface it cannot decide: tree.facts.lookup(node) refused on a
+// PartialFunction receiver while the byte-identical call on Map resolved. One concept, two answers,
+// decided by which spelling the author wrote.
+//
+// Under the five hand-authored spelling maps that preceded the roster, that state was not
+// expressible as a violated invariant at all -- it was a row nobody had written, in one of five
+// places, and the only way to find it was for a declaration to refuse. The roster makes the two
+// facts fields on the same spelling row, so the join below is authorable, and this witness asserts
+// it: for every carrier that declares any container_alias_row spelling, the ASCII-least such
+// spelling declares RowPresent method_surface. container_alias_canonical_spelling picks the first
+// sorted key, so the ASCII-least spelling is exactly the one the lookup will land on.
+//
+// THE RED IS AUTHORABLE AND IS AUTHORED HERE. carrier_missing_its_alias_surface() is a fixture
+// carrier shaped exactly like the PartialFunction row before its repair -- alias rows declared,
+// method surface absent -- and the same predicate returns false on it. Without that control the
+// invariant would be permanently green over a roster that happens to satisfy it, which DESIGN.md
+// section 4b calls a decoration rather than a wall.
 
 // The ASCII-least spelling is taken through `sorted_map_keys` rather than through a hand-written
 // comparison, because `sorted_map_keys` is the same primitive `container_alias_canonical_spelling`

dag/test/claim/altra_attachment_stack_witness_test.dag

@@ -68,9 +68,9 @@ fn count_of(xs: List<LayerBlocker>) -> Int {
 }
 
 // THE COMPLETENESS AUTHORITY CROSS-FOOTS. 1960 signal plus 2927 power and ground plus 39 reserved
-// is 4926, and that total must equal the socket's declared contact count reached through a
-// different path — the CPU catalog row. Two independent routes to one population is what makes
-// this a join rather than a number someone typed twice.
+// is 4926, which must equal the socket's declared contact count reached through a different path
+// — the CPU catalog row. Two independent routes to one population make this a join rather than a
+// number typed twice.
 test fn w_the_contact_population_cross_foots_at_4926() -> Bool {
   altra_pin_summary_total() == 4926
     && altra_declared_contact_count() == 4926
@@ -84,20 +84,17 @@ test fn w_the_board_side_termination_population_follows_the_package() -> Bool {
   board_side_termination_population() == 4926
 }
 
-// THE CENTRAL CLAIM, AND THE SPLIT MADE IT SHARPER RATHER THAN WEAKER. It used to read that
-// NEITHER the package nor the land pattern was established, which was true only because the fused
-// type filed a publicly documented dimension under "redistribution undecided" and called that not
-// established. Now the package IS established and the land pattern still is not — which is the
-// claim this test was always trying to make. The package sitting in an already-cited datasheet is
-// exactly what makes the conflation tempting, and asserting it from the established side is a
-// stronger statement than asserting it from two unknowns.
-// INVERTED 2026-08-23 BY THE SOCKET-BODY DRAWING, AND THE CLAIM IT DEFENDS IS UNCHANGED. This
-// witness never asserted that the land pattern is unobtainable; it asserted that the PROCESSOR
-// PACKAGE does not establish it. Both facts are established now, so the discriminating content
-// moved to where it always belonged: they are established by DIFFERENT authorities. A future edit
-// that derives the board land pattern from the package's underside -- the exact category error
-// this module's header exists to make unwritable -- collapses those two authorities into one and
-// fails here.
+// THE CENTRAL CLAIM, AND THE SPLIT MADE IT SHARPER. It used to read that NEITHER the package nor
+// the land pattern was established, true only because the fused type filed a publicly documented
+// dimension under "redistribution undecided". Now the package IS established and the land pattern
+// still is not — the claim this test always made. The package sitting in an already-cited
+// datasheet is what makes the conflation tempting, and asserting from the established side is
+// stronger than asserting from two unknowns.
+// INVERTED 2026-08-23 BY THE SOCKET-BODY DRAWING; THE CLAIM IT DEFENDS IS UNCHANGED. This witness
+// never asserted the land pattern is unobtainable, only that the PROCESSOR PACKAGE does not
+// establish it. Both are established now, by DIFFERENT authorities. A future edit deriving the
+// board land pattern from the package's underside — the category error this module's header makes
+// unwritable — collapses those authorities into one and fails here.
 test fn w_a_public_package_does_not_establish_the_board_land_pattern() -> Bool {
   fact_is_established(f: processor_package_standing.fact)
     && fact_is_established(f: board_land_pattern_standing.fact)
@@ -117,9 +114,9 @@ test fn w_a_public_package_does_not_establish_the_board_land_pattern() -> Bool {
 
 // THE TWO AXES ARE INDEPENDENT, asserted on the one row where both are decided. The package's
 // fact is established AND its carriage admits normalized facts — a pair the earlier type could
-// not represent at all, since it required choosing between "publicly cited" and "redistribution
-// undecided". This is the regression control for the fusion: if the axes are ever collapsed
-// again, one of these two conjuncts becomes unsayable.
+// not represent, since it forced a choice between "publicly cited" and "redistribution
+// undecided". Regression control for the fusion: collapse the axes again and one conjunct becomes
+// unsayable.
 test fn w_an_established_fact_and_a_decided_carriage_coexist() -> Bool {
   fact_is_established(f: processor_package_standing.fact)
     && match processor_package_standing.carriage {
@@ -149,19 +146,18 @@ test fn w_an_unresolved_fact_carries_no_carriage_decision() -> Bool {
 
 // THREE CATEGORIES, DISTINGUISHED BY WHO ACTS. An unresolved authority is someone reading a
 // datasheet, a redistribution question is a legal decision, an NDA gate is a commercial
-// relationship. If these collapsed to one "not ready" state the tractable blockers would be
-// indistinguishable from the intractable one — which is precisely the error that once had this
-// repository declaring a public pin map NDA-only.
-// THE SUBJECT AND THE ROUTE ARE DIFFERENT FACTS, and this asserts they have not been
-// swapped. An earlier revision put the subject label into the route field, so a consumer
-// asking WHERE to obtain the collateral was told WHAT it is. Both are checked, and the
-// route is checked as an authority rather than as text — which is what makes the swap
-// unwritable now rather than merely absent.
+// relationship. Collapsed to one "not ready" state, the tractable blockers would be
+// indistinguishable from the intractable one — the error that once had this repository declaring
+// a public pin map NDA-only.
+// THE SUBJECT AND THE ROUTE ARE DIFFERENT FACTS, asserted not swapped. An earlier revision put the
+// subject label into the route field, so a consumer asking WHERE to obtain the collateral was told
+// WHAT it is. Both are checked, the route as an authority rather than text — which makes the swap
+// unwritable rather than merely absent.
 //
 // The land-pattern blocker went from "commercial" to "none" on 2026-08-23 when the socket vendor
-// supplied the drawing. The witness still discriminates all three blocker KINDS -- that is what it
-// is named for -- and the reference-board collateral below still carries the commercial one, so
-// no arm of blocker_kind lost its coverage when this layer stopped being blocked.
+// supplied the drawing. The witness still discriminates all three blocker KINDS, and the
+// reference-board collateral below still carries the commercial one, so no arm of blocker_kind
+// lost coverage.
 test fn w_the_three_blocker_kinds_are_distinct() -> Bool {
   let package_blocker = match layer_blocker(row: processor_package_standing) {
     Absent => "none"
@@ -184,11 +180,10 @@ test fn w_the_three_blocker_kinds_are_distinct() -> Bool {
     }
 }
 
-// THE REDISTRIBUTION BLOCKER NEEDS A CONTROLLED FIXTURE NOW, and that is a improvement rather
-// than a workaround. It used to be demonstrated by the processor package row, whose carriage the
-// legal ruling has since decided — so the production row stopped being a specimen of the blocker
-// and the test would have quietly measured nothing. A planted row keeps the arm executed and
-// keeps it independent of any decision made about a real subject.
+// THE REDISTRIBUTION BLOCKER NEEDS A CONTROLLED FIXTURE NOW — an improvement, not a workaround. It
+// was demonstrated by the processor package row, whose carriage the legal ruling has since
+// decided, so that row stopped being a specimen and the test would have measured nothing. A
+// planted row keeps the arm executed and independent of decisions about real subjects.
 fn undecided_carriage_blocker() -> String {
   let planted = AttachmentLayerStanding {
     layer: board_land_pattern_standing.layer,
@@ -203,16 +198,14 @@ fn undecided_carriage_blocker() -> String {
 
 // NO ATTACHMENT LAYER IS BEHIND THE NDA BOUNDARY ANY MORE, AND THAT IS THE POINT OF THE RENAME.
 // This asserted "exactly one" while the board land pattern's only route ran through Ampere
-// Customer Connect. The socket vendor answered on 2026-08-23, so the count is now zero and the
-// witness is renamed rather than edited in place: a witness whose name says ONE while it asserts
-// ZERO is a stale claim that greps as a live one, which is the positional-citation failure applied
-// to test names.
+// Customer Connect. The socket vendor answered on 2026-08-23, so the count is zero and the witness
+// is renamed rather than edited in place: a name saying ONE over an assertion of ZERO is a stale
+// claim that greps as live — the positional-citation failure applied to test names.
 //
-// The claim it defends survives intact and is still executed rather than asserted in prose: the
-// land pattern is reached through a route this repository can publish, so the layer that was
-// gated is now established. If any layer regresses to FactAccessGated -- a future part whose only
-// geometry sits behind Customer Connect -- the count goes non-zero and this fails, which is
-// exactly the alarm the original witness existed to raise.
+// The claim survives and is still executed: the land pattern is reached through a route this
+// repository can publish, so the gated layer is established. If any layer regresses to
+// FactAccessGated — a future part whose only geometry sits behind Customer Connect — the count
+// goes non-zero and this fails, the alarm the original witness existed to raise.
 test fn w_no_attachment_layer_is_behind_the_nda_boundary() -> Bool {
   let nda_layers = fold(attachment_stack, init: 0, f: fn(acc, row) {
     match row.fact {
@@ -231,9 +224,9 @@ test fn w_no_attachment_layer_is_behind_the_nda_boundary() -> Bool {
     }
 }
 
-// SIX LAYERS, SIX BLOCKERS, NONE ESTABLISHED — and this is the honest state of the attachment
-// stack today rather than a target. It is asserted by count so that establishing one layer moves
-// the number instead of silently satisfying a name.
+// SIX LAYERS, SIX BLOCKERS, NONE ESTABLISHED — the honest state of the attachment stack today, not
+// a target. Asserted by count so establishing one layer moves the number instead of silently
+// satisfying a name.
 test fn w_every_attachment_layer_is_open_and_says_why() -> Bool {
   let layers = fold(attachment_stack, init: 0, f: fn(acc, _r) { acc + 1 })
   let package_resolved = match layer_blocker(row: processor_package_standing) {
@@ -261,20 +254,19 @@ test fn w_the_layers_are_named_distinctly() -> Bool {
     && (attachment_layer_name(l: ProcessorPackageLayer) as String) != (attachment_layer_name(l: BoardLandPatternLayer) as String)
 }
 
-// EVERY LAYER THIS BOARD CARRIES IS A COHERENT PAIR. This runs over the live population rather than
-// a fixture, so it is the claim that the six standings authored in this module actually mean
-// something -- and it is the one that would have caught the defect if it had existed when the axes
-// were split.
+// EVERY LAYER THIS BOARD CARRIES IS A COHERENT PAIR. Runs over the live population rather than a
+// fixture, so it is the claim that the six standings authored here mean something — and the one
+// that would have caught the defect had it existed when the axes were split.
 test fn w_every_layer_standing_is_a_coherent_pair() -> Bool {
   fold(attachment_stack, init: true, f: fn(acc, st) {
     acc && standing_pair_is_admitted(fact: st.fact, carriage: st.carriage)
   })
 }
 
 // THE THREE DISCRIMINATING REDS, one per incoherent combination, each authored here rather than
-// found in the tree. Without these the claim above is satisfied by a refusal function that never
-// fires -- which is exactly what subject_blocker was doing before this change: answering an
-// established fact with inapplicable carriage as though nothing blocked it.
+// found in the tree. Without them the claim above is satisfied by a refusal function that never
+// fires — what subject_blocker did before this change: answering an established fact with
+// inapplicable carriage as though nothing blocked it.
 test fn w_an_established_fact_cannot_have_inapplicable_carriage() -> Bool {
   match authority_standing_refusal(
     fact: processor_package_standing.fact,
@@ -321,13 +313,12 @@ test fn w_the_coherent_pairs_are_admitted() -> Bool {
     )
 }
 
-// THE DISCRIMINATING CONTROL FOR THE JOINT CHECK. This row is planted, not live: an established
-// fact whose carriage says the question does not apply, which is precisely the pair
-// authority_standing_refusal names EstablishedFactHasInapplicableCarriage. Before the projection
-// consulted that refusal, the coherence check called this row refused while layer_blocker answered
-// Absent, so a consumer reading the blockers saw a settled layer -- two answers about one row,
-// disagreeing, with the reassuring one on the path everything downstream reads. Both directions
-// are asserted here so neither half can quietly stop firing.
+// THE DISCRIMINATING CONTROL FOR THE JOINT CHECK. Planted, not live: an established fact whose
+// carriage says the question does not apply — the pair authority_standing_refusal names
+// EstablishedFactHasInapplicableCarriage. Before the projection consulted that refusal, the
+// coherence check called this row refused while layer_blocker answered Absent: two disagreeing
+// answers about one row, the reassuring one on the path everything downstream reads. Both
+// directions are asserted so neither half can quietly stop firing.
 fn incoherent_row() -> AttachmentLayerStanding {
   AttachmentLayerStanding {
     layer: BoardLandPatternLayer,

dag/test/claim/annotation_erasure_emission_witness_test.dag

@@ -1,6 +1,17 @@
 module test.claim.annotation_erasure_emission_witness_test
 
-data annotation_erasure_emission_migration_note: String = "Migrated from src/v1/tests/claim/v1_annotation_target_emission_test.dag (dead witness tree triage, dashboard node adhoc-9b80ec49-d63). That file's own NEXT TRIGGER named exactly what was missing: 'a .dag-reachable surface returning emitted files for a synthetic source... then all three arms enroll together in this file and this receipt dissolves.' compile_dag_rust_emit_check is that surface: it compiles a synthetic source through the real v1 pipeline and lets a witness assert on the emitted Rust text via includes/excludes. It does not hand back raw bytes for a diff, so this is not a byte-identical replay of the 2026-08-05 host-execution receipt (annotated vs bare fixtures, `diff -r` reporting zero difference) — that receipt stands as historical evidence and is not restated as a live claim. What migrates is the same D-C property 4 argument (prose reaches the target program nowhere) using excludes on the literal prose strings, paired with a non-vacuity control proving the check tracks real emitted content rather than passing on any input."
+// Migrated from src/v1/tests/claim/v1_annotation_target_emission_test.dag (dead witness tree
+// triage, dashboard node adhoc-9b80ec49-d63). That file's own NEXT TRIGGER named exactly what was
+// missing: 'a .dag-reachable surface returning emitted files for a synthetic source... then all
+// three arms enroll together in this file and this receipt dissolves.' compile_dag_rust_emit_check
+// is that surface: it compiles a synthetic source through the real v1 pipeline and lets a witness
+// assert on the emitted Rust text via includes/excludes. It does not hand back raw bytes for a
+// diff, so this is not a byte-identical replay of the 2026-08-05 host-execution receipt (annotated
+// vs bare fixtures, `diff -r` reporting zero difference) — that receipt stands as historical
+// evidence and is not restated as a live claim. What migrates is the same D-C property 4 argument
+// (prose reaches the target program nowhere) using excludes on the literal prose strings, paired
+// with a non-vacuity control proving the check tracks real emitted content rather than passing on
+// any input.
 
 data annotated_source_alpha_marker_a: String = "module emit_probe_one\n\n// prose about alpha\ndata alpha: Int = 424242\n\n// prose about probe\nfn probe(x: Int) -> Int {\n  x + alpha\n}\n"