FLOOR-POPULATION-PROJECTION: exact identity join of every declared witness to one disposition, no new carrier

dag/gunbc/discovery_census.dag

@@ -13,6 +13,7 @@ import gunbc.build_target {
 import v2.workflow.required_floor {
   RequiredFloorDisposition,
   Planned, DeclinedLongModule, DeclinedFixtureMember, DeclinedCostDebt,
+  DeclinedOutsideRequiredGate, DeclinedOutsideGateClosure, DeclinedDiscoveryExcluded,
   required_floor_site_disposition,
 }
 import v2.std.live_tree { LiveTreeDisposition }
@@ -256,6 +257,12 @@ fn census_partition_step(acc: CensusPartition, row: CensusRow) -> CensusPartitio
       CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) }
     DeclinedCostDebt =>
       CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) }
+    DeclinedOutsideRequiredGate =>
+      CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) }
+    DeclinedOutsideGateClosure =>
+      CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) }
+    DeclinedDiscoveryExcluded { matched_substring: _ } =>
+      CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) }
   }
 }
 
@@ -315,12 +322,25 @@ fn required_aggregate_from_census(census: SiteCensus) -> RequiredAggregateDeriva
 // written out rather than counted as "planned and everything else": a new decline reason
 // silently joining the non-planned remainder would leave the census reporting a population it no
 // longer distinguishes.
+// THE "MUST FAIL TO COMPILE" CLAIM ABOVE WAS FALSE WHEN THIS ROW WAS WRITTEN, and the correction
+// is recorded here rather than silently applied. `DeclinedOutsideRequiredGate` was added to
+// `RequiredFloorDisposition` and NEITHER of this module's two wildcard-free matches acquired an
+// arm for it; nothing refused, so the census counted a population it no longer distinguished for
+// as long as that arm existed — exactly the outcome the paragraph promises is unwritable. The
+// three arms below close that gap and the missing one, but the claim is now stated at its honest
+// rung: match exhaustiveness over an imported coproduct is NOT enforced for this module on any
+// executing path, because its own witness sits outside the required gate's import closure. NEXT
+// TRIGGER: the required gate reaching this module (or any executing consumer typechecking it),
+// at which point the omission fails the build instead of being found by a reader.
 type CensusCounts {
   offered: Int
   planned: Int
   declined_long_module: Int
   declined_fixture_member: Int
   declined_cost_debt: Int
+  declined_outside_required_gate: Int
+  declined_outside_gate_closure: Int
+  declined_discovery_excluded: Int
 }
 
 fn census_counts_zero() -> CensusCounts {
@@ -329,7 +349,10 @@ fn census_counts_zero() -> CensusCounts {
     planned: 0,
     declined_long_module: 0,
     declined_fixture_member: 0,
-    declined_cost_debt: 0
+    declined_cost_debt: 0,
+    declined_outside_required_gate: 0,
+    declined_outside_gate_closure: 0,
+    declined_discovery_excluded: 0
   }
 }
 
@@ -341,31 +364,76 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu
         planned: counts.planned + 1,
         declined_long_module: counts.declined_long_module,
         declined_fixture_member: counts.declined_fixture_member,
