From ed47ce748c5916f745d5728b2e0d661368c780a8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 22 Sep 2026 02:53:43 +0000 Subject: [PATCH 1/6] wip --- src/v2/std/symbol_index.dag | 35 ++- ...election_fold_two_implementations_test.dag | 194 ++++++++++++ .../claim/coercion/two_algebra_fork_test.dag | 279 ++++++++++++++++++ 3 files changed, 498 insertions(+), 10 deletions(-) create mode 100644 src/v2/test/claim/binding/selection_fold_two_implementations_test.dag create mode 100644 src/v2/test/claim/coercion/two_algebra_fork_test.dag diff --git a/src/v2/std/symbol_index.dag b/src/v2/std/symbol_index.dag index ff23a2a1b7f..b91ec51d341 100644 --- a/src/v2/std/symbol_index.dag +++ b/src/v2/std/symbol_index.dag @@ -175,17 +175,17 @@ fn symbol_index_lexical_collect( } } -fn symbol_index_lexical_lookup( - index: SymbolIndex, - position: QualifiedName, - name: Symbol +// THE SELECTION STEP, SPLIT FROM ITS PRODUCER SO THE BOUNDARY CAN BE ASKED DIRECTLY. +// This fold is the none/one/many trichotomy over an ALREADY-COLLECTED candidate population; the +// chain walk that produces that population is a separate, legitimately layered concern +// (symbol_index_lexical_collect). They were one function, so the trichotomy could only be reached +// by executing the walk -- which makes every claim about the SELECTION a claim about the walk too +// (DESIGN section 3, the witness standing rule: a witness discriminates at ONE interface with its +// inputs supplied at that boundary). Nothing about the answer changes: symbol_index_lexical_lookup +// below is the same composition it always was. +fn symbol_index_lexical_selection( + candidates: FreeMonoid ) -> LexicalLookup { - let candidates = symbol_index_lexical_collect( - index: index, - position: position, - name: name, - acc: Empty - ) match length(xs: candidates) { 0 => LexicalUnbound 1 => @@ -197,3 +197,18 @@ fn symbol_index_lexical_lookup( _ => LexicalAmbiguous { candidates: candidates } } } + +fn symbol_index_lexical_lookup( + index: SymbolIndex, + position: QualifiedName, + name: Symbol +) -> LexicalLookup { + symbol_index_lexical_selection( + candidates: symbol_index_lexical_collect( + index: index, + position: position, + name: name, + acc: Empty + ) + ) +} diff --git a/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag b/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag new file mode 100644 index 00000000000..7636788f956 --- /dev/null +++ b/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag @@ -0,0 +1,194 @@ +module v2.test.claim.binding.selection_fold_two_implementations + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// WHAT THIS WITNESS DISCRIMINATES, AND WHAT IT DELIBERATELY DOES NOT. +// +// One rule -- a candidate population is answered Unbound at none, Bound at exactly one, Ambiguous +// at more than one -- has TWO implementations. std.occurrence_binding +// occurrence_binding_from_candidates reaches it through an explicit +// FoldZero/FoldOne/FoldMany accumulator; v2.std.symbol_index symbol_index_lexical_selection reaches +// it through `match length(candidates)`. Nothing joins them, so a divergence would be silent. +// +// THE SUBJECT IS THE SELECTION FOLD ON A SUPPLIED POPULATION, and nothing wider. Their agreement on +// a PRODUCTION SITE is not measurable here and this witness does not claim it: no v2 resolution site +// is answered by std's fold, and std.occurrence_binding's own staged-adoption note states that +// LexicalLookup is not an interim consumer because it carries no exact reference-occurrence Node or +// occurrence containment identity. Binding the two at a production site would fabricate exactly the +// relation that carrier preserves. What is measurable today is whether the two folds classify one +// supplied population the same way, which is a different and narrower subject. +// +// THE CANDIDATE PRODUCERS ARE NOT COMPARED. std's candidates are supplied by its caller; v2's are +// produced by symbol_index_lexical_collect walking the containment chain. Those are legitimately +// layered and are not the fork. symbol_index_lexical_selection exists so the selection boundary can +// be asked with its inputs supplied (DESIGN section 3, the witness standing rule) rather than by +// executing the walk beneath it. +// +// NEITHER FOLD IS THE ORACLE FOR THE OTHER. Two implementations of one misunderstanding agree +// perfectly, so agreement alone is a change detector. Each row therefore carries an INDEPENDENTLY +// SPECIFIED expected class, read off the trichotomy as the modeled contract states it -- over the +// MULTIPLICITY of the supplied list, not over the cardinality of its distinct members. That is why +// the duplicate row below expects Ambiguous: neither contract declares a deduplication step, so a +// population naming one candidate twice is a two-candidate population. The first two claims below +// hold each fold to that expectation separately, so a row can report BOTH AGREE AND BOTH ARE WRONG; +// the third claim reports the join. + +type BindingSelectionClass + = SelectionUnbound + | SelectionBound + | SelectionAmbiguous + +type BindingSelectionFixture { + label: Symbol + candidate_names: List + expected: BindingSelectionClass +} + +// THE POPULATION, AND WHY IT IS THE DISCRIMINATING ONE. Each row sits on a boundary of the +// trichotomy rather than in the interior of an arm: the empty population (the arm a length-keyed +// match and an accumulator reach by different routes), the singleton (the only arm that must +// PRODUCE a candidate rather than classify), the first population above the singleton, the same +// population spelled with one name repeated (where a deduplicating implementation would answer +// Bound), and one above the pair (where an accumulator that only tracks first and second could +// lose a member). +data binding_selection_fixtures: List = [ + { + label: ^empty_population, + candidate_names: [], + expected: SelectionUnbound + }, + { + label: ^singleton_population, + candidate_names: [^alpha], + expected: SelectionBound + }, + { + label: ^two_distinct_candidates, + candidate_names: [^alpha, ^beta], + expected: SelectionAmbiguous + }, + { + label: ^duplicate_candidate, + candidate_names: [^alpha, ^alpha], + expected: SelectionAmbiguous + }, + { + label: ^three_distinct_candidates, + candidate_names: [^alpha, ^beta, ^gamma], + expected: SelectionAmbiguous + } +] + +fn binding_fixture_occurrence() -> BindingOccurrence { + BindingOccurrence { + containment: ContainmentPath { + ancestors: [^fixture_module], + terminal: ^fixture_reference + } + } +} + +fn binding_fixture_std_candidates(names: List) -> List> { + map(names, fn(n) { + BindingCandidate { + containment: ContainmentPath { + ancestors: [^fixture_module], + terminal: n + } + } + }) +} + +fn binding_fixture_node(name: Symbol) -> Node { + Node { + kind: TypeNode { connective: Atom { identity: name } }, + children: [], + occurrence_id: OccurrenceSynthetic + } +} + +fn binding_fixture_lexical_candidates(names: List) -> List { + map(names, fn(n) { + LexicalBindingCandidate { + path: qualified_name_snoc( + qn: qualified_name_from_dotted_string(dotted: "v2.test.binding_fixture"), + segment: n + ), + node: binding_fixture_node(name: n) + } + }) +} + +fn binding_std_class(names: List) -> BindingSelectionClass { + match occurrence_binding_from_candidates( + occurrence: binding_fixture_occurrence(), + candidates: binding_fixture_std_candidates(names: names) + ) { + OccurrenceUnbound { occurrence: _ } => SelectionUnbound + OccurrenceBound { binding: _ } => SelectionBound + OccurrenceAmbiguous { occurrence: _, candidates: _ } => SelectionAmbiguous + } +} + +fn binding_lexical_class(names: List) -> BindingSelectionClass { + match symbol_index_lexical_selection( + candidates: binding_fixture_lexical_candidates(names: names) + ) { + LexicalUnbound => SelectionUnbound + LexicalHit { node: _, path: _ } => SelectionBound + LexicalAmbiguous { candidates: _ } => SelectionAmbiguous + } +} + +fn binding_selection_class_equal( + left: BindingSelectionClass, + right: BindingSelectionClass +) -> Bool { + match left { + SelectionUnbound => match right { + SelectionUnbound => true + SelectionBound => false + SelectionAmbiguous => false + } + SelectionBound => match right { + SelectionUnbound => false + SelectionBound => true + SelectionAmbiguous => false + } + SelectionAmbiguous => match right { + SelectionUnbound => false + SelectionBound => false + SelectionAmbiguous => true + } + } +} + +// std's fold against the trichotomy, NOT against v2's answer. +test fn occurrence_binding_fold_matches_the_declared_trichotomy_holds() -> Bool { + fold(binding_selection_fixtures, init: true, f: fn(acc, row) { + acc && binding_selection_class_equal( + left: binding_std_class(names: row.candidate_names), + right: row.expected + ) + }) +} + +// v2's selection against the same independently specified trichotomy, NOT against std's answer. +test fn lexical_selection_matches_the_declared_trichotomy_holds() -> Bool { + fold(binding_selection_fixtures, init: true, f: fn(acc, row) { + acc && binding_selection_class_equal( + left: binding_lexical_class(names: row.candidate_names), + right: row.expected + ) + }) +} + +// The join the corpus does not otherwise carry: one rule, two implementations, one population. +test fn the_two_selection_folds_agree_on_the_supplied_population_holds() -> Bool { + fold(binding_selection_fixtures, init: true, f: fn(acc, row) { + acc && binding_selection_class_equal( + left: binding_std_class(names: row.candidate_names), + right: binding_lexical_class(names: row.candidate_names) + ) + }) +} diff --git a/src/v2/test/claim/coercion/two_algebra_fork_test.dag b/src/v2/test/claim/coercion/two_algebra_fork_test.dag new file mode 100644 index 00000000000..fcb45c03021 --- /dev/null +++ b/src/v2/test/claim/coercion/two_algebra_fork_test.dag @@ -0,0 +1,279 @@ +module v2.test.claim.coercion.two_algebra_fork + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// ONE QUESTION -- may this value cross from one model to another -- ANSWERED BY TWO UNRELATED +// ALGEBRAS, and until this witness nothing joined them. +// +// (a) THE NAME-KEYED ALGEBRA. std.coercion dag_can_cast folds over two authored rosters of +// (from_type, to_type) SPELLINGS: dag_cast_rules and grounded_primitive_coproduct_identities. +// This side executes and is load-bearing -- v1.compiler.infer consults it at argument-versus- +// formal admission, at literal admission, and in the type-relation fold, and +// v1.compiler.coercion builds on it. +// (b) THE HOMOMORPHISM ALGEBRA. v2.std.coercion coercion_fold asks v2.std.find_witness +// find_witness for a structure-preserving witness from the source node into a candidate set, +// and returns a CoercionResult carrying a CoercionWitness and a CoercionQuality. This is the +// form DESIGN section 4 specifies -- coercion as a homomorphism check, one procedure asked +// sideways. It has NO established executing consumer in the corpus today; that blank is a +// fact this witness records rather than one it repairs. +// +// WHY THIS IS ASKABLE WITH NO NEW CAPABILITY: both are pure folds in the interpreted corpus, so one +// supplied population of source-and-target pairs reaches both. Nothing is emitted, nothing beneath +// the two folds is executed to produce the inputs (DESIGN section 3, the witness standing rule). +// +// NEITHER FOLD IS THE ORACLE FOR THE OTHER, so each row carries TWO independently specified +// expectations and the claims below hold each algebra to its OWN contract before the join is read: +// +// expected_name_keyed_admits -- read off the declared rosters in std.coercion. A crossing is +// admitted exactly when a row spells it, in dag_cast_rules or in the grounded +// primitive-to-coproduct identities. This is a transcription of the DECLARATION, so a roster +// edit reds the first claim rather than silently moving the join. +// expected_homomorphism_admits -- read off the homomorphism contract as it is realized. The only +// preservation rule coercion_fold applies is +// preservation_rule_exact_structural_equality_zip_fold, whose predicate holds exactly when +// the candidate is structurally equal to the source. So the homomorphism algebra admits a +// crossing exactly when source and target are the SAME model, and admits it at quality +// Identity. Nothing in that side spells a non-identity crossing at all. +// +// A row can therefore report BOTH AGREE AND BOTH ARE WRONG, or either algebra deviating from its +// own declared contract, rather than only "the two folds match". + +type CoercionAdmission + = CrossingAdmitted + | CrossingRefused + +// A ROW CARRIES THE PAIR TWICE, AND THAT IS THE FORK ITSELF MADE VISIBLE. The name-keyed algebra +// keys on a type-name STRING; the homomorphism algebra keys on an atom's node IDENTITY. There is no +// conversion between them in the corpus, so a fixture that wanted to supply one pair to both must +// author both spellings and assert by construction that they denote one model. That missing +// conversion is not an inconvenience of the witness -- it is the measurement: two authorities for +// one fact share no key. +type CoercionForkFixture { + label: Symbol + source_type: String + target_type: String + source_name: Symbol + target_name: Symbol + expected_name_keyed: CoercionAdmission + expected_homomorphism: CoercionAdmission + expected_algebras_agree: Bool +} + +// THE POPULATION, AND WHY IT IS THE DISCRIMINATING ONE. The two algebras partition the pair space +// into four cells, and the population inhabits all four -- a witness restricted to the happy path +// would only ever see the first. +// +// both admit -- int_to_int, float_to_float: a declared row whose source and target are one +// model, the only shape on which the two algebras can coincide. +// both refuse -- bool_to_float: no declared row and no structural equality. +// name-only -- int_to_float (a declared widening), bool_to_int (a declared crossing with +// no structural relation at all), int_to_nat (a GROUNDED identity that the +// name-keyed side carries in its own second roster). Each is a crossing the +// executing algebra permits and the specified algebra cannot spell. +// homomorphism-only -- string_to_string: an IDENTITY crossing, which the name-keyed roster does +// not carry a row for, so the executing side refuses a value crossing to its +// own model while the homomorphism side admits it at quality Identity. This +// is the sharpest cell and it is the one an agreement-only witness would +// never reach. +data coercion_fork_fixtures: List = [ + { + label: ^int_to_int, + source_type: "Int", + target_type: "Int", + source_name: ^Int, + target_name: ^Int, + expected_name_keyed: CrossingAdmitted, + expected_homomorphism: CrossingAdmitted, + expected_algebras_agree: true + }, + { + label: ^float_to_float, + source_type: "Float", + target_type: "Float", + source_name: ^Float, + target_name: ^Float, + expected_name_keyed: CrossingAdmitted, + expected_homomorphism: CrossingAdmitted, + expected_algebras_agree: true + }, + { + label: ^int_to_float, + source_type: "Int", + target_type: "Float", + source_name: ^Int, + target_name: ^Float, + expected_name_keyed: CrossingAdmitted, + expected_homomorphism: CrossingRefused, + expected_algebras_agree: false + }, + { + label: ^bool_to_int, + source_type: "Bool", + target_type: "Int", + source_name: ^Bool, + target_name: ^Int, + expected_name_keyed: CrossingAdmitted, + expected_homomorphism: CrossingRefused, + expected_algebras_agree: false + }, + { + label: ^int_to_nat, + source_type: "Int", + target_type: "Nat", + source_name: ^Int, + target_name: ^Nat, + expected_name_keyed: CrossingAdmitted, + expected_homomorphism: CrossingRefused, + expected_algebras_agree: false + }, + { + label: ^string_to_string, + source_type: "String", + target_type: "String", + source_name: ^String, + target_name: ^String, + expected_name_keyed: CrossingRefused, + expected_homomorphism: CrossingAdmitted, + expected_algebras_agree: false + }, + { + label: ^bool_to_float, + source_type: "Bool", + target_type: "Float", + source_name: ^Bool, + target_name: ^Float, + expected_name_keyed: CrossingRefused, + expected_homomorphism: CrossingRefused, + expected_algebras_agree: true + } +] + +fn coercion_fork_model_node(name: Symbol) -> Node { + Node { + kind: TypeNode { connective: Atom { identity: name } }, + children: [], + occurrence_id: OccurrenceSynthetic + } +} + +fn coercion_fork_grounding(name: Symbol) -> CanonicalGrounding { + CanonicalGrounding { + node: coercion_fork_model_node(name: name), + witness: CanonicalGroundingWitness { + structural: StructuralPropertyWitness { + property: ^coercion_fork_fixture_structural_property, + evidence: coercion_fork_model_node(name: name) + }, + closedness: StructuralPropertyWitness { + property: ^coercion_fork_fixture_candidate_set_closedness, + evidence: coercion_fork_model_node(name: name) + } + } + } +} + +fn coercion_fork_candidate_set(target_name: Symbol) -> CoercionCandidateSet { + CoercionCandidateSet { + set: CandidateSet { + candidates: [coercion_fork_model_node(name: target_name)], + closedness: StructuralPropertyWitness { + property: ^coercion_fork_fixture_candidate_set_closedness, + evidence: coercion_fork_model_node(name: target_name) + } + } + } +} + +// (a) the name-keyed algebra, asked with the pair supplied as the two spellings it keys on. +fn coercion_fork_name_keyed_admission(row: CoercionForkFixture) -> CoercionAdmission { + if dag_can_cast( + source_type: row.source_type, + target_type: row.target_type + ) { + CrossingAdmitted + } else { + CrossingRefused + } +} + +// (b) the homomorphism algebra, asked with the same pair supplied as a source model and a +// one-member candidate set. The declared priority names the sole candidate, so multiplicity policy +// cannot be what decides the answer. +fn coercion_fork_homomorphism_outcome(row: CoercionForkFixture) -> Outcome { + coercion_fold( + source: coercion_fork_grounding(name: row.source_name), + candidates: coercion_fork_candidate_set(target_name: row.target_name), + policy: TargetDeclaredPriority { + priority: coercion_fork_model_node(name: row.target_name) + } + ) +} + +fn coercion_fork_homomorphism_admission(row: CoercionForkFixture) -> CoercionAdmission { + match coercion_fork_homomorphism_outcome(row: row) { + Accepted { value: _, diagnostics: _ } => CrossingAdmitted + Rejected { diagnostics: _ } => CrossingRefused + } +} + +fn coercion_admission_equal(left: CoercionAdmission, right: CoercionAdmission) -> Bool { + match left { + CrossingAdmitted => match right { + CrossingAdmitted => true + CrossingRefused => false + } + CrossingRefused => match right { + CrossingAdmitted => false + CrossingRefused => true + } + } +} + +// The name-keyed algebra against the DECLARED ROSTERS, not against the other algebra. +test fn name_keyed_coercion_matches_the_declared_cast_rosters_holds() -> Bool { + fold(coercion_fork_fixtures, init: true, f: fn(acc, row) { + acc && coercion_admission_equal( + left: coercion_fork_name_keyed_admission(row: row), + right: row.expected_name_keyed + ) + }) +} + +// The homomorphism algebra against the HOMOMORPHISM CONTRACT, not against the other algebra. +test fn homomorphism_coercion_matches_the_structural_preservation_contract_holds() -> Bool { + fold(coercion_fork_fixtures, init: true, f: fn(acc, row) { + acc && coercion_admission_equal( + left: coercion_fork_homomorphism_admission(row: row), + right: row.expected_homomorphism + ) + }) +} + +// An admitted crossing on the homomorphism side is an IDENTITY and never anything else: the only +// realized preservation rule is exact structural equality, so no row may come back Exact or Widened. +// This is what makes the name-only cells a missing SPELLING rather than a stricter policy. +test fn homomorphism_coercion_admits_only_identity_quality_holds() -> Bool { + fold(coercion_fork_fixtures, init: true, f: fn(acc, row) { + acc && match coercion_fork_homomorphism_outcome(row: row) { + Accepted { value: result, diagnostics: _ } => match result.quality { + Identity => true + Exact => false + Widened => false + } + Rejected { diagnostics: _ } => true + } + }) +} + +// THE JOIN. This claim pins the CURRENT, MEASURED relation between the two algebras pair by pair, +// including the four rows on which they disagree. It is green while the fork stands exactly as +// authored and reds the moment either side's admission set moves -- in either direction, so +// consolidating the fork reds it too and the consolidator is the one who must restate the row. +test fn the_two_coercion_algebras_agree_exactly_where_declared_holds() -> Bool { + fold(coercion_fork_fixtures, init: true, f: fn(acc, row) { + acc && (coercion_admission_equal( + left: coercion_fork_name_keyed_admission(row: row), + right: coercion_fork_homomorphism_admission(row: row) + ) == row.expected_algebras_agree) + }) +} From 352cab8ecb955faa853cc8ae16687c475010206c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 22 Sep 2026 07:31:16 +0000 Subject: [PATCH 2/6] wip: pairing-obligation inhabitance claim + W1 failure-mode row --- ...thorities_keyed_on_different_relations.dag | 30 +++++++ ...election_fold_two_implementations_test.dag | 90 +++++++++++++++++++ 2 files changed, 120 insertions(+) create mode 100644 dag/gunbc/recurring_failure_mode/two_admission_authorities_keyed_on_different_relations.dag diff --git a/dag/gunbc/recurring_failure_mode/two_admission_authorities_keyed_on_different_relations.dag b/dag/gunbc/recurring_failure_mode/two_admission_authorities_keyed_on_different_relations.dag new file mode 100644 index 00000000000..91a3d2e43ef --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/two_admission_authorities_keyed_on_different_relations.dag @@ -0,0 +1,30 @@ +module gunbc.recurring_failure_mode.two_admission_authorities_keyed_on_different_relations + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data two_admission_authorities_keyed_on_different_relations: RecurringFailureMode = RecurringFailureMode { + identity: "two_admission_authorities_keyed_on_different_relations" as NonEmptyStr, + + receipts: [ + "INVALID STATE: two authorities answer one admission question -- may this value cross from one model to another -- and each is keyed on a DIFFERENT IDENTITY RELATION, with no conversion between the two keys anywhere in the corpus.", + + "HARM: the ordinary single-authority fork (DESIGN section 3) is at least comparable -- two answers to one question, so a join can be written and a disagreement can be made to refuse. This class is worse in a way that hides it: the two answers cannot be compared AT ALL without an authored bridge, so no join exists to go red, no census counts the divergence, and the fork does not present as a fork. It presents as two unrelated modules. The cost is paid at consolidation, when the bridge must be authored anyway and every decision taken in the meantime was premised on whichever key the local caller happened to hold.", + + "DISTINGUISHING FACTS, and the first is the recognition rule: A FIXTURE THAT WANTS TO ASK BOTH AUTHORITIES ABOUT ONE SUBJECT MUST AUTHOR THE SUBJECT TWICE. That is not fixture awkwardness -- it IS the measurement, and it is available before any execution. Further tells: the two admission sets differ in BOTH directions, so neither authority is merely the stricter one and the comfortable reading is unavailable; and one side's key is a SPELLING while the other's is a resolved structural identity.", + + "SPECIMEN 1 (gunbc, 2026-09-22, v2.test.claim.coercion.two_algebra_fork). std.coercion dag_can_cast folds over dag_cast_rules and grounded_primitive_coproduct_identities, keyed on TYPE-NAME STRINGS, and it executes: v1.compiler.infer consults it at argument-versus-formal admission, at literal admission, and in the type-relation fold. v2.std.coercion coercion_fold asks v2.std.find_witness find_witness for a structure-preserving witness, keyed on NODE IDENTITY, and it has no established executing consumer. Measured over seven supplied pairs, the admission sets differ in both directions: Int->Float, Bool->Int and Int->Nat are admitted name-only, while String->String -- an IDENTITY crossing -- is admitted homomorphism-only, because dag_cast_rules carries no identity row for it. The sharpest single fact is that last one: the case everyone assumes is free is the case the executing authority refuses.", + + "SPECIMEN 2 (gunbc, 2026-09-22, smart-tern-891, a different surface and an independent sighting). One resource appeared under two labels, Network and std.resources.Network, because a diagnostic field carried the caller's IMPORT SPELLING while the wall itself compared through the resolved declaration identity. Correct by identity in one place, keyed by spelling in another, and only the second was load-bearing for the new consumer. Two independent sightings on one day is what makes this a class rather than a fact about coercion.", + + "RUNG FOUND AT: below the ladder for the divergence itself -- nothing refuses, nothing counts it, and each authority answers confidently within its own key. The coercion specimen is now MITIGATABLE at the measurement grain only: v2.test.claim.coercion.two_algebra_fork pins the admission relation pair by pair over a supplied population, so a change to either side's admission set reds a claim. That is a wall around the MEASUREMENT, not around the state.", + + "CEILING: structurally impossible, and the derivation is ordinary rather than aspirational. Admission over a key relation is decidable and fully modeled, so one authority keyed on one relation makes the divergent state unwritable -- there is no second admission set to diverge from. The ceiling is reached by a replacement migration (DESIGN section 3, replacement migrations cut over at the root), not by a check: one key wins, the other algebra is cut at its root, and the surviving authority carries every refusal the cut one carried.", + + "NEXT TRIGGER: the route belongs in the identity key. Concretely, an admission authority whose key is a resolved declaration identity rather than a spelling, and one conversion or one deletion -- not a bridge kept standing, which would be a third authority. The measurement lands first deliberately: the repair is a replacement migration with its own blast radius, and it should start from executed values rather than from the derivation that found them.", + + "WHAT IS NOT CLAIMED: no wrong compiled output is attributed to the coercion specimen. The homomorphism side has no executing consumer, so the divergence has had no opportunity to produce one. The class is filed on the STATE SPACE -- two admission authorities that cannot be compared -- and a class that has produced no incident is the one that will otherwise be found last.", + ], + + evidence: [], +} diff --git a/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag b/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag index 7636788f956..1fbadcfd8e0 100644 --- a/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag +++ b/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag @@ -192,3 +192,93 @@ test fn the_two_selection_folds_agree_on_the_supplied_population_holds() -> Bool ) }) } + +// THE PAIRING OBLIGATION FOR THE SUPPLIED BOUNDARY (DESIGN section 3). Every claim above hands +// symbol_index_lexical_selection a population it constructed, so those claims are hypotheses about +// a boundary until one claim establishes that the REAL producer emits that shape and still runs. +// This one does both, and it asserts the ROUTE rather than only the answer: it builds a real module +// root, fills a real SymbolIndex, walks the real containment chain with +// symbol_index_lexical_collect, and then feeds THAT population -- not a fixture -- into the same +// selection fold the claims above supply. So deleting the walk cannot leave the suite green. + +data binding_inhabitance_module_qn: List = qualified_name_from_dotted_string( + dotted: "v2.test.binding_inhabitance" +) + +fn binding_inhabitance_qn_spine(segments: List) -> Node { + fold_list_node( + xs: segments, + item_node: fn(sym) { binding_fixture_node(name: sym) } + ) +} + +fn binding_inhabitance_variant_edge(type_sym: Symbol, variants: List) -> Edge { + Edge { + label: Named { name: type_sym }, + target: Node { + kind: TypeNode { connective: Disj }, + children: fold(variants, init: [], f: fn(acc, variant_sym) { + concat(acc, [ + Edge { + label: Named { name: variant_sym }, + target: binding_fixture_node(name: variant_sym) + } + ]) + }), + occurrence_id: OccurrenceSynthetic + } + } +} + +data binding_inhabitance_module_root: Node = Node { + kind: TypeNode { connective: Conj }, + children: concat( + [ + dag_named_edge( + name: ^dag_surface_module_header, + target: dag_grammar_atom(id: ^dag_surface_module_header) + ), + dag_named_edge( + name: ^dag_surface_module_header_qualified_name, + target: binding_inhabitance_qn_spine(segments: binding_inhabitance_module_qn) + ) + ], + [ + binding_inhabitance_variant_edge(type_sym: ^Mood, variants: [^Shadowed]), + binding_inhabitance_variant_edge(type_sym: ^Classical, variants: [^Shadowed]) + ] + ), + occurrence_id: OccurrenceSynthetic +} + +data binding_inhabitance_index: SymbolIndex = symbol_index_fill_module_root( + index: empty_symbol_index(), + root: binding_inhabitance_module_root +) + +// The real chain walk, executed. Its result is the population the fixtures above only assert the +// shape of. +fn binding_inhabitance_real_population() -> List { + symbol_index_lexical_collect( + index: binding_inhabitance_index, + position: qualified_name_snoc(qn: binding_inhabitance_module_qn, segment: ^Classical), + name: ^Shadowed, + acc: Empty + ) +} + +// INHABITANCE: the real producer emits a multi-candidate population of the shape the supplied +// fixtures use, and the selection fold classifies THAT population -- so the fixtures are a reading +// of a boundary the program actually reaches, not a designed field of their own. +test fn the_real_chain_walk_emits_the_population_the_fixtures_supply_holds() -> Bool { + let real_population = binding_inhabitance_real_population() + (length(xs: real_population) == 2) + && binding_selection_class_equal( + left: match symbol_index_lexical_selection(candidates: real_population) { + LexicalUnbound => SelectionUnbound + LexicalHit { node: _, path: _ } => SelectionBound + LexicalAmbiguous { candidates: _ } => SelectionAmbiguous + }, + right: SelectionAmbiguous + ) +} From 563d62e473ad12dd8114a2d4f417b2c2237c545d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 22 Sep 2026 07:44:31 +0000 Subject: [PATCH 3/6] wip: inhabitance fixture emits a real two-candidate population --- .../binding/selection_fold_two_implementations_test.dag | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag b/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag index 1fbadcfd8e0..914f42e46f3 100644 --- a/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag +++ b/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag @@ -244,8 +244,8 @@ data binding_inhabitance_module_root: Node = Node { ) ], [ - binding_inhabitance_variant_edge(type_sym: ^Mood, variants: [^Shadowed]), - binding_inhabitance_variant_edge(type_sym: ^Classical, variants: [^Shadowed]) + binding_inhabitance_variant_edge(type_sym: ^Classical, variants: [^Shadowed]), + binding_inhabitance_variant_edge(type_sym: ^Shadowed, variants: [^Inner]) ] ), occurrence_id: OccurrenceSynthetic @@ -256,6 +256,11 @@ data binding_inhabitance_index: SymbolIndex = symbol_index_fill_module_root( root: binding_inhabitance_module_root ) +// TWO CANDIDATES BY CONSTRUCTION, AND THE SHAPE IS THE ORDINARY SHADOWING ONE: the module exports +// a type named Shadowed, and the type Classical exports a VARIANT of the same bare name. A walk +// starting inside Classical therefore finds Classical.Shadowed and then the module-level Shadowed, +// which is exactly the two-candidate population the duplicate and two-distinct fixtures above +// supply by hand. // The real chain walk, executed. Its result is the population the fixtures above only assert the // shape of. fn binding_inhabitance_real_population() -> List { From 2908b2315ea205b8db27902334f1263618e6b696 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 22 Sep 2026 08:25:06 +0000 Subject: [PATCH 4/6] audit correction 2B/2C + regenerated plan projection --- dag/gunbc/plans/dag_v2_defork_audit.dag | 11 +++++++++++ docs/plans/dag-v2-defork-audit.md | 22 ++++++++++++++++++++++ 2 files changed, 33 insertions(+) diff --git a/dag/gunbc/plans/dag_v2_defork_audit.dag b/dag/gunbc/plans/dag_v2_defork_audit.dag index 426ad3c1420..2784a414fbb 100644 --- a/dag/gunbc/plans/dag_v2_defork_audit.dag +++ b/dag/gunbc/plans/dag_v2_defork_audit.dag @@ -72,6 +72,17 @@ fn dag_v2_defork_audit_body() -> List { row(cells: [cell(text: "**node**"), cell(text: "**0**"), cell(text: "dag = `compiler_inductive_fields`/`compiler_recursive_types`/`is_compiler_recursive_type` — the complexity analyzer's inductive-structure *authority* (instance of `std/induction.dag`); v2 = 126-decl, 506-importer real Node substrate"), cell(text: "dag side imported by `src/v1/04_infer.dag`, emitted to `src/v1/stage0/src/std_node.rs`, guarded by `src/v1/tests/src/source_audit.rs`; `compiler_inductive_fields` is consumed **only by v1, never v2**"), cell(text: "**DEFERRED — self-dissolves.** Since `compiler_inductive_fields` is v1-only, on v1-delete `dag/std/node.dag` goes **dead → delete it, collision gone, no rename needed at all.** It is a live v1-only authority today (not a dead imposter); the collision with the v2 substrate is a v1-existence artifact.")]), ], }, + h3(text: "2B. 2026-09-22 executed correction to the `coercion` row — shared-symbol-count 0 was the wrong discriminator"), + p(text: "**This audit classified `coercion` as a genuine not-a-fork on a shared *symbol* count of 0. Measured by execution, that count answers the wrong question.** The two modules share no symbol and denote no different concept: they answer ONE question — may this value cross from one model to another — and they answer it with **two admission authorities keyed on different identity relations**. `std.coercion` `dag_can_cast` folds over `dag_cast_rules` + `grounded_primitive_coproduct_identities`, keyed on type-name **STRINGS**, and it EXECUTES (`v1.compiler.infer` consults it at argument-versus-formal admission, at literal admission, and in the type-relation fold). `v2.std.coercion` `coercion_fold` asks `v2.std.find_witness` `find_witness` for a structure-preserving witness, keyed on node **IDENTITY**, and has **no established executing consumer**. A shared-symbol count cannot see this, because the two sides cannot share a symbol: they cannot share a KEY."), + p(text: "**The recognition rule, available before any execution: a fixture that wants to ask both authorities about one subject must author the subject TWICE.** No conversion between a type-name spelling and a node identity exists anywhere in the corpus, so `v2.test.claim.coercion.two_algebra_fork` carries `source_type`/`target_type` (strings) beside `source_name`/`target_name` (symbols) on every row. That duplication is not fixture awkwardness — it **is** the measurement. This is a keys/hashing conformance subject (DESIGN §3b names structural node identity as a home there), not a coercion subject, and the finding generalizes: the class is filed as `gunbc.recurring_failure_mode` `two_admission_authorities_keyed_on_different_relations`, with an independent same-day specimen in a different surface (one resource under `Network` and `std.resources.Network`, a diagnostic field carrying the caller's import spelling while the wall compared resolved declaration identity)."), + p(text: "**EXECUTED RESULT over seven supplied source/target pairs — the admission sets differ in BOTH directions, so neither side is merely the stricter one.** `coercion_fold`'s only realized preservation rule is `preservation_rule_exact_structural_equality_zip_fold`, whose predicate holds exactly when the candidate is structurally equal to the source, so the homomorphism side cannot SPELL a non-identity crossing at all. **Admitted name-only:** `Int→Float`, `Bool→Int`, `Int→Nat`. **Admitted homomorphism-only:** `String→String` — an IDENTITY crossing, which `dag_cast_rules` carries no row for. That last is the sharpest single fact, because an identity coercion is the one case a reader assumes is free. Both sides matched their OWN independently specified contract on all seven pairs (the declared rosters for one, the structural-preservation predicate for the other), so this is a fork between two correct-by-their-own-lights authorities and not a defect in either."), + p(text: "**NOT REPAIRED, by ruling (snappy-deer-443, 2026-09-22).** The repair is a replacement migration (DESIGN §3, replacement migrations cut over at the root) — one key wins, the other algebra is cut at its root — with its own blast radius, and it is a separate lane that should start from these executed values rather than from the derivation that found them. The DEFERRED verdict in the table above is therefore **superseded as to its reasoning, not its timing**: the deferral was priced as a module-BASENAME rename held for v1-shrink, and the actual subject is an admission-key consolidation whose cost is not a rename at all."), + p(text: "**Instrument:** `gunbc test`-reachable claims in `v2.test.claim.coercion.two_algebra_fork` — `name_keyed_coercion_matches_the_declared_cast_rosters_holds`, `homomorphism_coercion_matches_the_structural_preservation_contract_holds`, `homomorphism_coercion_admits_only_identity_quality_holds`, `the_two_coercion_algebras_agree_exactly_where_declared_holds`. The last pins the agreement relation pair by pair and reds in EITHER direction, so consolidating the fork reds it too and the consolidator must restate the row. Two mutation arms establish it discriminates rather than detects change: adding a `Bool→Float` row to `dag_cast_rules` reds the roster claim and the join while leaving the homomorphism claims green, and weakening the structural-preservation predicate reds the homomorphism claims and the join while leaving the roster claim green."), + ThematicBreak, + h3(text: "2C. 2026-09-22 — the bindings selection fold is a NEGATIVE, and the shape of the negative matters"), + p(text: "`std.occurrence_binding` `occurrence_binding_from_candidates` (a FoldZero/FoldOne/FoldMany accumulator) and `v2.std.symbol_index` `symbol_index_lexical_selection` (`match length(candidates)`) are two implementations of one none/one/many trichotomy. Measured over five supplied populations — empty, singleton, two distinct, **duplicate**, three — **they agree on all five, and each independently matches the trichotomy as the modeled contract states it**, so this is not merely \"the two match\"."), + p(text: "**It is NOT agreement by construction, and the distinction is load-bearing.** Agreement-by-construction would mean both routes read one reader, making disagreement unwritable. Here nothing makes them agree: **both contracts are SILENT on duplicates and both realizations inherit that silence.** Neither declares a deduplication step, so a population naming one candidate twice is a two-candidate population in both — by omission, not by rule. The first side to declare a dedup rule silently forks the other. In inventory terms this is **no-evidence with a named absence**, not AgreesByConstruction. **What would close it:** a declared statement, on whichever carrier owns the trichotomy, of whether the rule ranges over list MULTIPLICITY or over the cardinality of DISTINCT candidates. The duplicate row stays enrolled although it is green on both sides — it is the probe that reds when that silence is broken on one side only."), + p(text: "**SCOPE, stated because it is the whole point.** The subject is the selection fold on a SUPPLIED population. Their agreement on a PRODUCTION SITE is not measured and is not measurable today: no v2 resolution site is answered by std's fold, and `std.occurrence_binding`'s own staged-adoption note states that `LexicalLookup` is not an interim consumer because it carries no exact reference-occurrence `Node` or occurrence containment identity. The candidate PRODUCERS (a supplied list versus the containment chain walk) are legitimately layered and are not compared. `symbol_index_lexical_selection` was split out of `symbol_index_lexical_lookup` — same composition, no behaviour change — so the boundary can be asked with its inputs supplied (DESIGN §3, the witness standing rule); the split's pairing obligation is discharged by `the_real_chain_walk_emits_the_population_the_fixtures_supply_holds`, which runs the real `symbol_index_lexical_collect` walk over a real `SymbolIndex` and feeds THAT population into the same selection fold, so deleting the walk cannot leave the suite green. Mutation arms: collapsing std's fold so it never leaves `FoldOne` reds std's claim and the join while v2's stays green; making v2's selection answer `Ambiguous` on the empty population reds v2's claim and the join while std's stays green."), h3(text: "Grounding cluster (operator authority) — 7 concepts, a unification *design*"), p(text: "Each row is **operator decision-input**: what is shared (and whether the shared body itself diverges), what each side uniquely carries, and the specific grounding entanglement that makes it a design, not a repoint."), TableBlock { diff --git a/docs/plans/dag-v2-defork-audit.md b/docs/plans/dag-v2-defork-audit.md index c7c17d7580e..bc36e44031a 100644 --- a/docs/plans/dag-v2-defork-audit.md +++ b/docs/plans/dag-v2-defork-audit.md @@ -100,6 +100,28 @@ Three tiers. **Mirror** = v2's used symbols ⊆ dag → mechanical delete + repo | **coercion** | **0** | dag = cast / type-representation vocab (`TypeCheckpoint`, `CastRule`, `CastSyntax`, `CallableRepr`, `dag_cast_rules`); v2 = coercion-as-homomorphism (`coercion_fold` via `find_witness`, `CoercionWitness/Result/Quality`) | dag side imported by `src/v1/coercion.dag` + `src/v1/04_infer.dag`, emitted to `src/v1/stage0/src/std_coercion.rs` (+ 4 `dag/extdeps/languages/*/types.dag` that survive v1) | **DEFERRED.** The 4 extdeps importers survive v1, so `dag/std/coercion.dag` persists — on v1-delete the rename **shrinks to a v1-free scope** (4 extdeps + v2, no seed / no `04_infer` / no guard test), a clean disambiguation. End-state (DESIGN §4): the *fold* **is** coercion → keep `coercion` for the v2 side, rename the dag cast vocab to `cast_rules`. (#5510 attempted it but broke v1 — missed the `src/v1` consumers — and over-scoped by renaming the v2 side; **closed**, not merged.) | | **node** | **0** | dag = `compiler_inductive_fields`/`compiler_recursive_types`/`is_compiler_recursive_type` — the complexity analyzer's inductive-structure *authority* (instance of `std/induction.dag`); v2 = 126-decl, 506-importer real Node substrate | dag side imported by `src/v1/04_infer.dag`, emitted to `src/v1/stage0/src/std_node.rs`, guarded by `src/v1/tests/src/source_audit.rs`; `compiler_inductive_fields` is consumed **only by v1, never v2** | **DEFERRED — self-dissolves.** Since `compiler_inductive_fields` is v1-only, on v1-delete `dag/std/node.dag` goes **dead → delete it, collision gone, no rename needed at all.** It is a live v1-only authority today (not a dead imposter); the collision with the v2 substrate is a v1-existence artifact. | +### 2B. 2026-09-22 executed correction to the `coercion` row — shared-symbol-count 0 was the wrong discriminator + +**This audit classified `coercion` as a genuine not-a-fork on a shared *symbol* count of 0. Measured by execution, that count answers the wrong question.** The two modules share no symbol and denote no different concept: they answer ONE question — may this value cross from one model to another — and they answer it with **two admission authorities keyed on different identity relations**. `std.coercion` `dag_can_cast` folds over `dag_cast_rules` + `grounded_primitive_coproduct_identities`, keyed on type-name **STRINGS**, and it EXECUTES (`v1.compiler.infer` consults it at argument-versus-formal admission, at literal admission, and in the type-relation fold). `v2.std.coercion` `coercion_fold` asks `v2.std.find_witness` `find_witness` for a structure-preserving witness, keyed on node **IDENTITY**, and has **no established executing consumer**. A shared-symbol count cannot see this, because the two sides cannot share a symbol: they cannot share a KEY. + +**The recognition rule, available before any execution: a fixture that wants to ask both authorities about one subject must author the subject TWICE.** No conversion between a type-name spelling and a node identity exists anywhere in the corpus, so `v2.test.claim.coercion.two_algebra_fork` carries `source_type`/`target_type` (strings) beside `source_name`/`target_name` (symbols) on every row. That duplication is not fixture awkwardness — it **is** the measurement. This is a keys/hashing conformance subject (DESIGN §3b names structural node identity as a home there), not a coercion subject, and the finding generalizes: the class is filed as `gunbc.recurring_failure_mode` `two_admission_authorities_keyed_on_different_relations`, with an independent same-day specimen in a different surface (one resource under `Network` and `std.resources.Network`, a diagnostic field carrying the caller's import spelling while the wall compared resolved declaration identity). + +**EXECUTED RESULT over seven supplied source/target pairs — the admission sets differ in BOTH directions, so neither side is merely the stricter one.** `coercion_fold`'s only realized preservation rule is `preservation_rule_exact_structural_equality_zip_fold`, whose predicate holds exactly when the candidate is structurally equal to the source, so the homomorphism side cannot SPELL a non-identity crossing at all. **Admitted name-only:** `Int→Float`, `Bool→Int`, `Int→Nat`. **Admitted homomorphism-only:** `String→String` — an IDENTITY crossing, which `dag_cast_rules` carries no row for. That last is the sharpest single fact, because an identity coercion is the one case a reader assumes is free. Both sides matched their OWN independently specified contract on all seven pairs (the declared rosters for one, the structural-preservation predicate for the other), so this is a fork between two correct-by-their-own-lights authorities and not a defect in either. + +**NOT REPAIRED, by ruling (snappy-deer-443, 2026-09-22).** The repair is a replacement migration (DESIGN §3, replacement migrations cut over at the root) — one key wins, the other algebra is cut at its root — with its own blast radius, and it is a separate lane that should start from these executed values rather than from the derivation that found them. The DEFERRED verdict in the table above is therefore **superseded as to its reasoning, not its timing**: the deferral was priced as a module-BASENAME rename held for v1-shrink, and the actual subject is an admission-key consolidation whose cost is not a rename at all. + +**Instrument:** `gunbc test`-reachable claims in `v2.test.claim.coercion.two_algebra_fork` — `name_keyed_coercion_matches_the_declared_cast_rosters_holds`, `homomorphism_coercion_matches_the_structural_preservation_contract_holds`, `homomorphism_coercion_admits_only_identity_quality_holds`, `the_two_coercion_algebras_agree_exactly_where_declared_holds`. The last pins the agreement relation pair by pair and reds in EITHER direction, so consolidating the fork reds it too and the consolidator must restate the row. Two mutation arms establish it discriminates rather than detects change: adding a `Bool→Float` row to `dag_cast_rules` reds the roster claim and the join while leaving the homomorphism claims green, and weakening the structural-preservation predicate reds the homomorphism claims and the join while leaving the roster claim green. + +--- + +### 2C. 2026-09-22 — the bindings selection fold is a NEGATIVE, and the shape of the negative matters + +`std.occurrence_binding` `occurrence_binding_from_candidates` (a FoldZero/FoldOne/FoldMany accumulator) and `v2.std.symbol_index` `symbol_index_lexical_selection` (`match length(candidates)`) are two implementations of one none/one/many trichotomy. Measured over five supplied populations — empty, singleton, two distinct, **duplicate**, three — **they agree on all five, and each independently matches the trichotomy as the modeled contract states it**, so this is not merely "the two match". + +**It is NOT agreement by construction, and the distinction is load-bearing.** Agreement-by-construction would mean both routes read one reader, making disagreement unwritable. Here nothing makes them agree: **both contracts are SILENT on duplicates and both realizations inherit that silence.** Neither declares a deduplication step, so a population naming one candidate twice is a two-candidate population in both — by omission, not by rule. The first side to declare a dedup rule silently forks the other. In inventory terms this is **no-evidence with a named absence**, not AgreesByConstruction. **What would close it:** a declared statement, on whichever carrier owns the trichotomy, of whether the rule ranges over list MULTIPLICITY or over the cardinality of DISTINCT candidates. The duplicate row stays enrolled although it is green on both sides — it is the probe that reds when that silence is broken on one side only. + +**SCOPE, stated because it is the whole point.** The subject is the selection fold on a SUPPLIED population. Their agreement on a PRODUCTION SITE is not measured and is not measurable today: no v2 resolution site is answered by std's fold, and `std.occurrence_binding`'s own staged-adoption note states that `LexicalLookup` is not an interim consumer because it carries no exact reference-occurrence `Node` or occurrence containment identity. The candidate PRODUCERS (a supplied list versus the containment chain walk) are legitimately layered and are not compared. `symbol_index_lexical_selection` was split out of `symbol_index_lexical_lookup` — same composition, no behaviour change — so the boundary can be asked with its inputs supplied (DESIGN §3, the witness standing rule); the split's pairing obligation is discharged by `the_real_chain_walk_emits_the_population_the_fixtures_supply_holds`, which runs the real `symbol_index_lexical_collect` walk over a real `SymbolIndex` and feeds THAT population into the same selection fold, so deleting the walk cannot leave the suite green. Mutation arms: collapsing std's fold so it never leaves `FoldOne` reds std's claim and the join while v2's stays green; making v2's selection answer `Ambiguous` on the empty population reds v2's claim and the join while std's stays green. + ### Grounding cluster (operator authority) — 7 concepts, a unification *design* Each row is **operator decision-input**: what is shared (and whether the shared body itself diverges), what each side uniquely carries, and the specific grounding entanglement that makes it a design, not a repoint. From ed7dad2164e1144bdca83a4c88f69ab9d6648996 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 22 Sep 2026 09:20:25 +0000 Subject: [PATCH 5/6] review 70065: delete both entailed comparison claims and the derived agree column Both joins were entailed by the per-side claims: each pins its side to the same independently specified expectation, so the comparison can never be the only thing red. DESIGN 4b rules that out before the check is written, and the derived agree column is DESIGN 2 re-invention. My own mutation table was the evidence -- the join never redded alone in any of the four arms. The agreement relation is derived from the expectation columns a row carries side by side, and is enforced by the per-side claims. Re-executed: 6 green, each mutation now reds only the claim owning the mutated side. --- dag/gunbc/plans/dag_v2_defork_audit.dag | 4 +- docs/plans/dag-v2-defork-audit.md | 4 +- ...election_fold_two_implementations_test.dag | 36 ++++++++---- .../claim/coercion/two_algebra_fork_test.dag | 56 +++++++++---------- 4 files changed, 56 insertions(+), 44 deletions(-) diff --git a/dag/gunbc/plans/dag_v2_defork_audit.dag b/dag/gunbc/plans/dag_v2_defork_audit.dag index 2784a414fbb..4cf3428d78b 100644 --- a/dag/gunbc/plans/dag_v2_defork_audit.dag +++ b/dag/gunbc/plans/dag_v2_defork_audit.dag @@ -77,12 +77,12 @@ fn dag_v2_defork_audit_body() -> List { p(text: "**The recognition rule, available before any execution: a fixture that wants to ask both authorities about one subject must author the subject TWICE.** No conversion between a type-name spelling and a node identity exists anywhere in the corpus, so `v2.test.claim.coercion.two_algebra_fork` carries `source_type`/`target_type` (strings) beside `source_name`/`target_name` (symbols) on every row. That duplication is not fixture awkwardness — it **is** the measurement. This is a keys/hashing conformance subject (DESIGN §3b names structural node identity as a home there), not a coercion subject, and the finding generalizes: the class is filed as `gunbc.recurring_failure_mode` `two_admission_authorities_keyed_on_different_relations`, with an independent same-day specimen in a different surface (one resource under `Network` and `std.resources.Network`, a diagnostic field carrying the caller's import spelling while the wall compared resolved declaration identity)."), p(text: "**EXECUTED RESULT over seven supplied source/target pairs — the admission sets differ in BOTH directions, so neither side is merely the stricter one.** `coercion_fold`'s only realized preservation rule is `preservation_rule_exact_structural_equality_zip_fold`, whose predicate holds exactly when the candidate is structurally equal to the source, so the homomorphism side cannot SPELL a non-identity crossing at all. **Admitted name-only:** `Int→Float`, `Bool→Int`, `Int→Nat`. **Admitted homomorphism-only:** `String→String` — an IDENTITY crossing, which `dag_cast_rules` carries no row for. That last is the sharpest single fact, because an identity coercion is the one case a reader assumes is free. Both sides matched their OWN independently specified contract on all seven pairs (the declared rosters for one, the structural-preservation predicate for the other), so this is a fork between two correct-by-their-own-lights authorities and not a defect in either."), p(text: "**NOT REPAIRED, by ruling (snappy-deer-443, 2026-09-22).** The repair is a replacement migration (DESIGN §3, replacement migrations cut over at the root) — one key wins, the other algebra is cut at its root — with its own blast radius, and it is a separate lane that should start from these executed values rather than from the derivation that found them. The DEFERRED verdict in the table above is therefore **superseded as to its reasoning, not its timing**: the deferral was priced as a module-BASENAME rename held for v1-shrink, and the actual subject is an admission-key consolidation whose cost is not a rename at all."), - p(text: "**Instrument:** `gunbc test`-reachable claims in `v2.test.claim.coercion.two_algebra_fork` — `name_keyed_coercion_matches_the_declared_cast_rosters_holds`, `homomorphism_coercion_matches_the_structural_preservation_contract_holds`, `homomorphism_coercion_admits_only_identity_quality_holds`, `the_two_coercion_algebras_agree_exactly_where_declared_holds`. The last pins the agreement relation pair by pair and reds in EITHER direction, so consolidating the fork reds it too and the consolidator must restate the row. Two mutation arms establish it discriminates rather than detects change: adding a `Bool→Float` row to `dag_cast_rules` reds the roster claim and the join while leaving the homomorphism claims green, and weakening the structural-preservation predicate reds the homomorphism claims and the join while leaving the roster claim green."), + p(text: "**Instrument:** `gunbc test`-reachable claims in `v2.test.claim.coercion.two_algebra_fork` — `name_keyed_coercion_matches_the_declared_cast_rosters_holds`, `homomorphism_coercion_matches_the_structural_preservation_contract_holds`, `homomorphism_coercion_admits_only_identity_quality_holds`. Each pins ONE algebra to its OWN independently specified contract, so a move in either side's admission set — consolidation included — reds the claim that owns it and the author must restate the row. **There is deliberately no fourth claim comparing the two algebras to each other** (review 70065): with both sides pinned to independent expectations, such a comparison is ENTAILED and its RED is not independently authorable, which DESIGN §4b rules out before the check is written. The agreement relation is DERIVED from the two expectation columns a row carries side by side. Two mutation arms establish discrimination rather than change detection: adding a `Bool→Float` row to `dag_cast_rules` reds ONLY the roster claim, and weakening the structural-preservation predicate reds ONLY the two homomorphism claims."), ThematicBreak, h3(text: "2C. 2026-09-22 — the bindings selection fold is a NEGATIVE, and the shape of the negative matters"), p(text: "`std.occurrence_binding` `occurrence_binding_from_candidates` (a FoldZero/FoldOne/FoldMany accumulator) and `v2.std.symbol_index` `symbol_index_lexical_selection` (`match length(candidates)`) are two implementations of one none/one/many trichotomy. Measured over five supplied populations — empty, singleton, two distinct, **duplicate**, three — **they agree on all five, and each independently matches the trichotomy as the modeled contract states it**, so this is not merely \"the two match\"."), p(text: "**It is NOT agreement by construction, and the distinction is load-bearing.** Agreement-by-construction would mean both routes read one reader, making disagreement unwritable. Here nothing makes them agree: **both contracts are SILENT on duplicates and both realizations inherit that silence.** Neither declares a deduplication step, so a population naming one candidate twice is a two-candidate population in both — by omission, not by rule. The first side to declare a dedup rule silently forks the other. In inventory terms this is **no-evidence with a named absence**, not AgreesByConstruction. **What would close it:** a declared statement, on whichever carrier owns the trichotomy, of whether the rule ranges over list MULTIPLICITY or over the cardinality of DISTINCT candidates. The duplicate row stays enrolled although it is green on both sides — it is the probe that reds when that silence is broken on one side only."), - p(text: "**SCOPE, stated because it is the whole point.** The subject is the selection fold on a SUPPLIED population. Their agreement on a PRODUCTION SITE is not measured and is not measurable today: no v2 resolution site is answered by std's fold, and `std.occurrence_binding`'s own staged-adoption note states that `LexicalLookup` is not an interim consumer because it carries no exact reference-occurrence `Node` or occurrence containment identity. The candidate PRODUCERS (a supplied list versus the containment chain walk) are legitimately layered and are not compared. `symbol_index_lexical_selection` was split out of `symbol_index_lexical_lookup` — same composition, no behaviour change — so the boundary can be asked with its inputs supplied (DESIGN §3, the witness standing rule); the split's pairing obligation is discharged by `the_real_chain_walk_emits_the_population_the_fixtures_supply_holds`, which runs the real `symbol_index_lexical_collect` walk over a real `SymbolIndex` and feeds THAT population into the same selection fold, so deleting the walk cannot leave the suite green. Mutation arms: collapsing std's fold so it never leaves `FoldOne` reds std's claim and the join while v2's stays green; making v2's selection answer `Ambiguous` on the empty population reds v2's claim and the join while std's stays green."), + p(text: "**SCOPE, stated because it is the whole point.** The subject is the selection fold on a SUPPLIED population. Their agreement on a PRODUCTION SITE is not measured and is not measurable today: no v2 resolution site is answered by std's fold, and `std.occurrence_binding`'s own staged-adoption note states that `LexicalLookup` is not an interim consumer because it carries no exact reference-occurrence `Node` or occurrence containment identity. The candidate PRODUCERS (a supplied list versus the containment chain walk) are legitimately layered and are not compared. `symbol_index_lexical_selection` was split out of `symbol_index_lexical_lookup` — same composition, no behaviour change — so the boundary can be asked with its inputs supplied (DESIGN §3, the witness standing rule); the split's pairing obligation is discharged by `the_real_chain_walk_emits_the_population_the_fixtures_supply_holds`, which runs the real `symbol_index_lexical_collect` walk over a real `SymbolIndex` and feeds THAT population into the same selection fold, so deleting the walk cannot leave the suite green. Mutation arms, each redding ONLY the claim that owns the mutated side: collapsing std's fold so it never leaves `FoldOne` reds std's claim alone; making v2's selection answer `Ambiguous` on the empty population reds v2's claim alone. As in §2B there is no third claim comparing the two folds — it would be entailed by these two, both being pinned to the same expected class."), h3(text: "Grounding cluster (operator authority) — 7 concepts, a unification *design*"), p(text: "Each row is **operator decision-input**: what is shared (and whether the shared body itself diverges), what each side uniquely carries, and the specific grounding entanglement that makes it a design, not a repoint."), TableBlock { diff --git a/docs/plans/dag-v2-defork-audit.md b/docs/plans/dag-v2-defork-audit.md index bc36e44031a..85e1140f235 100644 --- a/docs/plans/dag-v2-defork-audit.md +++ b/docs/plans/dag-v2-defork-audit.md @@ -110,7 +110,7 @@ Three tiers. **Mirror** = v2's used symbols ⊆ dag → mechanical delete + repo **NOT REPAIRED, by ruling (snappy-deer-443, 2026-09-22).** The repair is a replacement migration (DESIGN §3, replacement migrations cut over at the root) — one key wins, the other algebra is cut at its root — with its own blast radius, and it is a separate lane that should start from these executed values rather than from the derivation that found them. The DEFERRED verdict in the table above is therefore **superseded as to its reasoning, not its timing**: the deferral was priced as a module-BASENAME rename held for v1-shrink, and the actual subject is an admission-key consolidation whose cost is not a rename at all. -**Instrument:** `gunbc test`-reachable claims in `v2.test.claim.coercion.two_algebra_fork` — `name_keyed_coercion_matches_the_declared_cast_rosters_holds`, `homomorphism_coercion_matches_the_structural_preservation_contract_holds`, `homomorphism_coercion_admits_only_identity_quality_holds`, `the_two_coercion_algebras_agree_exactly_where_declared_holds`. The last pins the agreement relation pair by pair and reds in EITHER direction, so consolidating the fork reds it too and the consolidator must restate the row. Two mutation arms establish it discriminates rather than detects change: adding a `Bool→Float` row to `dag_cast_rules` reds the roster claim and the join while leaving the homomorphism claims green, and weakening the structural-preservation predicate reds the homomorphism claims and the join while leaving the roster claim green. +**Instrument:** `gunbc test`-reachable claims in `v2.test.claim.coercion.two_algebra_fork` — `name_keyed_coercion_matches_the_declared_cast_rosters_holds`, `homomorphism_coercion_matches_the_structural_preservation_contract_holds`, `homomorphism_coercion_admits_only_identity_quality_holds`. Each pins ONE algebra to its OWN independently specified contract, so a move in either side's admission set — consolidation included — reds the claim that owns it and the author must restate the row. **There is deliberately no fourth claim comparing the two algebras to each other** (review 70065): with both sides pinned to independent expectations, such a comparison is ENTAILED and its RED is not independently authorable, which DESIGN §4b rules out before the check is written. The agreement relation is DERIVED from the two expectation columns a row carries side by side. Two mutation arms establish discrimination rather than change detection: adding a `Bool→Float` row to `dag_cast_rules` reds ONLY the roster claim, and weakening the structural-preservation predicate reds ONLY the two homomorphism claims. --- @@ -120,7 +120,7 @@ Three tiers. **Mirror** = v2's used symbols ⊆ dag → mechanical delete + repo **It is NOT agreement by construction, and the distinction is load-bearing.** Agreement-by-construction would mean both routes read one reader, making disagreement unwritable. Here nothing makes them agree: **both contracts are SILENT on duplicates and both realizations inherit that silence.** Neither declares a deduplication step, so a population naming one candidate twice is a two-candidate population in both — by omission, not by rule. The first side to declare a dedup rule silently forks the other. In inventory terms this is **no-evidence with a named absence**, not AgreesByConstruction. **What would close it:** a declared statement, on whichever carrier owns the trichotomy, of whether the rule ranges over list MULTIPLICITY or over the cardinality of DISTINCT candidates. The duplicate row stays enrolled although it is green on both sides — it is the probe that reds when that silence is broken on one side only. -**SCOPE, stated because it is the whole point.** The subject is the selection fold on a SUPPLIED population. Their agreement on a PRODUCTION SITE is not measured and is not measurable today: no v2 resolution site is answered by std's fold, and `std.occurrence_binding`'s own staged-adoption note states that `LexicalLookup` is not an interim consumer because it carries no exact reference-occurrence `Node` or occurrence containment identity. The candidate PRODUCERS (a supplied list versus the containment chain walk) are legitimately layered and are not compared. `symbol_index_lexical_selection` was split out of `symbol_index_lexical_lookup` — same composition, no behaviour change — so the boundary can be asked with its inputs supplied (DESIGN §3, the witness standing rule); the split's pairing obligation is discharged by `the_real_chain_walk_emits_the_population_the_fixtures_supply_holds`, which runs the real `symbol_index_lexical_collect` walk over a real `SymbolIndex` and feeds THAT population into the same selection fold, so deleting the walk cannot leave the suite green. Mutation arms: collapsing std's fold so it never leaves `FoldOne` reds std's claim and the join while v2's stays green; making v2's selection answer `Ambiguous` on the empty population reds v2's claim and the join while std's stays green. +**SCOPE, stated because it is the whole point.** The subject is the selection fold on a SUPPLIED population. Their agreement on a PRODUCTION SITE is not measured and is not measurable today: no v2 resolution site is answered by std's fold, and `std.occurrence_binding`'s own staged-adoption note states that `LexicalLookup` is not an interim consumer because it carries no exact reference-occurrence `Node` or occurrence containment identity. The candidate PRODUCERS (a supplied list versus the containment chain walk) are legitimately layered and are not compared. `symbol_index_lexical_selection` was split out of `symbol_index_lexical_lookup` — same composition, no behaviour change — so the boundary can be asked with its inputs supplied (DESIGN §3, the witness standing rule); the split's pairing obligation is discharged by `the_real_chain_walk_emits_the_population_the_fixtures_supply_holds`, which runs the real `symbol_index_lexical_collect` walk over a real `SymbolIndex` and feeds THAT population into the same selection fold, so deleting the walk cannot leave the suite green. Mutation arms, each redding ONLY the claim that owns the mutated side: collapsing std's fold so it never leaves `FoldOne` reds std's claim alone; making v2's selection answer `Ambiguous` on the empty population reds v2's claim alone. As in §2B there is no third claim comparing the two folds — it would be entailed by these two, both being pinned to the same expected class. ### Grounding cluster (operator authority) — 7 concepts, a unification *design* diff --git a/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag b/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag index 914f42e46f3..5d197e943c9 100644 --- a/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag +++ b/src/v2/test/claim/binding/selection_fold_two_implementations_test.dag @@ -30,8 +30,9 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // MULTIPLICITY of the supplied list, not over the cardinality of its distinct members. That is why // the duplicate row below expects Ambiguous: neither contract declares a deduplication step, so a // population naming one candidate twice is a two-candidate population. The first two claims below -// hold each fold to that expectation separately, so a row can report BOTH AGREE AND BOTH ARE WRONG; -// the third claim reports the join. +// hold each fold to that expectation separately, so a row can report BOTH AGREE AND BOTH ARE WRONG. +// The agreement relation is then DERIVED from the rows rather than asserted by a further claim -- +// see the note above the claims for why a comparison claim would carry no information. type BindingSelectionClass = SelectionUnbound @@ -183,15 +184,28 @@ test fn lexical_selection_matches_the_declared_trichotomy_holds() -> Bool { }) } -// The join the corpus does not otherwise carry: one rule, two implementations, one population. -test fn the_two_selection_folds_agree_on_the_supplied_population_holds() -> Bool { - fold(binding_selection_fixtures, init: true, f: fn(acc, row) { - acc && binding_selection_class_equal( - left: binding_std_class(names: row.candidate_names), - right: binding_lexical_class(names: row.candidate_names) - ) - }) -} +// WHY THERE IS NO THIRD CLAIM COMPARING THE TWO FOLDS TO EACH OTHER, written here because the +// obvious edit is to add one back (review 70065). +// +// Such a claim -- std_class(row) == lexical_class(row) -- is ENTAILED by the two above it. Both +// pin their side to the SAME row.expected, so if either fold moves, the claim naming that fold +// reds first; the comparison can never be the only thing red. Its RED is not independently +// authorable, which DESIGN section 4b rules out before the check is written: permanently green by +// construction, carrying no information, and worse than absent because it will be cited as +// coverage. +// +// THE ENTAILMENT IS NOT AN OVERSIGHT, IT IS A CONSEQUENCE, and the consequence is worth stating +// because it generalizes. The reason each fold is held to an INDEPENDENTLY SPECIFIED expectation +// is that agreement between two implementations is not evidence either is right -- two folds +// derived from one misunderstanding agree perfectly. But once both sides are pinned to an +// independent expectation, THE AGREEMENT RELATION IS ALREADY FIXED: it is derived from the two +// expectations rather than asserted by a third claim. Independently specified verdicts and a +// separate join claim cannot both carry information; the first subsumes the second. +// +// So the join is carried by the FIXTURE ROW, which names one population and both expectations +// side by side, and it is enforced by the two claims above. A change to either fold's behaviour +// reds the claim that owns it and the author must restate the row -- which is the whole property +// a comparison claim was wanted for. // THE PAIRING OBLIGATION FOR THE SUPPLIED BOUNDARY (DESIGN section 3). Every claim above hands // symbol_index_lexical_selection a population it constructed, so those claims are hypotheses about diff --git a/src/v2/test/claim/coercion/two_algebra_fork_test.dag b/src/v2/test/claim/coercion/two_algebra_fork_test.dag index fcb45c03021..d98977bebe5 100644 --- a/src/v2/test/claim/coercion/two_algebra_fork_test.dag +++ b/src/v2/test/claim/coercion/two_algebra_fork_test.dag @@ -22,12 +22,14 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // the two folds is executed to produce the inputs (DESIGN section 3, the witness standing rule). // // NEITHER FOLD IS THE ORACLE FOR THE OTHER, so each row carries TWO independently specified -// expectations and the claims below hold each algebra to its OWN contract before the join is read: +// expectations, and the claims below hold each algebra to its OWN contract. The agreement relation +// is read off the two expectation columns of a row rather than asserted by a further claim -- see +// the note above the claims for why such a claim would carry no information: // // expected_name_keyed_admits -- read off the declared rosters in std.coercion. A crossing is // admitted exactly when a row spells it, in dag_cast_rules or in the grounded // primitive-to-coproduct identities. This is a transcription of the DECLARATION, so a roster -// edit reds the first claim rather than silently moving the join. +// edit reds the first claim rather than silently moving the measured relation. // expected_homomorphism_admits -- read off the homomorphism contract as it is realized. The only // preservation rule coercion_fold applies is // preservation_rule_exact_structural_equality_zip_fold, whose predicate holds exactly when @@ -56,7 +58,6 @@ type CoercionForkFixture { target_name: Symbol expected_name_keyed: CoercionAdmission expected_homomorphism: CoercionAdmission - expected_algebras_agree: Bool } // THE POPULATION, AND WHY IT IS THE DISCRIMINATING ONE. The two algebras partition the pair space @@ -83,8 +84,7 @@ data coercion_fork_fixtures: List = [ source_name: ^Int, target_name: ^Int, expected_name_keyed: CrossingAdmitted, - expected_homomorphism: CrossingAdmitted, - expected_algebras_agree: true + expected_homomorphism: CrossingAdmitted }, { label: ^float_to_float, @@ -93,8 +93,7 @@ data coercion_fork_fixtures: List = [ source_name: ^Float, target_name: ^Float, expected_name_keyed: CrossingAdmitted, - expected_homomorphism: CrossingAdmitted, - expected_algebras_agree: true + expected_homomorphism: CrossingAdmitted }, { label: ^int_to_float, @@ -103,8 +102,7 @@ data coercion_fork_fixtures: List = [ source_name: ^Int, target_name: ^Float, expected_name_keyed: CrossingAdmitted, - expected_homomorphism: CrossingRefused, - expected_algebras_agree: false + expected_homomorphism: CrossingRefused }, { label: ^bool_to_int, @@ -113,8 +111,7 @@ data coercion_fork_fixtures: List = [ source_name: ^Bool, target_name: ^Int, expected_name_keyed: CrossingAdmitted, - expected_homomorphism: CrossingRefused, - expected_algebras_agree: false + expected_homomorphism: CrossingRefused }, { label: ^int_to_nat, @@ -123,8 +120,7 @@ data coercion_fork_fixtures: List = [ source_name: ^Int, target_name: ^Nat, expected_name_keyed: CrossingAdmitted, - expected_homomorphism: CrossingRefused, - expected_algebras_agree: false + expected_homomorphism: CrossingRefused }, { label: ^string_to_string, @@ -133,8 +129,7 @@ data coercion_fork_fixtures: List = [ source_name: ^String, target_name: ^String, expected_name_keyed: CrossingRefused, - expected_homomorphism: CrossingAdmitted, - expected_algebras_agree: false + expected_homomorphism: CrossingAdmitted }, { label: ^bool_to_float, @@ -143,8 +138,7 @@ data coercion_fork_fixtures: List = [ source_name: ^Bool, target_name: ^Float, expected_name_keyed: CrossingRefused, - expected_homomorphism: CrossingRefused, - expected_algebras_agree: true + expected_homomorphism: CrossingRefused } ] @@ -265,15 +259,19 @@ test fn homomorphism_coercion_admits_only_identity_quality_holds() -> Bool { }) } -// THE JOIN. This claim pins the CURRENT, MEASURED relation between the two algebras pair by pair, -// including the four rows on which they disagree. It is green while the fork stands exactly as -// authored and reds the moment either side's admission set moves -- in either direction, so -// consolidating the fork reds it too and the consolidator is the one who must restate the row. -test fn the_two_coercion_algebras_agree_exactly_where_declared_holds() -> Bool { - fold(coercion_fork_fixtures, init: true, f: fn(acc, row) { - acc && (coercion_admission_equal( - left: coercion_fork_name_keyed_admission(row: row), - right: coercion_fork_homomorphism_admission(row: row) - ) == row.expected_algebras_agree) - }) -} +// WHY THERE IS NO CLAIM COMPARING THE TWO ALGEBRAS TO EACH OTHER, AND NO AUTHORED `AGREE` COLUMN +// (review 70065). A claim asserting name_keyed_admission(row) == homomorphism_admission(row), read +// against an authored third column, is ENTAILED by the two claims above: each pins its side to its +// own independently specified expectation, so the comparison reduces to asking whether that third +// column contradicts the first two -- a check of the fixture against itself, which reds on no +// behaviour change the first two do not already catch. DESIGN section 4b rules the check out before +// it is written, and DESIGN section 2 names the column: a third authored fact fully determined by +// two others is re-invention, not a reduction. +// +// THE MEASUREMENT SURVIVES WITHOUT IT, and this is the point rather than a concession. The +// agreement relation is DERIVED from the two expectation columns, which sit side by side on every +// row: four of the seven rows carry expectations that differ, in both directions, and that is the +// fork stated where a reader meets the population. If either algebra's admission set moves -- in +// either direction, consolidation included -- the claim that owns that side reds and the author +// must restate the row. Nothing was lost by deleting the comparison except a second spelling of a +// fact the table already carries. From 0e6435c585923d8569407672737d74dc12442c9c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 22 Sep 2026 09:47:06 +0000 Subject: [PATCH 6/6] fix parse: annotation left at EOF by the claim deletion needs a following subject Deleting the final test fn left the explanatory note at end-of-file with no module item after it, which DESIGN 4c refuses -- 15 'source annotation names no subject' errors, one per line, redding the parse phase and the floor with it. Moved above the claims, which is where both file headers already say it sits. Re-executed: 6 green. --- .../claim/coercion/two_algebra_fork_test.dag | 34 +++++++++---------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/src/v2/test/claim/coercion/two_algebra_fork_test.dag b/src/v2/test/claim/coercion/two_algebra_fork_test.dag index d98977bebe5..86ec4786625 100644 --- a/src/v2/test/claim/coercion/two_algebra_fork_test.dag +++ b/src/v2/test/claim/coercion/two_algebra_fork_test.dag @@ -223,6 +223,23 @@ fn coercion_admission_equal(left: CoercionAdmission, right: CoercionAdmission) - } } +// WHY THERE IS NO CLAIM COMPARING THE TWO ALGEBRAS TO EACH OTHER, AND NO AUTHORED `AGREE` COLUMN +// (review 70065). A claim asserting name_keyed_admission(row) == homomorphism_admission(row), read +// against an authored third column, is ENTAILED by the two claims above: each pins its side to its +// own independently specified expectation, so the comparison reduces to asking whether that third +// column contradicts the first two -- a check of the fixture against itself, which reds on no +// behaviour change the first two do not already catch. DESIGN section 4b rules the check out before +// it is written, and DESIGN section 2 names the column: a third authored fact fully determined by +// two others is re-invention, not a reduction. +// +// THE MEASUREMENT SURVIVES WITHOUT IT, and this is the point rather than a concession. The +// agreement relation is DERIVED from the two expectation columns, which sit side by side on every +// row: four of the seven rows carry expectations that differ, in both directions, and that is the +// fork stated where a reader meets the population. If either algebra's admission set moves -- in +// either direction, consolidation included -- the claim that owns that side reds and the author +// must restate the row. Nothing was lost by deleting the comparison except a second spelling of a +// fact the table already carries. + // The name-keyed algebra against the DECLARED ROSTERS, not against the other algebra. test fn name_keyed_coercion_matches_the_declared_cast_rosters_holds() -> Bool { fold(coercion_fork_fixtures, init: true, f: fn(acc, row) { @@ -258,20 +275,3 @@ test fn homomorphism_coercion_admits_only_identity_quality_holds() -> Bool { } }) } - -// WHY THERE IS NO CLAIM COMPARING THE TWO ALGEBRAS TO EACH OTHER, AND NO AUTHORED `AGREE` COLUMN -// (review 70065). A claim asserting name_keyed_admission(row) == homomorphism_admission(row), read -// against an authored third column, is ENTAILED by the two claims above: each pins its side to its -// own independently specified expectation, so the comparison reduces to asking whether that third -// column contradicts the first two -- a check of the fixture against itself, which reds on no -// behaviour change the first two do not already catch. DESIGN section 4b rules the check out before -// it is written, and DESIGN section 2 names the column: a third authored fact fully determined by -// two others is re-invention, not a reduction. -// -// THE MEASUREMENT SURVIVES WITHOUT IT, and this is the point rather than a concession. The -// agreement relation is DERIVED from the two expectation columns, which sit side by side on every -// row: four of the seven rows carry expectations that differ, in both directions, and that is the -// fork stated where a reader meets the population. If either algebra's admission set moves -- in -// either direction, consolidation included -- the claim that owns that side reds and the author -// must restate the row. Nothing was lost by deleting the comparison except a second spelling of a -// fact the table already carries.