From 3e09a99d36e0fc2a379bb8778ef4de122eae63b9 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 02:01:58 +0000 Subject: [PATCH 1/5] Enrol the five witness-test cadence recitals in the census that owns them, and correct their prose MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Follow-on to #9858. Five annotations asserted that a deleted cadence executes them; std.witness_admission witness_cadence_has_scheduled_route reports all three named arms routeless. SAME SUBJECT, ANSWERED AGAINST THE CENSUS'S OWN DECLARATION RATHER THAN BY RESEMBLANCE. gunbc.deleted_cadence_reference_census's twelve rows are authority rows that RELIED on the cadence for a coverage claim; these five are witness tests whose annotations asserted the cadence EXECUTES them. That is the same subject reached from the other side — the row's coverage rests on a dark cadence either way — and the precedent is already in the census: tools.namespace_import_closure_behavioral_transport nic_doc is a wet-receipt transport doc censused there, carrying the exact correction these five now match. So this is enrollment in an existing subject, not a widening of it, and no new authority is minted. THE CENSUS'S VOCABULARY CORRECTED MY OWN READING TWICE, which is the argument for using it rather than editing prose beside it. 1. NONE OF THE FIVE IS ReboundToExecutingConsumer, INCLUDING THE TWO CARRYING A LOCAL RECIPE. I had recorded on #9858 that instrument_sandbox's live half genuinely executes via its local recipe and should be corrected rather than past-tensed. Too generous: std.witness_admission answers OfflineLocalRecipe true, which is a statement about ROUTES, while this census asks the stricter question and its own note answers it — a command with no workflow is a local recipe, not a scheduled entry point. Two authorities, two questions; reading the looser answer into the stricter one would have manufactured coverage. The recipes are recorded as MANUAL routes instead. 2. The site is the DECLARATION THE ANNOTATION IS ATTACHED TO, because §4c annotations have no symbol of their own for a DeclarationRef to name. WHAT LANDS: - five PremiseInvalidated rows, plus substrate_long_lane_coverage for the third cadence (the other two coverage rows already existed and are reused). - the census's own arithmetic brought into agreement with itself: "THE TWELVE SITES … two more than the ten" becomes seventeen and fifteen, and the five are added to the drop population, because a PremiseInvalidated row IS one a re-add restores — which is the distinction that comment already spells out. - five prose corrections, one remedy arm each per gunbc.recurring_failure_mode unbacked_execution_claim, MATCHING THE TWO EXISTING EXEMPLARS rather than inventing a style beside them: nic_doc's "classification is membership, not execution" for the two self-host receipts, and ci_layer_roots bin_witness_wet_note's "THE JUSTIFYING HALF OF THAT SENTENCE IS PAST TENSE" for self_host_logic, which is the strongest instance. The perturb line keeps its true "Enrolled on" and loses only the false "nightly". NOT VERIFIED LOCALLY, DELIBERATELY: the census witness runs deleted_cadence_reference_census_live_holds over the live rows, so it checks every new row's cadence is genuinely routeless. Two remote attempts refused fail-closed with HostBudgetUnreadable — the BuildBuddy runner exposes no cgroup memory limit, so the corpus resolve cannot bound itself and refuses rather than defaulting. That is the runner, not this change, and it never reached the witness. CI's floor job is the executing evidence, as it was for #9858. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Li6e7cEDFodeBV7uPi3yTz --- .../deleted_cadence_reference_census.dag | 71 +++++++++++++++++-- .../claim/instrument_sandbox_witness_test.dag | 11 ++- ...pile_clean_perturb_corpus_witness_test.dag | 2 +- ..._body_producer_behavioral_witness_test.dag | 9 ++- ...elf_host_logic_behavioral_witness_test.dag | 13 +++- ...e_site_verdict_behavioral_witness_test.dag | 8 ++- 6 files changed, 99 insertions(+), 15 deletions(-) diff --git a/dag/gunbc/deleted_cadence_reference_census.dag b/dag/gunbc/deleted_cadence_reference_census.dag index 558ffa5eac5..3aabc8da204 100644 --- a/dag/gunbc/deleted_cadence_reference_census.dag +++ b/dag/gunbc/deleted_cadence_reference_census.dag @@ -189,14 +189,20 @@ data self_host_wet_roster_coverage: CoverageNotEstablished = CoverageNotEstablis restoration_trigger: "witness_cadence_has_scheduled_route(FalsifierSelfHostWet) returns true, which is the separate operator agreement std.witness_admission witness_cadence_has_scheduled_route_note reserves" as NonEmptyStr, } +data substrate_long_lane_coverage: CoverageNotEstablished = CoverageNotEstablished { + lost_with: FalsifierSubstrateLongLane, + restoration_trigger: "witness_cadence_has_scheduled_route(FalsifierSubstrateLongLane) returns true" as NonEmptyStr, +} + data bin_wet_template_coverage: CoverageNotEstablished = CoverageNotEstablished { lost_with: FalsifierRehomedBinWet, restoration_trigger: "witness_cadence_has_scheduled_route(FalsifierRehomedBinWet) returns true" as NonEmptyStr, } -// The DROP row for the class, filed once rather than per site. Twelve authority rows lost -// one shared thing -- the executor -- so twelve copies of the same five fields would be -// twelve places to update when the route returns. +// The DROP row for the class, filed once rather than per site. Seventeen rows lost one shared +// thing -- the executor -- so seventeen copies of the same five fields would be seventeen places +// to update when the route returns. That is also why the five sites added 2026-09-01 enrol here +// instead of carrying drops of their own. data deleted_cadence_reference_drop: GuaranteeRungDrop = GuaranteeRungDrop { subject: "authority rows whose stated enforcement, audit or backstop was the affected-set falsifier cadence", previous: Mitigatable, @@ -211,14 +217,20 @@ data deleted_cadence_reference_drop: GuaranteeRungDrop = GuaranteeRungDrop { "gunbc.ci_layer_roots bin_witness_wet_note", "tools.namespace_import_closure_behavioral_transport nic_doc", "v2.compiler.self_host.seed_emitter_behavioral_wet_module_bindings falsifier_self_host_wet_module_bindings_revocation_note", + "test.claim.instrument_sandbox_witness fixture_line_remaining", + "test.claim.self_host_use_site_verdict_behavioral_witness self_host_use_site_verdict_behavioral_receipt_holds", + "test.claim.self_host_body_producer_behavioral_witness self_host_body_producer_behavioral_receipt_holds", + "test.claim.self_host_logic_behavioral_witness self_host_logic_behavioral_receipt_holds", + "test.claim.long.dag_compile_clean_perturb_corpus perturb_cross_tree_import_corpus_green_holds", "v2.std.live_tree live_tree_disposition_stamp_provenance", "v1_compiler.cli_run parse_entry_live_tree_disposition", ], restoration_trigger: "a workflow or scheduled entry point exists that runs a predict-only cold comparison over the corpus, at which point each row above is reclassified from PremiseInvalidated to ReboundToExecutingConsumer with that consumer's receipt", } -// THE TWELVE SITES. Two more than the ten the drop population names, because two of them -// are HistoricalReceipt rows and a historical receipt is not a population a re-add restores. +// THE SEVENTEEN SITES (twelve at landing, five witness-test sites added 2026-09-01). Two more +// than the fifteen the drop population names, because two of them are HistoricalReceipt rows and +// a historical receipt is not a population a re-add restores. // // TWO SITES ARE CARRIED HERE AND EDITED NOWHERE, deliberately: `v2.std.live_tree` // `live_tree_disposition_stamp_provenance` and its near-verbatim host mirror @@ -325,6 +337,55 @@ fn deleted_cadence_references() -> List { current_coverage: self_host_wet_roster_coverage, }, }, + // FIVE WITNESS-TEST SITES (added 2026-09-01, XL-0-RECEIPT follow-on). The twelve rows above are + // authority rows that RELIED on the cadence for a coverage claim; these five are witness tests + // whose own annotations asserted the cadence EXECUTES them, which is the same subject reached + // from the other side -- the row's coverage rests on a dark cadence either way. The precedent is + // `tools.namespace_import_closure_behavioral_transport` `nic_doc`, already censused here and + // already carrying the exact correction these five now match, so this is enrollment in an + // existing subject rather than a widening of it. The site is the declaration the annotation is + // attached to, because §4c annotations have no symbol of their own for a `DeclarationRef` to name. + // + // NONE OF THE FIVE IS `ReboundToExecutingConsumer`, INCLUDING THE TWO THAT CARRY A LOCAL RECIPE. + // `std.witness_admission` answers OfflineLocalRecipe true, which is a statement about routes; + // this census asks the stricter question and its own note answers it -- a command with no + // workflow is a local recipe, not a scheduled entry point. Two authorities, two questions, and + // reading the looser answer into the stricter one would have manufactured coverage. + DeletedCadenceReference { + site: decl_ref(module_path: "test.claim.instrument_sandbox_witness", decl_name: "fixture_line_remaining"), + standing: PremiseInvalidated { + affected_decision: decl_ref(module_path: "gunbc.ci_layer_roots", decl_name: "falsifier_substrate_long_lane_rows"), + current_coverage: substrate_long_lane_coverage, + }, + }, + DeletedCadenceReference { + site: decl_ref(module_path: "test.claim.self_host_use_site_verdict_behavioral_witness", decl_name: "self_host_use_site_verdict_behavioral_receipt_holds"), + standing: PremiseInvalidated { + affected_decision: decl_ref(module_path: "v2.compiler.self_host.wet_receipt_enrollment", decl_name: "falsifier_self_host_wet_enrollment_note"), + current_coverage: self_host_wet_roster_coverage, + }, + }, + DeletedCadenceReference { + site: decl_ref(module_path: "test.claim.self_host_body_producer_behavioral_witness", decl_name: "self_host_body_producer_behavioral_receipt_holds"), + standing: PremiseInvalidated { + affected_decision: decl_ref(module_path: "v2.compiler.self_host.wet_receipt_enrollment", decl_name: "falsifier_self_host_wet_enrollment_note"), + current_coverage: self_host_wet_roster_coverage, + }, + }, + DeletedCadenceReference { + site: decl_ref(module_path: "test.claim.self_host_logic_behavioral_witness", decl_name: "self_host_logic_behavioral_receipt_holds"), + standing: PremiseInvalidated { + affected_decision: decl_ref(module_path: "v2.compiler.self_host.wet_receipt_enrollment", decl_name: "falsifier_self_host_wet_enrollment_note"), + current_coverage: self_host_wet_roster_coverage, + }, + }, + DeletedCadenceReference { + site: decl_ref(module_path: "test.claim.long.dag_compile_clean_perturb_corpus", decl_name: "perturb_cross_tree_import_corpus_green_holds"), + standing: PremiseInvalidated { + affected_decision: decl_ref(module_path: "gunbc.ci_layer_roots", decl_name: "falsifier_rehomed_bin_wet_rows"), + current_coverage: bin_wet_template_coverage, + }, + }, ] } diff --git a/dag/test/claim/instrument_sandbox_witness_test.dag b/dag/test/claim/instrument_sandbox_witness_test.dag index c844a941669..befe6ba9e66 100644 --- a/dag/test/claim/instrument_sandbox_witness_test.dag +++ b/dag/test/claim/instrument_sandbox_witness_test.dag @@ -147,8 +147,15 @@ fn witness_the_press_response_is_a_bounded_translation() -> Bool { // grain onto outcome grain is caught by VALUE and not merely by variant — asserting the variant // alone would still pass if some future arm returned a program-shaped reading built from the line's // own shape. Cheap by construction: the record is built directly rather than derived through -// program_view, so this mechanism claim costs microseconds and stays per-PR while the live half -// runs on the falsifier lane. +// program_view, so this mechanism claim costs microseconds and stays per-PR. The live half moved +// to dag/test/claim/long/instrument_sandbox_live_witness_test.dag, and THE SENTENCE HERE USED TO +// SAY IT RUNS ON THE FALSIFIER LANE (corrected 2026-09-01). That lane is dark: the half is enrolled +// on gunbc.ci_layer_roots falsifier_substrate_long_lane_rows, and std.witness_admission +// witness_cadence_has_scheduled_route answers FalsifierSubstrateLongLane false since falsifier.yml +// was deleted at 611fd02770 (#8283, 2026-08-15). Its only route today is the local recipe carried +// in that file's own header, which is a MANUAL route and not a scheduled executing consumer -- +// gunbc.deleted_cadence_reference_census requires a scheduled entry point for that, and a command +// with no workflow does not supply one. Censused as PremiseInvalidated there. fn fixture_line_remaining() -> RemainingShape { RemainingShape { diff --git a/dag/test/claim/long/dag_compile_clean_perturb_corpus_witness_test.dag b/dag/test/claim/long/dag_compile_clean_perturb_corpus_witness_test.dag index ddde6ce4a35..597ed21399e 100644 --- a/dag/test/claim/long/dag_compile_clean_perturb_corpus_witness_test.dag +++ b/dag/test/claim/long/dag_compile_clean_perturb_corpus_witness_test.dag @@ -8,7 +8,7 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -// Class C corpus-grain legs for compile-clean perturb receipts: cross_tree_import and dag_shell_primary_precedence compile against compile_clean_source_roots (live-tree pool). Enrolled on falsifier_rehomed_bin_wet_entries (nightly batch 5); local recipe: claim_batch --wet --source-root dag --source-root src/v2 --entry dag/test/claim/long/dag_compile_clean_perturb_corpus_witness_test.dag --function . +// Class C corpus-grain legs for compile-clean perturb receipts: cross_tree_import and dag_shell_primary_precedence compile against compile_clean_source_roots (live-tree pool). Enrolled on falsifier_rehomed_bin_wet_entries -- ENROLLMENT ONLY, NOT EXECUTION: this line said "nightly batch 5" until 2026-09-01, and while the enrollment is real the cadence is dark, since falsifier.yml was deleted at 611fd02770 (#8283, 2026-08-15) and std.witness_admission witness_cadence_has_scheduled_route answers FalsifierRehomedBinWet false. Censused as PremiseInvalidated in gunbc.deleted_cadence_reference_census. The local recipe below is the only route today, and it is manual rather than a scheduled consumer. Local recipe: claim_batch --wet --source-root dag --source-root src/v2 --entry dag/test/claim/long/dag_compile_clean_perturb_corpus_witness_test.dag --function . test fn perturb_cross_tree_import_corpus_green_holds() -> Bool { run_cross_tree_import_green_receipt() } diff --git a/dag/test/claim/self_host_body_producer_behavioral_witness_test.dag b/dag/test/claim/self_host_body_producer_behavioral_witness_test.dag index 8658f2c35a5..5c3412be0d5 100644 --- a/dag/test/claim/self_host_body_producer_behavioral_witness_test.dag +++ b/dag/test/claim/self_host_body_producer_behavioral_witness_test.dag @@ -6,8 +6,13 @@ import tools.self_host_module_behavioral_transport_roster { compiler_module_beha // tools.self_host_module_behavioral_transport_roster's compiler_module_behavioral_receipt_for emits // src/v2/compiler/03_body_producer.dag via gunbc --entry, assembles a seed-linked v1_compiled crate // (gunbc-emitted entry + dep shims + v1-compiler path dep), runs cargo build + witness (plain + -// --inject-fault), and claim-run on structured_body_dispatch. Live host effects — nightly falsifier -// Wet batch when frontier row is SelfEmitted with binding. +// --inject-fault), and claim-run on structured_body_dispatch. Live host effects, so it is +// CLASSIFIED onto the falsifier Wet batch when the frontier row is SelfEmitted with binding -- and +// classification is membership, not execution (corrected 2026-09-01, matching +// tools.namespace_import_closure_behavioral_transport nic_doc): falsifier.yml was deleted at +// 611fd02770 (#8283, 2026-08-15) and std.witness_admission witness_cadence_has_scheduled_route +// answers FalsifierSelfHostWet false, so nothing runs this receipt today. Censused as +// PremiseInvalidated in gunbc.deleted_cadence_reference_census. test fn self_host_body_producer_behavioral_receipt_holds() -> Bool { compiler_module_behavioral_receipt_for(module_path: "src/v2/compiler/03_body_producer.dag") diff --git a/dag/test/claim/self_host_logic_behavioral_witness_test.dag b/dag/test/claim/self_host_logic_behavioral_witness_test.dag index e48b1cc60a1..de07ec2c6aa 100644 --- a/dag/test/claim/self_host_logic_behavioral_witness_test.dag +++ b/dag/test/claim/self_host_logic_behavioral_witness_test.dag @@ -6,9 +6,16 @@ import tools.self_host_logic_behavioral_transport { slb_behavioral_receipt_holds // tools.self_host_logic_behavioral_transport emits dag/std/logic.dag via the real gunbc binary, // compiles the emitted Rust against the v1-compiler seed crate, and runs the resulting witness // binary (plain + --inject-fault) to prove emit -> compile -> run -> equals-seed behavioral -// equivalence by execution. Live host effects (cargo build, process execution), so it runs in the -// nightly falsifier Wet follow-on batch (falsifier_self_host_wet_entries), not per-PR hermetic -// discovery or bin_witness_wet — the proven template lane for Wave 2 self-host receipts. +// equivalence by execution. Live host effects (cargo build, process execution), so it is CLASSIFIED +// onto the falsifier Wet follow-on batch (falsifier_self_host_wet_entries) rather than per-PR +// hermetic discovery or bin_witness_wet. THE JUSTIFYING HALF OF THAT SENTENCE IS PAST TENSE +// (corrected 2026-09-01): the falsifier WAS the proven template lane for Wave 2 self-host receipts, +// and that was the reason this receipt could leave per-PR without leaving coverage. falsifier.yml +// was deleted at 611fd02770 (#8283, 2026-08-15), std.witness_admission +// witness_cadence_has_scheduled_route answers FalsifierSelfHostWet false, and no replacement +// executor exists -- so the destination this receipt was classified onto executes nothing, and the +// classification now removes it from per-PR coverage without adding any. Censused as +// PremiseInvalidated in gunbc.deleted_cadence_reference_census. test fn self_host_logic_behavioral_receipt_holds() -> Bool { slb_behavioral_receipt_holds() diff --git a/dag/test/claim/self_host_use_site_verdict_behavioral_witness_test.dag b/dag/test/claim/self_host_use_site_verdict_behavioral_witness_test.dag index 22d12168d9c..4614bc49454 100644 --- a/dag/test/claim/self_host_use_site_verdict_behavioral_witness_test.dag +++ b/dag/test/claim/self_host_use_site_verdict_behavioral_witness_test.dag @@ -7,8 +7,12 @@ import tools.self_host_module_behavioral_transport_roster { compiler_module_beha // src/v2/compiler/use_site_verdict.dag via gunbc --entry, assembles a seed-linked v1_compiled crate // (entry self-emitted + seed-retained dep shim + v1-compiler path dep), runs cargo build + witness // (plain + --inject-fault), and equals-eval on use_site_verdict_test claims (the two supplementary -// claim_runs the roster row declares). Live host effects — nightly falsifier Wet batch when -// frontier row is SelfEmitted with binding. +// claim_runs the roster row declares). Live host effects, so it is CLASSIFIED onto the falsifier +// Wet batch when the frontier row is SelfEmitted with binding -- and classification is membership, +// not execution (corrected 2026-09-01, matching tools.namespace_import_closure_behavioral_transport +// nic_doc): falsifier.yml was deleted at 611fd02770 (#8283, 2026-08-15) and std.witness_admission +// witness_cadence_has_scheduled_route answers FalsifierSelfHostWet false, so nothing runs this +// receipt today. Censused as PremiseInvalidated in gunbc.deleted_cadence_reference_census. test fn self_host_use_site_verdict_behavioral_receipt_holds() -> Bool { compiler_module_behavioral_receipt_for(module_path: "src/v2/compiler/use_site_verdict.dag") From f6f064ed85ad1699baea3f917929e249cc4ad2fd Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 02:30:30 +0000 Subject: [PATCH 2/5] =?UTF-8?q?Move=20the=20explanatory=20block=20out=20of?= =?UTF-8?q?=20the=20function=20body=20=E2=80=94=20=C2=A74c=20models=20modu?= =?UTF-8?q?le-item=20grain=20only?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The parse phase refused 14 times, once per line of a `//` block I placed INSIDE `deleted_cadence_references()` between the census rows: source annotation sits inside a declaration body. Only module-item grain is modeled; move it above the declaration. Moved verbatim to module scope, joining the existing header comment above that fn, where it reads better anyway because it now sits beside the "THE SEVENTEEN SITES" arithmetic it elaborates. WHAT THE FAILING RUN ACTUALLY ESTABLISHED, since it is easy to read a red job as a red change: the floor was CLEAN — verdict=FloorClean, planned=3349 executed=3349 failed=0, with 19 known-reds held and none newly passing. So `deleted_cadence_reference_census_live_holds` DID run over the five new rows and DID pass, which is the executing evidence this PR was waiting on: each new row's cadence is genuinely routeless. The two failing phases were parse (this defect) and namespace-wave-admission, which did not run at all because parse produced no index. One authoring defect, no modeling defect. Checked the same class across all six files this PR touches with a brace-depth scan rather than by eye: no `//` inside any body remains. This is a repeat of a class I had already been bitten by and had written down. Recording it here rather than only in the commit that fixes it, because the recurrence is the useful part: annotation grain is a rule the author must apply at authoring time, and a long explanatory block is exactly where the temptation to sit it beside the rows it explains is strongest. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Li6e7cEDFodeBV7uPi3yTz --- .../deleted_cadence_reference_census.dag | 30 ++++++++++--------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/dag/gunbc/deleted_cadence_reference_census.dag b/dag/gunbc/deleted_cadence_reference_census.dag index 3aabc8da204..f554b867495 100644 --- a/dag/gunbc/deleted_cadence_reference_census.dag +++ b/dag/gunbc/deleted_cadence_reference_census.dag @@ -239,6 +239,22 @@ data deleted_cadence_reference_drop: GuaranteeRungDrop = GuaranteeRungDrop { // authors correcting one sentence into a conflict. They are censused rather than skipped // because a census that omitted its already-owned rows would report a completeness it // does not have. +// +// THE FIVE WITNESS-TEST SITES (added 2026-09-01, XL-0-RECEIPT follow-on) are the last five rows +// below. The twelve before them are authority rows that RELIED on the cadence for a coverage claim; +// these five are witness tests whose own annotations asserted the cadence EXECUTES them, which is +// the same subject reached from the other side -- the row's coverage rests on a dark cadence either +// way. The precedent is `tools.namespace_import_closure_behavioral_transport` `nic_doc`, already +// censused here and already carrying the exact correction these five now match, so this is +// enrollment in an existing subject rather than a widening of it. The site is the declaration the +// annotation is attached to, because §4c annotations have no symbol of their own for a +// `DeclarationRef` to name. +// +// NONE OF THE FIVE IS `ReboundToExecutingConsumer`, INCLUDING THE TWO THAT CARRY A LOCAL RECIPE. +// `std.witness_admission` answers OfflineLocalRecipe true, which is a statement about routes; this +// census asks the stricter question and its own note answers it -- a command with no workflow is a +// local recipe, not a scheduled entry point. Two authorities, two questions, and reading the looser +// answer into the stricter one would have manufactured coverage. fn deleted_cadence_references() -> List { [ DeletedCadenceReference { @@ -337,20 +353,6 @@ fn deleted_cadence_references() -> List { current_coverage: self_host_wet_roster_coverage, }, }, - // FIVE WITNESS-TEST SITES (added 2026-09-01, XL-0-RECEIPT follow-on). The twelve rows above are - // authority rows that RELIED on the cadence for a coverage claim; these five are witness tests - // whose own annotations asserted the cadence EXECUTES them, which is the same subject reached - // from the other side -- the row's coverage rests on a dark cadence either way. The precedent is - // `tools.namespace_import_closure_behavioral_transport` `nic_doc`, already censused here and - // already carrying the exact correction these five now match, so this is enrollment in an - // existing subject rather than a widening of it. The site is the declaration the annotation is - // attached to, because §4c annotations have no symbol of their own for a `DeclarationRef` to name. - // - // NONE OF THE FIVE IS `ReboundToExecutingConsumer`, INCLUDING THE TWO THAT CARRY A LOCAL RECIPE. - // `std.witness_admission` answers OfflineLocalRecipe true, which is a statement about routes; - // this census asks the stricter question and its own note answers it -- a command with no - // workflow is a local recipe, not a scheduled entry point. Two authorities, two questions, and - // reading the looser answer into the stricter one would have manufactured coverage. DeletedCadenceReference { site: decl_ref(module_path: "test.claim.instrument_sandbox_witness", decl_name: "fixture_line_remaining"), standing: PremiseInvalidated { From b8429bbe8c53d983746cdf4803484016a1b31f09 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 03:55:48 +0000 Subject: [PATCH 3/5] File the third inhabitance seam: a bodyless declared type admits any argument MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit DESIGN §4b obliges every newly discovered error class to file or update one row. The row "a value that does not inhabit its declared type is accepted" already says its enumeration is unfinished and to assume a third seam exists until someone enumerates them. This is one, so it updates that row rather than opening a second authority for the same class. The seam is not a position. (a)/(b)/(c) all vary the position while holding the declared type ordinary; here the position is the already-covered direct-call parameter and the DECLARED TYPE is bodyless. Any `type X` with no body admits any argument, silently. Measured in an ordinary non-v2 module, so seam (1)'s exemption is not in play: a String is accepted against `Compose>`, against a bare `Phantom`, and against a locally declared `type Opaque` with no Phantom involved -- while the control `type MyRec = Word8` refuses with both a type mismatch and an inhabitance diagnostic. The control is what makes this a finding: the judgment RUNS here and admits, which is a different mechanism from seam (1), where the judgment never runs. It is neither Phantom-specific nor Compose-specific; both were the obvious readings and the third fixture refutes them. The population is recorded as syntactic and not as an exposure count, and the row says why 5227 is the wrong number for it. Also recorded: `tools.opaque_realization_census` decides opacity from the declaration line alone and carries an annotation asserting the multi-line body spelling does not occur in this corpus. It occurs 5269 times, and the function classifies every one of them DeclaredOpaque. Separately it matches by bare prefix with no name boundary, so a longer same-prefix name declared earlier in a file decides a shorter name's standing (304 pairs). Both read from the function rather than its annotation. It gates nothing, so it is a wrong instrument rather than a wrong wall -- but it is the instrument this row's population question would be handed to. Not enrolled: no probe asserts any of this, and the row says so and names the next trigger at capability grain. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_013wJU7jqGAEk8rj4UwpHdox --- docs/plans/compiler-guarantee-recovery-gap-analysis.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index 03758c9d00e..e67eb73c041 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -170,7 +170,7 @@ unless the row says otherwise, and `Unknown` is the honest default. | Closed-match exhaustiveness | **Path-split, measured 2026-08-01 — the class is not one rung.** Coproduct-typed scrutinee: **R2** (a missing arm on a declared closed variant refuses `NonExhaustiveMatch`, blocking, naming the absent variant). Type-variable scrutinee: **below floor — silent** (`fn pick(t: T) -> Int { match t { Red => 1 } }` compiles with zero diagnostics — one arm, an unconstrained subject, and a variant belonging to an unrelated type). Class rung is the minimum, so **below floor** | R3 (full arm population at elimination) | the silent arm is `PatternDynamic { span: _ } => []`, **not** `PatternLookupBlocked => []` as this row previously said — `pattern_subject_from_node` reaches `PatternLookupBlocked` only when the scrutinee's inferred type `is_compiler_error`, i.e. where a diagnostic already exists, so that arm is not the silent one and its silence is **not** established by these probes | first measured by a one-off execution 2026-08-01 via `compile_dag_diagnostic_census` on the v1 CompileAccept path (source and result in the §10 eighth-pass ledger), and **AUTHORED AS A PROBE PAIR 2026-08-22 — AUTHORED, NOT EXECUTING, AND THE DISTINCTION IS THE WHOLE POINT** (see §11 item 28): the measurement is now written as `test.claim.guarantee_floor_class_probe_witness` `floor_exhaustiveness_on_a_type_variable_scrutinee_is_still_silent`, against the registry row `gunbc.guarantee_probe_corpus` class `floor-closed-match-exhaustiveness`, with the coproduct-scrutinee arm already enrolled at `test.claim.match_exhaustiveness_coproduct_witness` `w_missing_coproduct_arm_reports_one_non_exhaustive`, on the same harness and the same floor run — not re-authored here, because a second copy would be a second authority for one fact as its probe-adequacy control. **It does not run in CI.** The witness declares `ReadsLiveTree` — truthfully, because `compile_dag_diagnostic_census` resolves its synthetic source against the live checkout — and the required floor DECLINES every `ReadsLiveTree` module before the fold sees it (`v2.workflow.required_floor` `RequiredFloorDisposition` `DeclinedLiveTree`), so the probe is discovered and never executed, exactly like the five guarantee carriers §11 item 28 counts. It is green by execution LOCALLY (`gunbc run --claim-run`, 2026-08-22, this session) and that is a strictly weaker fact. So this cell's rung is unchanged from the day before the probe was authored: it still rests on a measurement nothing re-runs. What the probe pair buys is that on the day the decline arm is deleted the measurement becomes standing evidence with no further authorship. Trigger: the `DeclinedLiveTree` deletion (§11 item 28), NOT this cell (§4b meta-obligation 4; the original gap was codex review 46306, §11 item 10) | `ExhaustivenessUnknown` refuses on the dynamic subject | | Record completeness | **R2 measured 2026-08-01** (a record literal omitting a declared required field refuses `MissingField`, blocking, naming the field and type — the class was carried as `Unknown — unmeasured` and the measurement raises it) | R3 | judgment is per-literal; construction-side and generic-instantiation completeness are separate and the latter measures **below floor** in the row above | first measured by a one-off execution 2026-08-01 via `compile_dag_diagnostic_census` on the v1 CompileAccept path (source and result in the §10 eighth-pass ledger), and **AUTHORED AS A PROBE PAIR 2026-08-22 — AUTHORED, NOT EXECUTING, AND THE DISTINCTION IS THE WHOLE POINT** (see §11 item 28): the measurement is now written as `test.claim.guarantee_floor_class_probe_witness` `floor_record_completeness_missing_field_refuses_blocking`, against the registry row `gunbc.guarantee_probe_corpus` class `floor-record-field-completeness`, with `floor_record_completeness_green_control_is_clean` as its probe-adequacy control. **It does not run in CI.** The witness declares `ReadsLiveTree` — truthfully, because `compile_dag_diagnostic_census` resolves its synthetic source against the live checkout — and the required floor DECLINES every `ReadsLiveTree` module before the fold sees it (`v2.workflow.required_floor` `RequiredFloorDisposition` `DeclinedLiveTree`), so the probe is discovered and never executed, exactly like the five guarantee carriers §11 item 28 counts. It is green by execution LOCALLY (`gunbc run --claim-run`, 2026-08-22, this session) and that is a strictly weaker fact. So this cell's rung is unchanged from the day before the probe was authored: it still rests on a measurement nothing re-runs. What the probe pair buys is that on the day the decline arm is deleted the measurement becomes standing evidence with no further authorship. Trigger: the `DeclinedLiveTree` deletion (§11 item 28), NOT this cell (§4b meta-obligation 4; the original gap was codex review 46306, §11 item 10) | required-field construction at every construction form | | Parse: list separator dropped | **Below floor — silent** (measured: `[ {a}, {b} {c} ]` compiles with zero diagnostics — a dropped comma is a silent semantic change, two- vs three-element list; survived regen, whole-corpus compile, fixed-point verify and a 15-case matrix, caught only by a human diff read) | R3 (decidable grammar fact) | separator omission parses as element juxtaposition | First measured by tidy-deer-730's throwaway probe on gunbc#7484 + review 45347, 2026-07-31. **PROBE PAIR AUTHORED 2026-08-22, NOT EXECUTING** (§11 item 28 — the witness is declined by the floor's `DeclinedLiveTree` arm and runs only under a local `gunbc run --claim-run`): `test.claim.guarantee_floor_class_probe_witness` `floor_parse_list_separator_omission_is_still_silent` re-executes it on every required-floor run against `gunbc.guarantee_probe_corpus` class `floor-parse-list-separator`, with `floor_parse_list_separator_doubled_separator_control_refuses` (a DOUBLED separator in the same position refuses `ParseError`, blocking) and `floor_parse_list_separator_green_control_is_clean` as its probe-adequacy controls, all three green locally and none of them executing in CI — so the omission's silence is measured against a parser that demonstrably refuses malformed separators | the probe pair is now in the corpus and pins the hole; what remains is the refusal in the list production (§11 item 6), on which the enrolled probe flips RED and its row is rewritten as `ExpectBlockingRefusal` | -| A value that does not inhabit its declared type is accepted — **seam-split, enumeration UNFINISHED** (was filed as "Direct-call argument TYPE conformance, v2 corpus"; renamed 2026-08-22, see the trigger cell) | **Below floor — the judgment never runs.** Not a hole a bad value slipped through: `v1.compiler.04_infer` gates `arg_compat_diags` on `module_skips_direct_call_arg_check(module_name: scope.module_name)`, which returns true for every module whose name begins with `v2.`. The key is the CALLER's module, so the entire active v2 corpus — compiler stages, extdeps, std, witnesses — has the direct-call argument-type judgment switched off. Measured consequence, 2026-08-22: `v2.extdeps.languages.dag` `dag_int_literal_node_from_lexeme` / `dag_int_literal_node_from_magnitude` declared `occurrence_id: OccurrenceId` since gunbc#6558 while storing that parameter straight into `Node.occurrence_id`, declared `NodeOccurrenceId`. For two months 15 call sites passed `SyntheticOccurrence` (a NodeOccurrenceId, contradicting the declaration) and nothing complained; gunbc#8833 made one call site OBEY the declaration and nothing complained about that either. The error surfaced only as an interpreter `non-exhaustive pattern match on: OccurrenceId { value: 79 }` across 16 witnesses, reddening main. **The inversion worth naming: a declaration that lies is inert while every caller contradicts it in the same direction, and detonates on the first caller who takes it at its word.** So the at-risk population is not "callers who got it wrong" but callers who might get it right — a genuinely counterintuitive census. Note this is the TYPE judgment only; the SHAPE judgment (`direct_call_shape_diags`, labels/arity) is exemption-free and does fire | R2 (a declared parameter type is a decidable conformance check the seam already computes — `direct_call_arg_mismatch_diags` exists, is written, and is simply not called, so the distance to the next rung is an if-statement plus a triage, not an implementation) | **THIS ROW IS A CORRECTION TO DESIGN §4b, NOT A NEW OBSERVATION BESIDE IT — read them together or the first will look like it already settled this.** DESIGN §4b names this exact symbol and reports that it "was found (code read, not execution) to be scoped entirely to the direct-call argument-type judgment and does not reach `sole_constructor`'s construction check at either call site — a positive finding that retires this axis, not an absence of any exemption anywhere." That finding is correct and is not disputed here. The question it asked was whether the exemption LEAKS into `sole_constructor`; the question it never asked is what the exemption COSTS inside the judgment it is scoped to. "Scoped entirely to the direct-call argument-type judgment" reads as reassuring only until that judgment is measured, and it is the argument-type check for the entire active v2 corpus. **Confinement was measured and then treated as safety, and the axis that got retired was not the one that mattered.** Two facts about why the seam nonetheless reads as covered: the SHAPE judgment (`direct_call_shape_diags` — labels, arity, duplicate binding) is exemption-free and DOES fire over every module including the compiler's own sources, so half-live is more deceptive than dead — every casual check finds something working. And the arm is NOT unreasoned: `direct_call_shape_wall_note` states the TYPE judgment's false-positive classes are representation gaps (brand aliases, optionality's two forms, anonymous literals, expansion depth — the conformance wall's four measured classes), which is a real stated reason and is why this row asks for a measurement rather than a deletion. What is unmeasured is whether those classes still fire in v2 today and at what rate. The neighbouring compiler-module arm of this same exemption was deleted in place after being found never to have been in force; the `v2.` arm was left standing at that moment without separate justification of its own | This incident, measured end to end: CI run 32542017600 (main, 67437fcbe9) 16 FAIL with the raw-`OccurrenceId` match error; caller census of both functions read at call grain (17 sites: 15 `SyntheticOccurrence`, 1 `node.occurrence_id`, 1 internal pass-through, 1 raw `minted.id`); exemption mechanism read at `v1.compiler.04_infer` `module_skips_direct_call_arg_check` and its single call site gating `arg_compat_diags` on `scope.module_name`. **NOT ENROLLED**: no probe pair asserts this exemption's reach, so nothing reds if it changes | **THE TRIGGER THIS ROW SHIPPED WITH WAS INCOMPLETE AND IS CORRECTED HERE (2026-08-22, swift-badger-524 retracting their own ruling).** As merged in gunbc#8854 this cell named ONE closing condition — delete the `v2.` exemption — which is a NECESSARY condition presented as a sufficient one. The class is not "direct-call argument type conformance"; it is **a value that does not inhabit its declared type is accepted**, and it has at least TWO seams: **(1) direct-call arguments** — gated off for `v2.*` by `module_skips_direct_call_arg_check`, the mechanism this row measures; **(2) record-literal fields** — gated by NOTHING, below floor in ORDINARY NON-v2 MODULES, receipt gunbc#8865 (gentle-eagle-360). Its minimal pair, no compiler internals involved: `CppHolder { subject: CppWrapped { inner: cpp_inner() } }` accepted and correct, against `CppHolder { subject: cpp_inner() }` — a coproduct PAYLOAD inhabiting a field declared as its parent COPRODUCT — ACCEPTED BY TYPING and dying at runtime as `PatternMatchFailure`. A record literal is not the direct-call seam, so deleting the exemption would not close it. **SEAM (2) NOW HAS A LIVE PRODUCTION SPECIMEN, WHICH RANKS IT DIFFERENTLY FROM A SYNTHETIC PAIR** (gentle-eagle-360, 2026-08-22, found while checking for a second content-identity authority before building on one): `v2.std.materialize` declares `MaterializedNode.hash` as `ContentHash` — the subject-generic union — and `materialize_fold_step` stores `content_hash(n)` into it, which returns `Fnv1a64Structural`, the PAYLOAD carried inside the union's `Fnv1a64` arm. Receipt, by execution against the module as it stands on main: taking the value materialize ACTUALLY STORED and asking the union's own family authority `content_hash_family` about it yields `PatternMatchFailure { value: "Fnv1a64Structural { digest: 7ac77ab0e29c6bd8 }" }`; the probe's fallback was a correctly wrapped `Fnv1a64(...)`, so an empty result or a well-formed value would have PASSED and only a stored value can produce that red. **The defect is LATENT and that is the instructive part**: peer lookup compares `e.hash == h`, raw payload against raw payload, which agrees with itself — so every current path is green and the error surfaces only when a materialize hash is routed through the union's own machinery (`content_hash_family`, or `compare_content_hash`, which exists precisely to refuse cross-family collapse). That is the same shape as this row's own originating incident: **a declaration that lies is inert while every consumer contradicts it in the same direction, and detonates on the first consumer that takes it at its word** — here the first cross-family artifact to reach the carrier. Disposition ruled ARM A, wrap the construction (`MaterializedNode { hash: Fnv1a64(h), ... }`), NOT narrow the declaration: narrowing would sever `MaterializedNode.hash` from `RealizationPlan.target`, and §2's Realization spans resolve-cost, sccache and OS provisioning on ONE content hash, so a structural-only key could never name a realization of a fetched artifact or a provisioned image (swift-badger-524 ruling, 2026-08-22; handed to silent-bear-842 with the receipt, unfixed here because it is that lane's module). **THE SEAM ITSELF IS THE FINDING, not this one site**: gunbc#7480 corrected the design document for asserting the wrong type at exactly this `Hash`/`ContentHash` boundary, and a production module now carries the mirror-image error — a boundary documentation has to keep re-explaining is a boundary that wants construction. ****THAT HAND-OFF IS SUPERSEDED AND THE SPECIMEN IS REPAIRED — corrected in place rather than left standing, because the sentence above says a live production defect is UNFIXED and awaiting another lane, which is the present-tense claim a reader would plan against (gunbc#8876, 2026-08-22).** The wrap landed in the wall's own change by operator ruling: a wall and the repair it forces must land together, since with the wall on and the wrap absent main is red, so only one PR can contain both. `v2.std.materialize` `materialize_fold_step` and `distinct_hashes` now build `Fnv1a64(content_hash(n))`, and the same construction was repaired at four further sites the wall refused for the identical reason — `v2.workflow.operand_flow`, `materialize_witness_test`, `materialization_provider_witness_test` and `heal_revalidation_witness_test`. The receipt above stays as the historical demonstration that the defect was real and reachable; it is no longer a description of the tree. THE ENUMERATION IS UNFINISHED: two is what has been measured, not the count.** Assume a third seam exists until someone enumerates them; note that this row's own originating incident (#8854) reached its victim through a record literal one hop downstream of the direct call, so the two seams are not even cleanly separable at a site. **SEAM (1) WAS EXECUTED TO A MEASURED, BLOCKED STOP ON 2026-08-22 — the arm is NOT deleted, and this paragraph is the §4b row for that state rather than a plan.** Rung: **below floor, unchanged** — the judgment still does not run for any `v2.*` caller. Ceiling: **R2** (a declared parameter type is a decidable conformance check the seam already computes). Next trigger, stated as §4b(2) requires and with its disposition: *a formal parameter declared as an applied generic carries its applied form through resolution rather than reaching the comparison seam as the bare constructor* — **DECLINED at the owning layer on 2026-08-22**, on the ground that a bounded compiler-floor packet whose completion condition has moved should close and hand its residue forward rather than extend into a type-system project. A declined trigger is a legitimate §4b state; **a blocked class with no row is how this exemption survived years in the first place**, which is the reason this row exists at all. Enrolled evidence, so the class stays countable while blocked: `direct_call_arg_type_v2_module_red_probe` (the discriminating RED, rostered in `v2.workflow.floor_expected_red` — it cannot pass while the arm stands and PASSES on a tree with the arm deleted, so it is a satisfiable assertion held open by a named cause), plus two controls that pass on main today (`direct_call_arg_type_ordinary_module_red_probe`, the paired nonzero the exemption never covered; and `direct_call_arg_type_v2_green_control_probe`). **What was measured before the stop, and how to read it:** deleting the arm produces **285+k** blocking diagnostics and **67+k** with gunbc#8873 merged, for some k ≥ 1 unmeasured — these are ROSTER-RESOLVED counts, not corpus counts, and `src/v2/extdeps/formatters/lean4_format.dag:184` is the proof: a live site, structurally identical to eight that refused, contributing zero to *both* arms and therefore invisible to their difference. **Zero genuine call-site defects were found in the residue** — every diagnostic examined was a deficit in the type judgment, so no call sites were edited, because 67 mechanical edits would have cemented three compiler deficits permanently. The per-mechanism split of that residue is deliberately NOT recorded here: it was published as 48/11/8, and the rule the 48 were attributed to was then found to admit nothing in this corpus, so the attribution was retracted before it was cited. Trigger for the count to be restated: the residue re-measured with its `why` column. **The counterexample that retracted it is worth carrying on its own, because it will bite anyone who reaches for a name-keyed alias relation:** `type Float = Float64` is declared in BOTH `dag/std/float.dag:18` and `src/v2/std/float.dag:33`, spelling the target identically — but `dag/std/float.dag:16` has `type Float64 = Real64` (a transparent alias) while `src/v2/std/float.dag:30` has `Float64` as a **record**. So the two declarations agree on a *spelling* and disagree on a *type*, and a unanimity rule keyed on the target's NAME admits them as the same concept. Requiring the target itself to be census-unique closes it — and once closed, that rule admits nothing in this corpus, which is what falsified the attribution above. Found by still-carp-717 while building the rule, before it shipped. **The original trigger text, kept because the sequence it specifies was followed and the record should show what was attempted:** seam (1) — turn the exemption off for `v2.` behind a measured diagnostic count, triage, then delete the arm, the disposition the compiler-module arm received; the measured prerequisite is ALIAS TRANSPARENCY, because proud-ant-819's report-only shadow on the 03_ingest closure found 115 `WouldDiagnose` relations at 78 sites of which 115 reduce to a transparent `type A = B` (92 via `type Hash = Fnv1a64Structural`, 23 via the `Node` phase carriers), residue ZERO — so on that closure the exemption is currently suppressing false positives, not defects. Seam (2) — its own wall at record-literal field conformance; nothing to turn off, it was never on. **Closing seam (1) MUST NOT be read as closing the class**, which is the specific failure this correction exists to prevent: a class that looks like it has one closing condition gets closed when that condition fires. Two blind spots neither instrument covers, named rather than left to be rediscovered: production itself SKIPS an anonymous record literal standing as an ACTUAL at a direct call, so its argument type is never judged (521 relations, 2.7%, `Unadjudicated` in proud-ant-819's shadow — upstream of the guard, so invisible to a flip-off arm too); and a function storing into a field from its own differently-named parameter is this class at yet another site, which a callee-name-keyed census cannot see. **THAT FIRST BLIND SPOT IS NOT SEAM (2), AND THE TWO WILL BE MERGED BY ANY READER WHO DOES NOT SEE THIS SENTENCE** (caught by proud-ant-819, who put the mirror-image clause in their own row): both descriptions begin "a record literal" and name DIFFERENT POSITIONS. The blind spot is a record literal at an ARGUMENT position whose type goes unjudged at the direct-call seam — seam (1)'s territory, and a population of 521 relations. Seam (2) / gunbc#8865 is a record literal's FIELD whose value does not inhabit the field's declared type — a different seam with a different mechanism and no measured population. Reading them as one would make the 521 look like evidence for gunbc#8865, or gunbc#8865's receipt look like it bounds the 521. Neither is true. **A CLAIM ABOUT THIS ROW'S EVIDENCE WAS MADE HERE AND IS RETRACTED, MEASURED WRONG (2026-08-22, the §11 item 28 lane, retracting itself).** The retracted claim was that these probes sit in the declined `ReadsLiveTree` carrier and therefore never execute, so the expected-red enrolment could only be `not_evaluated`. **It is false, and the measurement that refutes it is the run that was supposed to confirm it:** run `32586093086` reports `[expected-red-roster-join] roster=207 still_red=207 now_passes=0 not_evaluated=0` with `known_red_held=207`. The v2-module red EXECUTES and is held still-red exactly as its row intends. The error was reading an IMPORT as a location: `guarantee_probe_corpus_witness` imports the three probe ids for a roster assertion, and I took that for where the probes run; they run in `test.claim.direct_call_argument_type_witness`, a separate file. An import is evidence of visibility, never authority for where a name lives. **What survives is a different and sharper finding.** That file executes because it declares `SubstrateInputsOnly` while calling `compile_dag_diagnostic_census` — the same declaration `gunbc.compile_diagnostic_census`'s own live-tree note already adjudicated as a MIS-declaration when it found `transport_script_wall_compile_red_test` doing it (that census walks `build_module_path_index_from_witness_roots`, i.e. the live checkout). So the specimen population for that mis-declaration is now TWO, the second authored on 2026-08-22 after the first was adjudicated, and both are the only reason any census-compiling probe executes at all. Either these files' declaration is wrong or that authority's note is; they cannot both be right, and which one it is decides the size of §11 item 28's population. That is a question for the arm's owner, not a defect in this row's measurement, which stands. **SEAM (2) IS NOW CLOSED, AND CLOSING IT ENUMERATED TWO MORE — the count is FIVE measured, still not the total (gunbc#8876, 2026-08-22).** **OWNERSHIP, STATED PER SEAM BECAUSE THE CLASS NOW SPANS TWO LANES AND NEITHER CAN CLOSE IT ALONE:** seam (1) is the exemption-gated direct-call seam owned by the paragraph immediately preceding this one, whose next trigger is recorded there as DECLINED rather than pending; seams (2) through (5) belong to the field-inhabitance lane (snappy-tern-856). A lane that lands its last seam will be tempted to close this row. NEITHER MAY: 'my seams are done' is not 'the class is closed', and the row closes only when every seam does — including any seam not yet enumerated. The record-literal FIELD seam is walled: `v1.compiler.infer` `coproduct_payload_where_parent_required` refuses a value whose type is one of the declared coproduct's own variant payload types, consulting `transparent_alias_identity_agrees` over the `SymbolIndex` so an alias-mediated producer is caught too. Rung at that seam: **structurally guaranteed** — no `Accepted` program contains the state there. NOT structurally impossible, because the bad literal is still writable and the compiler refuses it; and NOT the class, which is why the two rows below exist. Evidence, enrolled permanently per §4b(4): `test.claim.coproduct_payload_soundness_witness_test` — the direct RED, the alias-mediated RED, and the positive control that stops a refuse-everything compiler from satisfying either. Turning the wall on WAS the census: EIGHT live sites, none previously known, all repaired in the same change — `ContentHash` from `Fnv1a64Structural` at `materialization_provider_witness_test`, `heal_revalidation_witness_test`, `materialize_witness_test`, `v2.std.materialize` and `v2.workflow.operand_flow`; `LexRules` from `LexRuleSet` at two `src/v2/test/claim/manual` fold tests. **SEAM (3), UNWALLED AND DECLARED, owner the field-inhabitance lane: the module-scope `data` initializer.** `data X: ContentHash = content_hash(...)` stores the payload into a `ContentHash`-declared row and is NOT refused, because a `data` initializer is not a record-literal field. Rung: **below floor**, exactly as seam (2) was. Unguarded: every module-scope `data` row in the corpus. Trigger: the same conformance judgment applied at the data-initializer seam, which needs no new relation — the declared type and the initializer's inferred type are both already in hand there. **SEAM (4), UNWALLED AND DECLARED, owner the field-inhabitance lane, AND IT IS RANKED FIRST OF THE TWO: the list element.** `v2.workflow.locality_affinity` built consumer identities as `list_add_distinct_hash(xs: cs, v: content_hash(n: e.dependent))` — a raw payload into a `List`. Rung: **below floor**, and it does not fail loudly. Measured: repairing the comparands while that producer stayed raw turned FOUR `locality_affinity` witnesses to `Bool(false)` with NOTHING refused at compile time — a wrong answer discovered later, not a diagnostic. That is what makes it rank above seam (3), and the ranking is fixed by a RULE rather than by judgment (operator ratification, 2026-08-22): seam (3) admits a wrong value a correctly-built peer can still catch by comparison — harmful, detectable, recoverable — while seam (4) admits a wrong value AND DISABLES THE COMPARISON THAT WOULD HAVE CAUGHT IT. That is a silent wrong answer, which DESIGN places OUTSIDE the guarantee ladder and forbids outright rather than ranking low, so the two are in different categories and no population argument reaches across the line: a larger set of loud failures does not outrank a smaller set of silent ones. The ranking is a priority order for collisions, NOT a serial queue — seam (3) needs no new relation and may land whenever it is ready. Unguarded: every list, map and collection element position whose element type is a coproduct. Trigger: element-position conformance against the container's declared element type. **SEAM (5), UNWALLED AND DECLARED, owner the field-inhabitance lane: the declared RETURN type.** `fn f(x: Node) -> ContentHash { content_hash(n: x) }` returns the payload where the parent coproduct is declared and is NOT refused. Rung: **below floor**. Measured 2026-08-22 on the gunbc#8876 merge commit, with a liveness control in the SAME compile that produced exactly one diagnostic (the record-literal RED), so the silence is a measurement and not an untested assumption. HOW IT WAS FOUND IS WORTH RECORDING, because it says something about the enumeration itself: it was found by a MIS-WRITTEN PROBE — the author intended an alias-mediated FIELD case and wrote a return position by mistake. Four of the five seams in this row were discovered by accident or by a downstream red rather than by anyone enumerating positions, which is the standing evidence for #8868's instruction to assume a further seam. Unguarded: every declared return type whose type is a coproduct. Trigger: `declared_type_conformance_diags` already runs at this seam and already holds both the declared and the inferred type, so the distance is a payload-membership arm on an existing judgment, not a new walk. **DO NOT READ SEAM (2)'s CLOSURE AS THE CLASS'S.** One seam of four measured is walled; a reader who sees only 'declared-field inhabitance wall landed' will conclude the class is closed, and the next lane would then build on a guarantee covering a quarter of it. Neither seam (3) nor seam (4) nor seam (5) is closed by gunbc#8876, which deliberately did not widen to chase them. **THIS ROW'S CEILING CELL SAYS THE DISTANCE TO R2 IS "AN IF-STATEMENT PLUS A TRIAGE". THAT IS MEASURED FALSE FOR THE PAYLOAD-WHERE-PARENT SHAPE, AND THE CORRECTION MATTERS BECAUSE IT IS THE SECOND NECESSARY-CONDITION-STATED-AS-SUFFICIENT TRIGGER THIS ONE ROW HAS CARRIED (snappy-tern-856, 2026-08-22).** The cell reasons that `direct_call_arg_mismatch_diags` exists, is written, and is simply not called, so flipping `module_skips_direct_call_arg_check` off closes seam (1). Flipping it off is NECESSARY. It is not SUFFICIENT, and the discriminating measurement is a module the exemption never applied to in the first place: in an ORDINARY NON-`v2.*` module, where the guard is false and the judgment demonstrably runs, `c4_takes(o: 5)` against `fn c4_takes(o: EOuter)` REFUSES (`expected 'Coproduct(EOuter)', got 'Primitive(Int)'`) while `c4_takes(o: e_inner())` — the coproduct's own payload type — is ACCEPTED in the same compile. The judgment is live at that seam and misses this shape, so deleting the arm leaves it accepted. **Read the two facts together or the row misleads:** the exemption really does switch the judgment off for every `v2.*` caller (that half is unchanged and still below floor), AND the judgment it switches off would not catch this shape anyway. A reader who acts only on the first will delete the arm, watch the diagnostics, and conclude the seam is closed. **THE DENOMINATOR THIS ROW HAS LACKED SINCE IT WAS WRITTEN NOW EXISTS, and it is what makes the sentence above checkable rather than another anecdote.** The row has said "assume a third seam until someone enumerates them" through two revisions while the count grew from two to five BY ACCIDENT — four of the five were found by a downstream red or by a mis-written probe, never by anyone enumerating positions, which samples the reviewer rather than the population. The positions are now enumerated FROM THE GRAMMAR: every call site of `parse_type_expr` in `v1.compiler.parse`, which is the finite set of places the language attaches a declared type. That is **14 sites**, and all five previously-known seams FALL OUT of it as rows rather than having been seeded into it — the falsifier the enumeration was required to pass. The list element seam falls out only because a container's element type is reached as a TYPE ARGUMENT rather than as a declaration of its own, which is why nobody had named it as a position before. **METHOD, because "not refused" is worthless without it.** Each position carries three arms: the payload-where-parent shape, a KERNEL mismatch (`Int` where the coproduct is declared), and an UNDEFINED NAME. The third is the reachability control: if it refuses, inference REACHES that position, so a passing kernel arm establishes that NO TYPE JUDGMENT RUNS there rather than that the position went unanalysed. All seven reachability controls refused. Dispositions, measured: **refuses** — record/variant NAMED field (`parse_field`), and only because gunbc#8876 walls it. **Judgment runs, misses the shape** — fn parameter at the direct-call seam. **Not refused, no judgment runs** — container type argument (list element), variant POSITIONAL payload, fn declared return, module-scope `data` initializer, annotated `let`. **Not refused** — `as` cast. **Not reachable from a source value** — type-alias RHS, `uses` resource type, service `exit` and `response` types (the last two are the reconstruction path's, not this row's). **Not refused, no judgment runs** (measured after the first pass, closing the census at 14 of 14) — the callable-type RETURN position (`cb: fn(Int) -> EOuter` given a lambda whose body yields the payload) and the callable-type PARAMETER position (`cb: fn(EOuter) -> Int` called with the payload); both reachability controls refused, so both positions are analysed. Three of these positions were previously unknown: variant positional payload, `as` cast, and annotated `let`. **AND THE ENUMERATION FOUND SOMETHING WIDER THAN THIS ROW'S CLASS, WHICH IS DELIBERATELY NOT CLAIMED HERE.** `data c6b: EOuter = 5` and `fn c5b() -> EOuter { 5 }` are both ACCEPTED, with the reachability control proving both positions are analysed. That is not payload-versus-parent; it is a plain kernel value where a declared coproduct is required, which is the ordinary-floor invariant DESIGN §4b names beside name resolution and exact-bijection binding. On the measured census that is **seven of fourteen grammar-admitted positions accepting a kernel value where a declared coproduct is required** — variant positional payload, fn declared return, module-scope `data` initializer, container type argument, annotated `let`, callable-type return, callable-type parameter — with the single refusing position owing its refusal to a PR that is held at the time of writing. (The count was first published as FIVE of fourteen, before the two callable-type positions were measured; it is corrected here rather than left standing, because an understated denominator on a floor breach is the same defect as an overstated rung. The `as` cast is deliberately not in the seven: it was never given a kernel arm, since a cast is an authored assertion and whether a kernel-to-coproduct cast should refuse is a different question this census did not ask.) This row's class is one INSTANCE of that breach rather than the breach itself, so the finding is routed for its own §4b row and its own owner rather than absorbed here — recording it inside this row would repeat the mistake this correction exists to fix, by making a wider unwalled invariant look like a seam of a narrower one **THAT WIDER BREACH NOW HAS ITS OWN OWNER AND FOUR OF ITS SEVEN POSITIONS ARE WALLED (2026-08-24, the declared-type-inhabitance lane).** Scope, stated first because the class and this row's class are neighbours that will be merged by anyone reading quickly: the subject is A PLAIN KERNEL VALUE (`Int`, `String`, `Bool`) where a declared record or coproduct is required — NOT a coproduct payload where its parent is required, which is this row's seam (2) and is separately walled. MEASURED BEFORE, on the pre-change binary, one fixture per position with an undefined-name reachability control beside it: all SEVEN positions compiled `0 diagnostics` and EMITTED 9 files (fn declared return, module-scope `data` annotation, annotated `let`, container element, variant positional payload, callable-type return, callable-type parameter); every reachability control refused (`function 'no_such_name_at_all' not found in scope`), so the silence measured an absent judgment rather than an unanalysed position; and the record-literal NAMED field refused (`expected 'Coproduct(KOuter)', got 'Primitive(Int)'`), which is what identified the relation that already existed. MEASURED AFTER, same fixtures, same flags: the declared return, the `data` annotation, the annotated `let` and the container element REFUSE with a located `TypeMismatch` (`expected 'Coproduct(KOuter)', got 'Primitive(Int)'`; the element position as `expected 'Container(List,Coproduct(KOuter))', got 'Container(List,Primitive(Int))'`); the conforming spelling at all four positions still compiles `0 diagnostics`; the named field refuses identically, which is the control proving the reused relation has not forked; and `fn f() -> KInner { 5 }` — a RECORD rather than a coproduct — now refuses too (`expected 'Product(KInner)', got 'Primitive(Int)'`), so the wall is the declared-type class and not a coproduct special case. NO SECOND RELATION WAS MINTED (DESIGN §3): `kernel_value_declared_type_mismatch` was already the corpus authority for this judgment and was consulted at exactly one of the fourteen positions; what landed is its peeling prologue lifted into `declared_type_conformance_diags`, so the fn return, the early `return`, the `data` annotation and the newly-wired annotated `let` all widen with that gate rather than beside it. FALSE-POSITIVE CENSUS, AND ITS FIRST STATEMENT HERE WAS WRONG ABOUT ITS OWN DENOMINATOR — corrected in place because the error is the instructive part. The regen corpus compile (`dag` + `src/v2`, `first_generation_equal=true`, `planned=133 executed=133`) reports zero hard diagnostics under the wall, and this row first read that as 'no live site was repaired'. The required floor then refused: its prepared subject resolves **3872 modules**, including `src/v2/test/**`, which the regen closure does not reach, and the wall found **six live sites in one file** — `src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test` declared six octet fixtures and one function parameter as `List` while holding integer literals (`[0, 255, 255, 255, 255]`) and forwarding them to `v2.compiler.emit_host` `emit_host_octets_byte_string`, whose declared parameter is `List` and which builds each `Byte` itself. `Byte` is a record over `List` and no `Int -> Byte` cast rule exists, so every one of those declarations was a lie that no consumer contradicted — the latent shape this row's originating incident already names, at the element position the wall now judges. Repaired to `List` (the entry then compiles with 0 blocking diagnostics), which makes TURNING THE WALL ON the census, exactly as gunbc#8876's field seam was. THE GENERAL LESSON, worth more than the six sites: a green whole-corpus compile is scoped to ITS OWN closure, and quoting it as 'the corpus' silently excludes whatever that closure omits; the floor's prepared subject is the wider denominator and disagreeing with it is how the gap was found. Zero further live sites were found beyond that file, which is a fact about this class's live population and not evidence that the other three positions are empty. RUNG: the four walled positions are **structurally guaranteed** (the bad value is still writable and the compiler refuses it); the class as a whole stays **below floor**, because three positions still admit it. STILL OPEN, each with its trigger, and NONE of them closed by this change: (a) the VARIANT POSITIONAL PAYLOAD — `KHeld(5)` routes through `infer_variant_constructor_call` into `infer_record_lit` under the synthetic field name `0`, and the declared type of that positional slot does not reach the field-conformance seam the NAMED field reaches; trigger is that slot resolving to its declared payload type there. (b) and (c) the CALLABLE-TYPE RETURN and PARAMETER — a lambda's body against `fn(Int) -> KOuter`, and an actual against `fn(KOuter) -> Int`; both reachability controls refused, so both positions are analysed and neither carries the callable's own declared component types into a conformance judgment; trigger is threading each callable boundary's declared parameter and return through the same relation, which is also what `explicit_return_conformance_note` names as its lambda narrowing. A NESTED container (`List>`) is likewise not judged: the element peel is ONE level, which is the depth measured, and deeper is unmeasured rather than covered. Enrolled evidence, permanent per §4b(4): `test.claim.declared_type_kernel_inhabitance_witness_test` — four discriminating REDs, the already-closed named-field RED as the no-fork control, and one positive control carrying the conforming spelling at all four closed positions so a refuse-everything compiler cannot satisfy them | +| A value that does not inhabit its declared type is accepted — **seam-split, enumeration UNFINISHED** (was filed as "Direct-call argument TYPE conformance, v2 corpus"; renamed 2026-08-22, see the trigger cell) | **Below floor — the judgment never runs.** Not a hole a bad value slipped through: `v1.compiler.04_infer` gates `arg_compat_diags` on `module_skips_direct_call_arg_check(module_name: scope.module_name)`, which returns true for every module whose name begins with `v2.`. The key is the CALLER's module, so the entire active v2 corpus — compiler stages, extdeps, std, witnesses — has the direct-call argument-type judgment switched off. Measured consequence, 2026-08-22: `v2.extdeps.languages.dag` `dag_int_literal_node_from_lexeme` / `dag_int_literal_node_from_magnitude` declared `occurrence_id: OccurrenceId` since gunbc#6558 while storing that parameter straight into `Node.occurrence_id`, declared `NodeOccurrenceId`. For two months 15 call sites passed `SyntheticOccurrence` (a NodeOccurrenceId, contradicting the declaration) and nothing complained; gunbc#8833 made one call site OBEY the declaration and nothing complained about that either. The error surfaced only as an interpreter `non-exhaustive pattern match on: OccurrenceId { value: 79 }` across 16 witnesses, reddening main. **The inversion worth naming: a declaration that lies is inert while every caller contradicts it in the same direction, and detonates on the first caller who takes it at its word.** So the at-risk population is not "callers who got it wrong" but callers who might get it right — a genuinely counterintuitive census. Note this is the TYPE judgment only; the SHAPE judgment (`direct_call_shape_diags`, labels/arity) is exemption-free and does fire | R2 (a declared parameter type is a decidable conformance check the seam already computes — `direct_call_arg_mismatch_diags` exists, is written, and is simply not called, so the distance to the next rung is an if-statement plus a triage, not an implementation) | **THIS ROW IS A CORRECTION TO DESIGN §4b, NOT A NEW OBSERVATION BESIDE IT — read them together or the first will look like it already settled this.** DESIGN §4b names this exact symbol and reports that it "was found (code read, not execution) to be scoped entirely to the direct-call argument-type judgment and does not reach `sole_constructor`'s construction check at either call site — a positive finding that retires this axis, not an absence of any exemption anywhere." That finding is correct and is not disputed here. The question it asked was whether the exemption LEAKS into `sole_constructor`; the question it never asked is what the exemption COSTS inside the judgment it is scoped to. "Scoped entirely to the direct-call argument-type judgment" reads as reassuring only until that judgment is measured, and it is the argument-type check for the entire active v2 corpus. **Confinement was measured and then treated as safety, and the axis that got retired was not the one that mattered.** Two facts about why the seam nonetheless reads as covered: the SHAPE judgment (`direct_call_shape_diags` — labels, arity, duplicate binding) is exemption-free and DOES fire over every module including the compiler's own sources, so half-live is more deceptive than dead — every casual check finds something working. And the arm is NOT unreasoned: `direct_call_shape_wall_note` states the TYPE judgment's false-positive classes are representation gaps (brand aliases, optionality's two forms, anonymous literals, expansion depth — the conformance wall's four measured classes), which is a real stated reason and is why this row asks for a measurement rather than a deletion. What is unmeasured is whether those classes still fire in v2 today and at what rate. The neighbouring compiler-module arm of this same exemption was deleted in place after being found never to have been in force; the `v2.` arm was left standing at that moment without separate justification of its own | This incident, measured end to end: CI run 32542017600 (main, 67437fcbe9) 16 FAIL with the raw-`OccurrenceId` match error; caller census of both functions read at call grain (17 sites: 15 `SyntheticOccurrence`, 1 `node.occurrence_id`, 1 internal pass-through, 1 raw `minted.id`); exemption mechanism read at `v1.compiler.04_infer` `module_skips_direct_call_arg_check` and its single call site gating `arg_compat_diags` on `scope.module_name`. **NOT ENROLLED**: no probe pair asserts this exemption's reach, so nothing reds if it changes | **THE TRIGGER THIS ROW SHIPPED WITH WAS INCOMPLETE AND IS CORRECTED HERE (2026-08-22, swift-badger-524 retracting their own ruling).** As merged in gunbc#8854 this cell named ONE closing condition — delete the `v2.` exemption — which is a NECESSARY condition presented as a sufficient one. The class is not "direct-call argument type conformance"; it is **a value that does not inhabit its declared type is accepted**, and it has at least TWO seams: **(1) direct-call arguments** — gated off for `v2.*` by `module_skips_direct_call_arg_check`, the mechanism this row measures; **(2) record-literal fields** — gated by NOTHING, below floor in ORDINARY NON-v2 MODULES, receipt gunbc#8865 (gentle-eagle-360). Its minimal pair, no compiler internals involved: `CppHolder { subject: CppWrapped { inner: cpp_inner() } }` accepted and correct, against `CppHolder { subject: cpp_inner() }` — a coproduct PAYLOAD inhabiting a field declared as its parent COPRODUCT — ACCEPTED BY TYPING and dying at runtime as `PatternMatchFailure`. A record literal is not the direct-call seam, so deleting the exemption would not close it. **SEAM (2) NOW HAS A LIVE PRODUCTION SPECIMEN, WHICH RANKS IT DIFFERENTLY FROM A SYNTHETIC PAIR** (gentle-eagle-360, 2026-08-22, found while checking for a second content-identity authority before building on one): `v2.std.materialize` declares `MaterializedNode.hash` as `ContentHash` — the subject-generic union — and `materialize_fold_step` stores `content_hash(n)` into it, which returns `Fnv1a64Structural`, the PAYLOAD carried inside the union's `Fnv1a64` arm. Receipt, by execution against the module as it stands on main: taking the value materialize ACTUALLY STORED and asking the union's own family authority `content_hash_family` about it yields `PatternMatchFailure { value: "Fnv1a64Structural { digest: 7ac77ab0e29c6bd8 }" }`; the probe's fallback was a correctly wrapped `Fnv1a64(...)`, so an empty result or a well-formed value would have PASSED and only a stored value can produce that red. **The defect is LATENT and that is the instructive part**: peer lookup compares `e.hash == h`, raw payload against raw payload, which agrees with itself — so every current path is green and the error surfaces only when a materialize hash is routed through the union's own machinery (`content_hash_family`, or `compare_content_hash`, which exists precisely to refuse cross-family collapse). That is the same shape as this row's own originating incident: **a declaration that lies is inert while every consumer contradicts it in the same direction, and detonates on the first consumer that takes it at its word** — here the first cross-family artifact to reach the carrier. Disposition ruled ARM A, wrap the construction (`MaterializedNode { hash: Fnv1a64(h), ... }`), NOT narrow the declaration: narrowing would sever `MaterializedNode.hash` from `RealizationPlan.target`, and §2's Realization spans resolve-cost, sccache and OS provisioning on ONE content hash, so a structural-only key could never name a realization of a fetched artifact or a provisioned image (swift-badger-524 ruling, 2026-08-22; handed to silent-bear-842 with the receipt, unfixed here because it is that lane's module). **THE SEAM ITSELF IS THE FINDING, not this one site**: gunbc#7480 corrected the design document for asserting the wrong type at exactly this `Hash`/`ContentHash` boundary, and a production module now carries the mirror-image error — a boundary documentation has to keep re-explaining is a boundary that wants construction. ****THAT HAND-OFF IS SUPERSEDED AND THE SPECIMEN IS REPAIRED — corrected in place rather than left standing, because the sentence above says a live production defect is UNFIXED and awaiting another lane, which is the present-tense claim a reader would plan against (gunbc#8876, 2026-08-22).** The wrap landed in the wall's own change by operator ruling: a wall and the repair it forces must land together, since with the wall on and the wrap absent main is red, so only one PR can contain both. `v2.std.materialize` `materialize_fold_step` and `distinct_hashes` now build `Fnv1a64(content_hash(n))`, and the same construction was repaired at four further sites the wall refused for the identical reason — `v2.workflow.operand_flow`, `materialize_witness_test`, `materialization_provider_witness_test` and `heal_revalidation_witness_test`. The receipt above stays as the historical demonstration that the defect was real and reachable; it is no longer a description of the tree. THE ENUMERATION IS UNFINISHED: two is what has been measured, not the count.** Assume a third seam exists until someone enumerates them; note that this row's own originating incident (#8854) reached its victim through a record literal one hop downstream of the direct call, so the two seams are not even cleanly separable at a site. **SEAM (1) WAS EXECUTED TO A MEASURED, BLOCKED STOP ON 2026-08-22 — the arm is NOT deleted, and this paragraph is the §4b row for that state rather than a plan.** Rung: **below floor, unchanged** — the judgment still does not run for any `v2.*` caller. Ceiling: **R2** (a declared parameter type is a decidable conformance check the seam already computes). Next trigger, stated as §4b(2) requires and with its disposition: *a formal parameter declared as an applied generic carries its applied form through resolution rather than reaching the comparison seam as the bare constructor* — **DECLINED at the owning layer on 2026-08-22**, on the ground that a bounded compiler-floor packet whose completion condition has moved should close and hand its residue forward rather than extend into a type-system project. A declined trigger is a legitimate §4b state; **a blocked class with no row is how this exemption survived years in the first place**, which is the reason this row exists at all. Enrolled evidence, so the class stays countable while blocked: `direct_call_arg_type_v2_module_red_probe` (the discriminating RED, rostered in `v2.workflow.floor_expected_red` — it cannot pass while the arm stands and PASSES on a tree with the arm deleted, so it is a satisfiable assertion held open by a named cause), plus two controls that pass on main today (`direct_call_arg_type_ordinary_module_red_probe`, the paired nonzero the exemption never covered; and `direct_call_arg_type_v2_green_control_probe`). **What was measured before the stop, and how to read it:** deleting the arm produces **285+k** blocking diagnostics and **67+k** with gunbc#8873 merged, for some k ≥ 1 unmeasured — these are ROSTER-RESOLVED counts, not corpus counts, and `src/v2/extdeps/formatters/lean4_format.dag:184` is the proof: a live site, structurally identical to eight that refused, contributing zero to *both* arms and therefore invisible to their difference. **Zero genuine call-site defects were found in the residue** — every diagnostic examined was a deficit in the type judgment, so no call sites were edited, because 67 mechanical edits would have cemented three compiler deficits permanently. The per-mechanism split of that residue is deliberately NOT recorded here: it was published as 48/11/8, and the rule the 48 were attributed to was then found to admit nothing in this corpus, so the attribution was retracted before it was cited. Trigger for the count to be restated: the residue re-measured with its `why` column. **The counterexample that retracted it is worth carrying on its own, because it will bite anyone who reaches for a name-keyed alias relation:** `type Float = Float64` is declared in BOTH `dag/std/float.dag:18` and `src/v2/std/float.dag:33`, spelling the target identically — but `dag/std/float.dag:16` has `type Float64 = Real64` (a transparent alias) while `src/v2/std/float.dag:30` has `Float64` as a **record**. So the two declarations agree on a *spelling* and disagree on a *type*, and a unanimity rule keyed on the target's NAME admits them as the same concept. Requiring the target itself to be census-unique closes it — and once closed, that rule admits nothing in this corpus, which is what falsified the attribution above. Found by still-carp-717 while building the rule, before it shipped. **The original trigger text, kept because the sequence it specifies was followed and the record should show what was attempted:** seam (1) — turn the exemption off for `v2.` behind a measured diagnostic count, triage, then delete the arm, the disposition the compiler-module arm received; the measured prerequisite is ALIAS TRANSPARENCY, because proud-ant-819's report-only shadow on the 03_ingest closure found 115 `WouldDiagnose` relations at 78 sites of which 115 reduce to a transparent `type A = B` (92 via `type Hash = Fnv1a64Structural`, 23 via the `Node` phase carriers), residue ZERO — so on that closure the exemption is currently suppressing false positives, not defects. Seam (2) — its own wall at record-literal field conformance; nothing to turn off, it was never on. **Closing seam (1) MUST NOT be read as closing the class**, which is the specific failure this correction exists to prevent: a class that looks like it has one closing condition gets closed when that condition fires. Two blind spots neither instrument covers, named rather than left to be rediscovered: production itself SKIPS an anonymous record literal standing as an ACTUAL at a direct call, so its argument type is never judged (521 relations, 2.7%, `Unadjudicated` in proud-ant-819's shadow — upstream of the guard, so invisible to a flip-off arm too); and a function storing into a field from its own differently-named parameter is this class at yet another site, which a callee-name-keyed census cannot see. **THAT FIRST BLIND SPOT IS NOT SEAM (2), AND THE TWO WILL BE MERGED BY ANY READER WHO DOES NOT SEE THIS SENTENCE** (caught by proud-ant-819, who put the mirror-image clause in their own row): both descriptions begin "a record literal" and name DIFFERENT POSITIONS. The blind spot is a record literal at an ARGUMENT position whose type goes unjudged at the direct-call seam — seam (1)'s territory, and a population of 521 relations. Seam (2) / gunbc#8865 is a record literal's FIELD whose value does not inhabit the field's declared type — a different seam with a different mechanism and no measured population. Reading them as one would make the 521 look like evidence for gunbc#8865, or gunbc#8865's receipt look like it bounds the 521. Neither is true. **A CLAIM ABOUT THIS ROW'S EVIDENCE WAS MADE HERE AND IS RETRACTED, MEASURED WRONG (2026-08-22, the §11 item 28 lane, retracting itself).** The retracted claim was that these probes sit in the declined `ReadsLiveTree` carrier and therefore never execute, so the expected-red enrolment could only be `not_evaluated`. **It is false, and the measurement that refutes it is the run that was supposed to confirm it:** run `32586093086` reports `[expected-red-roster-join] roster=207 still_red=207 now_passes=0 not_evaluated=0` with `known_red_held=207`. The v2-module red EXECUTES and is held still-red exactly as its row intends. The error was reading an IMPORT as a location: `guarantee_probe_corpus_witness` imports the three probe ids for a roster assertion, and I took that for where the probes run; they run in `test.claim.direct_call_argument_type_witness`, a separate file. An import is evidence of visibility, never authority for where a name lives. **What survives is a different and sharper finding.** That file executes because it declares `SubstrateInputsOnly` while calling `compile_dag_diagnostic_census` — the same declaration `gunbc.compile_diagnostic_census`'s own live-tree note already adjudicated as a MIS-declaration when it found `transport_script_wall_compile_red_test` doing it (that census walks `build_module_path_index_from_witness_roots`, i.e. the live checkout). So the specimen population for that mis-declaration is now TWO, the second authored on 2026-08-22 after the first was adjudicated, and both are the only reason any census-compiling probe executes at all. Either these files' declaration is wrong or that authority's note is; they cannot both be right, and which one it is decides the size of §11 item 28's population. That is a question for the arm's owner, not a defect in this row's measurement, which stands. **SEAM (2) IS NOW CLOSED, AND CLOSING IT ENUMERATED TWO MORE — the count is FIVE measured, still not the total (gunbc#8876, 2026-08-22).** **OWNERSHIP, STATED PER SEAM BECAUSE THE CLASS NOW SPANS TWO LANES AND NEITHER CAN CLOSE IT ALONE:** seam (1) is the exemption-gated direct-call seam owned by the paragraph immediately preceding this one, whose next trigger is recorded there as DECLINED rather than pending; seams (2) through (5) belong to the field-inhabitance lane (snappy-tern-856). A lane that lands its last seam will be tempted to close this row. NEITHER MAY: 'my seams are done' is not 'the class is closed', and the row closes only when every seam does — including any seam not yet enumerated. The record-literal FIELD seam is walled: `v1.compiler.infer` `coproduct_payload_where_parent_required` refuses a value whose type is one of the declared coproduct's own variant payload types, consulting `transparent_alias_identity_agrees` over the `SymbolIndex` so an alias-mediated producer is caught too. Rung at that seam: **structurally guaranteed** — no `Accepted` program contains the state there. NOT structurally impossible, because the bad literal is still writable and the compiler refuses it; and NOT the class, which is why the two rows below exist. Evidence, enrolled permanently per §4b(4): `test.claim.coproduct_payload_soundness_witness_test` — the direct RED, the alias-mediated RED, and the positive control that stops a refuse-everything compiler from satisfying either. Turning the wall on WAS the census: EIGHT live sites, none previously known, all repaired in the same change — `ContentHash` from `Fnv1a64Structural` at `materialization_provider_witness_test`, `heal_revalidation_witness_test`, `materialize_witness_test`, `v2.std.materialize` and `v2.workflow.operand_flow`; `LexRules` from `LexRuleSet` at two `src/v2/test/claim/manual` fold tests. **SEAM (3), UNWALLED AND DECLARED, owner the field-inhabitance lane: the module-scope `data` initializer.** `data X: ContentHash = content_hash(...)` stores the payload into a `ContentHash`-declared row and is NOT refused, because a `data` initializer is not a record-literal field. Rung: **below floor**, exactly as seam (2) was. Unguarded: every module-scope `data` row in the corpus. Trigger: the same conformance judgment applied at the data-initializer seam, which needs no new relation — the declared type and the initializer's inferred type are both already in hand there. **SEAM (4), UNWALLED AND DECLARED, owner the field-inhabitance lane, AND IT IS RANKED FIRST OF THE TWO: the list element.** `v2.workflow.locality_affinity` built consumer identities as `list_add_distinct_hash(xs: cs, v: content_hash(n: e.dependent))` — a raw payload into a `List`. Rung: **below floor**, and it does not fail loudly. Measured: repairing the comparands while that producer stayed raw turned FOUR `locality_affinity` witnesses to `Bool(false)` with NOTHING refused at compile time — a wrong answer discovered later, not a diagnostic. That is what makes it rank above seam (3), and the ranking is fixed by a RULE rather than by judgment (operator ratification, 2026-08-22): seam (3) admits a wrong value a correctly-built peer can still catch by comparison — harmful, detectable, recoverable — while seam (4) admits a wrong value AND DISABLES THE COMPARISON THAT WOULD HAVE CAUGHT IT. That is a silent wrong answer, which DESIGN places OUTSIDE the guarantee ladder and forbids outright rather than ranking low, so the two are in different categories and no population argument reaches across the line: a larger set of loud failures does not outrank a smaller set of silent ones. The ranking is a priority order for collisions, NOT a serial queue — seam (3) needs no new relation and may land whenever it is ready. Unguarded: every list, map and collection element position whose element type is a coproduct. Trigger: element-position conformance against the container's declared element type. **SEAM (5), UNWALLED AND DECLARED, owner the field-inhabitance lane: the declared RETURN type.** `fn f(x: Node) -> ContentHash { content_hash(n: x) }` returns the payload where the parent coproduct is declared and is NOT refused. Rung: **below floor**. Measured 2026-08-22 on the gunbc#8876 merge commit, with a liveness control in the SAME compile that produced exactly one diagnostic (the record-literal RED), so the silence is a measurement and not an untested assumption. HOW IT WAS FOUND IS WORTH RECORDING, because it says something about the enumeration itself: it was found by a MIS-WRITTEN PROBE — the author intended an alias-mediated FIELD case and wrote a return position by mistake. Four of the five seams in this row were discovered by accident or by a downstream red rather than by anyone enumerating positions, which is the standing evidence for #8868's instruction to assume a further seam. Unguarded: every declared return type whose type is a coproduct. Trigger: `declared_type_conformance_diags` already runs at this seam and already holds both the declared and the inferred type, so the distance is a payload-membership arm on an existing judgment, not a new walk. **DO NOT READ SEAM (2)'s CLOSURE AS THE CLASS'S.** One seam of four measured is walled; a reader who sees only 'declared-field inhabitance wall landed' will conclude the class is closed, and the next lane would then build on a guarantee covering a quarter of it. Neither seam (3) nor seam (4) nor seam (5) is closed by gunbc#8876, which deliberately did not widen to chase them. **THIS ROW'S CEILING CELL SAYS THE DISTANCE TO R2 IS "AN IF-STATEMENT PLUS A TRIAGE". THAT IS MEASURED FALSE FOR THE PAYLOAD-WHERE-PARENT SHAPE, AND THE CORRECTION MATTERS BECAUSE IT IS THE SECOND NECESSARY-CONDITION-STATED-AS-SUFFICIENT TRIGGER THIS ONE ROW HAS CARRIED (snappy-tern-856, 2026-08-22).** The cell reasons that `direct_call_arg_mismatch_diags` exists, is written, and is simply not called, so flipping `module_skips_direct_call_arg_check` off closes seam (1). Flipping it off is NECESSARY. It is not SUFFICIENT, and the discriminating measurement is a module the exemption never applied to in the first place: in an ORDINARY NON-`v2.*` module, where the guard is false and the judgment demonstrably runs, `c4_takes(o: 5)` against `fn c4_takes(o: EOuter)` REFUSES (`expected 'Coproduct(EOuter)', got 'Primitive(Int)'`) while `c4_takes(o: e_inner())` — the coproduct's own payload type — is ACCEPTED in the same compile. The judgment is live at that seam and misses this shape, so deleting the arm leaves it accepted. **Read the two facts together or the row misleads:** the exemption really does switch the judgment off for every `v2.*` caller (that half is unchanged and still below floor), AND the judgment it switches off would not catch this shape anyway. A reader who acts only on the first will delete the arm, watch the diagnostics, and conclude the seam is closed. **THE DENOMINATOR THIS ROW HAS LACKED SINCE IT WAS WRITTEN NOW EXISTS, and it is what makes the sentence above checkable rather than another anecdote.** The row has said "assume a third seam until someone enumerates them" through two revisions while the count grew from two to five BY ACCIDENT — four of the five were found by a downstream red or by a mis-written probe, never by anyone enumerating positions, which samples the reviewer rather than the population. The positions are now enumerated FROM THE GRAMMAR: every call site of `parse_type_expr` in `v1.compiler.parse`, which is the finite set of places the language attaches a declared type. That is **14 sites**, and all five previously-known seams FALL OUT of it as rows rather than having been seeded into it — the falsifier the enumeration was required to pass. The list element seam falls out only because a container's element type is reached as a TYPE ARGUMENT rather than as a declaration of its own, which is why nobody had named it as a position before. **METHOD, because "not refused" is worthless without it.** Each position carries three arms: the payload-where-parent shape, a KERNEL mismatch (`Int` where the coproduct is declared), and an UNDEFINED NAME. The third is the reachability control: if it refuses, inference REACHES that position, so a passing kernel arm establishes that NO TYPE JUDGMENT RUNS there rather than that the position went unanalysed. All seven reachability controls refused. Dispositions, measured: **refuses** — record/variant NAMED field (`parse_field`), and only because gunbc#8876 walls it. **Judgment runs, misses the shape** — fn parameter at the direct-call seam. **Not refused, no judgment runs** — container type argument (list element), variant POSITIONAL payload, fn declared return, module-scope `data` initializer, annotated `let`. **Not refused** — `as` cast. **Not reachable from a source value** — type-alias RHS, `uses` resource type, service `exit` and `response` types (the last two are the reconstruction path's, not this row's). **Not refused, no judgment runs** (measured after the first pass, closing the census at 14 of 14) — the callable-type RETURN position (`cb: fn(Int) -> EOuter` given a lambda whose body yields the payload) and the callable-type PARAMETER position (`cb: fn(EOuter) -> Int` called with the payload); both reachability controls refused, so both positions are analysed. Three of these positions were previously unknown: variant positional payload, `as` cast, and annotated `let`. **AND THE ENUMERATION FOUND SOMETHING WIDER THAN THIS ROW'S CLASS, WHICH IS DELIBERATELY NOT CLAIMED HERE.** `data c6b: EOuter = 5` and `fn c5b() -> EOuter { 5 }` are both ACCEPTED, with the reachability control proving both positions are analysed. That is not payload-versus-parent; it is a plain kernel value where a declared coproduct is required, which is the ordinary-floor invariant DESIGN §4b names beside name resolution and exact-bijection binding. On the measured census that is **seven of fourteen grammar-admitted positions accepting a kernel value where a declared coproduct is required** — variant positional payload, fn declared return, module-scope `data` initializer, container type argument, annotated `let`, callable-type return, callable-type parameter — with the single refusing position owing its refusal to a PR that is held at the time of writing. (The count was first published as FIVE of fourteen, before the two callable-type positions were measured; it is corrected here rather than left standing, because an understated denominator on a floor breach is the same defect as an overstated rung. The `as` cast is deliberately not in the seven: it was never given a kernel arm, since a cast is an authored assertion and whether a kernel-to-coproduct cast should refuse is a different question this census did not ask.) This row's class is one INSTANCE of that breach rather than the breach itself, so the finding is routed for its own §4b row and its own owner rather than absorbed here — recording it inside this row would repeat the mistake this correction exists to fix, by making a wider unwalled invariant look like a seam of a narrower one **THAT WIDER BREACH NOW HAS ITS OWN OWNER AND FOUR OF ITS SEVEN POSITIONS ARE WALLED (2026-08-24, the declared-type-inhabitance lane).** Scope, stated first because the class and this row's class are neighbours that will be merged by anyone reading quickly: the subject is A PLAIN KERNEL VALUE (`Int`, `String`, `Bool`) where a declared record or coproduct is required — NOT a coproduct payload where its parent is required, which is this row's seam (2) and is separately walled. MEASURED BEFORE, on the pre-change binary, one fixture per position with an undefined-name reachability control beside it: all SEVEN positions compiled `0 diagnostics` and EMITTED 9 files (fn declared return, module-scope `data` annotation, annotated `let`, container element, variant positional payload, callable-type return, callable-type parameter); every reachability control refused (`function 'no_such_name_at_all' not found in scope`), so the silence measured an absent judgment rather than an unanalysed position; and the record-literal NAMED field refused (`expected 'Coproduct(KOuter)', got 'Primitive(Int)'`), which is what identified the relation that already existed. MEASURED AFTER, same fixtures, same flags: the declared return, the `data` annotation, the annotated `let` and the container element REFUSE with a located `TypeMismatch` (`expected 'Coproduct(KOuter)', got 'Primitive(Int)'`; the element position as `expected 'Container(List,Coproduct(KOuter))', got 'Container(List,Primitive(Int))'`); the conforming spelling at all four positions still compiles `0 diagnostics`; the named field refuses identically, which is the control proving the reused relation has not forked; and `fn f() -> KInner { 5 }` — a RECORD rather than a coproduct — now refuses too (`expected 'Product(KInner)', got 'Primitive(Int)'`), so the wall is the declared-type class and not a coproduct special case. NO SECOND RELATION WAS MINTED (DESIGN §3): `kernel_value_declared_type_mismatch` was already the corpus authority for this judgment and was consulted at exactly one of the fourteen positions; what landed is its peeling prologue lifted into `declared_type_conformance_diags`, so the fn return, the early `return`, the `data` annotation and the newly-wired annotated `let` all widen with that gate rather than beside it. FALSE-POSITIVE CENSUS, AND ITS FIRST STATEMENT HERE WAS WRONG ABOUT ITS OWN DENOMINATOR — corrected in place because the error is the instructive part. The regen corpus compile (`dag` + `src/v2`, `first_generation_equal=true`, `planned=133 executed=133`) reports zero hard diagnostics under the wall, and this row first read that as 'no live site was repaired'. The required floor then refused: its prepared subject resolves **3872 modules**, including `src/v2/test/**`, which the regen closure does not reach, and the wall found **six live sites in one file** — `src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test` declared six octet fixtures and one function parameter as `List` while holding integer literals (`[0, 255, 255, 255, 255]`) and forwarding them to `v2.compiler.emit_host` `emit_host_octets_byte_string`, whose declared parameter is `List` and which builds each `Byte` itself. `Byte` is a record over `List` and no `Int -> Byte` cast rule exists, so every one of those declarations was a lie that no consumer contradicted — the latent shape this row's originating incident already names, at the element position the wall now judges. Repaired to `List` (the entry then compiles with 0 blocking diagnostics), which makes TURNING THE WALL ON the census, exactly as gunbc#8876's field seam was. THE GENERAL LESSON, worth more than the six sites: a green whole-corpus compile is scoped to ITS OWN closure, and quoting it as 'the corpus' silently excludes whatever that closure omits; the floor's prepared subject is the wider denominator and disagreeing with it is how the gap was found. Zero further live sites were found beyond that file, which is a fact about this class's live population and not evidence that the other three positions are empty. RUNG: the four walled positions are **structurally guaranteed** (the bad value is still writable and the compiler refuses it); the class as a whole stays **below floor**, because three positions still admit it. STILL OPEN, each with its trigger, and NONE of them closed by this change: (a) the VARIANT POSITIONAL PAYLOAD — `KHeld(5)` routes through `infer_variant_constructor_call` into `infer_record_lit` under the synthetic field name `0`, and the declared type of that positional slot does not reach the field-conformance seam the NAMED field reaches; trigger is that slot resolving to its declared payload type there. (b) and (c) the CALLABLE-TYPE RETURN and PARAMETER — a lambda's body against `fn(Int) -> KOuter`, and an actual against `fn(KOuter) -> Int`; both reachability controls refused, so both positions are analysed and neither carries the callable's own declared component types into a conformance judgment; trigger is threading each callable boundary's declared parameter and return through the same relation, which is also what `explicit_return_conformance_note` names as its lambda narrowing. A NESTED container (`List>`) is likewise not judged: the element peel is ONE level, which is the depth measured, and deeper is unmeasured rather than covered. Enrolled evidence, permanent per §4b(4): `test.claim.declared_type_kernel_inhabitance_witness_test` — four discriminating REDs, the already-closed named-field RED as the no-fork control, and one positive control carrying the conforming spelling at all four closed positions so a refuse-everything compiler cannot satisfy them **A THIRD SEAM, MEASURED 2026-09-01 (eager-hawk-376), AND IT IS NOT A SEAM AT A POSITION — IT IS A PROPERTY OF THE DECLARED TYPE.** The row above says to assume a third seam exists until someone enumerates them; this is one, and it is orthogonal to (a)/(b)/(c), which all vary the POSITION while holding the declared type ordinary. Here the position is the already-covered one and the DECLARED TYPE is bodyless: **any `type X` declared with no body admits any argument in parameter position, silently.** Receipt, four fixtures in an ORDINARY (non-`v2.*`) module, so seam (1)'s `module_skips_direct_call_arg_check` exemption is not in play, against a binary carrying main's semantics: `fn takes(x: Compose>) -> Int` given a `String` — ACCEPTED, zero diagnostics naming the file; the same with a bare `Phantom` parameter — ACCEPTED; with a locally declared `type Opaque` and no `Phantom` anywhere — ACCEPTED; and the control `type MyRec = Word8`, an alias to a record — REFUSES with both `type mismatch: expected 'Primitive(MyRec)', got 'Primitive(String)'` and the paired inhabitance diagnostic. **The control is what makes this a finding rather than a silence: the judgment RUNS in that module and admits, which is a different mechanism from seam (1), where the judgment never runs.** It is not `Phantom`-specific and not `Compose`-specific — both were the obvious readings and both are refuted by the third fixture. POPULATION: 69 bodyless declarations corpus-wide, including `std.constructors` `Phantom`, `Product` and `Coproduct`, and `std.machine_constraints` `MachineWidth` / `PointerWidth`. **That 69 is the SYNTACTIC population and an upper bound on nothing else** — a bodyless type never used in parameter position cannot exhibit the hole, so the exposed subset is smaller and unmeasured. A naive line-oriented count returns 5227 because the multi-line coproduct spelling (`type X` then `= A \| B` on the following line) reads as bodyless; re-derive rather than quoting either number. Rung: **below floor** — a value that does not inhabit its declared type is accepted, in an ordinary module, with the judgment live. Ceiling: **R2** — membership is decidable from the declaration, since the refusing control proves the comparison seam already reaches this position and already has both types in hand. **NOT ENROLLED**: no probe asserts this, so nothing reds if it changes; the fixtures above are reconstructable but were deleted with the worktree. Next trigger, at capability grain rather than artifact grain per §4b(3): *the conformance seam decides a bodyless declared type by a stated rule — admit-nothing-but-its-own-constructions, or a declared and typed opacity — rather than by falling through*, with the four fixtures above enrolled as the discriminating REDs and the alias-to-record case kept as the no-fork control. **A SECOND, INDEPENDENT DEFECT FOUND IN THE SAME PASS, RECORDED HERE BECAUSE IT IS THE INSTRUMENT THAT WOULD OTHERWISE BE CITED AS THIS CLASS'S CENSUS:** `tools.opaque_realization_census` `declaration_body_standing_in` decides opacity from the `type X` line alone and carries the annotation *"No such spelling occurs in this corpus today, so the reading is exact for the corpus it is run over"* about the multi-line body form. **That premise is false by 5269 declarations**, every one of which the function classifies `DeclaredOpaque`; and separately it matches the declaration by bare prefix, with no name-boundary check, so a longer same-prefix name declared EARLIER in the file decides a shorter name's standing — 304 such pairs, e.g. `Userset` shadowing `User` in `extdeps.access.zanzibar`. Both are read from the function, not from its annotation. The census gates nothing today, so this is a wrong instrument rather than a wrong wall — but it is the instrument this row's population question would be handed to. | | Direct-call argument TYPE conformance — **transparent-alias identity**, v2 corpus | **R2 built and approved for the alias-identity class (gunbc#8873 — OPEN, approved, mergeable as of 2026-08-22; NOT merged, and this row must not be read as landed until it is).** A precomputed transparent-alias identity relation, derived once at census build and consumed as a `String -> String` map lookup per comparison, admits two names that alias the same declaration and refuses everything else. It peels ONLY `type A = B` with zero params, no connective, no children, no properties and no type annotation, and a target with zero children/params/annotation and `return_cardinality == Required` — so brands, `sole_constructor` carriers, refinements, coproduct arms and applied generics are all excluded BY THE ADMISSION TEST rather than by a later filter. Cost bar was declared before implementation and measured after: four crossed A/B pairs, +2.0s on a 454s regen (+0.4%) against per-arm spreads of 29.9s and 40.9s — a measured null. **What it does NOT do is create substitutability: it makes an existing fact visible.** A pre-relation binary already accepts `CommitSha` at an `AttemptKey` formal and already refuses `IntKey` there | R2 for this class. R3 is not reachable at this seam and that is a property of the seam, not of the relation | **The residual population is a DIFFERENT class and the distinction is load-bearing.** Measured 2026-08-22 against the exemption-deleted corpus: 67 refusals, silent-badger-817's CI run 32562740527 at commit `d42bb3eb57c`. **Provenance caveat, stated because it changes what the 48 means:** that tree merged this relation at `9bfd5388c03`, TWO COMMITS behind head `c40ab2d8248`, and the intervening `b0f72158c80` ("Qualify alias targets at census-build time") is exactly the commit that decides the `CoreNode` group — those refusals turn on `Node` being ambiguous by BARE name. So the 67 is a measurement of an OLDER revision of this relation, not of a broken copy of it. Classification of those 67, derived from declarations and independent of any binary: 48 are this alias class; 8 are applied generics (row below); 11 are `Optional` against `String`/`Bool`/`Int` in `v2.extdeps.github.gha_fold_pilot_emit` and are NOT an alias class at all. **The 48-cleared half is verified on 5 specimens, not 48:** at head, with the exemption deleted in the mirror and `exempt=judged` on all 20352 ledger rows, the five comparisons that CI reports as errors in `00_compile.dag` (lines 319, 342, 408, 446, 497) are all present in the ledger and all read `Compatible`. The remaining 43 sit outside that entry's import closure and a whole-corpus re-run against head was in flight when this row landed — treat 48 as classified-and-partially-verified, never as measured. **Also NOT the alias class: the 11** — the diagnostic reads got `Primitive(String)`, so the optional marker is already gone upstream at pattern destructuring and no comparison-seam mechanism can reach them. That 11 was carried as alias residue by two independent sessions and by this lane's own framing; it is recorded here so it is not handed forward under a label that guarantees the next attempt fails. **Open question for whoever takes it, to be CHECKED rather than inherited from this row:** an optionality marker erased at destructuring means a value reaches a position whose declared type it does not inhabit, which is the same floor rule as the direct-call seam census (record-literal walled; data-initializer and list-element open). If Group C is a FIFTH seam of that class it belongs on that row and not on a new one — decide that before minting a class for it. **A second mechanism, `unanimity`, was designed, measured and ABANDONED as unsound, not deferred.** Its specimen and refutation are carried on the seam-split row above and are deliberately NOT restated here — one fact, one authority | gunbc#8873, 9 enrolled floor witnesses in `dag/test/claim/transparent_alias_identity_witness_test.dag` including the over-peel boundary (`IntHandle` at a `String` formal), a coproduct-projection climb, and a blast-radius pair whose Int-alias discriminator refuses. Shadow ledger re-run before the exemption was touched: 20527 rows, all 115 `WouldDiagnose` rows one mechanism. Receipt: `docs/probes/transparent_alias_identity_2026-08-22/README.md` — **FORWARD REFERENCE, NOT A PRESENT FACT:** that receipt lands with gunbc#8873, which is open at the time this row merges. Do not cite it as evidence until that PR is in | the `v2.` exemption arm cannot be deleted while the applied-generic class below still refuses 8 live sites; the exemption is NOT narrowed to those modules (a narrowing would be a shape test correlating with the distinction rather than naming it) | | Direct-call argument TYPE conformance — **applied-generic alias**, v2 corpus | **Below floor — 8 live false refusals, structurally unreachable from the comparison seam.** An alias whose right-hand side is a generic application (`type BlackConfigPatch = ConfigPatchRecord`) refuses at every call site passing it to the matching formal. Specimen, measured by execution 2026-08-22 on a fixture diffed byte-for-byte against the live `v2.std.patch` declaration, with the exemption deleted in the Rust MIRROR and `exempt=judged` on all 20352 ledger rows as the control: `formal_type = Primitive(ConfigPatchRecord)`, `actual_type = Node(BlackConfigPatch)`, `nominal=true container=false kernel=false`, `fname=ConfigPatchRecord aname=BlackConfigPatch`. Population: 9 declarations, all under `src/v2/extdeps/formatters/` (`black`, `clang_format`, `gofmt`, `google_java_format`, `ktfmt`, `lean4_format`, `prettier`, `rustfmt`, `swift_format`), of which 8 produced diagnostics in the CI arm — `lean4_format` is structurally identical and produced none in EITHER arm, so the population is 9 and the measured count is 8+k | R2, and it is decidable — the same equality already accepts the applied form when it is written directly at the formal | **THE FORMAL SIDE IS WHERE THE INFORMATION DIES, and that is the sentence that should stop the next attempt from this direction.** The formal is DECLARED `ConfigPatchRecord` and REACHES the comparison as the bare constructor, with the type argument already discarded. So the equality has one side that structurally cannot hold an argument, and the case split over any representative is EXHAUSTIVE: (a) representative = the applied form with every argument retained never equals the bare constructor, so it admits nothing and all 9 sites keep refusing; (b) representative = the bare constructor admits `ConfigPatchRecord` at `ConfigPatchRecord` for any X and Y, which is exactly the over-peel that erases the distinction. There is no third representative, and widening the carrier does not help — a node-valued map fails identically, because the missing information is not on the relation's side of the map. **Not to be confused with gunbc#8879**, the withdrawn repair that widened transparency AT RESOLVE and was refused by CI in three classes at once (20 direct-call comparisons, 18 variant projections, 3 files of regen drift). What that established is that resolve is the wrong place for a transparency JUDGMENT; preserving an applied form is resolve DISCARDING LESS, which hands the same consumers MORE structure, and is a different claim that has not been measured | executed fixture + shadow ledger with a positive control (`black.dag` must refuse; a zero there is decidably wrong). **NOT ENROLLED**: no probe pair asserts this class, so nothing reds if it changes. Three false zeros were produced while measuring it — twice from patching the `.dag` authority while the binary is built from the emitted Rust mirror, once from a run that PANICKED and reported zero diagnostics — each caught only by a positive control or by another session's raw per-line export, never by an aggregate | **RESOLVE CARRIES APPLIED FORMS AT THE FORMAL POSITION.** Explicitly NOT scoped as of 2026-08-22 (operator-lane ruling, swift-badger-524): a bounded floor-recovery lane whose completion condition has moved is closed honestly rather than extended, and nothing in that ruling says the change is wrong. Until it lands, the `v2.` exemption stays whole and gunbc#8886 stays blocked | | Direct-call argument TYPE conformance — **container element**, non-exempt module; and the witness family that reported it was **rung INFLATION** (DESIGN §4b(1) — *not* §4b(3): nothing regressed, the wall was never there, so "restore the previous behaviour" is not the remedy and a regression row would have read as authorising it) | **Below floor — the container-element judgment does not fire at a direct call argument.** Measured 2026-08-27 with the witness's OWN oracle (`compile_dag_rust_emit_check`) alongside `compile_dag_diagnostic_census`, over two corpora in two remote dispatches: `main` @ `ddb7f533e4e` and gunbc#9428's head. A fixture handing `FreeMonoid` to a declared `FreeMonoid` parameter — locally declared record, corpus-unique wrapper name, no `Node`, no `v2.std.node`, no occurrence identity anywhere in it — **compiles clean ON `main`**, 0 blocking; the argument surfaces only as advisory `DeclaredTypeInhabitanceUndecided` at "direct call argument". Distinct from the `module_skips_direct_call_arg_check` row above: that exemption keys on the CALLER's module name and this fixture's module is not `v2.`-prefixed, so the judgment is not switched off here — it is written, reached, and answers no. **THE INFLATION:** the class read as mechanically preventable on the strength of `test.claim.record_literal_call_arg_handoff_witness.record_literal_container_element_mismatch_at_call_arg_still_refuses` being green. That witness was green on an UNRELATED defect in its own closure — `v2.std.node` referenced `std.occurrence_identity.OccurrenceId` and `ScopedOccurrenceRef` fully qualified WITHOUT importing that module, so every closure importing `v2.std.node` inherited two `UnresolvedType` diagnostics and refused for that reason; measured on `main`, the fixture's refusal is exactly `UnresolvedType/std.occurrence_identity.OccurrenceId` ×2 + `ScopedOccurrenceRef` ×1, and contains no type-mismatch diagnostic at all. gunbc#9428 adds the import, those resolve, and the accidental refusal goes with them. **A witness green on a defect in its own closure is not weak coverage, it is NEGATIVE coverage** — it is cited as evidence the wall is live, so the class never ranks for climbing. That is DESIGN §4b's worse-than-absent case reached from a direction the document does not yet record: not an unauthorable RED, but an AUTHORABLE one satisfied by the WRONG CAUSE, which no reader of the witness can distinguish from the right one. The nominal sibling `record_literal_nominal_mismatch_at_call_arg_still_refuses` stays green through a DIFFERENT path (`literal_introduction_type_mismatch`, whose actual is a record LITERAL rather than a call), which is why the family read as coherent and was not | R2 (two distinct nominal element types under one container template is a decidable comparison the seam already reaches) | `container_element_nominal_brand_mismatch` is written and IS reached from `direct_call_arg_type_mismatch`, but it delegates to `nominal_call_arg_brand_mismatch`, which requires `structural_carrier_template_name(formal_el) == structural_carrier_template_name(actual_el)`; that name falls through `canonical_template_name` to the element's own authored name for any non-container type, so two DISTINCT nominal element types can never satisfy the conjunct that the mismatch arm needs. **Stated as a CODE READ, consistent with the measurement but not independently executed** — what is executed is that the compile is clean, not which conjunct declined | Measurement above (both corpora, `emit_check` + census). **Instrument not committed:** a throwaway cargo example over the two `pub` entry points in `cli_run`, kept out of the tree per the no-ad-hoc-script rule; re-deriving it needs a `.dag` entry point, which is this row's standing "name the instrument" debt | `container_element_nominal_brand_mismatch` reaching the direct-call-argument position — i.e. `nominal_call_arg_brand_mismatch` admitting distinct nominal element types under a shared container template. The witness is the ready-made RED and needs no new fixture; it is enrolled as expected-red in gunbc#9428, where it FAILS (on `main` it still passes on the accident, so enrolling it here would trip the roster's stale-quarantine arm and red main's own floor) | From 345a5d965499bd6a9b10979fa31173c9e50fa8c6 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 03:57:47 +0000 Subject: [PATCH 4/5] =?UTF-8?q?The=20false=20annotation=20is=20the=20findi?= =?UTF-8?q?ng:=20record=20it=20as=20a=20=C2=A74c=20receipt,=20and=20rank?= =?UTF-8?q?=20the=20two=20census=20defects?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit bold-carp-449's reading, adopted. The census annotation asserting "No such spelling occurs in this corpus today" is not merely a rotted comment: it certifies the exact trap its own function falls into, so a reader checking whether the author considered the continuation form finds a sentence saying yes. DESIGN §4c already names that shape -- an annotation is never evidence that a machine claim holds, because no Accepted program can read one -- so this belongs to that rule as a receipt, not only to this census as a defect. Also records which of the two defects ranks first for repair, and why they are not one defect: the continuation misclassification is systematic and one control exposes it, while the bare-prefix match is silent, name-dependent, and changes its answer with declaration order -- so it survives a fix of the continuation reading alone, and 304 pairs is enough that such a fix would look correct on a spot check. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_013wJU7jqGAEk8rj4UwpHdox --- docs/plans/compiler-guarantee-recovery-gap-analysis.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index e67eb73c041..0fa8cd1be4b 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -170,7 +170,7 @@ unless the row says otherwise, and `Unknown` is the honest default. | Closed-match exhaustiveness | **Path-split, measured 2026-08-01 — the class is not one rung.** Coproduct-typed scrutinee: **R2** (a missing arm on a declared closed variant refuses `NonExhaustiveMatch`, blocking, naming the absent variant). Type-variable scrutinee: **below floor — silent** (`fn pick(t: T) -> Int { match t { Red => 1 } }` compiles with zero diagnostics — one arm, an unconstrained subject, and a variant belonging to an unrelated type). Class rung is the minimum, so **below floor** | R3 (full arm population at elimination) | the silent arm is `PatternDynamic { span: _ } => []`, **not** `PatternLookupBlocked => []` as this row previously said — `pattern_subject_from_node` reaches `PatternLookupBlocked` only when the scrutinee's inferred type `is_compiler_error`, i.e. where a diagnostic already exists, so that arm is not the silent one and its silence is **not** established by these probes | first measured by a one-off execution 2026-08-01 via `compile_dag_diagnostic_census` on the v1 CompileAccept path (source and result in the §10 eighth-pass ledger), and **AUTHORED AS A PROBE PAIR 2026-08-22 — AUTHORED, NOT EXECUTING, AND THE DISTINCTION IS THE WHOLE POINT** (see §11 item 28): the measurement is now written as `test.claim.guarantee_floor_class_probe_witness` `floor_exhaustiveness_on_a_type_variable_scrutinee_is_still_silent`, against the registry row `gunbc.guarantee_probe_corpus` class `floor-closed-match-exhaustiveness`, with the coproduct-scrutinee arm already enrolled at `test.claim.match_exhaustiveness_coproduct_witness` `w_missing_coproduct_arm_reports_one_non_exhaustive`, on the same harness and the same floor run — not re-authored here, because a second copy would be a second authority for one fact as its probe-adequacy control. **It does not run in CI.** The witness declares `ReadsLiveTree` — truthfully, because `compile_dag_diagnostic_census` resolves its synthetic source against the live checkout — and the required floor DECLINES every `ReadsLiveTree` module before the fold sees it (`v2.workflow.required_floor` `RequiredFloorDisposition` `DeclinedLiveTree`), so the probe is discovered and never executed, exactly like the five guarantee carriers §11 item 28 counts. It is green by execution LOCALLY (`gunbc run --claim-run`, 2026-08-22, this session) and that is a strictly weaker fact. So this cell's rung is unchanged from the day before the probe was authored: it still rests on a measurement nothing re-runs. What the probe pair buys is that on the day the decline arm is deleted the measurement becomes standing evidence with no further authorship. Trigger: the `DeclinedLiveTree` deletion (§11 item 28), NOT this cell (§4b meta-obligation 4; the original gap was codex review 46306, §11 item 10) | `ExhaustivenessUnknown` refuses on the dynamic subject | | Record completeness | **R2 measured 2026-08-01** (a record literal omitting a declared required field refuses `MissingField`, blocking, naming the field and type — the class was carried as `Unknown — unmeasured` and the measurement raises it) | R3 | judgment is per-literal; construction-side and generic-instantiation completeness are separate and the latter measures **below floor** in the row above | first measured by a one-off execution 2026-08-01 via `compile_dag_diagnostic_census` on the v1 CompileAccept path (source and result in the §10 eighth-pass ledger), and **AUTHORED AS A PROBE PAIR 2026-08-22 — AUTHORED, NOT EXECUTING, AND THE DISTINCTION IS THE WHOLE POINT** (see §11 item 28): the measurement is now written as `test.claim.guarantee_floor_class_probe_witness` `floor_record_completeness_missing_field_refuses_blocking`, against the registry row `gunbc.guarantee_probe_corpus` class `floor-record-field-completeness`, with `floor_record_completeness_green_control_is_clean` as its probe-adequacy control. **It does not run in CI.** The witness declares `ReadsLiveTree` — truthfully, because `compile_dag_diagnostic_census` resolves its synthetic source against the live checkout — and the required floor DECLINES every `ReadsLiveTree` module before the fold sees it (`v2.workflow.required_floor` `RequiredFloorDisposition` `DeclinedLiveTree`), so the probe is discovered and never executed, exactly like the five guarantee carriers §11 item 28 counts. It is green by execution LOCALLY (`gunbc run --claim-run`, 2026-08-22, this session) and that is a strictly weaker fact. So this cell's rung is unchanged from the day before the probe was authored: it still rests on a measurement nothing re-runs. What the probe pair buys is that on the day the decline arm is deleted the measurement becomes standing evidence with no further authorship. Trigger: the `DeclinedLiveTree` deletion (§11 item 28), NOT this cell (§4b meta-obligation 4; the original gap was codex review 46306, §11 item 10) | required-field construction at every construction form | | Parse: list separator dropped | **Below floor — silent** (measured: `[ {a}, {b} {c} ]` compiles with zero diagnostics — a dropped comma is a silent semantic change, two- vs three-element list; survived regen, whole-corpus compile, fixed-point verify and a 15-case matrix, caught only by a human diff read) | R3 (decidable grammar fact) | separator omission parses as element juxtaposition | First measured by tidy-deer-730's throwaway probe on gunbc#7484 + review 45347, 2026-07-31. **PROBE PAIR AUTHORED 2026-08-22, NOT EXECUTING** (§11 item 28 — the witness is declined by the floor's `DeclinedLiveTree` arm and runs only under a local `gunbc run --claim-run`): `test.claim.guarantee_floor_class_probe_witness` `floor_parse_list_separator_omission_is_still_silent` re-executes it on every required-floor run against `gunbc.guarantee_probe_corpus` class `floor-parse-list-separator`, with `floor_parse_list_separator_doubled_separator_control_refuses` (a DOUBLED separator in the same position refuses `ParseError`, blocking) and `floor_parse_list_separator_green_control_is_clean` as its probe-adequacy controls, all three green locally and none of them executing in CI — so the omission's silence is measured against a parser that demonstrably refuses malformed separators | the probe pair is now in the corpus and pins the hole; what remains is the refusal in the list production (§11 item 6), on which the enrolled probe flips RED and its row is rewritten as `ExpectBlockingRefusal` | -| A value that does not inhabit its declared type is accepted — **seam-split, enumeration UNFINISHED** (was filed as "Direct-call argument TYPE conformance, v2 corpus"; renamed 2026-08-22, see the trigger cell) | **Below floor — the judgment never runs.** Not a hole a bad value slipped through: `v1.compiler.04_infer` gates `arg_compat_diags` on `module_skips_direct_call_arg_check(module_name: scope.module_name)`, which returns true for every module whose name begins with `v2.`. The key is the CALLER's module, so the entire active v2 corpus — compiler stages, extdeps, std, witnesses — has the direct-call argument-type judgment switched off. Measured consequence, 2026-08-22: `v2.extdeps.languages.dag` `dag_int_literal_node_from_lexeme` / `dag_int_literal_node_from_magnitude` declared `occurrence_id: OccurrenceId` since gunbc#6558 while storing that parameter straight into `Node.occurrence_id`, declared `NodeOccurrenceId`. For two months 15 call sites passed `SyntheticOccurrence` (a NodeOccurrenceId, contradicting the declaration) and nothing complained; gunbc#8833 made one call site OBEY the declaration and nothing complained about that either. The error surfaced only as an interpreter `non-exhaustive pattern match on: OccurrenceId { value: 79 }` across 16 witnesses, reddening main. **The inversion worth naming: a declaration that lies is inert while every caller contradicts it in the same direction, and detonates on the first caller who takes it at its word.** So the at-risk population is not "callers who got it wrong" but callers who might get it right — a genuinely counterintuitive census. Note this is the TYPE judgment only; the SHAPE judgment (`direct_call_shape_diags`, labels/arity) is exemption-free and does fire | R2 (a declared parameter type is a decidable conformance check the seam already computes — `direct_call_arg_mismatch_diags` exists, is written, and is simply not called, so the distance to the next rung is an if-statement plus a triage, not an implementation) | **THIS ROW IS A CORRECTION TO DESIGN §4b, NOT A NEW OBSERVATION BESIDE IT — read them together or the first will look like it already settled this.** DESIGN §4b names this exact symbol and reports that it "was found (code read, not execution) to be scoped entirely to the direct-call argument-type judgment and does not reach `sole_constructor`'s construction check at either call site — a positive finding that retires this axis, not an absence of any exemption anywhere." That finding is correct and is not disputed here. The question it asked was whether the exemption LEAKS into `sole_constructor`; the question it never asked is what the exemption COSTS inside the judgment it is scoped to. "Scoped entirely to the direct-call argument-type judgment" reads as reassuring only until that judgment is measured, and it is the argument-type check for the entire active v2 corpus. **Confinement was measured and then treated as safety, and the axis that got retired was not the one that mattered.** Two facts about why the seam nonetheless reads as covered: the SHAPE judgment (`direct_call_shape_diags` — labels, arity, duplicate binding) is exemption-free and DOES fire over every module including the compiler's own sources, so half-live is more deceptive than dead — every casual check finds something working. And the arm is NOT unreasoned: `direct_call_shape_wall_note` states the TYPE judgment's false-positive classes are representation gaps (brand aliases, optionality's two forms, anonymous literals, expansion depth — the conformance wall's four measured classes), which is a real stated reason and is why this row asks for a measurement rather than a deletion. What is unmeasured is whether those classes still fire in v2 today and at what rate. The neighbouring compiler-module arm of this same exemption was deleted in place after being found never to have been in force; the `v2.` arm was left standing at that moment without separate justification of its own | This incident, measured end to end: CI run 32542017600 (main, 67437fcbe9) 16 FAIL with the raw-`OccurrenceId` match error; caller census of both functions read at call grain (17 sites: 15 `SyntheticOccurrence`, 1 `node.occurrence_id`, 1 internal pass-through, 1 raw `minted.id`); exemption mechanism read at `v1.compiler.04_infer` `module_skips_direct_call_arg_check` and its single call site gating `arg_compat_diags` on `scope.module_name`. **NOT ENROLLED**: no probe pair asserts this exemption's reach, so nothing reds if it changes | **THE TRIGGER THIS ROW SHIPPED WITH WAS INCOMPLETE AND IS CORRECTED HERE (2026-08-22, swift-badger-524 retracting their own ruling).** As merged in gunbc#8854 this cell named ONE closing condition — delete the `v2.` exemption — which is a NECESSARY condition presented as a sufficient one. The class is not "direct-call argument type conformance"; it is **a value that does not inhabit its declared type is accepted**, and it has at least TWO seams: **(1) direct-call arguments** — gated off for `v2.*` by `module_skips_direct_call_arg_check`, the mechanism this row measures; **(2) record-literal fields** — gated by NOTHING, below floor in ORDINARY NON-v2 MODULES, receipt gunbc#8865 (gentle-eagle-360). Its minimal pair, no compiler internals involved: `CppHolder { subject: CppWrapped { inner: cpp_inner() } }` accepted and correct, against `CppHolder { subject: cpp_inner() }` — a coproduct PAYLOAD inhabiting a field declared as its parent COPRODUCT — ACCEPTED BY TYPING and dying at runtime as `PatternMatchFailure`. A record literal is not the direct-call seam, so deleting the exemption would not close it. **SEAM (2) NOW HAS A LIVE PRODUCTION SPECIMEN, WHICH RANKS IT DIFFERENTLY FROM A SYNTHETIC PAIR** (gentle-eagle-360, 2026-08-22, found while checking for a second content-identity authority before building on one): `v2.std.materialize` declares `MaterializedNode.hash` as `ContentHash` — the subject-generic union — and `materialize_fold_step` stores `content_hash(n)` into it, which returns `Fnv1a64Structural`, the PAYLOAD carried inside the union's `Fnv1a64` arm. Receipt, by execution against the module as it stands on main: taking the value materialize ACTUALLY STORED and asking the union's own family authority `content_hash_family` about it yields `PatternMatchFailure { value: "Fnv1a64Structural { digest: 7ac77ab0e29c6bd8 }" }`; the probe's fallback was a correctly wrapped `Fnv1a64(...)`, so an empty result or a well-formed value would have PASSED and only a stored value can produce that red. **The defect is LATENT and that is the instructive part**: peer lookup compares `e.hash == h`, raw payload against raw payload, which agrees with itself — so every current path is green and the error surfaces only when a materialize hash is routed through the union's own machinery (`content_hash_family`, or `compare_content_hash`, which exists precisely to refuse cross-family collapse). That is the same shape as this row's own originating incident: **a declaration that lies is inert while every consumer contradicts it in the same direction, and detonates on the first consumer that takes it at its word** — here the first cross-family artifact to reach the carrier. Disposition ruled ARM A, wrap the construction (`MaterializedNode { hash: Fnv1a64(h), ... }`), NOT narrow the declaration: narrowing would sever `MaterializedNode.hash` from `RealizationPlan.target`, and §2's Realization spans resolve-cost, sccache and OS provisioning on ONE content hash, so a structural-only key could never name a realization of a fetched artifact or a provisioned image (swift-badger-524 ruling, 2026-08-22; handed to silent-bear-842 with the receipt, unfixed here because it is that lane's module). **THE SEAM ITSELF IS THE FINDING, not this one site**: gunbc#7480 corrected the design document for asserting the wrong type at exactly this `Hash`/`ContentHash` boundary, and a production module now carries the mirror-image error — a boundary documentation has to keep re-explaining is a boundary that wants construction. ****THAT HAND-OFF IS SUPERSEDED AND THE SPECIMEN IS REPAIRED — corrected in place rather than left standing, because the sentence above says a live production defect is UNFIXED and awaiting another lane, which is the present-tense claim a reader would plan against (gunbc#8876, 2026-08-22).** The wrap landed in the wall's own change by operator ruling: a wall and the repair it forces must land together, since with the wall on and the wrap absent main is red, so only one PR can contain both. `v2.std.materialize` `materialize_fold_step` and `distinct_hashes` now build `Fnv1a64(content_hash(n))`, and the same construction was repaired at four further sites the wall refused for the identical reason — `v2.workflow.operand_flow`, `materialize_witness_test`, `materialization_provider_witness_test` and `heal_revalidation_witness_test`. The receipt above stays as the historical demonstration that the defect was real and reachable; it is no longer a description of the tree. THE ENUMERATION IS UNFINISHED: two is what has been measured, not the count.** Assume a third seam exists until someone enumerates them; note that this row's own originating incident (#8854) reached its victim through a record literal one hop downstream of the direct call, so the two seams are not even cleanly separable at a site. **SEAM (1) WAS EXECUTED TO A MEASURED, BLOCKED STOP ON 2026-08-22 — the arm is NOT deleted, and this paragraph is the §4b row for that state rather than a plan.** Rung: **below floor, unchanged** — the judgment still does not run for any `v2.*` caller. Ceiling: **R2** (a declared parameter type is a decidable conformance check the seam already computes). Next trigger, stated as §4b(2) requires and with its disposition: *a formal parameter declared as an applied generic carries its applied form through resolution rather than reaching the comparison seam as the bare constructor* — **DECLINED at the owning layer on 2026-08-22**, on the ground that a bounded compiler-floor packet whose completion condition has moved should close and hand its residue forward rather than extend into a type-system project. A declined trigger is a legitimate §4b state; **a blocked class with no row is how this exemption survived years in the first place**, which is the reason this row exists at all. Enrolled evidence, so the class stays countable while blocked: `direct_call_arg_type_v2_module_red_probe` (the discriminating RED, rostered in `v2.workflow.floor_expected_red` — it cannot pass while the arm stands and PASSES on a tree with the arm deleted, so it is a satisfiable assertion held open by a named cause), plus two controls that pass on main today (`direct_call_arg_type_ordinary_module_red_probe`, the paired nonzero the exemption never covered; and `direct_call_arg_type_v2_green_control_probe`). **What was measured before the stop, and how to read it:** deleting the arm produces **285+k** blocking diagnostics and **67+k** with gunbc#8873 merged, for some k ≥ 1 unmeasured — these are ROSTER-RESOLVED counts, not corpus counts, and `src/v2/extdeps/formatters/lean4_format.dag:184` is the proof: a live site, structurally identical to eight that refused, contributing zero to *both* arms and therefore invisible to their difference. **Zero genuine call-site defects were found in the residue** — every diagnostic examined was a deficit in the type judgment, so no call sites were edited, because 67 mechanical edits would have cemented three compiler deficits permanently. The per-mechanism split of that residue is deliberately NOT recorded here: it was published as 48/11/8, and the rule the 48 were attributed to was then found to admit nothing in this corpus, so the attribution was retracted before it was cited. Trigger for the count to be restated: the residue re-measured with its `why` column. **The counterexample that retracted it is worth carrying on its own, because it will bite anyone who reaches for a name-keyed alias relation:** `type Float = Float64` is declared in BOTH `dag/std/float.dag:18` and `src/v2/std/float.dag:33`, spelling the target identically — but `dag/std/float.dag:16` has `type Float64 = Real64` (a transparent alias) while `src/v2/std/float.dag:30` has `Float64` as a **record**. So the two declarations agree on a *spelling* and disagree on a *type*, and a unanimity rule keyed on the target's NAME admits them as the same concept. Requiring the target itself to be census-unique closes it — and once closed, that rule admits nothing in this corpus, which is what falsified the attribution above. Found by still-carp-717 while building the rule, before it shipped. **The original trigger text, kept because the sequence it specifies was followed and the record should show what was attempted:** seam (1) — turn the exemption off for `v2.` behind a measured diagnostic count, triage, then delete the arm, the disposition the compiler-module arm received; the measured prerequisite is ALIAS TRANSPARENCY, because proud-ant-819's report-only shadow on the 03_ingest closure found 115 `WouldDiagnose` relations at 78 sites of which 115 reduce to a transparent `type A = B` (92 via `type Hash = Fnv1a64Structural`, 23 via the `Node` phase carriers), residue ZERO — so on that closure the exemption is currently suppressing false positives, not defects. Seam (2) — its own wall at record-literal field conformance; nothing to turn off, it was never on. **Closing seam (1) MUST NOT be read as closing the class**, which is the specific failure this correction exists to prevent: a class that looks like it has one closing condition gets closed when that condition fires. Two blind spots neither instrument covers, named rather than left to be rediscovered: production itself SKIPS an anonymous record literal standing as an ACTUAL at a direct call, so its argument type is never judged (521 relations, 2.7%, `Unadjudicated` in proud-ant-819's shadow — upstream of the guard, so invisible to a flip-off arm too); and a function storing into a field from its own differently-named parameter is this class at yet another site, which a callee-name-keyed census cannot see. **THAT FIRST BLIND SPOT IS NOT SEAM (2), AND THE TWO WILL BE MERGED BY ANY READER WHO DOES NOT SEE THIS SENTENCE** (caught by proud-ant-819, who put the mirror-image clause in their own row): both descriptions begin "a record literal" and name DIFFERENT POSITIONS. The blind spot is a record literal at an ARGUMENT position whose type goes unjudged at the direct-call seam — seam (1)'s territory, and a population of 521 relations. Seam (2) / gunbc#8865 is a record literal's FIELD whose value does not inhabit the field's declared type — a different seam with a different mechanism and no measured population. Reading them as one would make the 521 look like evidence for gunbc#8865, or gunbc#8865's receipt look like it bounds the 521. Neither is true. **A CLAIM ABOUT THIS ROW'S EVIDENCE WAS MADE HERE AND IS RETRACTED, MEASURED WRONG (2026-08-22, the §11 item 28 lane, retracting itself).** The retracted claim was that these probes sit in the declined `ReadsLiveTree` carrier and therefore never execute, so the expected-red enrolment could only be `not_evaluated`. **It is false, and the measurement that refutes it is the run that was supposed to confirm it:** run `32586093086` reports `[expected-red-roster-join] roster=207 still_red=207 now_passes=0 not_evaluated=0` with `known_red_held=207`. The v2-module red EXECUTES and is held still-red exactly as its row intends. The error was reading an IMPORT as a location: `guarantee_probe_corpus_witness` imports the three probe ids for a roster assertion, and I took that for where the probes run; they run in `test.claim.direct_call_argument_type_witness`, a separate file. An import is evidence of visibility, never authority for where a name lives. **What survives is a different and sharper finding.** That file executes because it declares `SubstrateInputsOnly` while calling `compile_dag_diagnostic_census` — the same declaration `gunbc.compile_diagnostic_census`'s own live-tree note already adjudicated as a MIS-declaration when it found `transport_script_wall_compile_red_test` doing it (that census walks `build_module_path_index_from_witness_roots`, i.e. the live checkout). So the specimen population for that mis-declaration is now TWO, the second authored on 2026-08-22 after the first was adjudicated, and both are the only reason any census-compiling probe executes at all. Either these files' declaration is wrong or that authority's note is; they cannot both be right, and which one it is decides the size of §11 item 28's population. That is a question for the arm's owner, not a defect in this row's measurement, which stands. **SEAM (2) IS NOW CLOSED, AND CLOSING IT ENUMERATED TWO MORE — the count is FIVE measured, still not the total (gunbc#8876, 2026-08-22).** **OWNERSHIP, STATED PER SEAM BECAUSE THE CLASS NOW SPANS TWO LANES AND NEITHER CAN CLOSE IT ALONE:** seam (1) is the exemption-gated direct-call seam owned by the paragraph immediately preceding this one, whose next trigger is recorded there as DECLINED rather than pending; seams (2) through (5) belong to the field-inhabitance lane (snappy-tern-856). A lane that lands its last seam will be tempted to close this row. NEITHER MAY: 'my seams are done' is not 'the class is closed', and the row closes only when every seam does — including any seam not yet enumerated. The record-literal FIELD seam is walled: `v1.compiler.infer` `coproduct_payload_where_parent_required` refuses a value whose type is one of the declared coproduct's own variant payload types, consulting `transparent_alias_identity_agrees` over the `SymbolIndex` so an alias-mediated producer is caught too. Rung at that seam: **structurally guaranteed** — no `Accepted` program contains the state there. NOT structurally impossible, because the bad literal is still writable and the compiler refuses it; and NOT the class, which is why the two rows below exist. Evidence, enrolled permanently per §4b(4): `test.claim.coproduct_payload_soundness_witness_test` — the direct RED, the alias-mediated RED, and the positive control that stops a refuse-everything compiler from satisfying either. Turning the wall on WAS the census: EIGHT live sites, none previously known, all repaired in the same change — `ContentHash` from `Fnv1a64Structural` at `materialization_provider_witness_test`, `heal_revalidation_witness_test`, `materialize_witness_test`, `v2.std.materialize` and `v2.workflow.operand_flow`; `LexRules` from `LexRuleSet` at two `src/v2/test/claim/manual` fold tests. **SEAM (3), UNWALLED AND DECLARED, owner the field-inhabitance lane: the module-scope `data` initializer.** `data X: ContentHash = content_hash(...)` stores the payload into a `ContentHash`-declared row and is NOT refused, because a `data` initializer is not a record-literal field. Rung: **below floor**, exactly as seam (2) was. Unguarded: every module-scope `data` row in the corpus. Trigger: the same conformance judgment applied at the data-initializer seam, which needs no new relation — the declared type and the initializer's inferred type are both already in hand there. **SEAM (4), UNWALLED AND DECLARED, owner the field-inhabitance lane, AND IT IS RANKED FIRST OF THE TWO: the list element.** `v2.workflow.locality_affinity` built consumer identities as `list_add_distinct_hash(xs: cs, v: content_hash(n: e.dependent))` — a raw payload into a `List`. Rung: **below floor**, and it does not fail loudly. Measured: repairing the comparands while that producer stayed raw turned FOUR `locality_affinity` witnesses to `Bool(false)` with NOTHING refused at compile time — a wrong answer discovered later, not a diagnostic. That is what makes it rank above seam (3), and the ranking is fixed by a RULE rather than by judgment (operator ratification, 2026-08-22): seam (3) admits a wrong value a correctly-built peer can still catch by comparison — harmful, detectable, recoverable — while seam (4) admits a wrong value AND DISABLES THE COMPARISON THAT WOULD HAVE CAUGHT IT. That is a silent wrong answer, which DESIGN places OUTSIDE the guarantee ladder and forbids outright rather than ranking low, so the two are in different categories and no population argument reaches across the line: a larger set of loud failures does not outrank a smaller set of silent ones. The ranking is a priority order for collisions, NOT a serial queue — seam (3) needs no new relation and may land whenever it is ready. Unguarded: every list, map and collection element position whose element type is a coproduct. Trigger: element-position conformance against the container's declared element type. **SEAM (5), UNWALLED AND DECLARED, owner the field-inhabitance lane: the declared RETURN type.** `fn f(x: Node) -> ContentHash { content_hash(n: x) }` returns the payload where the parent coproduct is declared and is NOT refused. Rung: **below floor**. Measured 2026-08-22 on the gunbc#8876 merge commit, with a liveness control in the SAME compile that produced exactly one diagnostic (the record-literal RED), so the silence is a measurement and not an untested assumption. HOW IT WAS FOUND IS WORTH RECORDING, because it says something about the enumeration itself: it was found by a MIS-WRITTEN PROBE — the author intended an alias-mediated FIELD case and wrote a return position by mistake. Four of the five seams in this row were discovered by accident or by a downstream red rather than by anyone enumerating positions, which is the standing evidence for #8868's instruction to assume a further seam. Unguarded: every declared return type whose type is a coproduct. Trigger: `declared_type_conformance_diags` already runs at this seam and already holds both the declared and the inferred type, so the distance is a payload-membership arm on an existing judgment, not a new walk. **DO NOT READ SEAM (2)'s CLOSURE AS THE CLASS'S.** One seam of four measured is walled; a reader who sees only 'declared-field inhabitance wall landed' will conclude the class is closed, and the next lane would then build on a guarantee covering a quarter of it. Neither seam (3) nor seam (4) nor seam (5) is closed by gunbc#8876, which deliberately did not widen to chase them. **THIS ROW'S CEILING CELL SAYS THE DISTANCE TO R2 IS "AN IF-STATEMENT PLUS A TRIAGE". THAT IS MEASURED FALSE FOR THE PAYLOAD-WHERE-PARENT SHAPE, AND THE CORRECTION MATTERS BECAUSE IT IS THE SECOND NECESSARY-CONDITION-STATED-AS-SUFFICIENT TRIGGER THIS ONE ROW HAS CARRIED (snappy-tern-856, 2026-08-22).** The cell reasons that `direct_call_arg_mismatch_diags` exists, is written, and is simply not called, so flipping `module_skips_direct_call_arg_check` off closes seam (1). Flipping it off is NECESSARY. It is not SUFFICIENT, and the discriminating measurement is a module the exemption never applied to in the first place: in an ORDINARY NON-`v2.*` module, where the guard is false and the judgment demonstrably runs, `c4_takes(o: 5)` against `fn c4_takes(o: EOuter)` REFUSES (`expected 'Coproduct(EOuter)', got 'Primitive(Int)'`) while `c4_takes(o: e_inner())` — the coproduct's own payload type — is ACCEPTED in the same compile. The judgment is live at that seam and misses this shape, so deleting the arm leaves it accepted. **Read the two facts together or the row misleads:** the exemption really does switch the judgment off for every `v2.*` caller (that half is unchanged and still below floor), AND the judgment it switches off would not catch this shape anyway. A reader who acts only on the first will delete the arm, watch the diagnostics, and conclude the seam is closed. **THE DENOMINATOR THIS ROW HAS LACKED SINCE IT WAS WRITTEN NOW EXISTS, and it is what makes the sentence above checkable rather than another anecdote.** The row has said "assume a third seam until someone enumerates them" through two revisions while the count grew from two to five BY ACCIDENT — four of the five were found by a downstream red or by a mis-written probe, never by anyone enumerating positions, which samples the reviewer rather than the population. The positions are now enumerated FROM THE GRAMMAR: every call site of `parse_type_expr` in `v1.compiler.parse`, which is the finite set of places the language attaches a declared type. That is **14 sites**, and all five previously-known seams FALL OUT of it as rows rather than having been seeded into it — the falsifier the enumeration was required to pass. The list element seam falls out only because a container's element type is reached as a TYPE ARGUMENT rather than as a declaration of its own, which is why nobody had named it as a position before. **METHOD, because "not refused" is worthless without it.** Each position carries three arms: the payload-where-parent shape, a KERNEL mismatch (`Int` where the coproduct is declared), and an UNDEFINED NAME. The third is the reachability control: if it refuses, inference REACHES that position, so a passing kernel arm establishes that NO TYPE JUDGMENT RUNS there rather than that the position went unanalysed. All seven reachability controls refused. Dispositions, measured: **refuses** — record/variant NAMED field (`parse_field`), and only because gunbc#8876 walls it. **Judgment runs, misses the shape** — fn parameter at the direct-call seam. **Not refused, no judgment runs** — container type argument (list element), variant POSITIONAL payload, fn declared return, module-scope `data` initializer, annotated `let`. **Not refused** — `as` cast. **Not reachable from a source value** — type-alias RHS, `uses` resource type, service `exit` and `response` types (the last two are the reconstruction path's, not this row's). **Not refused, no judgment runs** (measured after the first pass, closing the census at 14 of 14) — the callable-type RETURN position (`cb: fn(Int) -> EOuter` given a lambda whose body yields the payload) and the callable-type PARAMETER position (`cb: fn(EOuter) -> Int` called with the payload); both reachability controls refused, so both positions are analysed. Three of these positions were previously unknown: variant positional payload, `as` cast, and annotated `let`. **AND THE ENUMERATION FOUND SOMETHING WIDER THAN THIS ROW'S CLASS, WHICH IS DELIBERATELY NOT CLAIMED HERE.** `data c6b: EOuter = 5` and `fn c5b() -> EOuter { 5 }` are both ACCEPTED, with the reachability control proving both positions are analysed. That is not payload-versus-parent; it is a plain kernel value where a declared coproduct is required, which is the ordinary-floor invariant DESIGN §4b names beside name resolution and exact-bijection binding. On the measured census that is **seven of fourteen grammar-admitted positions accepting a kernel value where a declared coproduct is required** — variant positional payload, fn declared return, module-scope `data` initializer, container type argument, annotated `let`, callable-type return, callable-type parameter — with the single refusing position owing its refusal to a PR that is held at the time of writing. (The count was first published as FIVE of fourteen, before the two callable-type positions were measured; it is corrected here rather than left standing, because an understated denominator on a floor breach is the same defect as an overstated rung. The `as` cast is deliberately not in the seven: it was never given a kernel arm, since a cast is an authored assertion and whether a kernel-to-coproduct cast should refuse is a different question this census did not ask.) This row's class is one INSTANCE of that breach rather than the breach itself, so the finding is routed for its own §4b row and its own owner rather than absorbed here — recording it inside this row would repeat the mistake this correction exists to fix, by making a wider unwalled invariant look like a seam of a narrower one **THAT WIDER BREACH NOW HAS ITS OWN OWNER AND FOUR OF ITS SEVEN POSITIONS ARE WALLED (2026-08-24, the declared-type-inhabitance lane).** Scope, stated first because the class and this row's class are neighbours that will be merged by anyone reading quickly: the subject is A PLAIN KERNEL VALUE (`Int`, `String`, `Bool`) where a declared record or coproduct is required — NOT a coproduct payload where its parent is required, which is this row's seam (2) and is separately walled. MEASURED BEFORE, on the pre-change binary, one fixture per position with an undefined-name reachability control beside it: all SEVEN positions compiled `0 diagnostics` and EMITTED 9 files (fn declared return, module-scope `data` annotation, annotated `let`, container element, variant positional payload, callable-type return, callable-type parameter); every reachability control refused (`function 'no_such_name_at_all' not found in scope`), so the silence measured an absent judgment rather than an unanalysed position; and the record-literal NAMED field refused (`expected 'Coproduct(KOuter)', got 'Primitive(Int)'`), which is what identified the relation that already existed. MEASURED AFTER, same fixtures, same flags: the declared return, the `data` annotation, the annotated `let` and the container element REFUSE with a located `TypeMismatch` (`expected 'Coproduct(KOuter)', got 'Primitive(Int)'`; the element position as `expected 'Container(List,Coproduct(KOuter))', got 'Container(List,Primitive(Int))'`); the conforming spelling at all four positions still compiles `0 diagnostics`; the named field refuses identically, which is the control proving the reused relation has not forked; and `fn f() -> KInner { 5 }` — a RECORD rather than a coproduct — now refuses too (`expected 'Product(KInner)', got 'Primitive(Int)'`), so the wall is the declared-type class and not a coproduct special case. NO SECOND RELATION WAS MINTED (DESIGN §3): `kernel_value_declared_type_mismatch` was already the corpus authority for this judgment and was consulted at exactly one of the fourteen positions; what landed is its peeling prologue lifted into `declared_type_conformance_diags`, so the fn return, the early `return`, the `data` annotation and the newly-wired annotated `let` all widen with that gate rather than beside it. FALSE-POSITIVE CENSUS, AND ITS FIRST STATEMENT HERE WAS WRONG ABOUT ITS OWN DENOMINATOR — corrected in place because the error is the instructive part. The regen corpus compile (`dag` + `src/v2`, `first_generation_equal=true`, `planned=133 executed=133`) reports zero hard diagnostics under the wall, and this row first read that as 'no live site was repaired'. The required floor then refused: its prepared subject resolves **3872 modules**, including `src/v2/test/**`, which the regen closure does not reach, and the wall found **six live sites in one file** — `src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test` declared six octet fixtures and one function parameter as `List` while holding integer literals (`[0, 255, 255, 255, 255]`) and forwarding them to `v2.compiler.emit_host` `emit_host_octets_byte_string`, whose declared parameter is `List` and which builds each `Byte` itself. `Byte` is a record over `List` and no `Int -> Byte` cast rule exists, so every one of those declarations was a lie that no consumer contradicted — the latent shape this row's originating incident already names, at the element position the wall now judges. Repaired to `List` (the entry then compiles with 0 blocking diagnostics), which makes TURNING THE WALL ON the census, exactly as gunbc#8876's field seam was. THE GENERAL LESSON, worth more than the six sites: a green whole-corpus compile is scoped to ITS OWN closure, and quoting it as 'the corpus' silently excludes whatever that closure omits; the floor's prepared subject is the wider denominator and disagreeing with it is how the gap was found. Zero further live sites were found beyond that file, which is a fact about this class's live population and not evidence that the other three positions are empty. RUNG: the four walled positions are **structurally guaranteed** (the bad value is still writable and the compiler refuses it); the class as a whole stays **below floor**, because three positions still admit it. STILL OPEN, each with its trigger, and NONE of them closed by this change: (a) the VARIANT POSITIONAL PAYLOAD — `KHeld(5)` routes through `infer_variant_constructor_call` into `infer_record_lit` under the synthetic field name `0`, and the declared type of that positional slot does not reach the field-conformance seam the NAMED field reaches; trigger is that slot resolving to its declared payload type there. (b) and (c) the CALLABLE-TYPE RETURN and PARAMETER — a lambda's body against `fn(Int) -> KOuter`, and an actual against `fn(KOuter) -> Int`; both reachability controls refused, so both positions are analysed and neither carries the callable's own declared component types into a conformance judgment; trigger is threading each callable boundary's declared parameter and return through the same relation, which is also what `explicit_return_conformance_note` names as its lambda narrowing. A NESTED container (`List>`) is likewise not judged: the element peel is ONE level, which is the depth measured, and deeper is unmeasured rather than covered. Enrolled evidence, permanent per §4b(4): `test.claim.declared_type_kernel_inhabitance_witness_test` — four discriminating REDs, the already-closed named-field RED as the no-fork control, and one positive control carrying the conforming spelling at all four closed positions so a refuse-everything compiler cannot satisfy them **A THIRD SEAM, MEASURED 2026-09-01 (eager-hawk-376), AND IT IS NOT A SEAM AT A POSITION — IT IS A PROPERTY OF THE DECLARED TYPE.** The row above says to assume a third seam exists until someone enumerates them; this is one, and it is orthogonal to (a)/(b)/(c), which all vary the POSITION while holding the declared type ordinary. Here the position is the already-covered one and the DECLARED TYPE is bodyless: **any `type X` declared with no body admits any argument in parameter position, silently.** Receipt, four fixtures in an ORDINARY (non-`v2.*`) module, so seam (1)'s `module_skips_direct_call_arg_check` exemption is not in play, against a binary carrying main's semantics: `fn takes(x: Compose>) -> Int` given a `String` — ACCEPTED, zero diagnostics naming the file; the same with a bare `Phantom` parameter — ACCEPTED; with a locally declared `type Opaque` and no `Phantom` anywhere — ACCEPTED; and the control `type MyRec = Word8`, an alias to a record — REFUSES with both `type mismatch: expected 'Primitive(MyRec)', got 'Primitive(String)'` and the paired inhabitance diagnostic. **The control is what makes this a finding rather than a silence: the judgment RUNS in that module and admits, which is a different mechanism from seam (1), where the judgment never runs.** It is not `Phantom`-specific and not `Compose`-specific — both were the obvious readings and both are refuted by the third fixture. POPULATION: 69 bodyless declarations corpus-wide, including `std.constructors` `Phantom`, `Product` and `Coproduct`, and `std.machine_constraints` `MachineWidth` / `PointerWidth`. **That 69 is the SYNTACTIC population and an upper bound on nothing else** — a bodyless type never used in parameter position cannot exhibit the hole, so the exposed subset is smaller and unmeasured. A naive line-oriented count returns 5227 because the multi-line coproduct spelling (`type X` then `= A \| B` on the following line) reads as bodyless; re-derive rather than quoting either number. Rung: **below floor** — a value that does not inhabit its declared type is accepted, in an ordinary module, with the judgment live. Ceiling: **R2** — membership is decidable from the declaration, since the refusing control proves the comparison seam already reaches this position and already has both types in hand. **NOT ENROLLED**: no probe asserts this, so nothing reds if it changes; the fixtures above are reconstructable but were deleted with the worktree. Next trigger, at capability grain rather than artifact grain per §4b(3): *the conformance seam decides a bodyless declared type by a stated rule — admit-nothing-but-its-own-constructions, or a declared and typed opacity — rather than by falling through*, with the four fixtures above enrolled as the discriminating REDs and the alias-to-record case kept as the no-fork control. **A SECOND, INDEPENDENT DEFECT FOUND IN THE SAME PASS, RECORDED HERE BECAUSE IT IS THE INSTRUMENT THAT WOULD OTHERWISE BE CITED AS THIS CLASS'S CENSUS:** `tools.opaque_realization_census` `declaration_body_standing_in` decides opacity from the `type X` line alone and carries the annotation *"No such spelling occurs in this corpus today, so the reading is exact for the corpus it is run over"* about the multi-line body form. **That premise is false by 5269 declarations**, every one of which the function classifies `DeclaredOpaque`; and separately it matches the declaration by bare prefix, with no name-boundary check, so a longer same-prefix name declared EARLIER in the file decides a shorter name's standing — 304 such pairs, e.g. `Userset` shadowing `User` in `extdeps.access.zanzibar`. Both are read from the function, not from its annotation. The census gates nothing today, so this is a wrong instrument rather than a wrong wall — but it is the instrument this row's population question would be handed to. | +| A value that does not inhabit its declared type is accepted — **seam-split, enumeration UNFINISHED** (was filed as "Direct-call argument TYPE conformance, v2 corpus"; renamed 2026-08-22, see the trigger cell) | **Below floor — the judgment never runs.** Not a hole a bad value slipped through: `v1.compiler.04_infer` gates `arg_compat_diags` on `module_skips_direct_call_arg_check(module_name: scope.module_name)`, which returns true for every module whose name begins with `v2.`. The key is the CALLER's module, so the entire active v2 corpus — compiler stages, extdeps, std, witnesses — has the direct-call argument-type judgment switched off. Measured consequence, 2026-08-22: `v2.extdeps.languages.dag` `dag_int_literal_node_from_lexeme` / `dag_int_literal_node_from_magnitude` declared `occurrence_id: OccurrenceId` since gunbc#6558 while storing that parameter straight into `Node.occurrence_id`, declared `NodeOccurrenceId`. For two months 15 call sites passed `SyntheticOccurrence` (a NodeOccurrenceId, contradicting the declaration) and nothing complained; gunbc#8833 made one call site OBEY the declaration and nothing complained about that either. The error surfaced only as an interpreter `non-exhaustive pattern match on: OccurrenceId { value: 79 }` across 16 witnesses, reddening main. **The inversion worth naming: a declaration that lies is inert while every caller contradicts it in the same direction, and detonates on the first caller who takes it at its word.** So the at-risk population is not "callers who got it wrong" but callers who might get it right — a genuinely counterintuitive census. Note this is the TYPE judgment only; the SHAPE judgment (`direct_call_shape_diags`, labels/arity) is exemption-free and does fire | R2 (a declared parameter type is a decidable conformance check the seam already computes — `direct_call_arg_mismatch_diags` exists, is written, and is simply not called, so the distance to the next rung is an if-statement plus a triage, not an implementation) | **THIS ROW IS A CORRECTION TO DESIGN §4b, NOT A NEW OBSERVATION BESIDE IT — read them together or the first will look like it already settled this.** DESIGN §4b names this exact symbol and reports that it "was found (code read, not execution) to be scoped entirely to the direct-call argument-type judgment and does not reach `sole_constructor`'s construction check at either call site — a positive finding that retires this axis, not an absence of any exemption anywhere." That finding is correct and is not disputed here. The question it asked was whether the exemption LEAKS into `sole_constructor`; the question it never asked is what the exemption COSTS inside the judgment it is scoped to. "Scoped entirely to the direct-call argument-type judgment" reads as reassuring only until that judgment is measured, and it is the argument-type check for the entire active v2 corpus. **Confinement was measured and then treated as safety, and the axis that got retired was not the one that mattered.** Two facts about why the seam nonetheless reads as covered: the SHAPE judgment (`direct_call_shape_diags` — labels, arity, duplicate binding) is exemption-free and DOES fire over every module including the compiler's own sources, so half-live is more deceptive than dead — every casual check finds something working. And the arm is NOT unreasoned: `direct_call_shape_wall_note` states the TYPE judgment's false-positive classes are representation gaps (brand aliases, optionality's two forms, anonymous literals, expansion depth — the conformance wall's four measured classes), which is a real stated reason and is why this row asks for a measurement rather than a deletion. What is unmeasured is whether those classes still fire in v2 today and at what rate. The neighbouring compiler-module arm of this same exemption was deleted in place after being found never to have been in force; the `v2.` arm was left standing at that moment without separate justification of its own | This incident, measured end to end: CI run 32542017600 (main, 67437fcbe9) 16 FAIL with the raw-`OccurrenceId` match error; caller census of both functions read at call grain (17 sites: 15 `SyntheticOccurrence`, 1 `node.occurrence_id`, 1 internal pass-through, 1 raw `minted.id`); exemption mechanism read at `v1.compiler.04_infer` `module_skips_direct_call_arg_check` and its single call site gating `arg_compat_diags` on `scope.module_name`. **NOT ENROLLED**: no probe pair asserts this exemption's reach, so nothing reds if it changes | **THE TRIGGER THIS ROW SHIPPED WITH WAS INCOMPLETE AND IS CORRECTED HERE (2026-08-22, swift-badger-524 retracting their own ruling).** As merged in gunbc#8854 this cell named ONE closing condition — delete the `v2.` exemption — which is a NECESSARY condition presented as a sufficient one. The class is not "direct-call argument type conformance"; it is **a value that does not inhabit its declared type is accepted**, and it has at least TWO seams: **(1) direct-call arguments** — gated off for `v2.*` by `module_skips_direct_call_arg_check`, the mechanism this row measures; **(2) record-literal fields** — gated by NOTHING, below floor in ORDINARY NON-v2 MODULES, receipt gunbc#8865 (gentle-eagle-360). Its minimal pair, no compiler internals involved: `CppHolder { subject: CppWrapped { inner: cpp_inner() } }` accepted and correct, against `CppHolder { subject: cpp_inner() }` — a coproduct PAYLOAD inhabiting a field declared as its parent COPRODUCT — ACCEPTED BY TYPING and dying at runtime as `PatternMatchFailure`. A record literal is not the direct-call seam, so deleting the exemption would not close it. **SEAM (2) NOW HAS A LIVE PRODUCTION SPECIMEN, WHICH RANKS IT DIFFERENTLY FROM A SYNTHETIC PAIR** (gentle-eagle-360, 2026-08-22, found while checking for a second content-identity authority before building on one): `v2.std.materialize` declares `MaterializedNode.hash` as `ContentHash` — the subject-generic union — and `materialize_fold_step` stores `content_hash(n)` into it, which returns `Fnv1a64Structural`, the PAYLOAD carried inside the union's `Fnv1a64` arm. Receipt, by execution against the module as it stands on main: taking the value materialize ACTUALLY STORED and asking the union's own family authority `content_hash_family` about it yields `PatternMatchFailure { value: "Fnv1a64Structural { digest: 7ac77ab0e29c6bd8 }" }`; the probe's fallback was a correctly wrapped `Fnv1a64(...)`, so an empty result or a well-formed value would have PASSED and only a stored value can produce that red. **The defect is LATENT and that is the instructive part**: peer lookup compares `e.hash == h`, raw payload against raw payload, which agrees with itself — so every current path is green and the error surfaces only when a materialize hash is routed through the union's own machinery (`content_hash_family`, or `compare_content_hash`, which exists precisely to refuse cross-family collapse). That is the same shape as this row's own originating incident: **a declaration that lies is inert while every consumer contradicts it in the same direction, and detonates on the first consumer that takes it at its word** — here the first cross-family artifact to reach the carrier. Disposition ruled ARM A, wrap the construction (`MaterializedNode { hash: Fnv1a64(h), ... }`), NOT narrow the declaration: narrowing would sever `MaterializedNode.hash` from `RealizationPlan.target`, and §2's Realization spans resolve-cost, sccache and OS provisioning on ONE content hash, so a structural-only key could never name a realization of a fetched artifact or a provisioned image (swift-badger-524 ruling, 2026-08-22; handed to silent-bear-842 with the receipt, unfixed here because it is that lane's module). **THE SEAM ITSELF IS THE FINDING, not this one site**: gunbc#7480 corrected the design document for asserting the wrong type at exactly this `Hash`/`ContentHash` boundary, and a production module now carries the mirror-image error — a boundary documentation has to keep re-explaining is a boundary that wants construction. ****THAT HAND-OFF IS SUPERSEDED AND THE SPECIMEN IS REPAIRED — corrected in place rather than left standing, because the sentence above says a live production defect is UNFIXED and awaiting another lane, which is the present-tense claim a reader would plan against (gunbc#8876, 2026-08-22).** The wrap landed in the wall's own change by operator ruling: a wall and the repair it forces must land together, since with the wall on and the wrap absent main is red, so only one PR can contain both. `v2.std.materialize` `materialize_fold_step` and `distinct_hashes` now build `Fnv1a64(content_hash(n))`, and the same construction was repaired at four further sites the wall refused for the identical reason — `v2.workflow.operand_flow`, `materialize_witness_test`, `materialization_provider_witness_test` and `heal_revalidation_witness_test`. The receipt above stays as the historical demonstration that the defect was real and reachable; it is no longer a description of the tree. THE ENUMERATION IS UNFINISHED: two is what has been measured, not the count.** Assume a third seam exists until someone enumerates them; note that this row's own originating incident (#8854) reached its victim through a record literal one hop downstream of the direct call, so the two seams are not even cleanly separable at a site. **SEAM (1) WAS EXECUTED TO A MEASURED, BLOCKED STOP ON 2026-08-22 — the arm is NOT deleted, and this paragraph is the §4b row for that state rather than a plan.** Rung: **below floor, unchanged** — the judgment still does not run for any `v2.*` caller. Ceiling: **R2** (a declared parameter type is a decidable conformance check the seam already computes). Next trigger, stated as §4b(2) requires and with its disposition: *a formal parameter declared as an applied generic carries its applied form through resolution rather than reaching the comparison seam as the bare constructor* — **DECLINED at the owning layer on 2026-08-22**, on the ground that a bounded compiler-floor packet whose completion condition has moved should close and hand its residue forward rather than extend into a type-system project. A declined trigger is a legitimate §4b state; **a blocked class with no row is how this exemption survived years in the first place**, which is the reason this row exists at all. Enrolled evidence, so the class stays countable while blocked: `direct_call_arg_type_v2_module_red_probe` (the discriminating RED, rostered in `v2.workflow.floor_expected_red` — it cannot pass while the arm stands and PASSES on a tree with the arm deleted, so it is a satisfiable assertion held open by a named cause), plus two controls that pass on main today (`direct_call_arg_type_ordinary_module_red_probe`, the paired nonzero the exemption never covered; and `direct_call_arg_type_v2_green_control_probe`). **What was measured before the stop, and how to read it:** deleting the arm produces **285+k** blocking diagnostics and **67+k** with gunbc#8873 merged, for some k ≥ 1 unmeasured — these are ROSTER-RESOLVED counts, not corpus counts, and `src/v2/extdeps/formatters/lean4_format.dag:184` is the proof: a live site, structurally identical to eight that refused, contributing zero to *both* arms and therefore invisible to their difference. **Zero genuine call-site defects were found in the residue** — every diagnostic examined was a deficit in the type judgment, so no call sites were edited, because 67 mechanical edits would have cemented three compiler deficits permanently. The per-mechanism split of that residue is deliberately NOT recorded here: it was published as 48/11/8, and the rule the 48 were attributed to was then found to admit nothing in this corpus, so the attribution was retracted before it was cited. Trigger for the count to be restated: the residue re-measured with its `why` column. **The counterexample that retracted it is worth carrying on its own, because it will bite anyone who reaches for a name-keyed alias relation:** `type Float = Float64` is declared in BOTH `dag/std/float.dag:18` and `src/v2/std/float.dag:33`, spelling the target identically — but `dag/std/float.dag:16` has `type Float64 = Real64` (a transparent alias) while `src/v2/std/float.dag:30` has `Float64` as a **record**. So the two declarations agree on a *spelling* and disagree on a *type*, and a unanimity rule keyed on the target's NAME admits them as the same concept. Requiring the target itself to be census-unique closes it — and once closed, that rule admits nothing in this corpus, which is what falsified the attribution above. Found by still-carp-717 while building the rule, before it shipped. **The original trigger text, kept because the sequence it specifies was followed and the record should show what was attempted:** seam (1) — turn the exemption off for `v2.` behind a measured diagnostic count, triage, then delete the arm, the disposition the compiler-module arm received; the measured prerequisite is ALIAS TRANSPARENCY, because proud-ant-819's report-only shadow on the 03_ingest closure found 115 `WouldDiagnose` relations at 78 sites of which 115 reduce to a transparent `type A = B` (92 via `type Hash = Fnv1a64Structural`, 23 via the `Node` phase carriers), residue ZERO — so on that closure the exemption is currently suppressing false positives, not defects. Seam (2) — its own wall at record-literal field conformance; nothing to turn off, it was never on. **Closing seam (1) MUST NOT be read as closing the class**, which is the specific failure this correction exists to prevent: a class that looks like it has one closing condition gets closed when that condition fires. Two blind spots neither instrument covers, named rather than left to be rediscovered: production itself SKIPS an anonymous record literal standing as an ACTUAL at a direct call, so its argument type is never judged (521 relations, 2.7%, `Unadjudicated` in proud-ant-819's shadow — upstream of the guard, so invisible to a flip-off arm too); and a function storing into a field from its own differently-named parameter is this class at yet another site, which a callee-name-keyed census cannot see. **THAT FIRST BLIND SPOT IS NOT SEAM (2), AND THE TWO WILL BE MERGED BY ANY READER WHO DOES NOT SEE THIS SENTENCE** (caught by proud-ant-819, who put the mirror-image clause in their own row): both descriptions begin "a record literal" and name DIFFERENT POSITIONS. The blind spot is a record literal at an ARGUMENT position whose type goes unjudged at the direct-call seam — seam (1)'s territory, and a population of 521 relations. Seam (2) / gunbc#8865 is a record literal's FIELD whose value does not inhabit the field's declared type — a different seam with a different mechanism and no measured population. Reading them as one would make the 521 look like evidence for gunbc#8865, or gunbc#8865's receipt look like it bounds the 521. Neither is true. **A CLAIM ABOUT THIS ROW'S EVIDENCE WAS MADE HERE AND IS RETRACTED, MEASURED WRONG (2026-08-22, the §11 item 28 lane, retracting itself).** The retracted claim was that these probes sit in the declined `ReadsLiveTree` carrier and therefore never execute, so the expected-red enrolment could only be `not_evaluated`. **It is false, and the measurement that refutes it is the run that was supposed to confirm it:** run `32586093086` reports `[expected-red-roster-join] roster=207 still_red=207 now_passes=0 not_evaluated=0` with `known_red_held=207`. The v2-module red EXECUTES and is held still-red exactly as its row intends. The error was reading an IMPORT as a location: `guarantee_probe_corpus_witness` imports the three probe ids for a roster assertion, and I took that for where the probes run; they run in `test.claim.direct_call_argument_type_witness`, a separate file. An import is evidence of visibility, never authority for where a name lives. **What survives is a different and sharper finding.** That file executes because it declares `SubstrateInputsOnly` while calling `compile_dag_diagnostic_census` — the same declaration `gunbc.compile_diagnostic_census`'s own live-tree note already adjudicated as a MIS-declaration when it found `transport_script_wall_compile_red_test` doing it (that census walks `build_module_path_index_from_witness_roots`, i.e. the live checkout). So the specimen population for that mis-declaration is now TWO, the second authored on 2026-08-22 after the first was adjudicated, and both are the only reason any census-compiling probe executes at all. Either these files' declaration is wrong or that authority's note is; they cannot both be right, and which one it is decides the size of §11 item 28's population. That is a question for the arm's owner, not a defect in this row's measurement, which stands. **SEAM (2) IS NOW CLOSED, AND CLOSING IT ENUMERATED TWO MORE — the count is FIVE measured, still not the total (gunbc#8876, 2026-08-22).** **OWNERSHIP, STATED PER SEAM BECAUSE THE CLASS NOW SPANS TWO LANES AND NEITHER CAN CLOSE IT ALONE:** seam (1) is the exemption-gated direct-call seam owned by the paragraph immediately preceding this one, whose next trigger is recorded there as DECLINED rather than pending; seams (2) through (5) belong to the field-inhabitance lane (snappy-tern-856). A lane that lands its last seam will be tempted to close this row. NEITHER MAY: 'my seams are done' is not 'the class is closed', and the row closes only when every seam does — including any seam not yet enumerated. The record-literal FIELD seam is walled: `v1.compiler.infer` `coproduct_payload_where_parent_required` refuses a value whose type is one of the declared coproduct's own variant payload types, consulting `transparent_alias_identity_agrees` over the `SymbolIndex` so an alias-mediated producer is caught too. Rung at that seam: **structurally guaranteed** — no `Accepted` program contains the state there. NOT structurally impossible, because the bad literal is still writable and the compiler refuses it; and NOT the class, which is why the two rows below exist. Evidence, enrolled permanently per §4b(4): `test.claim.coproduct_payload_soundness_witness_test` — the direct RED, the alias-mediated RED, and the positive control that stops a refuse-everything compiler from satisfying either. Turning the wall on WAS the census: EIGHT live sites, none previously known, all repaired in the same change — `ContentHash` from `Fnv1a64Structural` at `materialization_provider_witness_test`, `heal_revalidation_witness_test`, `materialize_witness_test`, `v2.std.materialize` and `v2.workflow.operand_flow`; `LexRules` from `LexRuleSet` at two `src/v2/test/claim/manual` fold tests. **SEAM (3), UNWALLED AND DECLARED, owner the field-inhabitance lane: the module-scope `data` initializer.** `data X: ContentHash = content_hash(...)` stores the payload into a `ContentHash`-declared row and is NOT refused, because a `data` initializer is not a record-literal field. Rung: **below floor**, exactly as seam (2) was. Unguarded: every module-scope `data` row in the corpus. Trigger: the same conformance judgment applied at the data-initializer seam, which needs no new relation — the declared type and the initializer's inferred type are both already in hand there. **SEAM (4), UNWALLED AND DECLARED, owner the field-inhabitance lane, AND IT IS RANKED FIRST OF THE TWO: the list element.** `v2.workflow.locality_affinity` built consumer identities as `list_add_distinct_hash(xs: cs, v: content_hash(n: e.dependent))` — a raw payload into a `List`. Rung: **below floor**, and it does not fail loudly. Measured: repairing the comparands while that producer stayed raw turned FOUR `locality_affinity` witnesses to `Bool(false)` with NOTHING refused at compile time — a wrong answer discovered later, not a diagnostic. That is what makes it rank above seam (3), and the ranking is fixed by a RULE rather than by judgment (operator ratification, 2026-08-22): seam (3) admits a wrong value a correctly-built peer can still catch by comparison — harmful, detectable, recoverable — while seam (4) admits a wrong value AND DISABLES THE COMPARISON THAT WOULD HAVE CAUGHT IT. That is a silent wrong answer, which DESIGN places OUTSIDE the guarantee ladder and forbids outright rather than ranking low, so the two are in different categories and no population argument reaches across the line: a larger set of loud failures does not outrank a smaller set of silent ones. The ranking is a priority order for collisions, NOT a serial queue — seam (3) needs no new relation and may land whenever it is ready. Unguarded: every list, map and collection element position whose element type is a coproduct. Trigger: element-position conformance against the container's declared element type. **SEAM (5), UNWALLED AND DECLARED, owner the field-inhabitance lane: the declared RETURN type.** `fn f(x: Node) -> ContentHash { content_hash(n: x) }` returns the payload where the parent coproduct is declared and is NOT refused. Rung: **below floor**. Measured 2026-08-22 on the gunbc#8876 merge commit, with a liveness control in the SAME compile that produced exactly one diagnostic (the record-literal RED), so the silence is a measurement and not an untested assumption. HOW IT WAS FOUND IS WORTH RECORDING, because it says something about the enumeration itself: it was found by a MIS-WRITTEN PROBE — the author intended an alias-mediated FIELD case and wrote a return position by mistake. Four of the five seams in this row were discovered by accident or by a downstream red rather than by anyone enumerating positions, which is the standing evidence for #8868's instruction to assume a further seam. Unguarded: every declared return type whose type is a coproduct. Trigger: `declared_type_conformance_diags` already runs at this seam and already holds both the declared and the inferred type, so the distance is a payload-membership arm on an existing judgment, not a new walk. **DO NOT READ SEAM (2)'s CLOSURE AS THE CLASS'S.** One seam of four measured is walled; a reader who sees only 'declared-field inhabitance wall landed' will conclude the class is closed, and the next lane would then build on a guarantee covering a quarter of it. Neither seam (3) nor seam (4) nor seam (5) is closed by gunbc#8876, which deliberately did not widen to chase them. **THIS ROW'S CEILING CELL SAYS THE DISTANCE TO R2 IS "AN IF-STATEMENT PLUS A TRIAGE". THAT IS MEASURED FALSE FOR THE PAYLOAD-WHERE-PARENT SHAPE, AND THE CORRECTION MATTERS BECAUSE IT IS THE SECOND NECESSARY-CONDITION-STATED-AS-SUFFICIENT TRIGGER THIS ONE ROW HAS CARRIED (snappy-tern-856, 2026-08-22).** The cell reasons that `direct_call_arg_mismatch_diags` exists, is written, and is simply not called, so flipping `module_skips_direct_call_arg_check` off closes seam (1). Flipping it off is NECESSARY. It is not SUFFICIENT, and the discriminating measurement is a module the exemption never applied to in the first place: in an ORDINARY NON-`v2.*` module, where the guard is false and the judgment demonstrably runs, `c4_takes(o: 5)` against `fn c4_takes(o: EOuter)` REFUSES (`expected 'Coproduct(EOuter)', got 'Primitive(Int)'`) while `c4_takes(o: e_inner())` — the coproduct's own payload type — is ACCEPTED in the same compile. The judgment is live at that seam and misses this shape, so deleting the arm leaves it accepted. **Read the two facts together or the row misleads:** the exemption really does switch the judgment off for every `v2.*` caller (that half is unchanged and still below floor), AND the judgment it switches off would not catch this shape anyway. A reader who acts only on the first will delete the arm, watch the diagnostics, and conclude the seam is closed. **THE DENOMINATOR THIS ROW HAS LACKED SINCE IT WAS WRITTEN NOW EXISTS, and it is what makes the sentence above checkable rather than another anecdote.** The row has said "assume a third seam until someone enumerates them" through two revisions while the count grew from two to five BY ACCIDENT — four of the five were found by a downstream red or by a mis-written probe, never by anyone enumerating positions, which samples the reviewer rather than the population. The positions are now enumerated FROM THE GRAMMAR: every call site of `parse_type_expr` in `v1.compiler.parse`, which is the finite set of places the language attaches a declared type. That is **14 sites**, and all five previously-known seams FALL OUT of it as rows rather than having been seeded into it — the falsifier the enumeration was required to pass. The list element seam falls out only because a container's element type is reached as a TYPE ARGUMENT rather than as a declaration of its own, which is why nobody had named it as a position before. **METHOD, because "not refused" is worthless without it.** Each position carries three arms: the payload-where-parent shape, a KERNEL mismatch (`Int` where the coproduct is declared), and an UNDEFINED NAME. The third is the reachability control: if it refuses, inference REACHES that position, so a passing kernel arm establishes that NO TYPE JUDGMENT RUNS there rather than that the position went unanalysed. All seven reachability controls refused. Dispositions, measured: **refuses** — record/variant NAMED field (`parse_field`), and only because gunbc#8876 walls it. **Judgment runs, misses the shape** — fn parameter at the direct-call seam. **Not refused, no judgment runs** — container type argument (list element), variant POSITIONAL payload, fn declared return, module-scope `data` initializer, annotated `let`. **Not refused** — `as` cast. **Not reachable from a source value** — type-alias RHS, `uses` resource type, service `exit` and `response` types (the last two are the reconstruction path's, not this row's). **Not refused, no judgment runs** (measured after the first pass, closing the census at 14 of 14) — the callable-type RETURN position (`cb: fn(Int) -> EOuter` given a lambda whose body yields the payload) and the callable-type PARAMETER position (`cb: fn(EOuter) -> Int` called with the payload); both reachability controls refused, so both positions are analysed. Three of these positions were previously unknown: variant positional payload, `as` cast, and annotated `let`. **AND THE ENUMERATION FOUND SOMETHING WIDER THAN THIS ROW'S CLASS, WHICH IS DELIBERATELY NOT CLAIMED HERE.** `data c6b: EOuter = 5` and `fn c5b() -> EOuter { 5 }` are both ACCEPTED, with the reachability control proving both positions are analysed. That is not payload-versus-parent; it is a plain kernel value where a declared coproduct is required, which is the ordinary-floor invariant DESIGN §4b names beside name resolution and exact-bijection binding. On the measured census that is **seven of fourteen grammar-admitted positions accepting a kernel value where a declared coproduct is required** — variant positional payload, fn declared return, module-scope `data` initializer, container type argument, annotated `let`, callable-type return, callable-type parameter — with the single refusing position owing its refusal to a PR that is held at the time of writing. (The count was first published as FIVE of fourteen, before the two callable-type positions were measured; it is corrected here rather than left standing, because an understated denominator on a floor breach is the same defect as an overstated rung. The `as` cast is deliberately not in the seven: it was never given a kernel arm, since a cast is an authored assertion and whether a kernel-to-coproduct cast should refuse is a different question this census did not ask.) This row's class is one INSTANCE of that breach rather than the breach itself, so the finding is routed for its own §4b row and its own owner rather than absorbed here — recording it inside this row would repeat the mistake this correction exists to fix, by making a wider unwalled invariant look like a seam of a narrower one **THAT WIDER BREACH NOW HAS ITS OWN OWNER AND FOUR OF ITS SEVEN POSITIONS ARE WALLED (2026-08-24, the declared-type-inhabitance lane).** Scope, stated first because the class and this row's class are neighbours that will be merged by anyone reading quickly: the subject is A PLAIN KERNEL VALUE (`Int`, `String`, `Bool`) where a declared record or coproduct is required — NOT a coproduct payload where its parent is required, which is this row's seam (2) and is separately walled. MEASURED BEFORE, on the pre-change binary, one fixture per position with an undefined-name reachability control beside it: all SEVEN positions compiled `0 diagnostics` and EMITTED 9 files (fn declared return, module-scope `data` annotation, annotated `let`, container element, variant positional payload, callable-type return, callable-type parameter); every reachability control refused (`function 'no_such_name_at_all' not found in scope`), so the silence measured an absent judgment rather than an unanalysed position; and the record-literal NAMED field refused (`expected 'Coproduct(KOuter)', got 'Primitive(Int)'`), which is what identified the relation that already existed. MEASURED AFTER, same fixtures, same flags: the declared return, the `data` annotation, the annotated `let` and the container element REFUSE with a located `TypeMismatch` (`expected 'Coproduct(KOuter)', got 'Primitive(Int)'`; the element position as `expected 'Container(List,Coproduct(KOuter))', got 'Container(List,Primitive(Int))'`); the conforming spelling at all four positions still compiles `0 diagnostics`; the named field refuses identically, which is the control proving the reused relation has not forked; and `fn f() -> KInner { 5 }` — a RECORD rather than a coproduct — now refuses too (`expected 'Product(KInner)', got 'Primitive(Int)'`), so the wall is the declared-type class and not a coproduct special case. NO SECOND RELATION WAS MINTED (DESIGN §3): `kernel_value_declared_type_mismatch` was already the corpus authority for this judgment and was consulted at exactly one of the fourteen positions; what landed is its peeling prologue lifted into `declared_type_conformance_diags`, so the fn return, the early `return`, the `data` annotation and the newly-wired annotated `let` all widen with that gate rather than beside it. FALSE-POSITIVE CENSUS, AND ITS FIRST STATEMENT HERE WAS WRONG ABOUT ITS OWN DENOMINATOR — corrected in place because the error is the instructive part. The regen corpus compile (`dag` + `src/v2`, `first_generation_equal=true`, `planned=133 executed=133`) reports zero hard diagnostics under the wall, and this row first read that as 'no live site was repaired'. The required floor then refused: its prepared subject resolves **3872 modules**, including `src/v2/test/**`, which the regen closure does not reach, and the wall found **six live sites in one file** — `src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test` declared six octet fixtures and one function parameter as `List` while holding integer literals (`[0, 255, 255, 255, 255]`) and forwarding them to `v2.compiler.emit_host` `emit_host_octets_byte_string`, whose declared parameter is `List` and which builds each `Byte` itself. `Byte` is a record over `List` and no `Int -> Byte` cast rule exists, so every one of those declarations was a lie that no consumer contradicted — the latent shape this row's originating incident already names, at the element position the wall now judges. Repaired to `List` (the entry then compiles with 0 blocking diagnostics), which makes TURNING THE WALL ON the census, exactly as gunbc#8876's field seam was. THE GENERAL LESSON, worth more than the six sites: a green whole-corpus compile is scoped to ITS OWN closure, and quoting it as 'the corpus' silently excludes whatever that closure omits; the floor's prepared subject is the wider denominator and disagreeing with it is how the gap was found. Zero further live sites were found beyond that file, which is a fact about this class's live population and not evidence that the other three positions are empty. RUNG: the four walled positions are **structurally guaranteed** (the bad value is still writable and the compiler refuses it); the class as a whole stays **below floor**, because three positions still admit it. STILL OPEN, each with its trigger, and NONE of them closed by this change: (a) the VARIANT POSITIONAL PAYLOAD — `KHeld(5)` routes through `infer_variant_constructor_call` into `infer_record_lit` under the synthetic field name `0`, and the declared type of that positional slot does not reach the field-conformance seam the NAMED field reaches; trigger is that slot resolving to its declared payload type there. (b) and (c) the CALLABLE-TYPE RETURN and PARAMETER — a lambda's body against `fn(Int) -> KOuter`, and an actual against `fn(KOuter) -> Int`; both reachability controls refused, so both positions are analysed and neither carries the callable's own declared component types into a conformance judgment; trigger is threading each callable boundary's declared parameter and return through the same relation, which is also what `explicit_return_conformance_note` names as its lambda narrowing. A NESTED container (`List>`) is likewise not judged: the element peel is ONE level, which is the depth measured, and deeper is unmeasured rather than covered. Enrolled evidence, permanent per §4b(4): `test.claim.declared_type_kernel_inhabitance_witness_test` — four discriminating REDs, the already-closed named-field RED as the no-fork control, and one positive control carrying the conforming spelling at all four closed positions so a refuse-everything compiler cannot satisfy them **A THIRD SEAM, MEASURED 2026-09-01 (eager-hawk-376), AND IT IS NOT A SEAM AT A POSITION — IT IS A PROPERTY OF THE DECLARED TYPE.** The row above says to assume a third seam exists until someone enumerates them; this is one, and it is orthogonal to (a)/(b)/(c), which all vary the POSITION while holding the declared type ordinary. Here the position is the already-covered one and the DECLARED TYPE is bodyless: **any `type X` declared with no body admits any argument in parameter position, silently.** Receipt, four fixtures in an ORDINARY (non-`v2.*`) module, so seam (1)'s `module_skips_direct_call_arg_check` exemption is not in play, against a binary carrying main's semantics: `fn takes(x: Compose>) -> Int` given a `String` — ACCEPTED, zero diagnostics naming the file; the same with a bare `Phantom` parameter — ACCEPTED; with a locally declared `type Opaque` and no `Phantom` anywhere — ACCEPTED; and the control `type MyRec = Word8`, an alias to a record — REFUSES with both `type mismatch: expected 'Primitive(MyRec)', got 'Primitive(String)'` and the paired inhabitance diagnostic. **The control is what makes this a finding rather than a silence: the judgment RUNS in that module and admits, which is a different mechanism from seam (1), where the judgment never runs.** It is not `Phantom`-specific and not `Compose`-specific — both were the obvious readings and both are refuted by the third fixture. POPULATION: 69 bodyless declarations corpus-wide, including `std.constructors` `Phantom`, `Product` and `Coproduct`, and `std.machine_constraints` `MachineWidth` / `PointerWidth`. **That 69 is the SYNTACTIC population and an upper bound on nothing else** — a bodyless type never used in parameter position cannot exhibit the hole, so the exposed subset is smaller and unmeasured. A naive line-oriented count returns 5227 because the multi-line coproduct spelling (`type X` then `= A \| B` on the following line) reads as bodyless; re-derive rather than quoting either number. Rung: **below floor** — a value that does not inhabit its declared type is accepted, in an ordinary module, with the judgment live. Ceiling: **R2** — membership is decidable from the declaration, since the refusing control proves the comparison seam already reaches this position and already has both types in hand. **NOT ENROLLED**: no probe asserts this, so nothing reds if it changes; the fixtures above are reconstructable but were deleted with the worktree. Next trigger, at capability grain rather than artifact grain per §4b(3): *the conformance seam decides a bodyless declared type by a stated rule — admit-nothing-but-its-own-constructions, or a declared and typed opacity — rather than by falling through*, with the four fixtures above enrolled as the discriminating REDs and the alias-to-record case kept as the no-fork control. **A SECOND, INDEPENDENT DEFECT FOUND IN THE SAME PASS, RECORDED HERE BECAUSE IT IS THE INSTRUMENT THAT WOULD OTHERWISE BE CITED AS THIS CLASS'S CENSUS:** `tools.opaque_realization_census` `declaration_body_standing_in` decides opacity from the `type X` line alone and carries the annotation *"No such spelling occurs in this corpus today, so the reading is exact for the corpus it is run over"* about the multi-line body form. **That premise is false by 5269 declarations**, every one of which the function classifies `DeclaredOpaque`; and separately it matches the declaration by bare prefix, with no name-boundary check, so a longer same-prefix name declared EARLIER in the file decides a shorter name's standing — 304 such pairs, e.g. `Userset` shadowing `User` in `extdeps.access.zanzibar`. Both are read from the function, not from its annotation. **THE ANNOTATION IS THE FINDING, AND DESIGN §4c ALREADY NAMES ITS SHAPE:** an annotation is never evidence that a machine claim holds, because no `Accepted` program can read one. This one does not merely rot — it CERTIFIES the exact trap its function falls into, so a reader doing the diligent thing and checking whether the author considered the continuation form finds a sentence saying yes. It is therefore a receipt for §4c's rule and not only a defect in one census. **Of the two, the bare-prefix bug ranks first for repair**, because they fail differently: the continuation misclassification is systematic and one control exposes it, while `Userset` deciding `User`'s standing is silent, name-dependent, and yields a different wrong answer according to declaration ORDER within a file — so it survives a fix of the continuation reading alone, and 304 pairs is enough that such a fix would look correct on a spot check. The census gates nothing today, so this is a wrong instrument rather than a wrong wall — but it is the instrument this row's population question would be handed to. | | Direct-call argument TYPE conformance — **transparent-alias identity**, v2 corpus | **R2 built and approved for the alias-identity class (gunbc#8873 — OPEN, approved, mergeable as of 2026-08-22; NOT merged, and this row must not be read as landed until it is).** A precomputed transparent-alias identity relation, derived once at census build and consumed as a `String -> String` map lookup per comparison, admits two names that alias the same declaration and refuses everything else. It peels ONLY `type A = B` with zero params, no connective, no children, no properties and no type annotation, and a target with zero children/params/annotation and `return_cardinality == Required` — so brands, `sole_constructor` carriers, refinements, coproduct arms and applied generics are all excluded BY THE ADMISSION TEST rather than by a later filter. Cost bar was declared before implementation and measured after: four crossed A/B pairs, +2.0s on a 454s regen (+0.4%) against per-arm spreads of 29.9s and 40.9s — a measured null. **What it does NOT do is create substitutability: it makes an existing fact visible.** A pre-relation binary already accepts `CommitSha` at an `AttemptKey` formal and already refuses `IntKey` there | R2 for this class. R3 is not reachable at this seam and that is a property of the seam, not of the relation | **The residual population is a DIFFERENT class and the distinction is load-bearing.** Measured 2026-08-22 against the exemption-deleted corpus: 67 refusals, silent-badger-817's CI run 32562740527 at commit `d42bb3eb57c`. **Provenance caveat, stated because it changes what the 48 means:** that tree merged this relation at `9bfd5388c03`, TWO COMMITS behind head `c40ab2d8248`, and the intervening `b0f72158c80` ("Qualify alias targets at census-build time") is exactly the commit that decides the `CoreNode` group — those refusals turn on `Node` being ambiguous by BARE name. So the 67 is a measurement of an OLDER revision of this relation, not of a broken copy of it. Classification of those 67, derived from declarations and independent of any binary: 48 are this alias class; 8 are applied generics (row below); 11 are `Optional` against `String`/`Bool`/`Int` in `v2.extdeps.github.gha_fold_pilot_emit` and are NOT an alias class at all. **The 48-cleared half is verified on 5 specimens, not 48:** at head, with the exemption deleted in the mirror and `exempt=judged` on all 20352 ledger rows, the five comparisons that CI reports as errors in `00_compile.dag` (lines 319, 342, 408, 446, 497) are all present in the ledger and all read `Compatible`. The remaining 43 sit outside that entry's import closure and a whole-corpus re-run against head was in flight when this row landed — treat 48 as classified-and-partially-verified, never as measured. **Also NOT the alias class: the 11** — the diagnostic reads got `Primitive(String)`, so the optional marker is already gone upstream at pattern destructuring and no comparison-seam mechanism can reach them. That 11 was carried as alias residue by two independent sessions and by this lane's own framing; it is recorded here so it is not handed forward under a label that guarantees the next attempt fails. **Open question for whoever takes it, to be CHECKED rather than inherited from this row:** an optionality marker erased at destructuring means a value reaches a position whose declared type it does not inhabit, which is the same floor rule as the direct-call seam census (record-literal walled; data-initializer and list-element open). If Group C is a FIFTH seam of that class it belongs on that row and not on a new one — decide that before minting a class for it. **A second mechanism, `unanimity`, was designed, measured and ABANDONED as unsound, not deferred.** Its specimen and refutation are carried on the seam-split row above and are deliberately NOT restated here — one fact, one authority | gunbc#8873, 9 enrolled floor witnesses in `dag/test/claim/transparent_alias_identity_witness_test.dag` including the over-peel boundary (`IntHandle` at a `String` formal), a coproduct-projection climb, and a blast-radius pair whose Int-alias discriminator refuses. Shadow ledger re-run before the exemption was touched: 20527 rows, all 115 `WouldDiagnose` rows one mechanism. Receipt: `docs/probes/transparent_alias_identity_2026-08-22/README.md` — **FORWARD REFERENCE, NOT A PRESENT FACT:** that receipt lands with gunbc#8873, which is open at the time this row merges. Do not cite it as evidence until that PR is in | the `v2.` exemption arm cannot be deleted while the applied-generic class below still refuses 8 live sites; the exemption is NOT narrowed to those modules (a narrowing would be a shape test correlating with the distinction rather than naming it) | | Direct-call argument TYPE conformance — **applied-generic alias**, v2 corpus | **Below floor — 8 live false refusals, structurally unreachable from the comparison seam.** An alias whose right-hand side is a generic application (`type BlackConfigPatch = ConfigPatchRecord`) refuses at every call site passing it to the matching formal. Specimen, measured by execution 2026-08-22 on a fixture diffed byte-for-byte against the live `v2.std.patch` declaration, with the exemption deleted in the Rust MIRROR and `exempt=judged` on all 20352 ledger rows as the control: `formal_type = Primitive(ConfigPatchRecord)`, `actual_type = Node(BlackConfigPatch)`, `nominal=true container=false kernel=false`, `fname=ConfigPatchRecord aname=BlackConfigPatch`. Population: 9 declarations, all under `src/v2/extdeps/formatters/` (`black`, `clang_format`, `gofmt`, `google_java_format`, `ktfmt`, `lean4_format`, `prettier`, `rustfmt`, `swift_format`), of which 8 produced diagnostics in the CI arm — `lean4_format` is structurally identical and produced none in EITHER arm, so the population is 9 and the measured count is 8+k | R2, and it is decidable — the same equality already accepts the applied form when it is written directly at the formal | **THE FORMAL SIDE IS WHERE THE INFORMATION DIES, and that is the sentence that should stop the next attempt from this direction.** The formal is DECLARED `ConfigPatchRecord` and REACHES the comparison as the bare constructor, with the type argument already discarded. So the equality has one side that structurally cannot hold an argument, and the case split over any representative is EXHAUSTIVE: (a) representative = the applied form with every argument retained never equals the bare constructor, so it admits nothing and all 9 sites keep refusing; (b) representative = the bare constructor admits `ConfigPatchRecord` at `ConfigPatchRecord` for any X and Y, which is exactly the over-peel that erases the distinction. There is no third representative, and widening the carrier does not help — a node-valued map fails identically, because the missing information is not on the relation's side of the map. **Not to be confused with gunbc#8879**, the withdrawn repair that widened transparency AT RESOLVE and was refused by CI in three classes at once (20 direct-call comparisons, 18 variant projections, 3 files of regen drift). What that established is that resolve is the wrong place for a transparency JUDGMENT; preserving an applied form is resolve DISCARDING LESS, which hands the same consumers MORE structure, and is a different claim that has not been measured | executed fixture + shadow ledger with a positive control (`black.dag` must refuse; a zero there is decidably wrong). **NOT ENROLLED**: no probe pair asserts this class, so nothing reds if it changes. Three false zeros were produced while measuring it — twice from patching the `.dag` authority while the binary is built from the emitted Rust mirror, once from a run that PANICKED and reported zero diagnostics — each caught only by a positive control or by another session's raw per-line export, never by an aggregate | **RESOLVE CARRIES APPLIED FORMS AT THE FORMAL POSITION.** Explicitly NOT scoped as of 2026-08-22 (operator-lane ruling, swift-badger-524): a bounded floor-recovery lane whose completion condition has moved is closed honestly rather than extended, and nothing in that ruling says the change is wrong. Until it lands, the `v2.` exemption stays whole and gunbc#8886 stays blocked | | Direct-call argument TYPE conformance — **container element**, non-exempt module; and the witness family that reported it was **rung INFLATION** (DESIGN §4b(1) — *not* §4b(3): nothing regressed, the wall was never there, so "restore the previous behaviour" is not the remedy and a regression row would have read as authorising it) | **Below floor — the container-element judgment does not fire at a direct call argument.** Measured 2026-08-27 with the witness's OWN oracle (`compile_dag_rust_emit_check`) alongside `compile_dag_diagnostic_census`, over two corpora in two remote dispatches: `main` @ `ddb7f533e4e` and gunbc#9428's head. A fixture handing `FreeMonoid` to a declared `FreeMonoid` parameter — locally declared record, corpus-unique wrapper name, no `Node`, no `v2.std.node`, no occurrence identity anywhere in it — **compiles clean ON `main`**, 0 blocking; the argument surfaces only as advisory `DeclaredTypeInhabitanceUndecided` at "direct call argument". Distinct from the `module_skips_direct_call_arg_check` row above: that exemption keys on the CALLER's module name and this fixture's module is not `v2.`-prefixed, so the judgment is not switched off here — it is written, reached, and answers no. **THE INFLATION:** the class read as mechanically preventable on the strength of `test.claim.record_literal_call_arg_handoff_witness.record_literal_container_element_mismatch_at_call_arg_still_refuses` being green. That witness was green on an UNRELATED defect in its own closure — `v2.std.node` referenced `std.occurrence_identity.OccurrenceId` and `ScopedOccurrenceRef` fully qualified WITHOUT importing that module, so every closure importing `v2.std.node` inherited two `UnresolvedType` diagnostics and refused for that reason; measured on `main`, the fixture's refusal is exactly `UnresolvedType/std.occurrence_identity.OccurrenceId` ×2 + `ScopedOccurrenceRef` ×1, and contains no type-mismatch diagnostic at all. gunbc#9428 adds the import, those resolve, and the accidental refusal goes with them. **A witness green on a defect in its own closure is not weak coverage, it is NEGATIVE coverage** — it is cited as evidence the wall is live, so the class never ranks for climbing. That is DESIGN §4b's worse-than-absent case reached from a direction the document does not yet record: not an unauthorable RED, but an AUTHORABLE one satisfied by the WRONG CAUSE, which no reader of the witness can distinguish from the right one. The nominal sibling `record_literal_nominal_mismatch_at_call_arg_still_refuses` stays green through a DIFFERENT path (`literal_introduction_type_mismatch`, whose actual is a record LITERAL rather than a call), which is why the family read as coherent and was not | R2 (two distinct nominal element types under one container template is a decidable comparison the seam already reaches) | `container_element_nominal_brand_mismatch` is written and IS reached from `direct_call_arg_type_mismatch`, but it delegates to `nominal_call_arg_brand_mismatch`, which requires `structural_carrier_template_name(formal_el) == structural_carrier_template_name(actual_el)`; that name falls through `canonical_template_name` to the element's own authored name for any non-container type, so two DISTINCT nominal element types can never satisfy the conjunct that the mismatch arm needs. **Stated as a CODE READ, consistent with the measurement but not independently executed** — what is executed is that the compile is clean, not which conjunct declined | Measurement above (both corpora, `emit_check` + census). **Instrument not committed:** a throwaway cargo example over the two `pub` entry points in `cli_run`, kept out of the tree per the no-ad-hoc-script rule; re-deriving it needs a `.dag` entry point, which is this row's standing "name the instrument" debt | `container_element_nominal_brand_mismatch` reaching the direct-call-argument position — i.e. `nominal_call_arg_brand_mismatch` admitting distinct nominal element types under a shared container template. The witness is the ready-made RED and needs no new fixture; it is enrolled as expected-red in gunbc#9428, where it FAILS (on `main` it still passes on the accident, so enrolling it here would trip the roster's stale-quarantine arm and red main's own floor) | From e1d64c427a847b805b87739a9cdbefa8bfd36535 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 04:12:15 +0000 Subject: [PATCH 5/5] Name the enrollment decision: the RED is authorable now, so unenrolled is a choice MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit test.claim.declared_type_expected_type_path_witness landed on main tonight and compiles caller-authored source strings through gunbc.compile_diagnostic_census, asserting on census_ran plus a blocking refusing-count rather than on a diagnostic spelling. The four fixtures in this row are ordinary source strings, so that harness can express them. §4b says declining enrollment where the RED is authorable is specification-without-execution, so the row may not simply say NOT ENROLLED and stop. It now says why: the seam ADMITS today, so the assertion is red on main and enrollment needs a floor_expected_red row -- a roster another lane edited the same night, and a decision about the required gate rather than about this class. Named as the immediate next step with an owner, so the gap stays countable instead of quietly permanent. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_013wJU7jqGAEk8rj4UwpHdox --- docs/plans/compiler-guarantee-recovery-gap-analysis.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index 0fa8cd1be4b..4b84a86436d 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -170,7 +170,7 @@ unless the row says otherwise, and `Unknown` is the honest default. | Closed-match exhaustiveness | **Path-split, measured 2026-08-01 — the class is not one rung.** Coproduct-typed scrutinee: **R2** (a missing arm on a declared closed variant refuses `NonExhaustiveMatch`, blocking, naming the absent variant). Type-variable scrutinee: **below floor — silent** (`fn pick(t: T) -> Int { match t { Red => 1 } }` compiles with zero diagnostics — one arm, an unconstrained subject, and a variant belonging to an unrelated type). Class rung is the minimum, so **below floor** | R3 (full arm population at elimination) | the silent arm is `PatternDynamic { span: _ } => []`, **not** `PatternLookupBlocked => []` as this row previously said — `pattern_subject_from_node` reaches `PatternLookupBlocked` only when the scrutinee's inferred type `is_compiler_error`, i.e. where a diagnostic already exists, so that arm is not the silent one and its silence is **not** established by these probes | first measured by a one-off execution 2026-08-01 via `compile_dag_diagnostic_census` on the v1 CompileAccept path (source and result in the §10 eighth-pass ledger), and **AUTHORED AS A PROBE PAIR 2026-08-22 — AUTHORED, NOT EXECUTING, AND THE DISTINCTION IS THE WHOLE POINT** (see §11 item 28): the measurement is now written as `test.claim.guarantee_floor_class_probe_witness` `floor_exhaustiveness_on_a_type_variable_scrutinee_is_still_silent`, against the registry row `gunbc.guarantee_probe_corpus` class `floor-closed-match-exhaustiveness`, with the coproduct-scrutinee arm already enrolled at `test.claim.match_exhaustiveness_coproduct_witness` `w_missing_coproduct_arm_reports_one_non_exhaustive`, on the same harness and the same floor run — not re-authored here, because a second copy would be a second authority for one fact as its probe-adequacy control. **It does not run in CI.** The witness declares `ReadsLiveTree` — truthfully, because `compile_dag_diagnostic_census` resolves its synthetic source against the live checkout — and the required floor DECLINES every `ReadsLiveTree` module before the fold sees it (`v2.workflow.required_floor` `RequiredFloorDisposition` `DeclinedLiveTree`), so the probe is discovered and never executed, exactly like the five guarantee carriers §11 item 28 counts. It is green by execution LOCALLY (`gunbc run --claim-run`, 2026-08-22, this session) and that is a strictly weaker fact. So this cell's rung is unchanged from the day before the probe was authored: it still rests on a measurement nothing re-runs. What the probe pair buys is that on the day the decline arm is deleted the measurement becomes standing evidence with no further authorship. Trigger: the `DeclinedLiveTree` deletion (§11 item 28), NOT this cell (§4b meta-obligation 4; the original gap was codex review 46306, §11 item 10) | `ExhaustivenessUnknown` refuses on the dynamic subject | | Record completeness | **R2 measured 2026-08-01** (a record literal omitting a declared required field refuses `MissingField`, blocking, naming the field and type — the class was carried as `Unknown — unmeasured` and the measurement raises it) | R3 | judgment is per-literal; construction-side and generic-instantiation completeness are separate and the latter measures **below floor** in the row above | first measured by a one-off execution 2026-08-01 via `compile_dag_diagnostic_census` on the v1 CompileAccept path (source and result in the §10 eighth-pass ledger), and **AUTHORED AS A PROBE PAIR 2026-08-22 — AUTHORED, NOT EXECUTING, AND THE DISTINCTION IS THE WHOLE POINT** (see §11 item 28): the measurement is now written as `test.claim.guarantee_floor_class_probe_witness` `floor_record_completeness_missing_field_refuses_blocking`, against the registry row `gunbc.guarantee_probe_corpus` class `floor-record-field-completeness`, with `floor_record_completeness_green_control_is_clean` as its probe-adequacy control. **It does not run in CI.** The witness declares `ReadsLiveTree` — truthfully, because `compile_dag_diagnostic_census` resolves its synthetic source against the live checkout — and the required floor DECLINES every `ReadsLiveTree` module before the fold sees it (`v2.workflow.required_floor` `RequiredFloorDisposition` `DeclinedLiveTree`), so the probe is discovered and never executed, exactly like the five guarantee carriers §11 item 28 counts. It is green by execution LOCALLY (`gunbc run --claim-run`, 2026-08-22, this session) and that is a strictly weaker fact. So this cell's rung is unchanged from the day before the probe was authored: it still rests on a measurement nothing re-runs. What the probe pair buys is that on the day the decline arm is deleted the measurement becomes standing evidence with no further authorship. Trigger: the `DeclinedLiveTree` deletion (§11 item 28), NOT this cell (§4b meta-obligation 4; the original gap was codex review 46306, §11 item 10) | required-field construction at every construction form | | Parse: list separator dropped | **Below floor — silent** (measured: `[ {a}, {b} {c} ]` compiles with zero diagnostics — a dropped comma is a silent semantic change, two- vs three-element list; survived regen, whole-corpus compile, fixed-point verify and a 15-case matrix, caught only by a human diff read) | R3 (decidable grammar fact) | separator omission parses as element juxtaposition | First measured by tidy-deer-730's throwaway probe on gunbc#7484 + review 45347, 2026-07-31. **PROBE PAIR AUTHORED 2026-08-22, NOT EXECUTING** (§11 item 28 — the witness is declined by the floor's `DeclinedLiveTree` arm and runs only under a local `gunbc run --claim-run`): `test.claim.guarantee_floor_class_probe_witness` `floor_parse_list_separator_omission_is_still_silent` re-executes it on every required-floor run against `gunbc.guarantee_probe_corpus` class `floor-parse-list-separator`, with `floor_parse_list_separator_doubled_separator_control_refuses` (a DOUBLED separator in the same position refuses `ParseError`, blocking) and `floor_parse_list_separator_green_control_is_clean` as its probe-adequacy controls, all three green locally and none of them executing in CI — so the omission's silence is measured against a parser that demonstrably refuses malformed separators | the probe pair is now in the corpus and pins the hole; what remains is the refusal in the list production (§11 item 6), on which the enrolled probe flips RED and its row is rewritten as `ExpectBlockingRefusal` | -| A value that does not inhabit its declared type is accepted — **seam-split, enumeration UNFINISHED** (was filed as "Direct-call argument TYPE conformance, v2 corpus"; renamed 2026-08-22, see the trigger cell) | **Below floor — the judgment never runs.** Not a hole a bad value slipped through: `v1.compiler.04_infer` gates `arg_compat_diags` on `module_skips_direct_call_arg_check(module_name: scope.module_name)`, which returns true for every module whose name begins with `v2.`. The key is the CALLER's module, so the entire active v2 corpus — compiler stages, extdeps, std, witnesses — has the direct-call argument-type judgment switched off. Measured consequence, 2026-08-22: `v2.extdeps.languages.dag` `dag_int_literal_node_from_lexeme` / `dag_int_literal_node_from_magnitude` declared `occurrence_id: OccurrenceId` since gunbc#6558 while storing that parameter straight into `Node.occurrence_id`, declared `NodeOccurrenceId`. For two months 15 call sites passed `SyntheticOccurrence` (a NodeOccurrenceId, contradicting the declaration) and nothing complained; gunbc#8833 made one call site OBEY the declaration and nothing complained about that either. The error surfaced only as an interpreter `non-exhaustive pattern match on: OccurrenceId { value: 79 }` across 16 witnesses, reddening main. **The inversion worth naming: a declaration that lies is inert while every caller contradicts it in the same direction, and detonates on the first caller who takes it at its word.** So the at-risk population is not "callers who got it wrong" but callers who might get it right — a genuinely counterintuitive census. Note this is the TYPE judgment only; the SHAPE judgment (`direct_call_shape_diags`, labels/arity) is exemption-free and does fire | R2 (a declared parameter type is a decidable conformance check the seam already computes — `direct_call_arg_mismatch_diags` exists, is written, and is simply not called, so the distance to the next rung is an if-statement plus a triage, not an implementation) | **THIS ROW IS A CORRECTION TO DESIGN §4b, NOT A NEW OBSERVATION BESIDE IT — read them together or the first will look like it already settled this.** DESIGN §4b names this exact symbol and reports that it "was found (code read, not execution) to be scoped entirely to the direct-call argument-type judgment and does not reach `sole_constructor`'s construction check at either call site — a positive finding that retires this axis, not an absence of any exemption anywhere." That finding is correct and is not disputed here. The question it asked was whether the exemption LEAKS into `sole_constructor`; the question it never asked is what the exemption COSTS inside the judgment it is scoped to. "Scoped entirely to the direct-call argument-type judgment" reads as reassuring only until that judgment is measured, and it is the argument-type check for the entire active v2 corpus. **Confinement was measured and then treated as safety, and the axis that got retired was not the one that mattered.** Two facts about why the seam nonetheless reads as covered: the SHAPE judgment (`direct_call_shape_diags` — labels, arity, duplicate binding) is exemption-free and DOES fire over every module including the compiler's own sources, so half-live is more deceptive than dead — every casual check finds something working. And the arm is NOT unreasoned: `direct_call_shape_wall_note` states the TYPE judgment's false-positive classes are representation gaps (brand aliases, optionality's two forms, anonymous literals, expansion depth — the conformance wall's four measured classes), which is a real stated reason and is why this row asks for a measurement rather than a deletion. What is unmeasured is whether those classes still fire in v2 today and at what rate. The neighbouring compiler-module arm of this same exemption was deleted in place after being found never to have been in force; the `v2.` arm was left standing at that moment without separate justification of its own | This incident, measured end to end: CI run 32542017600 (main, 67437fcbe9) 16 FAIL with the raw-`OccurrenceId` match error; caller census of both functions read at call grain (17 sites: 15 `SyntheticOccurrence`, 1 `node.occurrence_id`, 1 internal pass-through, 1 raw `minted.id`); exemption mechanism read at `v1.compiler.04_infer` `module_skips_direct_call_arg_check` and its single call site gating `arg_compat_diags` on `scope.module_name`. **NOT ENROLLED**: no probe pair asserts this exemption's reach, so nothing reds if it changes | **THE TRIGGER THIS ROW SHIPPED WITH WAS INCOMPLETE AND IS CORRECTED HERE (2026-08-22, swift-badger-524 retracting their own ruling).** As merged in gunbc#8854 this cell named ONE closing condition — delete the `v2.` exemption — which is a NECESSARY condition presented as a sufficient one. The class is not "direct-call argument type conformance"; it is **a value that does not inhabit its declared type is accepted**, and it has at least TWO seams: **(1) direct-call arguments** — gated off for `v2.*` by `module_skips_direct_call_arg_check`, the mechanism this row measures; **(2) record-literal fields** — gated by NOTHING, below floor in ORDINARY NON-v2 MODULES, receipt gunbc#8865 (gentle-eagle-360). Its minimal pair, no compiler internals involved: `CppHolder { subject: CppWrapped { inner: cpp_inner() } }` accepted and correct, against `CppHolder { subject: cpp_inner() }` — a coproduct PAYLOAD inhabiting a field declared as its parent COPRODUCT — ACCEPTED BY TYPING and dying at runtime as `PatternMatchFailure`. A record literal is not the direct-call seam, so deleting the exemption would not close it. **SEAM (2) NOW HAS A LIVE PRODUCTION SPECIMEN, WHICH RANKS IT DIFFERENTLY FROM A SYNTHETIC PAIR** (gentle-eagle-360, 2026-08-22, found while checking for a second content-identity authority before building on one): `v2.std.materialize` declares `MaterializedNode.hash` as `ContentHash` — the subject-generic union — and `materialize_fold_step` stores `content_hash(n)` into it, which returns `Fnv1a64Structural`, the PAYLOAD carried inside the union's `Fnv1a64` arm. Receipt, by execution against the module as it stands on main: taking the value materialize ACTUALLY STORED and asking the union's own family authority `content_hash_family` about it yields `PatternMatchFailure { value: "Fnv1a64Structural { digest: 7ac77ab0e29c6bd8 }" }`; the probe's fallback was a correctly wrapped `Fnv1a64(...)`, so an empty result or a well-formed value would have PASSED and only a stored value can produce that red. **The defect is LATENT and that is the instructive part**: peer lookup compares `e.hash == h`, raw payload against raw payload, which agrees with itself — so every current path is green and the error surfaces only when a materialize hash is routed through the union's own machinery (`content_hash_family`, or `compare_content_hash`, which exists precisely to refuse cross-family collapse). That is the same shape as this row's own originating incident: **a declaration that lies is inert while every consumer contradicts it in the same direction, and detonates on the first consumer that takes it at its word** — here the first cross-family artifact to reach the carrier. Disposition ruled ARM A, wrap the construction (`MaterializedNode { hash: Fnv1a64(h), ... }`), NOT narrow the declaration: narrowing would sever `MaterializedNode.hash` from `RealizationPlan.target`, and §2's Realization spans resolve-cost, sccache and OS provisioning on ONE content hash, so a structural-only key could never name a realization of a fetched artifact or a provisioned image (swift-badger-524 ruling, 2026-08-22; handed to silent-bear-842 with the receipt, unfixed here because it is that lane's module). **THE SEAM ITSELF IS THE FINDING, not this one site**: gunbc#7480 corrected the design document for asserting the wrong type at exactly this `Hash`/`ContentHash` boundary, and a production module now carries the mirror-image error — a boundary documentation has to keep re-explaining is a boundary that wants construction. ****THAT HAND-OFF IS SUPERSEDED AND THE SPECIMEN IS REPAIRED — corrected in place rather than left standing, because the sentence above says a live production defect is UNFIXED and awaiting another lane, which is the present-tense claim a reader would plan against (gunbc#8876, 2026-08-22).** The wrap landed in the wall's own change by operator ruling: a wall and the repair it forces must land together, since with the wall on and the wrap absent main is red, so only one PR can contain both. `v2.std.materialize` `materialize_fold_step` and `distinct_hashes` now build `Fnv1a64(content_hash(n))`, and the same construction was repaired at four further sites the wall refused for the identical reason — `v2.workflow.operand_flow`, `materialize_witness_test`, `materialization_provider_witness_test` and `heal_revalidation_witness_test`. The receipt above stays as the historical demonstration that the defect was real and reachable; it is no longer a description of the tree. THE ENUMERATION IS UNFINISHED: two is what has been measured, not the count.** Assume a third seam exists until someone enumerates them; note that this row's own originating incident (#8854) reached its victim through a record literal one hop downstream of the direct call, so the two seams are not even cleanly separable at a site. **SEAM (1) WAS EXECUTED TO A MEASURED, BLOCKED STOP ON 2026-08-22 — the arm is NOT deleted, and this paragraph is the §4b row for that state rather than a plan.** Rung: **below floor, unchanged** — the judgment still does not run for any `v2.*` caller. Ceiling: **R2** (a declared parameter type is a decidable conformance check the seam already computes). Next trigger, stated as §4b(2) requires and with its disposition: *a formal parameter declared as an applied generic carries its applied form through resolution rather than reaching the comparison seam as the bare constructor* — **DECLINED at the owning layer on 2026-08-22**, on the ground that a bounded compiler-floor packet whose completion condition has moved should close and hand its residue forward rather than extend into a type-system project. A declined trigger is a legitimate §4b state; **a blocked class with no row is how this exemption survived years in the first place**, which is the reason this row exists at all. Enrolled evidence, so the class stays countable while blocked: `direct_call_arg_type_v2_module_red_probe` (the discriminating RED, rostered in `v2.workflow.floor_expected_red` — it cannot pass while the arm stands and PASSES on a tree with the arm deleted, so it is a satisfiable assertion held open by a named cause), plus two controls that pass on main today (`direct_call_arg_type_ordinary_module_red_probe`, the paired nonzero the exemption never covered; and `direct_call_arg_type_v2_green_control_probe`). **What was measured before the stop, and how to read it:** deleting the arm produces **285+k** blocking diagnostics and **67+k** with gunbc#8873 merged, for some k ≥ 1 unmeasured — these are ROSTER-RESOLVED counts, not corpus counts, and `src/v2/extdeps/formatters/lean4_format.dag:184` is the proof: a live site, structurally identical to eight that refused, contributing zero to *both* arms and therefore invisible to their difference. **Zero genuine call-site defects were found in the residue** — every diagnostic examined was a deficit in the type judgment, so no call sites were edited, because 67 mechanical edits would have cemented three compiler deficits permanently. The per-mechanism split of that residue is deliberately NOT recorded here: it was published as 48/11/8, and the rule the 48 were attributed to was then found to admit nothing in this corpus, so the attribution was retracted before it was cited. Trigger for the count to be restated: the residue re-measured with its `why` column. **The counterexample that retracted it is worth carrying on its own, because it will bite anyone who reaches for a name-keyed alias relation:** `type Float = Float64` is declared in BOTH `dag/std/float.dag:18` and `src/v2/std/float.dag:33`, spelling the target identically — but `dag/std/float.dag:16` has `type Float64 = Real64` (a transparent alias) while `src/v2/std/float.dag:30` has `Float64` as a **record**. So the two declarations agree on a *spelling* and disagree on a *type*, and a unanimity rule keyed on the target's NAME admits them as the same concept. Requiring the target itself to be census-unique closes it — and once closed, that rule admits nothing in this corpus, which is what falsified the attribution above. Found by still-carp-717 while building the rule, before it shipped. **The original trigger text, kept because the sequence it specifies was followed and the record should show what was attempted:** seam (1) — turn the exemption off for `v2.` behind a measured diagnostic count, triage, then delete the arm, the disposition the compiler-module arm received; the measured prerequisite is ALIAS TRANSPARENCY, because proud-ant-819's report-only shadow on the 03_ingest closure found 115 `WouldDiagnose` relations at 78 sites of which 115 reduce to a transparent `type A = B` (92 via `type Hash = Fnv1a64Structural`, 23 via the `Node` phase carriers), residue ZERO — so on that closure the exemption is currently suppressing false positives, not defects. Seam (2) — its own wall at record-literal field conformance; nothing to turn off, it was never on. **Closing seam (1) MUST NOT be read as closing the class**, which is the specific failure this correction exists to prevent: a class that looks like it has one closing condition gets closed when that condition fires. Two blind spots neither instrument covers, named rather than left to be rediscovered: production itself SKIPS an anonymous record literal standing as an ACTUAL at a direct call, so its argument type is never judged (521 relations, 2.7%, `Unadjudicated` in proud-ant-819's shadow — upstream of the guard, so invisible to a flip-off arm too); and a function storing into a field from its own differently-named parameter is this class at yet another site, which a callee-name-keyed census cannot see. **THAT FIRST BLIND SPOT IS NOT SEAM (2), AND THE TWO WILL BE MERGED BY ANY READER WHO DOES NOT SEE THIS SENTENCE** (caught by proud-ant-819, who put the mirror-image clause in their own row): both descriptions begin "a record literal" and name DIFFERENT POSITIONS. The blind spot is a record literal at an ARGUMENT position whose type goes unjudged at the direct-call seam — seam (1)'s territory, and a population of 521 relations. Seam (2) / gunbc#8865 is a record literal's FIELD whose value does not inhabit the field's declared type — a different seam with a different mechanism and no measured population. Reading them as one would make the 521 look like evidence for gunbc#8865, or gunbc#8865's receipt look like it bounds the 521. Neither is true. **A CLAIM ABOUT THIS ROW'S EVIDENCE WAS MADE HERE AND IS RETRACTED, MEASURED WRONG (2026-08-22, the §11 item 28 lane, retracting itself).** The retracted claim was that these probes sit in the declined `ReadsLiveTree` carrier and therefore never execute, so the expected-red enrolment could only be `not_evaluated`. **It is false, and the measurement that refutes it is the run that was supposed to confirm it:** run `32586093086` reports `[expected-red-roster-join] roster=207 still_red=207 now_passes=0 not_evaluated=0` with `known_red_held=207`. The v2-module red EXECUTES and is held still-red exactly as its row intends. The error was reading an IMPORT as a location: `guarantee_probe_corpus_witness` imports the three probe ids for a roster assertion, and I took that for where the probes run; they run in `test.claim.direct_call_argument_type_witness`, a separate file. An import is evidence of visibility, never authority for where a name lives. **What survives is a different and sharper finding.** That file executes because it declares `SubstrateInputsOnly` while calling `compile_dag_diagnostic_census` — the same declaration `gunbc.compile_diagnostic_census`'s own live-tree note already adjudicated as a MIS-declaration when it found `transport_script_wall_compile_red_test` doing it (that census walks `build_module_path_index_from_witness_roots`, i.e. the live checkout). So the specimen population for that mis-declaration is now TWO, the second authored on 2026-08-22 after the first was adjudicated, and both are the only reason any census-compiling probe executes at all. Either these files' declaration is wrong or that authority's note is; they cannot both be right, and which one it is decides the size of §11 item 28's population. That is a question for the arm's owner, not a defect in this row's measurement, which stands. **SEAM (2) IS NOW CLOSED, AND CLOSING IT ENUMERATED TWO MORE — the count is FIVE measured, still not the total (gunbc#8876, 2026-08-22).** **OWNERSHIP, STATED PER SEAM BECAUSE THE CLASS NOW SPANS TWO LANES AND NEITHER CAN CLOSE IT ALONE:** seam (1) is the exemption-gated direct-call seam owned by the paragraph immediately preceding this one, whose next trigger is recorded there as DECLINED rather than pending; seams (2) through (5) belong to the field-inhabitance lane (snappy-tern-856). A lane that lands its last seam will be tempted to close this row. NEITHER MAY: 'my seams are done' is not 'the class is closed', and the row closes only when every seam does — including any seam not yet enumerated. The record-literal FIELD seam is walled: `v1.compiler.infer` `coproduct_payload_where_parent_required` refuses a value whose type is one of the declared coproduct's own variant payload types, consulting `transparent_alias_identity_agrees` over the `SymbolIndex` so an alias-mediated producer is caught too. Rung at that seam: **structurally guaranteed** — no `Accepted` program contains the state there. NOT structurally impossible, because the bad literal is still writable and the compiler refuses it; and NOT the class, which is why the two rows below exist. Evidence, enrolled permanently per §4b(4): `test.claim.coproduct_payload_soundness_witness_test` — the direct RED, the alias-mediated RED, and the positive control that stops a refuse-everything compiler from satisfying either. Turning the wall on WAS the census: EIGHT live sites, none previously known, all repaired in the same change — `ContentHash` from `Fnv1a64Structural` at `materialization_provider_witness_test`, `heal_revalidation_witness_test`, `materialize_witness_test`, `v2.std.materialize` and `v2.workflow.operand_flow`; `LexRules` from `LexRuleSet` at two `src/v2/test/claim/manual` fold tests. **SEAM (3), UNWALLED AND DECLARED, owner the field-inhabitance lane: the module-scope `data` initializer.** `data X: ContentHash = content_hash(...)` stores the payload into a `ContentHash`-declared row and is NOT refused, because a `data` initializer is not a record-literal field. Rung: **below floor**, exactly as seam (2) was. Unguarded: every module-scope `data` row in the corpus. Trigger: the same conformance judgment applied at the data-initializer seam, which needs no new relation — the declared type and the initializer's inferred type are both already in hand there. **SEAM (4), UNWALLED AND DECLARED, owner the field-inhabitance lane, AND IT IS RANKED FIRST OF THE TWO: the list element.** `v2.workflow.locality_affinity` built consumer identities as `list_add_distinct_hash(xs: cs, v: content_hash(n: e.dependent))` — a raw payload into a `List`. Rung: **below floor**, and it does not fail loudly. Measured: repairing the comparands while that producer stayed raw turned FOUR `locality_affinity` witnesses to `Bool(false)` with NOTHING refused at compile time — a wrong answer discovered later, not a diagnostic. That is what makes it rank above seam (3), and the ranking is fixed by a RULE rather than by judgment (operator ratification, 2026-08-22): seam (3) admits a wrong value a correctly-built peer can still catch by comparison — harmful, detectable, recoverable — while seam (4) admits a wrong value AND DISABLES THE COMPARISON THAT WOULD HAVE CAUGHT IT. That is a silent wrong answer, which DESIGN places OUTSIDE the guarantee ladder and forbids outright rather than ranking low, so the two are in different categories and no population argument reaches across the line: a larger set of loud failures does not outrank a smaller set of silent ones. The ranking is a priority order for collisions, NOT a serial queue — seam (3) needs no new relation and may land whenever it is ready. Unguarded: every list, map and collection element position whose element type is a coproduct. Trigger: element-position conformance against the container's declared element type. **SEAM (5), UNWALLED AND DECLARED, owner the field-inhabitance lane: the declared RETURN type.** `fn f(x: Node) -> ContentHash { content_hash(n: x) }` returns the payload where the parent coproduct is declared and is NOT refused. Rung: **below floor**. Measured 2026-08-22 on the gunbc#8876 merge commit, with a liveness control in the SAME compile that produced exactly one diagnostic (the record-literal RED), so the silence is a measurement and not an untested assumption. HOW IT WAS FOUND IS WORTH RECORDING, because it says something about the enumeration itself: it was found by a MIS-WRITTEN PROBE — the author intended an alias-mediated FIELD case and wrote a return position by mistake. Four of the five seams in this row were discovered by accident or by a downstream red rather than by anyone enumerating positions, which is the standing evidence for #8868's instruction to assume a further seam. Unguarded: every declared return type whose type is a coproduct. Trigger: `declared_type_conformance_diags` already runs at this seam and already holds both the declared and the inferred type, so the distance is a payload-membership arm on an existing judgment, not a new walk. **DO NOT READ SEAM (2)'s CLOSURE AS THE CLASS'S.** One seam of four measured is walled; a reader who sees only 'declared-field inhabitance wall landed' will conclude the class is closed, and the next lane would then build on a guarantee covering a quarter of it. Neither seam (3) nor seam (4) nor seam (5) is closed by gunbc#8876, which deliberately did not widen to chase them. **THIS ROW'S CEILING CELL SAYS THE DISTANCE TO R2 IS "AN IF-STATEMENT PLUS A TRIAGE". THAT IS MEASURED FALSE FOR THE PAYLOAD-WHERE-PARENT SHAPE, AND THE CORRECTION MATTERS BECAUSE IT IS THE SECOND NECESSARY-CONDITION-STATED-AS-SUFFICIENT TRIGGER THIS ONE ROW HAS CARRIED (snappy-tern-856, 2026-08-22).** The cell reasons that `direct_call_arg_mismatch_diags` exists, is written, and is simply not called, so flipping `module_skips_direct_call_arg_check` off closes seam (1). Flipping it off is NECESSARY. It is not SUFFICIENT, and the discriminating measurement is a module the exemption never applied to in the first place: in an ORDINARY NON-`v2.*` module, where the guard is false and the judgment demonstrably runs, `c4_takes(o: 5)` against `fn c4_takes(o: EOuter)` REFUSES (`expected 'Coproduct(EOuter)', got 'Primitive(Int)'`) while `c4_takes(o: e_inner())` — the coproduct's own payload type — is ACCEPTED in the same compile. The judgment is live at that seam and misses this shape, so deleting the arm leaves it accepted. **Read the two facts together or the row misleads:** the exemption really does switch the judgment off for every `v2.*` caller (that half is unchanged and still below floor), AND the judgment it switches off would not catch this shape anyway. A reader who acts only on the first will delete the arm, watch the diagnostics, and conclude the seam is closed. **THE DENOMINATOR THIS ROW HAS LACKED SINCE IT WAS WRITTEN NOW EXISTS, and it is what makes the sentence above checkable rather than another anecdote.** The row has said "assume a third seam until someone enumerates them" through two revisions while the count grew from two to five BY ACCIDENT — four of the five were found by a downstream red or by a mis-written probe, never by anyone enumerating positions, which samples the reviewer rather than the population. The positions are now enumerated FROM THE GRAMMAR: every call site of `parse_type_expr` in `v1.compiler.parse`, which is the finite set of places the language attaches a declared type. That is **14 sites**, and all five previously-known seams FALL OUT of it as rows rather than having been seeded into it — the falsifier the enumeration was required to pass. The list element seam falls out only because a container's element type is reached as a TYPE ARGUMENT rather than as a declaration of its own, which is why nobody had named it as a position before. **METHOD, because "not refused" is worthless without it.** Each position carries three arms: the payload-where-parent shape, a KERNEL mismatch (`Int` where the coproduct is declared), and an UNDEFINED NAME. The third is the reachability control: if it refuses, inference REACHES that position, so a passing kernel arm establishes that NO TYPE JUDGMENT RUNS there rather than that the position went unanalysed. All seven reachability controls refused. Dispositions, measured: **refuses** — record/variant NAMED field (`parse_field`), and only because gunbc#8876 walls it. **Judgment runs, misses the shape** — fn parameter at the direct-call seam. **Not refused, no judgment runs** — container type argument (list element), variant POSITIONAL payload, fn declared return, module-scope `data` initializer, annotated `let`. **Not refused** — `as` cast. **Not reachable from a source value** — type-alias RHS, `uses` resource type, service `exit` and `response` types (the last two are the reconstruction path's, not this row's). **Not refused, no judgment runs** (measured after the first pass, closing the census at 14 of 14) — the callable-type RETURN position (`cb: fn(Int) -> EOuter` given a lambda whose body yields the payload) and the callable-type PARAMETER position (`cb: fn(EOuter) -> Int` called with the payload); both reachability controls refused, so both positions are analysed. Three of these positions were previously unknown: variant positional payload, `as` cast, and annotated `let`. **AND THE ENUMERATION FOUND SOMETHING WIDER THAN THIS ROW'S CLASS, WHICH IS DELIBERATELY NOT CLAIMED HERE.** `data c6b: EOuter = 5` and `fn c5b() -> EOuter { 5 }` are both ACCEPTED, with the reachability control proving both positions are analysed. That is not payload-versus-parent; it is a plain kernel value where a declared coproduct is required, which is the ordinary-floor invariant DESIGN §4b names beside name resolution and exact-bijection binding. On the measured census that is **seven of fourteen grammar-admitted positions accepting a kernel value where a declared coproduct is required** — variant positional payload, fn declared return, module-scope `data` initializer, container type argument, annotated `let`, callable-type return, callable-type parameter — with the single refusing position owing its refusal to a PR that is held at the time of writing. (The count was first published as FIVE of fourteen, before the two callable-type positions were measured; it is corrected here rather than left standing, because an understated denominator on a floor breach is the same defect as an overstated rung. The `as` cast is deliberately not in the seven: it was never given a kernel arm, since a cast is an authored assertion and whether a kernel-to-coproduct cast should refuse is a different question this census did not ask.) This row's class is one INSTANCE of that breach rather than the breach itself, so the finding is routed for its own §4b row and its own owner rather than absorbed here — recording it inside this row would repeat the mistake this correction exists to fix, by making a wider unwalled invariant look like a seam of a narrower one **THAT WIDER BREACH NOW HAS ITS OWN OWNER AND FOUR OF ITS SEVEN POSITIONS ARE WALLED (2026-08-24, the declared-type-inhabitance lane).** Scope, stated first because the class and this row's class are neighbours that will be merged by anyone reading quickly: the subject is A PLAIN KERNEL VALUE (`Int`, `String`, `Bool`) where a declared record or coproduct is required — NOT a coproduct payload where its parent is required, which is this row's seam (2) and is separately walled. MEASURED BEFORE, on the pre-change binary, one fixture per position with an undefined-name reachability control beside it: all SEVEN positions compiled `0 diagnostics` and EMITTED 9 files (fn declared return, module-scope `data` annotation, annotated `let`, container element, variant positional payload, callable-type return, callable-type parameter); every reachability control refused (`function 'no_such_name_at_all' not found in scope`), so the silence measured an absent judgment rather than an unanalysed position; and the record-literal NAMED field refused (`expected 'Coproduct(KOuter)', got 'Primitive(Int)'`), which is what identified the relation that already existed. MEASURED AFTER, same fixtures, same flags: the declared return, the `data` annotation, the annotated `let` and the container element REFUSE with a located `TypeMismatch` (`expected 'Coproduct(KOuter)', got 'Primitive(Int)'`; the element position as `expected 'Container(List,Coproduct(KOuter))', got 'Container(List,Primitive(Int))'`); the conforming spelling at all four positions still compiles `0 diagnostics`; the named field refuses identically, which is the control proving the reused relation has not forked; and `fn f() -> KInner { 5 }` — a RECORD rather than a coproduct — now refuses too (`expected 'Product(KInner)', got 'Primitive(Int)'`), so the wall is the declared-type class and not a coproduct special case. NO SECOND RELATION WAS MINTED (DESIGN §3): `kernel_value_declared_type_mismatch` was already the corpus authority for this judgment and was consulted at exactly one of the fourteen positions; what landed is its peeling prologue lifted into `declared_type_conformance_diags`, so the fn return, the early `return`, the `data` annotation and the newly-wired annotated `let` all widen with that gate rather than beside it. FALSE-POSITIVE CENSUS, AND ITS FIRST STATEMENT HERE WAS WRONG ABOUT ITS OWN DENOMINATOR — corrected in place because the error is the instructive part. The regen corpus compile (`dag` + `src/v2`, `first_generation_equal=true`, `planned=133 executed=133`) reports zero hard diagnostics under the wall, and this row first read that as 'no live site was repaired'. The required floor then refused: its prepared subject resolves **3872 modules**, including `src/v2/test/**`, which the regen closure does not reach, and the wall found **six live sites in one file** — `src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test` declared six octet fixtures and one function parameter as `List` while holding integer literals (`[0, 255, 255, 255, 255]`) and forwarding them to `v2.compiler.emit_host` `emit_host_octets_byte_string`, whose declared parameter is `List` and which builds each `Byte` itself. `Byte` is a record over `List` and no `Int -> Byte` cast rule exists, so every one of those declarations was a lie that no consumer contradicted — the latent shape this row's originating incident already names, at the element position the wall now judges. Repaired to `List` (the entry then compiles with 0 blocking diagnostics), which makes TURNING THE WALL ON the census, exactly as gunbc#8876's field seam was. THE GENERAL LESSON, worth more than the six sites: a green whole-corpus compile is scoped to ITS OWN closure, and quoting it as 'the corpus' silently excludes whatever that closure omits; the floor's prepared subject is the wider denominator and disagreeing with it is how the gap was found. Zero further live sites were found beyond that file, which is a fact about this class's live population and not evidence that the other three positions are empty. RUNG: the four walled positions are **structurally guaranteed** (the bad value is still writable and the compiler refuses it); the class as a whole stays **below floor**, because three positions still admit it. STILL OPEN, each with its trigger, and NONE of them closed by this change: (a) the VARIANT POSITIONAL PAYLOAD — `KHeld(5)` routes through `infer_variant_constructor_call` into `infer_record_lit` under the synthetic field name `0`, and the declared type of that positional slot does not reach the field-conformance seam the NAMED field reaches; trigger is that slot resolving to its declared payload type there. (b) and (c) the CALLABLE-TYPE RETURN and PARAMETER — a lambda's body against `fn(Int) -> KOuter`, and an actual against `fn(KOuter) -> Int`; both reachability controls refused, so both positions are analysed and neither carries the callable's own declared component types into a conformance judgment; trigger is threading each callable boundary's declared parameter and return through the same relation, which is also what `explicit_return_conformance_note` names as its lambda narrowing. A NESTED container (`List>`) is likewise not judged: the element peel is ONE level, which is the depth measured, and deeper is unmeasured rather than covered. Enrolled evidence, permanent per §4b(4): `test.claim.declared_type_kernel_inhabitance_witness_test` — four discriminating REDs, the already-closed named-field RED as the no-fork control, and one positive control carrying the conforming spelling at all four closed positions so a refuse-everything compiler cannot satisfy them **A THIRD SEAM, MEASURED 2026-09-01 (eager-hawk-376), AND IT IS NOT A SEAM AT A POSITION — IT IS A PROPERTY OF THE DECLARED TYPE.** The row above says to assume a third seam exists until someone enumerates them; this is one, and it is orthogonal to (a)/(b)/(c), which all vary the POSITION while holding the declared type ordinary. Here the position is the already-covered one and the DECLARED TYPE is bodyless: **any `type X` declared with no body admits any argument in parameter position, silently.** Receipt, four fixtures in an ORDINARY (non-`v2.*`) module, so seam (1)'s `module_skips_direct_call_arg_check` exemption is not in play, against a binary carrying main's semantics: `fn takes(x: Compose>) -> Int` given a `String` — ACCEPTED, zero diagnostics naming the file; the same with a bare `Phantom` parameter — ACCEPTED; with a locally declared `type Opaque` and no `Phantom` anywhere — ACCEPTED; and the control `type MyRec = Word8`, an alias to a record — REFUSES with both `type mismatch: expected 'Primitive(MyRec)', got 'Primitive(String)'` and the paired inhabitance diagnostic. **The control is what makes this a finding rather than a silence: the judgment RUNS in that module and admits, which is a different mechanism from seam (1), where the judgment never runs.** It is not `Phantom`-specific and not `Compose`-specific — both were the obvious readings and both are refuted by the third fixture. POPULATION: 69 bodyless declarations corpus-wide, including `std.constructors` `Phantom`, `Product` and `Coproduct`, and `std.machine_constraints` `MachineWidth` / `PointerWidth`. **That 69 is the SYNTACTIC population and an upper bound on nothing else** — a bodyless type never used in parameter position cannot exhibit the hole, so the exposed subset is smaller and unmeasured. A naive line-oriented count returns 5227 because the multi-line coproduct spelling (`type X` then `= A \| B` on the following line) reads as bodyless; re-derive rather than quoting either number. Rung: **below floor** — a value that does not inhabit its declared type is accepted, in an ordinary module, with the judgment live. Ceiling: **R2** — membership is decidable from the declaration, since the refusing control proves the comparison seam already reaches this position and already has both types in hand. **NOT ENROLLED**: no probe asserts this, so nothing reds if it changes; the fixtures above are reconstructable but were deleted with the worktree. Next trigger, at capability grain rather than artifact grain per §4b(3): *the conformance seam decides a bodyless declared type by a stated rule — admit-nothing-but-its-own-constructions, or a declared and typed opacity — rather than by falling through*, with the four fixtures above enrolled as the discriminating REDs and the alias-to-record case kept as the no-fork control. **A SECOND, INDEPENDENT DEFECT FOUND IN THE SAME PASS, RECORDED HERE BECAUSE IT IS THE INSTRUMENT THAT WOULD OTHERWISE BE CITED AS THIS CLASS'S CENSUS:** `tools.opaque_realization_census` `declaration_body_standing_in` decides opacity from the `type X` line alone and carries the annotation *"No such spelling occurs in this corpus today, so the reading is exact for the corpus it is run over"* about the multi-line body form. **That premise is false by 5269 declarations**, every one of which the function classifies `DeclaredOpaque`; and separately it matches the declaration by bare prefix, with no name-boundary check, so a longer same-prefix name declared EARLIER in the file decides a shorter name's standing — 304 such pairs, e.g. `Userset` shadowing `User` in `extdeps.access.zanzibar`. Both are read from the function, not from its annotation. **THE ANNOTATION IS THE FINDING, AND DESIGN §4c ALREADY NAMES ITS SHAPE:** an annotation is never evidence that a machine claim holds, because no `Accepted` program can read one. This one does not merely rot — it CERTIFIES the exact trap its function falls into, so a reader doing the diligent thing and checking whether the author considered the continuation form finds a sentence saying yes. It is therefore a receipt for §4c's rule and not only a defect in one census. **Of the two, the bare-prefix bug ranks first for repair**, because they fail differently: the continuation misclassification is systematic and one control exposes it, while `Userset` deciding `User`'s standing is silent, name-dependent, and yields a different wrong answer according to declaration ORDER within a file — so it survives a fix of the continuation reading alone, and 304 pairs is enough that such a fix would look correct on a spot check. The census gates nothing today, so this is a wrong instrument rather than a wrong wall — but it is the instrument this row's population question would be handed to. | +| A value that does not inhabit its declared type is accepted — **seam-split, enumeration UNFINISHED** (was filed as "Direct-call argument TYPE conformance, v2 corpus"; renamed 2026-08-22, see the trigger cell) | **Below floor — the judgment never runs.** Not a hole a bad value slipped through: `v1.compiler.04_infer` gates `arg_compat_diags` on `module_skips_direct_call_arg_check(module_name: scope.module_name)`, which returns true for every module whose name begins with `v2.`. The key is the CALLER's module, so the entire active v2 corpus — compiler stages, extdeps, std, witnesses — has the direct-call argument-type judgment switched off. Measured consequence, 2026-08-22: `v2.extdeps.languages.dag` `dag_int_literal_node_from_lexeme` / `dag_int_literal_node_from_magnitude` declared `occurrence_id: OccurrenceId` since gunbc#6558 while storing that parameter straight into `Node.occurrence_id`, declared `NodeOccurrenceId`. For two months 15 call sites passed `SyntheticOccurrence` (a NodeOccurrenceId, contradicting the declaration) and nothing complained; gunbc#8833 made one call site OBEY the declaration and nothing complained about that either. The error surfaced only as an interpreter `non-exhaustive pattern match on: OccurrenceId { value: 79 }` across 16 witnesses, reddening main. **The inversion worth naming: a declaration that lies is inert while every caller contradicts it in the same direction, and detonates on the first caller who takes it at its word.** So the at-risk population is not "callers who got it wrong" but callers who might get it right — a genuinely counterintuitive census. Note this is the TYPE judgment only; the SHAPE judgment (`direct_call_shape_diags`, labels/arity) is exemption-free and does fire | R2 (a declared parameter type is a decidable conformance check the seam already computes — `direct_call_arg_mismatch_diags` exists, is written, and is simply not called, so the distance to the next rung is an if-statement plus a triage, not an implementation) | **THIS ROW IS A CORRECTION TO DESIGN §4b, NOT A NEW OBSERVATION BESIDE IT — read them together or the first will look like it already settled this.** DESIGN §4b names this exact symbol and reports that it "was found (code read, not execution) to be scoped entirely to the direct-call argument-type judgment and does not reach `sole_constructor`'s construction check at either call site — a positive finding that retires this axis, not an absence of any exemption anywhere." That finding is correct and is not disputed here. The question it asked was whether the exemption LEAKS into `sole_constructor`; the question it never asked is what the exemption COSTS inside the judgment it is scoped to. "Scoped entirely to the direct-call argument-type judgment" reads as reassuring only until that judgment is measured, and it is the argument-type check for the entire active v2 corpus. **Confinement was measured and then treated as safety, and the axis that got retired was not the one that mattered.** Two facts about why the seam nonetheless reads as covered: the SHAPE judgment (`direct_call_shape_diags` — labels, arity, duplicate binding) is exemption-free and DOES fire over every module including the compiler's own sources, so half-live is more deceptive than dead — every casual check finds something working. And the arm is NOT unreasoned: `direct_call_shape_wall_note` states the TYPE judgment's false-positive classes are representation gaps (brand aliases, optionality's two forms, anonymous literals, expansion depth — the conformance wall's four measured classes), which is a real stated reason and is why this row asks for a measurement rather than a deletion. What is unmeasured is whether those classes still fire in v2 today and at what rate. The neighbouring compiler-module arm of this same exemption was deleted in place after being found never to have been in force; the `v2.` arm was left standing at that moment without separate justification of its own | This incident, measured end to end: CI run 32542017600 (main, 67437fcbe9) 16 FAIL with the raw-`OccurrenceId` match error; caller census of both functions read at call grain (17 sites: 15 `SyntheticOccurrence`, 1 `node.occurrence_id`, 1 internal pass-through, 1 raw `minted.id`); exemption mechanism read at `v1.compiler.04_infer` `module_skips_direct_call_arg_check` and its single call site gating `arg_compat_diags` on `scope.module_name`. **NOT ENROLLED**: no probe pair asserts this exemption's reach, so nothing reds if it changes | **THE TRIGGER THIS ROW SHIPPED WITH WAS INCOMPLETE AND IS CORRECTED HERE (2026-08-22, swift-badger-524 retracting their own ruling).** As merged in gunbc#8854 this cell named ONE closing condition — delete the `v2.` exemption — which is a NECESSARY condition presented as a sufficient one. The class is not "direct-call argument type conformance"; it is **a value that does not inhabit its declared type is accepted**, and it has at least TWO seams: **(1) direct-call arguments** — gated off for `v2.*` by `module_skips_direct_call_arg_check`, the mechanism this row measures; **(2) record-literal fields** — gated by NOTHING, below floor in ORDINARY NON-v2 MODULES, receipt gunbc#8865 (gentle-eagle-360). Its minimal pair, no compiler internals involved: `CppHolder { subject: CppWrapped { inner: cpp_inner() } }` accepted and correct, against `CppHolder { subject: cpp_inner() }` — a coproduct PAYLOAD inhabiting a field declared as its parent COPRODUCT — ACCEPTED BY TYPING and dying at runtime as `PatternMatchFailure`. A record literal is not the direct-call seam, so deleting the exemption would not close it. **SEAM (2) NOW HAS A LIVE PRODUCTION SPECIMEN, WHICH RANKS IT DIFFERENTLY FROM A SYNTHETIC PAIR** (gentle-eagle-360, 2026-08-22, found while checking for a second content-identity authority before building on one): `v2.std.materialize` declares `MaterializedNode.hash` as `ContentHash` — the subject-generic union — and `materialize_fold_step` stores `content_hash(n)` into it, which returns `Fnv1a64Structural`, the PAYLOAD carried inside the union's `Fnv1a64` arm. Receipt, by execution against the module as it stands on main: taking the value materialize ACTUALLY STORED and asking the union's own family authority `content_hash_family` about it yields `PatternMatchFailure { value: "Fnv1a64Structural { digest: 7ac77ab0e29c6bd8 }" }`; the probe's fallback was a correctly wrapped `Fnv1a64(...)`, so an empty result or a well-formed value would have PASSED and only a stored value can produce that red. **The defect is LATENT and that is the instructive part**: peer lookup compares `e.hash == h`, raw payload against raw payload, which agrees with itself — so every current path is green and the error surfaces only when a materialize hash is routed through the union's own machinery (`content_hash_family`, or `compare_content_hash`, which exists precisely to refuse cross-family collapse). That is the same shape as this row's own originating incident: **a declaration that lies is inert while every consumer contradicts it in the same direction, and detonates on the first consumer that takes it at its word** — here the first cross-family artifact to reach the carrier. Disposition ruled ARM A, wrap the construction (`MaterializedNode { hash: Fnv1a64(h), ... }`), NOT narrow the declaration: narrowing would sever `MaterializedNode.hash` from `RealizationPlan.target`, and §2's Realization spans resolve-cost, sccache and OS provisioning on ONE content hash, so a structural-only key could never name a realization of a fetched artifact or a provisioned image (swift-badger-524 ruling, 2026-08-22; handed to silent-bear-842 with the receipt, unfixed here because it is that lane's module). **THE SEAM ITSELF IS THE FINDING, not this one site**: gunbc#7480 corrected the design document for asserting the wrong type at exactly this `Hash`/`ContentHash` boundary, and a production module now carries the mirror-image error — a boundary documentation has to keep re-explaining is a boundary that wants construction. ****THAT HAND-OFF IS SUPERSEDED AND THE SPECIMEN IS REPAIRED — corrected in place rather than left standing, because the sentence above says a live production defect is UNFIXED and awaiting another lane, which is the present-tense claim a reader would plan against (gunbc#8876, 2026-08-22).** The wrap landed in the wall's own change by operator ruling: a wall and the repair it forces must land together, since with the wall on and the wrap absent main is red, so only one PR can contain both. `v2.std.materialize` `materialize_fold_step` and `distinct_hashes` now build `Fnv1a64(content_hash(n))`, and the same construction was repaired at four further sites the wall refused for the identical reason — `v2.workflow.operand_flow`, `materialize_witness_test`, `materialization_provider_witness_test` and `heal_revalidation_witness_test`. The receipt above stays as the historical demonstration that the defect was real and reachable; it is no longer a description of the tree. THE ENUMERATION IS UNFINISHED: two is what has been measured, not the count.** Assume a third seam exists until someone enumerates them; note that this row's own originating incident (#8854) reached its victim through a record literal one hop downstream of the direct call, so the two seams are not even cleanly separable at a site. **SEAM (1) WAS EXECUTED TO A MEASURED, BLOCKED STOP ON 2026-08-22 — the arm is NOT deleted, and this paragraph is the §4b row for that state rather than a plan.** Rung: **below floor, unchanged** — the judgment still does not run for any `v2.*` caller. Ceiling: **R2** (a declared parameter type is a decidable conformance check the seam already computes). Next trigger, stated as §4b(2) requires and with its disposition: *a formal parameter declared as an applied generic carries its applied form through resolution rather than reaching the comparison seam as the bare constructor* — **DECLINED at the owning layer on 2026-08-22**, on the ground that a bounded compiler-floor packet whose completion condition has moved should close and hand its residue forward rather than extend into a type-system project. A declined trigger is a legitimate §4b state; **a blocked class with no row is how this exemption survived years in the first place**, which is the reason this row exists at all. Enrolled evidence, so the class stays countable while blocked: `direct_call_arg_type_v2_module_red_probe` (the discriminating RED, rostered in `v2.workflow.floor_expected_red` — it cannot pass while the arm stands and PASSES on a tree with the arm deleted, so it is a satisfiable assertion held open by a named cause), plus two controls that pass on main today (`direct_call_arg_type_ordinary_module_red_probe`, the paired nonzero the exemption never covered; and `direct_call_arg_type_v2_green_control_probe`). **What was measured before the stop, and how to read it:** deleting the arm produces **285+k** blocking diagnostics and **67+k** with gunbc#8873 merged, for some k ≥ 1 unmeasured — these are ROSTER-RESOLVED counts, not corpus counts, and `src/v2/extdeps/formatters/lean4_format.dag:184` is the proof: a live site, structurally identical to eight that refused, contributing zero to *both* arms and therefore invisible to their difference. **Zero genuine call-site defects were found in the residue** — every diagnostic examined was a deficit in the type judgment, so no call sites were edited, because 67 mechanical edits would have cemented three compiler deficits permanently. The per-mechanism split of that residue is deliberately NOT recorded here: it was published as 48/11/8, and the rule the 48 were attributed to was then found to admit nothing in this corpus, so the attribution was retracted before it was cited. Trigger for the count to be restated: the residue re-measured with its `why` column. **The counterexample that retracted it is worth carrying on its own, because it will bite anyone who reaches for a name-keyed alias relation:** `type Float = Float64` is declared in BOTH `dag/std/float.dag:18` and `src/v2/std/float.dag:33`, spelling the target identically — but `dag/std/float.dag:16` has `type Float64 = Real64` (a transparent alias) while `src/v2/std/float.dag:30` has `Float64` as a **record**. So the two declarations agree on a *spelling* and disagree on a *type*, and a unanimity rule keyed on the target's NAME admits them as the same concept. Requiring the target itself to be census-unique closes it — and once closed, that rule admits nothing in this corpus, which is what falsified the attribution above. Found by still-carp-717 while building the rule, before it shipped. **The original trigger text, kept because the sequence it specifies was followed and the record should show what was attempted:** seam (1) — turn the exemption off for `v2.` behind a measured diagnostic count, triage, then delete the arm, the disposition the compiler-module arm received; the measured prerequisite is ALIAS TRANSPARENCY, because proud-ant-819's report-only shadow on the 03_ingest closure found 115 `WouldDiagnose` relations at 78 sites of which 115 reduce to a transparent `type A = B` (92 via `type Hash = Fnv1a64Structural`, 23 via the `Node` phase carriers), residue ZERO — so on that closure the exemption is currently suppressing false positives, not defects. Seam (2) — its own wall at record-literal field conformance; nothing to turn off, it was never on. **Closing seam (1) MUST NOT be read as closing the class**, which is the specific failure this correction exists to prevent: a class that looks like it has one closing condition gets closed when that condition fires. Two blind spots neither instrument covers, named rather than left to be rediscovered: production itself SKIPS an anonymous record literal standing as an ACTUAL at a direct call, so its argument type is never judged (521 relations, 2.7%, `Unadjudicated` in proud-ant-819's shadow — upstream of the guard, so invisible to a flip-off arm too); and a function storing into a field from its own differently-named parameter is this class at yet another site, which a callee-name-keyed census cannot see. **THAT FIRST BLIND SPOT IS NOT SEAM (2), AND THE TWO WILL BE MERGED BY ANY READER WHO DOES NOT SEE THIS SENTENCE** (caught by proud-ant-819, who put the mirror-image clause in their own row): both descriptions begin "a record literal" and name DIFFERENT POSITIONS. The blind spot is a record literal at an ARGUMENT position whose type goes unjudged at the direct-call seam — seam (1)'s territory, and a population of 521 relations. Seam (2) / gunbc#8865 is a record literal's FIELD whose value does not inhabit the field's declared type — a different seam with a different mechanism and no measured population. Reading them as one would make the 521 look like evidence for gunbc#8865, or gunbc#8865's receipt look like it bounds the 521. Neither is true. **A CLAIM ABOUT THIS ROW'S EVIDENCE WAS MADE HERE AND IS RETRACTED, MEASURED WRONG (2026-08-22, the §11 item 28 lane, retracting itself).** The retracted claim was that these probes sit in the declined `ReadsLiveTree` carrier and therefore never execute, so the expected-red enrolment could only be `not_evaluated`. **It is false, and the measurement that refutes it is the run that was supposed to confirm it:** run `32586093086` reports `[expected-red-roster-join] roster=207 still_red=207 now_passes=0 not_evaluated=0` with `known_red_held=207`. The v2-module red EXECUTES and is held still-red exactly as its row intends. The error was reading an IMPORT as a location: `guarantee_probe_corpus_witness` imports the three probe ids for a roster assertion, and I took that for where the probes run; they run in `test.claim.direct_call_argument_type_witness`, a separate file. An import is evidence of visibility, never authority for where a name lives. **What survives is a different and sharper finding.** That file executes because it declares `SubstrateInputsOnly` while calling `compile_dag_diagnostic_census` — the same declaration `gunbc.compile_diagnostic_census`'s own live-tree note already adjudicated as a MIS-declaration when it found `transport_script_wall_compile_red_test` doing it (that census walks `build_module_path_index_from_witness_roots`, i.e. the live checkout). So the specimen population for that mis-declaration is now TWO, the second authored on 2026-08-22 after the first was adjudicated, and both are the only reason any census-compiling probe executes at all. Either these files' declaration is wrong or that authority's note is; they cannot both be right, and which one it is decides the size of §11 item 28's population. That is a question for the arm's owner, not a defect in this row's measurement, which stands. **SEAM (2) IS NOW CLOSED, AND CLOSING IT ENUMERATED TWO MORE — the count is FIVE measured, still not the total (gunbc#8876, 2026-08-22).** **OWNERSHIP, STATED PER SEAM BECAUSE THE CLASS NOW SPANS TWO LANES AND NEITHER CAN CLOSE IT ALONE:** seam (1) is the exemption-gated direct-call seam owned by the paragraph immediately preceding this one, whose next trigger is recorded there as DECLINED rather than pending; seams (2) through (5) belong to the field-inhabitance lane (snappy-tern-856). A lane that lands its last seam will be tempted to close this row. NEITHER MAY: 'my seams are done' is not 'the class is closed', and the row closes only when every seam does — including any seam not yet enumerated. The record-literal FIELD seam is walled: `v1.compiler.infer` `coproduct_payload_where_parent_required` refuses a value whose type is one of the declared coproduct's own variant payload types, consulting `transparent_alias_identity_agrees` over the `SymbolIndex` so an alias-mediated producer is caught too. Rung at that seam: **structurally guaranteed** — no `Accepted` program contains the state there. NOT structurally impossible, because the bad literal is still writable and the compiler refuses it; and NOT the class, which is why the two rows below exist. Evidence, enrolled permanently per §4b(4): `test.claim.coproduct_payload_soundness_witness_test` — the direct RED, the alias-mediated RED, and the positive control that stops a refuse-everything compiler from satisfying either. Turning the wall on WAS the census: EIGHT live sites, none previously known, all repaired in the same change — `ContentHash` from `Fnv1a64Structural` at `materialization_provider_witness_test`, `heal_revalidation_witness_test`, `materialize_witness_test`, `v2.std.materialize` and `v2.workflow.operand_flow`; `LexRules` from `LexRuleSet` at two `src/v2/test/claim/manual` fold tests. **SEAM (3), UNWALLED AND DECLARED, owner the field-inhabitance lane: the module-scope `data` initializer.** `data X: ContentHash = content_hash(...)` stores the payload into a `ContentHash`-declared row and is NOT refused, because a `data` initializer is not a record-literal field. Rung: **below floor**, exactly as seam (2) was. Unguarded: every module-scope `data` row in the corpus. Trigger: the same conformance judgment applied at the data-initializer seam, which needs no new relation — the declared type and the initializer's inferred type are both already in hand there. **SEAM (4), UNWALLED AND DECLARED, owner the field-inhabitance lane, AND IT IS RANKED FIRST OF THE TWO: the list element.** `v2.workflow.locality_affinity` built consumer identities as `list_add_distinct_hash(xs: cs, v: content_hash(n: e.dependent))` — a raw payload into a `List`. Rung: **below floor**, and it does not fail loudly. Measured: repairing the comparands while that producer stayed raw turned FOUR `locality_affinity` witnesses to `Bool(false)` with NOTHING refused at compile time — a wrong answer discovered later, not a diagnostic. That is what makes it rank above seam (3), and the ranking is fixed by a RULE rather than by judgment (operator ratification, 2026-08-22): seam (3) admits a wrong value a correctly-built peer can still catch by comparison — harmful, detectable, recoverable — while seam (4) admits a wrong value AND DISABLES THE COMPARISON THAT WOULD HAVE CAUGHT IT. That is a silent wrong answer, which DESIGN places OUTSIDE the guarantee ladder and forbids outright rather than ranking low, so the two are in different categories and no population argument reaches across the line: a larger set of loud failures does not outrank a smaller set of silent ones. The ranking is a priority order for collisions, NOT a serial queue — seam (3) needs no new relation and may land whenever it is ready. Unguarded: every list, map and collection element position whose element type is a coproduct. Trigger: element-position conformance against the container's declared element type. **SEAM (5), UNWALLED AND DECLARED, owner the field-inhabitance lane: the declared RETURN type.** `fn f(x: Node) -> ContentHash { content_hash(n: x) }` returns the payload where the parent coproduct is declared and is NOT refused. Rung: **below floor**. Measured 2026-08-22 on the gunbc#8876 merge commit, with a liveness control in the SAME compile that produced exactly one diagnostic (the record-literal RED), so the silence is a measurement and not an untested assumption. HOW IT WAS FOUND IS WORTH RECORDING, because it says something about the enumeration itself: it was found by a MIS-WRITTEN PROBE — the author intended an alias-mediated FIELD case and wrote a return position by mistake. Four of the five seams in this row were discovered by accident or by a downstream red rather than by anyone enumerating positions, which is the standing evidence for #8868's instruction to assume a further seam. Unguarded: every declared return type whose type is a coproduct. Trigger: `declared_type_conformance_diags` already runs at this seam and already holds both the declared and the inferred type, so the distance is a payload-membership arm on an existing judgment, not a new walk. **DO NOT READ SEAM (2)'s CLOSURE AS THE CLASS'S.** One seam of four measured is walled; a reader who sees only 'declared-field inhabitance wall landed' will conclude the class is closed, and the next lane would then build on a guarantee covering a quarter of it. Neither seam (3) nor seam (4) nor seam (5) is closed by gunbc#8876, which deliberately did not widen to chase them. **THIS ROW'S CEILING CELL SAYS THE DISTANCE TO R2 IS "AN IF-STATEMENT PLUS A TRIAGE". THAT IS MEASURED FALSE FOR THE PAYLOAD-WHERE-PARENT SHAPE, AND THE CORRECTION MATTERS BECAUSE IT IS THE SECOND NECESSARY-CONDITION-STATED-AS-SUFFICIENT TRIGGER THIS ONE ROW HAS CARRIED (snappy-tern-856, 2026-08-22).** The cell reasons that `direct_call_arg_mismatch_diags` exists, is written, and is simply not called, so flipping `module_skips_direct_call_arg_check` off closes seam (1). Flipping it off is NECESSARY. It is not SUFFICIENT, and the discriminating measurement is a module the exemption never applied to in the first place: in an ORDINARY NON-`v2.*` module, where the guard is false and the judgment demonstrably runs, `c4_takes(o: 5)` against `fn c4_takes(o: EOuter)` REFUSES (`expected 'Coproduct(EOuter)', got 'Primitive(Int)'`) while `c4_takes(o: e_inner())` — the coproduct's own payload type — is ACCEPTED in the same compile. The judgment is live at that seam and misses this shape, so deleting the arm leaves it accepted. **Read the two facts together or the row misleads:** the exemption really does switch the judgment off for every `v2.*` caller (that half is unchanged and still below floor), AND the judgment it switches off would not catch this shape anyway. A reader who acts only on the first will delete the arm, watch the diagnostics, and conclude the seam is closed. **THE DENOMINATOR THIS ROW HAS LACKED SINCE IT WAS WRITTEN NOW EXISTS, and it is what makes the sentence above checkable rather than another anecdote.** The row has said "assume a third seam until someone enumerates them" through two revisions while the count grew from two to five BY ACCIDENT — four of the five were found by a downstream red or by a mis-written probe, never by anyone enumerating positions, which samples the reviewer rather than the population. The positions are now enumerated FROM THE GRAMMAR: every call site of `parse_type_expr` in `v1.compiler.parse`, which is the finite set of places the language attaches a declared type. That is **14 sites**, and all five previously-known seams FALL OUT of it as rows rather than having been seeded into it — the falsifier the enumeration was required to pass. The list element seam falls out only because a container's element type is reached as a TYPE ARGUMENT rather than as a declaration of its own, which is why nobody had named it as a position before. **METHOD, because "not refused" is worthless without it.** Each position carries three arms: the payload-where-parent shape, a KERNEL mismatch (`Int` where the coproduct is declared), and an UNDEFINED NAME. The third is the reachability control: if it refuses, inference REACHES that position, so a passing kernel arm establishes that NO TYPE JUDGMENT RUNS there rather than that the position went unanalysed. All seven reachability controls refused. Dispositions, measured: **refuses** — record/variant NAMED field (`parse_field`), and only because gunbc#8876 walls it. **Judgment runs, misses the shape** — fn parameter at the direct-call seam. **Not refused, no judgment runs** — container type argument (list element), variant POSITIONAL payload, fn declared return, module-scope `data` initializer, annotated `let`. **Not refused** — `as` cast. **Not reachable from a source value** — type-alias RHS, `uses` resource type, service `exit` and `response` types (the last two are the reconstruction path's, not this row's). **Not refused, no judgment runs** (measured after the first pass, closing the census at 14 of 14) — the callable-type RETURN position (`cb: fn(Int) -> EOuter` given a lambda whose body yields the payload) and the callable-type PARAMETER position (`cb: fn(EOuter) -> Int` called with the payload); both reachability controls refused, so both positions are analysed. Three of these positions were previously unknown: variant positional payload, `as` cast, and annotated `let`. **AND THE ENUMERATION FOUND SOMETHING WIDER THAN THIS ROW'S CLASS, WHICH IS DELIBERATELY NOT CLAIMED HERE.** `data c6b: EOuter = 5` and `fn c5b() -> EOuter { 5 }` are both ACCEPTED, with the reachability control proving both positions are analysed. That is not payload-versus-parent; it is a plain kernel value where a declared coproduct is required, which is the ordinary-floor invariant DESIGN §4b names beside name resolution and exact-bijection binding. On the measured census that is **seven of fourteen grammar-admitted positions accepting a kernel value where a declared coproduct is required** — variant positional payload, fn declared return, module-scope `data` initializer, container type argument, annotated `let`, callable-type return, callable-type parameter — with the single refusing position owing its refusal to a PR that is held at the time of writing. (The count was first published as FIVE of fourteen, before the two callable-type positions were measured; it is corrected here rather than left standing, because an understated denominator on a floor breach is the same defect as an overstated rung. The `as` cast is deliberately not in the seven: it was never given a kernel arm, since a cast is an authored assertion and whether a kernel-to-coproduct cast should refuse is a different question this census did not ask.) This row's class is one INSTANCE of that breach rather than the breach itself, so the finding is routed for its own §4b row and its own owner rather than absorbed here — recording it inside this row would repeat the mistake this correction exists to fix, by making a wider unwalled invariant look like a seam of a narrower one **THAT WIDER BREACH NOW HAS ITS OWN OWNER AND FOUR OF ITS SEVEN POSITIONS ARE WALLED (2026-08-24, the declared-type-inhabitance lane).** Scope, stated first because the class and this row's class are neighbours that will be merged by anyone reading quickly: the subject is A PLAIN KERNEL VALUE (`Int`, `String`, `Bool`) where a declared record or coproduct is required — NOT a coproduct payload where its parent is required, which is this row's seam (2) and is separately walled. MEASURED BEFORE, on the pre-change binary, one fixture per position with an undefined-name reachability control beside it: all SEVEN positions compiled `0 diagnostics` and EMITTED 9 files (fn declared return, module-scope `data` annotation, annotated `let`, container element, variant positional payload, callable-type return, callable-type parameter); every reachability control refused (`function 'no_such_name_at_all' not found in scope`), so the silence measured an absent judgment rather than an unanalysed position; and the record-literal NAMED field refused (`expected 'Coproduct(KOuter)', got 'Primitive(Int)'`), which is what identified the relation that already existed. MEASURED AFTER, same fixtures, same flags: the declared return, the `data` annotation, the annotated `let` and the container element REFUSE with a located `TypeMismatch` (`expected 'Coproduct(KOuter)', got 'Primitive(Int)'`; the element position as `expected 'Container(List,Coproduct(KOuter))', got 'Container(List,Primitive(Int))'`); the conforming spelling at all four positions still compiles `0 diagnostics`; the named field refuses identically, which is the control proving the reused relation has not forked; and `fn f() -> KInner { 5 }` — a RECORD rather than a coproduct — now refuses too (`expected 'Product(KInner)', got 'Primitive(Int)'`), so the wall is the declared-type class and not a coproduct special case. NO SECOND RELATION WAS MINTED (DESIGN §3): `kernel_value_declared_type_mismatch` was already the corpus authority for this judgment and was consulted at exactly one of the fourteen positions; what landed is its peeling prologue lifted into `declared_type_conformance_diags`, so the fn return, the early `return`, the `data` annotation and the newly-wired annotated `let` all widen with that gate rather than beside it. FALSE-POSITIVE CENSUS, AND ITS FIRST STATEMENT HERE WAS WRONG ABOUT ITS OWN DENOMINATOR — corrected in place because the error is the instructive part. The regen corpus compile (`dag` + `src/v2`, `first_generation_equal=true`, `planned=133 executed=133`) reports zero hard diagnostics under the wall, and this row first read that as 'no live site was repaired'. The required floor then refused: its prepared subject resolves **3872 modules**, including `src/v2/test/**`, which the regen closure does not reach, and the wall found **six live sites in one file** — `src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test` declared six octet fixtures and one function parameter as `List` while holding integer literals (`[0, 255, 255, 255, 255]`) and forwarding them to `v2.compiler.emit_host` `emit_host_octets_byte_string`, whose declared parameter is `List` and which builds each `Byte` itself. `Byte` is a record over `List` and no `Int -> Byte` cast rule exists, so every one of those declarations was a lie that no consumer contradicted — the latent shape this row's originating incident already names, at the element position the wall now judges. Repaired to `List` (the entry then compiles with 0 blocking diagnostics), which makes TURNING THE WALL ON the census, exactly as gunbc#8876's field seam was. THE GENERAL LESSON, worth more than the six sites: a green whole-corpus compile is scoped to ITS OWN closure, and quoting it as 'the corpus' silently excludes whatever that closure omits; the floor's prepared subject is the wider denominator and disagreeing with it is how the gap was found. Zero further live sites were found beyond that file, which is a fact about this class's live population and not evidence that the other three positions are empty. RUNG: the four walled positions are **structurally guaranteed** (the bad value is still writable and the compiler refuses it); the class as a whole stays **below floor**, because three positions still admit it. STILL OPEN, each with its trigger, and NONE of them closed by this change: (a) the VARIANT POSITIONAL PAYLOAD — `KHeld(5)` routes through `infer_variant_constructor_call` into `infer_record_lit` under the synthetic field name `0`, and the declared type of that positional slot does not reach the field-conformance seam the NAMED field reaches; trigger is that slot resolving to its declared payload type there. (b) and (c) the CALLABLE-TYPE RETURN and PARAMETER — a lambda's body against `fn(Int) -> KOuter`, and an actual against `fn(KOuter) -> Int`; both reachability controls refused, so both positions are analysed and neither carries the callable's own declared component types into a conformance judgment; trigger is threading each callable boundary's declared parameter and return through the same relation, which is also what `explicit_return_conformance_note` names as its lambda narrowing. A NESTED container (`List>`) is likewise not judged: the element peel is ONE level, which is the depth measured, and deeper is unmeasured rather than covered. Enrolled evidence, permanent per §4b(4): `test.claim.declared_type_kernel_inhabitance_witness_test` — four discriminating REDs, the already-closed named-field RED as the no-fork control, and one positive control carrying the conforming spelling at all four closed positions so a refuse-everything compiler cannot satisfy them **A THIRD SEAM, MEASURED 2026-09-01 (eager-hawk-376), AND IT IS NOT A SEAM AT A POSITION — IT IS A PROPERTY OF THE DECLARED TYPE.** The row above says to assume a third seam exists until someone enumerates them; this is one, and it is orthogonal to (a)/(b)/(c), which all vary the POSITION while holding the declared type ordinary. Here the position is the already-covered one and the DECLARED TYPE is bodyless: **any `type X` declared with no body admits any argument in parameter position, silently.** Receipt, four fixtures in an ORDINARY (non-`v2.*`) module, so seam (1)'s `module_skips_direct_call_arg_check` exemption is not in play, against a binary carrying main's semantics: `fn takes(x: Compose>) -> Int` given a `String` — ACCEPTED, zero diagnostics naming the file; the same with a bare `Phantom` parameter — ACCEPTED; with a locally declared `type Opaque` and no `Phantom` anywhere — ACCEPTED; and the control `type MyRec = Word8`, an alias to a record — REFUSES with both `type mismatch: expected 'Primitive(MyRec)', got 'Primitive(String)'` and the paired inhabitance diagnostic. **The control is what makes this a finding rather than a silence: the judgment RUNS in that module and admits, which is a different mechanism from seam (1), where the judgment never runs.** It is not `Phantom`-specific and not `Compose`-specific — both were the obvious readings and both are refuted by the third fixture. POPULATION: 69 bodyless declarations corpus-wide, including `std.constructors` `Phantom`, `Product` and `Coproduct`, and `std.machine_constraints` `MachineWidth` / `PointerWidth`. **That 69 is the SYNTACTIC population and an upper bound on nothing else** — a bodyless type never used in parameter position cannot exhibit the hole, so the exposed subset is smaller and unmeasured. A naive line-oriented count returns 5227 because the multi-line coproduct spelling (`type X` then `= A \| B` on the following line) reads as bodyless; re-derive rather than quoting either number. Rung: **below floor** — a value that does not inhabit its declared type is accepted, in an ordinary module, with the judgment live. Ceiling: **R2** — membership is decidable from the declaration, since the refusing control proves the comparison seam already reaches this position and already has both types in hand. **NOT ENROLLED**: no probe asserts this, so nothing reds if it changes; the fixtures above are reconstructable but were deleted with the worktree. **AND THAT STATE IS NOW A CHOICE RATHER THAN A CONSTRAINT, WHICH §4b WOULD NOT LET STAND SILENTLY:** `test.claim.declared_type_expected_type_path_witness` landed on main the same night, and it compiles caller-authored SOURCE STRINGS through `gunbc.compile_diagnostic_census`, asserting on `census_ran` plus a blocking refusing-count rather than on a diagnostic spelling. The four fixtures above are ordinary source strings, so that harness can express them — which means the refusal is authorable, and §4b's own rule is that declining enrollment where the RED is authorable is specification-without-execution. The reason it is not enrolled in this diff is not that it cannot be: the seam ADMITS today, so the assertion is red on main and enrollment requires a `v2.workflow.floor_expected_red` row — a roster another lane edited the same night, and a decision about the required gate rather than about this class. That decision is named here as the immediate next step, owner-ruled, so the gap is countable rather than quietly permanent. Next trigger, at capability grain rather than artifact grain per §4b(3): *the conformance seam decides a bodyless declared type by a stated rule — admit-nothing-but-its-own-constructions, or a declared and typed opacity — rather than by falling through*, with the four fixtures above enrolled as the discriminating REDs and the alias-to-record case kept as the no-fork control. **A SECOND, INDEPENDENT DEFECT FOUND IN THE SAME PASS, RECORDED HERE BECAUSE IT IS THE INSTRUMENT THAT WOULD OTHERWISE BE CITED AS THIS CLASS'S CENSUS:** `tools.opaque_realization_census` `declaration_body_standing_in` decides opacity from the `type X` line alone and carries the annotation *"No such spelling occurs in this corpus today, so the reading is exact for the corpus it is run over"* about the multi-line body form. **That premise is false by 5269 declarations**, every one of which the function classifies `DeclaredOpaque`; and separately it matches the declaration by bare prefix, with no name-boundary check, so a longer same-prefix name declared EARLIER in the file decides a shorter name's standing — 304 such pairs, e.g. `Userset` shadowing `User` in `extdeps.access.zanzibar`. Both are read from the function, not from its annotation. **THE ANNOTATION IS THE FINDING, AND DESIGN §4c ALREADY NAMES ITS SHAPE:** an annotation is never evidence that a machine claim holds, because no `Accepted` program can read one. This one does not merely rot — it CERTIFIES the exact trap its function falls into, so a reader doing the diligent thing and checking whether the author considered the continuation form finds a sentence saying yes. It is therefore a receipt for §4c's rule and not only a defect in one census. **Of the two, the bare-prefix bug ranks first for repair**, because they fail differently: the continuation misclassification is systematic and one control exposes it, while `Userset` deciding `User`'s standing is silent, name-dependent, and yields a different wrong answer according to declaration ORDER within a file — so it survives a fix of the continuation reading alone, and 304 pairs is enough that such a fix would look correct on a spot check. The census gates nothing today, so this is a wrong instrument rather than a wrong wall — but it is the instrument this row's population question would be handed to. | | Direct-call argument TYPE conformance — **transparent-alias identity**, v2 corpus | **R2 built and approved for the alias-identity class (gunbc#8873 — OPEN, approved, mergeable as of 2026-08-22; NOT merged, and this row must not be read as landed until it is).** A precomputed transparent-alias identity relation, derived once at census build and consumed as a `String -> String` map lookup per comparison, admits two names that alias the same declaration and refuses everything else. It peels ONLY `type A = B` with zero params, no connective, no children, no properties and no type annotation, and a target with zero children/params/annotation and `return_cardinality == Required` — so brands, `sole_constructor` carriers, refinements, coproduct arms and applied generics are all excluded BY THE ADMISSION TEST rather than by a later filter. Cost bar was declared before implementation and measured after: four crossed A/B pairs, +2.0s on a 454s regen (+0.4%) against per-arm spreads of 29.9s and 40.9s — a measured null. **What it does NOT do is create substitutability: it makes an existing fact visible.** A pre-relation binary already accepts `CommitSha` at an `AttemptKey` formal and already refuses `IntKey` there | R2 for this class. R3 is not reachable at this seam and that is a property of the seam, not of the relation | **The residual population is a DIFFERENT class and the distinction is load-bearing.** Measured 2026-08-22 against the exemption-deleted corpus: 67 refusals, silent-badger-817's CI run 32562740527 at commit `d42bb3eb57c`. **Provenance caveat, stated because it changes what the 48 means:** that tree merged this relation at `9bfd5388c03`, TWO COMMITS behind head `c40ab2d8248`, and the intervening `b0f72158c80` ("Qualify alias targets at census-build time") is exactly the commit that decides the `CoreNode` group — those refusals turn on `Node` being ambiguous by BARE name. So the 67 is a measurement of an OLDER revision of this relation, not of a broken copy of it. Classification of those 67, derived from declarations and independent of any binary: 48 are this alias class; 8 are applied generics (row below); 11 are `Optional` against `String`/`Bool`/`Int` in `v2.extdeps.github.gha_fold_pilot_emit` and are NOT an alias class at all. **The 48-cleared half is verified on 5 specimens, not 48:** at head, with the exemption deleted in the mirror and `exempt=judged` on all 20352 ledger rows, the five comparisons that CI reports as errors in `00_compile.dag` (lines 319, 342, 408, 446, 497) are all present in the ledger and all read `Compatible`. The remaining 43 sit outside that entry's import closure and a whole-corpus re-run against head was in flight when this row landed — treat 48 as classified-and-partially-verified, never as measured. **Also NOT the alias class: the 11** — the diagnostic reads got `Primitive(String)`, so the optional marker is already gone upstream at pattern destructuring and no comparison-seam mechanism can reach them. That 11 was carried as alias residue by two independent sessions and by this lane's own framing; it is recorded here so it is not handed forward under a label that guarantees the next attempt fails. **Open question for whoever takes it, to be CHECKED rather than inherited from this row:** an optionality marker erased at destructuring means a value reaches a position whose declared type it does not inhabit, which is the same floor rule as the direct-call seam census (record-literal walled; data-initializer and list-element open). If Group C is a FIFTH seam of that class it belongs on that row and not on a new one — decide that before minting a class for it. **A second mechanism, `unanimity`, was designed, measured and ABANDONED as unsound, not deferred.** Its specimen and refutation are carried on the seam-split row above and are deliberately NOT restated here — one fact, one authority | gunbc#8873, 9 enrolled floor witnesses in `dag/test/claim/transparent_alias_identity_witness_test.dag` including the over-peel boundary (`IntHandle` at a `String` formal), a coproduct-projection climb, and a blast-radius pair whose Int-alias discriminator refuses. Shadow ledger re-run before the exemption was touched: 20527 rows, all 115 `WouldDiagnose` rows one mechanism. Receipt: `docs/probes/transparent_alias_identity_2026-08-22/README.md` — **FORWARD REFERENCE, NOT A PRESENT FACT:** that receipt lands with gunbc#8873, which is open at the time this row merges. Do not cite it as evidence until that PR is in | the `v2.` exemption arm cannot be deleted while the applied-generic class below still refuses 8 live sites; the exemption is NOT narrowed to those modules (a narrowing would be a shape test correlating with the distinction rather than naming it) | | Direct-call argument TYPE conformance — **applied-generic alias**, v2 corpus | **Below floor — 8 live false refusals, structurally unreachable from the comparison seam.** An alias whose right-hand side is a generic application (`type BlackConfigPatch = ConfigPatchRecord`) refuses at every call site passing it to the matching formal. Specimen, measured by execution 2026-08-22 on a fixture diffed byte-for-byte against the live `v2.std.patch` declaration, with the exemption deleted in the Rust MIRROR and `exempt=judged` on all 20352 ledger rows as the control: `formal_type = Primitive(ConfigPatchRecord)`, `actual_type = Node(BlackConfigPatch)`, `nominal=true container=false kernel=false`, `fname=ConfigPatchRecord aname=BlackConfigPatch`. Population: 9 declarations, all under `src/v2/extdeps/formatters/` (`black`, `clang_format`, `gofmt`, `google_java_format`, `ktfmt`, `lean4_format`, `prettier`, `rustfmt`, `swift_format`), of which 8 produced diagnostics in the CI arm — `lean4_format` is structurally identical and produced none in EITHER arm, so the population is 9 and the measured count is 8+k | R2, and it is decidable — the same equality already accepts the applied form when it is written directly at the formal | **THE FORMAL SIDE IS WHERE THE INFORMATION DIES, and that is the sentence that should stop the next attempt from this direction.** The formal is DECLARED `ConfigPatchRecord` and REACHES the comparison as the bare constructor, with the type argument already discarded. So the equality has one side that structurally cannot hold an argument, and the case split over any representative is EXHAUSTIVE: (a) representative = the applied form with every argument retained never equals the bare constructor, so it admits nothing and all 9 sites keep refusing; (b) representative = the bare constructor admits `ConfigPatchRecord` at `ConfigPatchRecord` for any X and Y, which is exactly the over-peel that erases the distinction. There is no third representative, and widening the carrier does not help — a node-valued map fails identically, because the missing information is not on the relation's side of the map. **Not to be confused with gunbc#8879**, the withdrawn repair that widened transparency AT RESOLVE and was refused by CI in three classes at once (20 direct-call comparisons, 18 variant projections, 3 files of regen drift). What that established is that resolve is the wrong place for a transparency JUDGMENT; preserving an applied form is resolve DISCARDING LESS, which hands the same consumers MORE structure, and is a different claim that has not been measured | executed fixture + shadow ledger with a positive control (`black.dag` must refuse; a zero there is decidably wrong). **NOT ENROLLED**: no probe pair asserts this class, so nothing reds if it changes. Three false zeros were produced while measuring it — twice from patching the `.dag` authority while the binary is built from the emitted Rust mirror, once from a run that PANICKED and reported zero diagnostics — each caught only by a positive control or by another session's raw per-line export, never by an aggregate | **RESOLVE CARRIES APPLIED FORMS AT THE FORMAL POSITION.** Explicitly NOT scoped as of 2026-08-22 (operator-lane ruling, swift-badger-524): a bounded floor-recovery lane whose completion condition has moved is closed honestly rather than extended, and nothing in that ruling says the change is wrong. Until it lands, the `v2.` exemption stays whole and gunbc#8886 stays blocked | | Direct-call argument TYPE conformance — **container element**, non-exempt module; and the witness family that reported it was **rung INFLATION** (DESIGN §4b(1) — *not* §4b(3): nothing regressed, the wall was never there, so "restore the previous behaviour" is not the remedy and a regression row would have read as authorising it) | **Below floor — the container-element judgment does not fire at a direct call argument.** Measured 2026-08-27 with the witness's OWN oracle (`compile_dag_rust_emit_check`) alongside `compile_dag_diagnostic_census`, over two corpora in two remote dispatches: `main` @ `ddb7f533e4e` and gunbc#9428's head. A fixture handing `FreeMonoid` to a declared `FreeMonoid` parameter — locally declared record, corpus-unique wrapper name, no `Node`, no `v2.std.node`, no occurrence identity anywhere in it — **compiles clean ON `main`**, 0 blocking; the argument surfaces only as advisory `DeclaredTypeInhabitanceUndecided` at "direct call argument". Distinct from the `module_skips_direct_call_arg_check` row above: that exemption keys on the CALLER's module name and this fixture's module is not `v2.`-prefixed, so the judgment is not switched off here — it is written, reached, and answers no. **THE INFLATION:** the class read as mechanically preventable on the strength of `test.claim.record_literal_call_arg_handoff_witness.record_literal_container_element_mismatch_at_call_arg_still_refuses` being green. That witness was green on an UNRELATED defect in its own closure — `v2.std.node` referenced `std.occurrence_identity.OccurrenceId` and `ScopedOccurrenceRef` fully qualified WITHOUT importing that module, so every closure importing `v2.std.node` inherited two `UnresolvedType` diagnostics and refused for that reason; measured on `main`, the fixture's refusal is exactly `UnresolvedType/std.occurrence_identity.OccurrenceId` ×2 + `ScopedOccurrenceRef` ×1, and contains no type-mismatch diagnostic at all. gunbc#9428 adds the import, those resolve, and the accidental refusal goes with them. **A witness green on a defect in its own closure is not weak coverage, it is NEGATIVE coverage** — it is cited as evidence the wall is live, so the class never ranks for climbing. That is DESIGN §4b's worse-than-absent case reached from a direction the document does not yet record: not an unauthorable RED, but an AUTHORABLE one satisfied by the WRONG CAUSE, which no reader of the witness can distinguish from the right one. The nominal sibling `record_literal_nominal_mismatch_at_call_arg_still_refuses` stays green through a DIFFERENT path (`literal_introduction_type_mismatch`, whose actual is a record LITERAL rather than a call), which is why the family read as coherent and was not | R2 (two distinct nominal element types under one container template is a decidable comparison the seam already reaches) | `container_element_nominal_brand_mismatch` is written and IS reached from `direct_call_arg_type_mismatch`, but it delegates to `nominal_call_arg_brand_mismatch`, which requires `structural_carrier_template_name(formal_el) == structural_carrier_template_name(actual_el)`; that name falls through `canonical_template_name` to the element's own authored name for any non-container type, so two DISTINCT nominal element types can never satisfy the conjunct that the mismatch arm needs. **Stated as a CODE READ, consistent with the measurement but not independently executed** — what is executed is that the compile is clean, not which conjunct declined | Measurement above (both corpora, `emit_check` + census). **Instrument not committed:** a throwaway cargo example over the two `pub` entry points in `cli_run`, kept out of the tree per the no-ad-hoc-script rule; re-deriving it needs a `.dag` entry point, which is this row's standing "name the instrument" debt | `container_element_nominal_brand_mismatch` reaching the direct-call-argument position — i.e. `nominal_call_arg_brand_mismatch` admitting distinct nominal element types under a shared container template. The witness is the ready-made RED and needs no new fixture; it is enrolled as expected-red in gunbc#9428, where it FAILS (on `main` it still passes on the accident, so enrolling it here would trip the roster's stale-quarantine arm and red main's own floor) |