-        declined_cost_debt: counts.declined_cost_debt
+        declined_cost_debt: counts.declined_cost_debt,
+        declined_outside_required_gate: counts.declined_outside_required_gate,
+        declined_outside_gate_closure: counts.declined_outside_gate_closure,
+        declined_discovery_excluded: counts.declined_discovery_excluded
       }
     DeclinedLongModule { matched_prefix: _ } =>
       CensusCounts {
         offered: counts.offered + 1,
         planned: counts.planned,
         declined_long_module: counts.declined_long_module + 1,
         declined_fixture_member: counts.declined_fixture_member,
-        declined_cost_debt: counts.declined_cost_debt
+        declined_cost_debt: counts.declined_cost_debt,
+        declined_outside_required_gate: counts.declined_outside_required_gate,
+        declined_outside_gate_closure: counts.declined_outside_gate_closure,
+        declined_discovery_excluded: counts.declined_discovery_excluded
       }
     DeclinedFixtureMember { matched_prefix: _ } =>
       CensusCounts {
         offered: counts.offered + 1,
         planned: counts.planned,
         declined_long_module: counts.declined_long_module,
         declined_fixture_member: counts.declined_fixture_member + 1,
-        declined_cost_debt: counts.declined_cost_debt
+        declined_cost_debt: counts.declined_cost_debt,
+        declined_outside_required_gate: counts.declined_outside_required_gate,
+        declined_outside_gate_closure: counts.declined_outside_gate_closure,
+        declined_discovery_excluded: counts.declined_discovery_excluded
       }
     DeclinedCostDebt =>
       CensusCounts {
         offered: counts.offered + 1,
         planned: counts.planned,
         declined_long_module: counts.declined_long_module,
         declined_fixture_member: counts.declined_fixture_member,
-        declined_cost_debt: counts.declined_cost_debt + 1
+        declined_cost_debt: counts.declined_cost_debt + 1,
+        declined_outside_required_gate: counts.declined_outside_required_gate,
+        declined_outside_gate_closure: counts.declined_outside_gate_closure,
+        declined_discovery_excluded: counts.declined_discovery_excluded
+      }
+    DeclinedOutsideRequiredGate =>
+      CensusCounts {
+        offered: counts.offered + 1,
+        planned: counts.planned,
+        declined_long_module: counts.declined_long_module,
+        declined_fixture_member: counts.declined_fixture_member,
+        declined_cost_debt: counts.declined_cost_debt,
+        declined_outside_required_gate: counts.declined_outside_required_gate + 1,
+        declined_outside_gate_closure: counts.declined_outside_gate_closure,
+        declined_discovery_excluded: counts.declined_discovery_excluded
+      }
+    DeclinedOutsideGateClosure =>
+      CensusCounts {
+        offered: counts.offered + 1,
+        planned: counts.planned,
+        declined_long_module: counts.declined_long_module,
+        declined_fixture_member: counts.declined_fixture_member,
+        declined_cost_debt: counts.declined_cost_debt,
+        declined_outside_required_gate: counts.declined_outside_required_gate,
+        declined_outside_gate_closure: counts.declined_outside_gate_closure + 1,
+        declined_discovery_excluded: counts.declined_discovery_excluded
+      }
+    DeclinedDiscoveryExcluded { matched_substring: _ } =>
+      CensusCounts {
+        offered: counts.offered + 1,
+        planned: counts.planned,
+        declined_long_module: counts.declined_long_module,
+        declined_fixture_member: counts.declined_fixture_member,
+        declined_cost_debt: counts.declined_cost_debt,
+        declined_outside_required_gate: counts.declined_outside_required_gate,
+        declined_outside_gate_closure: counts.declined_outside_gate_closure,
+        declined_discovery_excluded: counts.declined_discovery_excluded + 1
       }
   }
 }

dag/test/claim/discovery_census_witness_test.dag

@@ -26,9 +26,15 @@ import gunbc.discovery_census {
   RequiredAggregateDerivation, RequiredAggregateDerived, RequiredAggregateUnderivable,
   required_aggregate_from_census,
 }
+// THE TWO PREPARATION-STAGE DECLINES ARE IMPORTED AND ANSWERED `false` EVERYWHERE BELOW.
+// `required_floor_site_disposition` can never RETURN `DeclinedOutsideGateClosure` or
+// `DeclinedDiscoveryExcluded`: both are decided before a module reaches the prepared subject,
+// from facts a module NAME cannot carry. So their arms here are a claim about that
+// unreachability, not an omission padded out to satisfy exhaustiveness.
 import v2.workflow.required_floor {
   RequiredFloorDisposition,
   Planned, DeclinedLongModule, DeclinedFixtureMember, DeclinedOutsideRequiredGate, DeclinedCostDebt,
+  DeclinedOutsideGateClosure, DeclinedDiscoveryExcluded,
   required_floor_site_disposition,
 }
 import v2.workflow.floor_terminal_ledger { ClaimDisposition, Passed }
@@ -207,6 +213,8 @@ test fn w_fixture_home_declines_with_its_matched_prefix() -> Bool {
     DeclinedLongModule { matched_prefix: _ } => false
     DeclinedOutsideRequiredGate => false
     DeclinedCostDebt => false
+    DeclinedOutsideGateClosure => false
+    DeclinedDiscoveryExcluded { matched_substring: _ } => false
   }
 }
 
@@ -220,6 +228,8 @@ test fn w_long_home_module_declines_with_its_matched_prefix() -> Bool {
     DeclinedFixtureMember { matched_prefix: _ } => false
     DeclinedOutsideRequiredGate => false
     DeclinedCostDebt => false
+    DeclinedOutsideGateClosure => false
+    DeclinedDiscoveryExcluded { matched_substring: _ } => false
   }
 }
 
@@ -236,6 +246,8 @@ test fn w_long_home_is_a_prefix_not_a_substring() -> Bool {
     DeclinedFixtureMember { matched_prefix: _ } => false
     DeclinedOutsideRequiredGate => false
     DeclinedCostDebt => false
+    DeclinedOutsideGateClosure => false
+    DeclinedDiscoveryExcluded { matched_substring: _ } => false
   }
 }
 
@@ -249,6 +261,8 @@ test fn w_site_is_planned_when_no_home_matched() -> Bool {
     DeclinedFixtureMember { matched_prefix: _ } => false
     DeclinedOutsideRequiredGate => false
     DeclinedCostDebt => false
+    DeclinedOutsideGateClosure => false
+    DeclinedDiscoveryExcluded { matched_substring: _ } => false
   }
 }
 
@@ -265,6 +279,8 @@ test fn w_site_outside_the_required_gate_is_declined() -> Bool {
     DeclinedLongModule { matched_prefix: _ } => false
     DeclinedFixtureMember { matched_prefix: _ } => false
     DeclinedCostDebt => false
+    DeclinedOutsideGateClosure => false
+    DeclinedDiscoveryExcluded { matched_substring: _ } => false
   }
 }
 
@@ -283,10 +299,14 @@ test fn w_counts_partition_the_offered_population() -> Bool {
     && (counts.declined_fixture_member == 1)
     && (counts.declined_outside_required_gate == 0)
     && (counts.declined_cost_debt == 1)
+    && (counts.declined_outside_gate_closure == 0)
+    && (counts.declined_discovery_excluded == 0)
     && (counts.offered ==
         counts.planned + counts.declined_long_module
           + counts.declined_fixture_member
           + counts.declined_outside_required_gate
+          + counts.declined_outside_gate_closure
+          + counts.declined_discovery_excluded
           + counts.declined_cost_debt)
 }
 
@@ -316,6 +336,9 @@ test fn w_rostered_identity_declines_for_cost_debt() -> Bool {
     identity: "dag.test.claim.lifecycle_survivor_corpus_census.no_raw_lifecycle_string_survivors_remain"
   ) {
     DeclinedCostDebt => true
+    DeclinedOutsideRequiredGate => false
+    DeclinedOutsideGateClosure => false
+    DeclinedDiscoveryExcluded { matched_substring: _ } => false
     Planned => false
     DeclinedLongModule { matched_prefix: _ } => false
     DeclinedFixtureMember { matched_prefix: _ } => false
@@ -333,6 +356,8 @@ test fn w_unrostered_sibling_in_the_same_module_is_planned() -> Bool {
     Planned => true
     DeclinedOutsideRequiredGate => false
     DeclinedCostDebt => false
+    DeclinedOutsideGateClosure => false
+    DeclinedDiscoveryExcluded { matched_substring: _ } => false
     DeclinedLongModule { matched_prefix: _ } => false
     DeclinedFixtureMember { matched_prefix: _ } => false
   }
@@ -351,6 +376,8 @@ test fn w_home_decline_outranks_cost_debt() -> Bool {
     DeclinedLongModule { matched_prefix: p } => p == "test.claim.long."
     DeclinedOutsideRequiredGate => false
     DeclinedCostDebt => false
+    DeclinedOutsideGateClosure => false
+    DeclinedDiscoveryExcluded { matched_substring: _ } => false
     Planned => false
     DeclinedFixtureMember { matched_prefix: _ } => false
   }

dag/test/claim/scm/scm_repository_envelope_witness_test.dag

@@ -61,7 +61,7 @@ import gunbc.scm.repository_envelope {
 // THIS DECLARATION DOES NOT CHANGE WHETHER THESE CLAIMS EXECUTE, AND TWO EARLIER REVISIONS OF THIS
 // ANNOTATION SAID IT DID. Both are retracted here against the source rather than against a rerun.
 //
-// THE FLOOR'S AUTOMATIC ROUTE IS A COLUMN-ZERO TEXT SCAN (`witness_file_from_source`, v1 seed):
+// THE FLOOR'S AUTOMATIC ROUTE WAS A COLUMN-ZERO TEXT SCAN (former v1 seed scanner):
 // a line must `starts_with("data ")` AND contain BOTH `LiveTreeDisposition` AND `ReadsLiveTree`.
 // An undeclared module matches nothing, so `reads_live_tree` is false and the module is ROUTED.
 // A module declaring SubstrateInputsOnly also matches nothing -- the second token is absent -- so it