diff --git a/dag/gunbc/product/altra_motherboard/minimal_design.dag b/dag/gunbc/product/altra_motherboard/minimal_design.dag
index 1dede6ae702..cf8c0c41b0d 100644
--- a/dag/gunbc/product/altra_motherboard/minimal_design.dag
+++ b/dag/gunbc/product/altra_motherboard/minimal_design.dag
@@ -47,6 +47,10 @@ type DesignRefusal
   | ChannelHasNoDimmPositions
   | DimmPositionRepeatedOnChannel { position: Int }
   | PcieLanesExceedPackage { requested: Int, available: Int }
+  | PopulatedChannelIsNotRouted { channel: Int }
+  | PopulatedPositionIsNotRouted { position: Int }
+  | NoProductionQualifiedPopulationIsReachable { routed_channels: Int }
+  | NoProductionQualifiedChannelCountExists
 
 // A CHANNEL HAS AN IDENTITY, AND IT IS NOT ITS ORDINAL POSITION IN A COUNT. An earlier revision
 // derived the populated set from the count by generating [0..n), which is cardinality standing
@@ -166,9 +170,9 @@ fn position_occurrences(ps: List<DimmSlotPosition>, p: DimmSlotPosition) -> Int
   })
 }
 
-fn duplicate_position_causes(t: ActiveDdrTopology) -> List<DesignRefusal> {
-  fold(t.positions_per_channel, init: [], f: fn(acc, p) {
-    if position_occurrences(ps: t.positions_per_channel, p: p) > 1
+fn duplicate_position_causes(ps: List<DimmSlotPosition>) -> List<DesignRefusal> {
+  fold(ps, init: [], f: fn(acc, p) {
+    if position_occurrences(ps: ps, p: p) > 1
       && !fold(acc, init: false, f: fn(seen, r) {
         seen || match r {
           DimmPositionRepeatedOnChannel { position: n } => n == dimm_slot_position_ordinal(p: p)
@@ -178,6 +182,10 @@ fn duplicate_position_causes(t: ActiveDdrTopology) -> List<DesignRefusal> {
           ChannelPopulationIsNotAnAdmittedCount { populated: _ } => false
           ChannelHasNoDimmPositions => false
           PcieLanesExceedPackage { requested: _, available: _ } => false
+          PopulatedChannelIsNotRouted { channel: _ } => false
+          PopulatedPositionIsNotRouted { position: _ } => false
+          NoProductionQualifiedPopulationIsReachable { routed_channels: _ } => false
+          NoProductionQualifiedChannelCountExists => false
         }
       }) {
       concat(acc, [DimmPositionRepeatedOnChannel { position: dimm_slot_position_ordinal(p: p) }])
@@ -191,9 +199,9 @@ fn duplicate_position_causes(t: ActiveDdrTopology) -> List<DesignRefusal> {
 // clearest evidence that identity was the missing fact rather than a nicety. A generated range
 // is duplicate-free by construction, so this class did not exist to be caught; naming the
 // channels makes it writable, and this makes it refused.
-fn duplicate_channel_causes(t: ActiveDdrTopology) -> List<DesignRefusal> {
-  fold(t.populated_channels, init: [], f: fn(acc, c) {
-    if channel_occurrences(cs: t.populated_channels, c: c) > 1
+fn duplicate_channel_causes(cs: List<DdrChannelIdentity>) -> List<DesignRefusal> {
+  fold(cs, init: [], f: fn(acc, c) {
+    if channel_occurrences(cs: cs, c: c) > 1
       && !fold(acc, init: false, f: fn(seen, r) {
         seen || match r {
           ChannelPopulatedMoreThanOnce { channel: n } => n == ddr_channel_ordinal(c: c)
@@ -203,6 +211,10 @@ fn duplicate_channel_causes(t: ActiveDdrTopology) -> List<DesignRefusal> {
           ChannelHasNoDimmPositions => false
           DimmPositionRepeatedOnChannel { position: _ } => false
           PcieLanesExceedPackage { requested: _, available: _ } => false
+          PopulatedChannelIsNotRouted { channel: _ } => false
+          PopulatedPositionIsNotRouted { position: _ } => false
+          NoProductionQualifiedPopulationIsReachable { routed_channels: _ } => false
+          NoProductionQualifiedChannelCountExists => false
         }
       }) {
       concat(acc, [ChannelPopulatedMoreThanOnce { channel: ddr_channel_ordinal(c: c) }])
@@ -264,12 +276,12 @@ fn design_causes(d: AltraMinimalMotherboard) -> List<DesignRefusal> {
   let population_cause = if selected > altra_ddr4_channel_count {
     [ChannelCountExceedsControllerPopulation { selected: selected, available: altra_ddr4_channel_count }]
   } else {
-    concat([], duplicate_channel_causes(t: d.memory.topology))
+    concat([], duplicate_channel_causes(cs: d.memory.topology.populated_channels))
   }
   let dimm_cause = if list_length(items: d.memory.topology.positions_per_channel) < 1 {
     [ChannelHasNoDimmPositions]
   } else {
-    duplicate_position_causes(t: d.memory.topology)
+    duplicate_position_causes(ps: d.memory.topology.positions_per_channel)
   }
   let pcie_cause = if d.pcie_lanes_broken_out > altra_pcie_gen4_lane_count {
     [PcieLanesExceedPackage { requested: d.pcie_lanes_broken_out, available: altra_pcie_gen4_lane_count }]
@@ -298,6 +310,212 @@ fn admit_design(d: AltraMinimalMotherboard) -> DesignAdmission {
 // constrains the choice is an open question against a document nobody has read on that point,
 // carried on the source-document roster rather than settled by picking a set that looks
 // symmetric and calling it advice.
+// ROUTING IS NOT POPULATION, AND CONFLATING THEM MAKES ONE OF THEM UNRECOVERABLE. A PCB routes a
+// set of channels and positions in copper; which of those ship with a module in them is a build
+// decision taken later and changed often. ActiveDdrTopology alone answers only the second
+// question, so a design that says "four channels" cannot distinguish a board that ROUTED four --
+// permanently, in fabrication -- from a board that routed eight and populated four. Those are
+// different products with different escape problems, different layer counts and different upgrade
+// stories, and the difference is invisible at the moment it is decided and expensive afterwards.
+//
+// THE SUBSET LAW IS THE WHOLE POINT. Copper is the ceiling: a board can leave a routed slot empty,
+// and can never fill a slot it did not route. Stating the population as a topology in its own
+// right rather than as a flag on the routed one is what makes the violating case WRITABLE and
+// therefore refusable -- exactly the move the named-channel comment above describes, applied one
+// level up.
+// ROUTING AND POPULATION ARE TWO FACTS AND THEY NOW HAVE TWO CARRIERS. An earlier revision gave
+// both fields the type ActiveDdrTopology, so the SAME type -- and a field literally spelled
+// populated_channels -- meant copper under `routed` and shipped memory under `initially_populated`.
+// Meaning that depends on which field a value was stored in is a meaning fork wearing one name: it
+// cannot be read locally, and nothing refuses the two being swapped at a call site.
+type RoutedDdrTopology {
+  routed_channels: List<DdrChannelIdentity>
+  routed_positions_per_channel: List<DimmSlotPosition>
+}
+
+fn routed_channel_count(r: RoutedDdrTopology) -> Int {
+  list_length(items: r.routed_channels)
+}
+
+// A BOARD IS NOT ONE POPULATION, IT IS A POPULATION OVER TIME. One production board may route
+// eight channels, come up on two under bring-up intent, and ship on four. A single topology under
+// a single intent cannot say that: judging it once as EngineeringBringUp establishes nothing about
+// the shipped product, and judging it separately as Production produces a second verdict with no
+// structural relation to the first. The lifecycle makes the relation a modelled fact, so both
+// populations are judged under their own intent against ONE routed ceiling.
+type MemoryPopulationLifecycle
+  = ShipsWithProductionPopulation { production: ActiveDdrTopology }
+  | BringUpThenFill { bringup: ActiveDdrTopology, production: ActiveDdrTopology }
+
+fn lifecycle_production_population(l: MemoryPopulationLifecycle) -> ActiveDdrTopology {
+  match l {
+    ShipsWithProductionPopulation { production: p } => p
+    BringUpThenFill { bringup: _, production: p } => p
+  }
+}
+
+type RevARoutedMemoryDesign {
+  routed: RoutedDdrTopology
+  lifecycle: MemoryPopulationLifecycle
+}
+
+fn channel_is_in(cs: List<DdrChannelIdentity>, c: DdrChannelIdentity) -> Bool {
+  fold(cs, init: false, f: fn(acc, x) { acc || ddr_channel_ordinal(c: x) == ddr_channel_ordinal(c: c) })
+}
+
+fn position_is_in(ps: List<DimmSlotPosition>, p: DimmSlotPosition) -> Bool {
+  fold(ps, init: false, f: fn(acc, x) { acc || dimm_slot_position_ordinal(p: x) == dimm_slot_position_ordinal(p: p) })
+}
+
+// EVERY POPULATED IDENTITY MUST BE A ROUTED ONE, reported per offending identity rather than as a
+// single "not a subset" boolean, so the refusal names which channel or position is unroutable
+// instead of only that something is. Applied to EACH population in the lifecycle: copper is the
+// ceiling for the bring-up population exactly as it is for the shipped one.
+fn population_subset_causes(routed: RoutedDdrTopology, populated: ActiveDdrTopology) -> List<DesignRefusal> {
+  let channel_causes = fold(populated.populated_channels, init: [], f: fn(acc, c) {
+    if channel_is_in(cs: routed.routed_channels, c: c) {
+      acc
+    } else {
+      concat(acc, [PopulatedChannelIsNotRouted { channel: ddr_channel_ordinal(c: c) }])
+    }
+  })
+  let position_causes = fold(populated.positions_per_channel, init: [], f: fn(acc, p) {
+    if position_is_in(ps: routed.routed_positions_per_channel, p: p) {
+      acc
+    } else {
+      concat(acc, [PopulatedPositionIsNotRouted { position: dimm_slot_position_ordinal(p: p) }])
+    }
+  })
+  concat(channel_causes, position_causes)
+}
+
+// ONE STRUCTURAL LAW, STATED OVER THE IDENTITY LISTS THEMSELVES so that both carriers are judged
+// by it rather than only the one it was first written for. The earlier revision applied duplicate
+// and empty-position refusal to the ROUTED topology alone, which left two states writable and
+// admitted, both proven by execution before this law landed:
+//   [DDR0, DDR0, DDR1, DDR2] -- list length four, so it reached the production-qualified arm, and
+//     every identity in it IS routed, so the subset law above could not see the repeat.
+//   four channels with NO dimm positions -- the empty-position refusal was routed-only, and the
+//     position subset fold succeeds vacuously on an empty list.
+// Neither is a near-miss: the first names four channels while populating three, and the second
+// describes a board that populates no slot at all.
+fn identity_structural_causes(channels: List<DdrChannelIdentity>, positions: List<DimmSlotPosition>) -> List<DesignRefusal> {
+  let count_cause = if list_length(items: channels) > altra_ddr4_channel_count {
+    [ChannelCountExceedsControllerPopulation { selected: list_length(items: channels), available: altra_ddr4_channel_count }]
+  } else {
+    duplicate_channel_causes(cs: channels)
+  }
+  let dimm_cause = if list_length(items: positions) < 1 {
+    [ChannelHasNoDimmPositions]
+  } else {
+    duplicate_position_causes(ps: positions)
+  }
+  concat(count_cause, dimm_cause)
+}
+
+// TWO AXES, TWO DIFFERENT LAWS. An earlier revision applied the ACTIVE-channel authority to
+// copper. The datasheet qualifies "active channels", and says nothing of the form "a production
+// motherboard may route exactly four, six or eight channel interfaces". Judging copper by that
+// sentence produced a fail-open -- eight routed with two active under Production was ADMITTED --
+// and an over-refusal of a five-routed/four-active board that nothing in the source refuses.
+//
+// SO THE ROUTED SIDE RECEIVES A REACHABILITY LAW INSTEAD: every subset of a two-channel routed set
+// has at most two active channels, and one and two are both non-production, so no
+// production-qualified population is reachable from it. That refuses the two-route board while
+// leaving the five-route/four-active board admitted.
+//
+// THE MINIMUM IS OPTIONAL BECAUSE ITS ABSENCE IS A REAL STATE. The previous fold seeded init: 0 and
+// returned an Int, so a vendor roster in which NO count was production-qualified yielded 0, and
+// `routed_count >= 0` admitted every routed topology at exactly the moment no production population
+// existed at all. Absence must refuse, not return the identity of the comparison.
+fn smallest_production_channel_count() -> Int? {
+  fold([OneChannel, TwoChannels, FourChannels, SixChannels, EightChannels], init: none, f: fn(acc, c) {
+    if channel_count_is_production_qualified(c: c) {
+      match acc {
+        Absent => Present { value: active_channel_count(c: c) }
+        Present { value: best } =>
+          if active_channel_count(c: c) < best { Present { value: active_channel_count(c: c) } } else { acc }
+      }
+    } else {
+      acc
+    }
+  })
+}
+
+fn routed_reachability_causes(routed: RoutedDdrTopology) -> List<DesignRefusal> {
+  match smallest_production_channel_count() {
+    Absent => [NoProductionQualifiedChannelCountExists]
+    Present { value: m } =>
+      if routed_channel_count(r: routed) >= m {
+        []
+      } else {
+        [NoProductionQualifiedPopulationIsReachable { routed_channels: routed_channel_count(r: routed) }]
+      }
+  }
+}
+
+fn routed_structural_causes(routed: RoutedDdrTopology, pcie_lanes: Int) -> List<DesignRefusal> {
+  let pcie_cause = if pcie_lanes > altra_pcie_gen4_lane_count {
+    [PcieLanesExceedPackage { requested: pcie_lanes, available: altra_pcie_gen4_lane_count }]
+  } else {
+    []
+  }
+  concat(identity_structural_causes(channels: routed.routed_channels, positions: routed.routed_positions_per_channel), pcie_cause)
+}
+
+// THE ACTIVE POPULATION CARRIES THE VENDOR PREDICATE, under its own declared intent, AND the same
+// structural law as copper.
+fn active_population_causes(populated: ActiveDdrTopology, intent: DesignIntent) -> List<DesignRefusal> {
+  let selected = topology_channel_count(t: populated)
+  let vendor_causes = match admitted_channel_count(n: selected) {
+    Absent => [ChannelPopulationIsNotAnAdmittedCount { populated: selected }]
+    Present { value: c } =>
+      match intent {
+        EngineeringBringUp => []
+        Production =>
+          if channel_count_is_production_qualified(c: c) {
+            []
+          } else {
+            [DebugOnlyChannelCountUnderProductionIntent { selected: selected }]
+          }
+      }
+  }
+  concat(identity_structural_causes(channels: populated.populated_channels, positions: populated.positions_per_channel), vendor_causes)
+}
+
+// EACH POPULATION IN THE LIFECYCLE IS JUDGED UNDER ITS OWN INTENT, and both against one ceiling.
+fn lifecycle_causes(routed: RoutedDdrTopology, l: MemoryPopulationLifecycle) -> List<DesignRefusal> {
+  match l {
+    ShipsWithProductionPopulation { production: p } =>
+      concat(active_population_causes(populated: p, intent: Production), population_subset_causes(routed: routed, populated: p))
+    BringUpThenFill { bringup: b, production: p } =>
+      concat(
+        concat(active_population_causes(populated: b, intent: EngineeringBringUp), population_subset_causes(routed: routed, populated: b)),
+        concat(active_population_causes(populated: p, intent: Production), population_subset_causes(routed: routed, populated: p))
+      )
+  }
+}
+
+// THE ADMITTED VALUE RETAINS THE ROUTING IT WAS JUDGED AGAINST. The earlier success constructor
+// built a motherboard carrying only the initial active population, discarding the exact routed
+// copper the admission had just checked. A downstream selector could then not consume the accepted
+// design at all: it would have to keep the original input beside the result and assert the two
+// belong together, which is the adjacent-but-unbound shape this module exists to remove.
+type RoutedDesignAdmission
+  = RoutedDesignAdmitted { admitted: RevARoutedMemoryDesign, pcie_lanes_broken_out: Int }
+  | RoutedDesignRefused { causes: DesignRefusalSet }
+
+fn admit_routed_design(d: RevARoutedMemoryDesign, pcie_lanes: Int) -> RoutedDesignAdmission {
+  let causes = concat(
+    concat(routed_structural_causes(routed: d.routed, pcie_lanes: pcie_lanes), routed_reachability_causes(routed: d.routed)),
+    lifecycle_causes(routed: d.routed, l: d.lifecycle)
+  )
+  match fold(causes, init: none, f: fn(acc, c) { push_design_refusal(acc: acc, r: c) }) {
+    Absent => RoutedDesignAdmitted { admitted: d, pcie_lanes_broken_out: pcie_lanes }
+    Present { value: s } => RoutedDesignRefused { causes: s }
+  }
+}
+
 data altra_1p_minimum: AltraMinimalMotherboard = AltraMinimalMotherboard {
   intent: Production,
   memory: MemoryConfiguration {
diff --git a/dag/test/claim/altra_routed_vs_populated_witness_test.dag b/dag/test/claim/altra_routed_vs_populated_witness_test.dag
new file mode 100644
index 00000000000..090c04a352a
--- /dev/null
+++ b/dag/test/claim/altra_routed_vs_populated_witness_test.dag
@@ -0,0 +1,231 @@
+module test.claim.altra_routed_vs_populated_witness_test
+
+import std.types { Bool, List, list_length }
+import std.integer { Int }
+import product.altra_motherboard.minimal_design {
+  RevARoutedMemoryDesign, RoutedDdrTopology, ActiveDdrTopology,
+  MemoryPopulationLifecycle, ShipsWithProductionPopulation, BringUpThenFill,
+  RoutedDesignAdmission, RoutedDesignAdmitted, RoutedDesignRefused,
+  DdrChannel0, DdrChannel1, DdrChannel2, DdrChannel3, DdrChannel4, DdrChannel5, DdrChannel6, DdrChannel7,
+  FirstDimmOnChannel, SecondDimmOnChannel,
+  admit_routed_design, population_subset_causes,
+  DesignRefusal, PopulatedChannelIsNotRouted, PopulatedPositionIsNotRouted,
+  NoProductionQualifiedPopulationIsReachable, NoProductionQualifiedChannelCountExists,
+  DebugOnlyChannelCountUnderProductionIntent, ChannelCountExceedsControllerPopulation,
+  ChannelPopulationIsNotAnAdmittedCount, ChannelPopulatedMoreThanOnce,
+  ChannelHasNoDimmPositions, DimmPositionRepeatedOnChannel, PcieLanesExceedPackage,
+}
+
+// EXECUTING EVIDENCE that routing and population are separate facts and that copper is the
+// ceiling. The motivating case is the one a single topology could not express at all: a board
+// that routes eight channels and ships four populated.
+
+fn all_eight_routed() -> RoutedDdrTopology {
+  RoutedDdrTopology {
+    routed_channels: [DdrChannel0, DdrChannel1, DdrChannel2, DdrChannel3, DdrChannel4, DdrChannel5, DdrChannel6, DdrChannel7],
+    routed_positions_per_channel: [FirstDimmOnChannel],
+  }
+}
+
+fn four_active() -> ActiveDdrTopology {
+  ActiveDdrTopology {
+    populated_channels: [DdrChannel0, DdrChannel1, DdrChannel2, DdrChannel3],
+    positions_per_channel: [FirstDimmOnChannel],
+  }
+}
+
+fn ships(p: ActiveDdrTopology) -> MemoryPopulationLifecycle {
+  ShipsWithProductionPopulation { production: p }
+}
+
+fn is_admitted(a: RoutedDesignAdmission) -> Bool {
+  match a {
+    RoutedDesignAdmitted { admitted: _, pcie_lanes_broken_out: _ } => true
+    RoutedDesignRefused { causes: _ } => false
+  }
+}
+
+fn admit(routed: RoutedDdrTopology, l: MemoryPopulationLifecycle) -> RoutedDesignAdmission {
+  admit_routed_design(d: RevARoutedMemoryDesign { routed: routed, lifecycle: l }, pcie_lanes: 4)
+}
+
+// THE MOTIVATING CASE: eight routed, four populated, admitted.
+test fn w_a_board_may_route_eight_and_populate_four() -> Bool {
+  is_admitted(a: admit(routed: all_eight_routed(), l: ships(p: four_active())))
+}
+
+test fn w_populating_an_unrouted_channel_refuses() -> Bool {
+  !is_admitted(a: admit(
+    routed: RoutedDdrTopology {
+      routed_channels: [DdrChannel0, DdrChannel1, DdrChannel2, DdrChannel3],
+      routed_positions_per_channel: [FirstDimmOnChannel],
+    },
+    l: ships(p: ActiveDdrTopology {
+      populated_channels: [DdrChannel0, DdrChannel1, DdrChannel2, DdrChannel7],
+      positions_per_channel: [FirstDimmOnChannel],
+    })))
+}
+
+test fn w_populating_an_unrouted_position_refuses() -> Bool {
+  !is_admitted(a: admit(
+    routed: all_eight_routed(),
+    l: ships(p: ActiveDdrTopology {
+      populated_channels: [DdrChannel0, DdrChannel1, DdrChannel2, DdrChannel3],
+      positions_per_channel: [FirstDimmOnChannel, SecondDimmOnChannel],
+    })))
+}
+
+// THE ORIGINAL FAIL-OPEN: eight routed, two active, Production. Admitted by the law that
+// qualified copper instead of the active population.
+test fn w_eight_routed_but_two_active_refuses_under_production() -> Bool {
+  !is_admitted(a: admit(
+    routed: all_eight_routed(),
+    l: ships(p: ActiveDdrTopology {
+      populated_channels: [DdrChannel0, DdrChannel1],
+      positions_per_channel: [FirstDimmOnChannel],
+    })))
+}
+
+// THE PAIRED OVER-REFUSAL: five routed interfaces operating a supported four-channel population
+// is refused by nothing in the source.
+test fn w_five_routed_with_four_active_is_admitted() -> Bool {
+  is_admitted(a: admit(
+    routed: RoutedDdrTopology {
+      routed_channels: [DdrChannel0, DdrChannel1, DdrChannel2, DdrChannel3, DdrChannel4],
+      routed_positions_per_channel: [FirstDimmOnChannel],
+    },
+    l: ships(p: four_active())))
+}
+
+test fn w_a_two_route_board_has_no_reachable_production_population() -> Bool {
+  !is_admitted(a: admit(
+    routed: RoutedDdrTopology {
+      routed_channels: [DdrChannel0, DdrChannel1],
+      routed_positions_per_channel: [FirstDimmOnChannel],
+    },
+    l: ships(p: ActiveDdrTopology {
+      populated_channels: [DdrChannel0, DdrChannel1],
+      positions_per_channel: [FirstDimmOnChannel],
+    })))
+}
+
+// STRUCTURAL LAW ON THE ACTIVE POPULATION. Both of these were ADMITTED before the shared law
+// landed, each proven by running the counterexample against the old module.
+
+// [DDR0, DDR0, DDR1, DDR2] has list length four, so it reached the production-qualified arm,
+// and every identity in it IS routed, so the subset law could not see the repeat.
+test fn w_a_repeated_active_channel_refuses() -> Bool {
+  !is_admitted(a: admit(
+    routed: all_eight_routed(),
+    l: ships(p: ActiveDdrTopology {
+      populated_channels: [DdrChannel0, DdrChannel0, DdrChannel1, DdrChannel2],
+      positions_per_channel: [FirstDimmOnChannel],
+    })))
+}
+
+// Four channels and NO dimm position at all: the empty-position refusal used to be routed-only,
+// and the position subset fold succeeds vacuously on an empty list.
+test fn w_an_active_population_with_no_dimm_positions_refuses() -> Bool {
+  !is_admitted(a: admit(
+    routed: all_eight_routed(),
+    l: ships(p: ActiveDdrTopology {
+      populated_channels: [DdrChannel0, DdrChannel1, DdrChannel2, DdrChannel3],
+      positions_per_channel: [],
+    })))
+}
+
+// THE LIFECYCLE. A production board may legitimately come up on two channels and ship on four;
+// the bring-up population is judged under bring-up intent, so it does not refuse.
+test fn w_a_board_may_bring_up_on_two_and_ship_on_four() -> Bool {
+  is_admitted(a: admit(
+    routed: all_eight_routed(),
+    l: BringUpThenFill {
+      bringup: ActiveDdrTopology {
+        populated_channels: [DdrChannel0, DdrChannel1],
+        positions_per_channel: [FirstDimmOnChannel],
+      },
+      production: four_active(),
+    }))
+}
+
+// AND THE SHIPPED POPULATION IS STILL JUDGED AS PRODUCTION. Declaring a lifecycle does not
+// launder a debug-only shipped population through the bring-up arm.
+test fn w_a_lifecycle_may_not_ship_a_debug_only_population() -> Bool {
+  !is_admitted(a: admit(
+    routed: all_eight_routed(),
+    l: BringUpThenFill {
+      bringup: ActiveDdrTopology {
+        populated_channels: [DdrChannel0],
+        positions_per_channel: [FirstDimmOnChannel],
+      },
+      production: ActiveDdrTopology {
+        populated_channels: [DdrChannel0, DdrChannel1],
+        positions_per_channel: [FirstDimmOnChannel],
+      },
+    }))
+}
+
+// THE BRING-UP POPULATION IS STILL BOUND BY COPPER. Its intent excuses the channel COUNT, never
+// the subset law.
+test fn w_a_bring_up_population_may_not_leave_the_routed_set() -> Bool {
+  !is_admitted(a: admit(
+    routed: RoutedDdrTopology {
+      routed_channels: [DdrChannel0, DdrChannel1, DdrChannel2, DdrChannel3],
+      routed_positions_per_channel: [FirstDimmOnChannel],
+    },
+    l: BringUpThenFill {
+      bringup: ActiveDdrTopology {
+        populated_channels: [DdrChannel7],
+        positions_per_channel: [FirstDimmOnChannel],
+      },
+      production: four_active(),
+    }))
+}
+
+// THE ADMITTED VALUE RETAINS ITS ROUTING, which is what a downstream selector must consume. The
+// earlier success constructor discarded it, so this reads the routed set back OUT of the result.
+test fn w_the_admitted_design_retains_the_routed_topology() -> Bool {
+  match admit(routed: all_eight_routed(), l: ships(p: four_active())) {
+    RoutedDesignRefused { causes: _ } => false
+    RoutedDesignAdmitted { admitted: d, pcie_lanes_broken_out: _ } =>
+      list_length(items: d.routed.routed_channels) == 8
+  }
+}
+
+fn names_unrouted_channel(rs: List<DesignRefusal>, ordinal: Int) -> Bool {
+  fold(rs, init: false, f: fn(acc, r) {
+    acc || match r {
+      PopulatedChannelIsNotRouted { channel: n } => n == ordinal
+      PopulatedPositionIsNotRouted { position: _ } => false
+      NoProductionQualifiedPopulationIsReachable { routed_channels: _ } => false
+      NoProductionQualifiedChannelCountExists => false
+      DebugOnlyChannelCountUnderProductionIntent { selected: _ } => false
+      ChannelCountExceedsControllerPopulation { selected: _, available: _ } => false
+      ChannelPopulationIsNotAnAdmittedCount { populated: _ } => false
+      ChannelPopulatedMoreThanOnce { channel: _ } => false
+      ChannelHasNoDimmPositions => false
+      DimmPositionRepeatedOnChannel { position: _ } => false
+      PcieLanesExceedPackage { requested: _, available: _ } => false
+    }
+  })
+}
+
+// THE REFUSAL NAMES WHICH CHANNEL, rather than only that something was unroutable.
+test fn w_the_refusal_names_which_channel_was_unrouted() -> Bool {
+  let routed = RoutedDdrTopology {
+    routed_channels: [DdrChannel0, DdrChannel1, DdrChannel2, DdrChannel3],
+    routed_positions_per_channel: [FirstDimmOnChannel],
+  }
+  let populated = ActiveDdrTopology {
+    populated_channels: [DdrChannel0, DdrChannel1, DdrChannel2, DdrChannel7],
+    positions_per_channel: [FirstDimmOnChannel],
+  }
+  names_unrouted_channel(rs: population_subset_causes(routed: routed, populated: populated), ordinal: 7)
+    && !names_unrouted_channel(rs: population_subset_causes(routed: routed, populated: populated), ordinal: 3)
+}
+
+// NON-VACUITY: a clean design yields no subset causes at all, so the reds above are discriminating
+// rather than a law that refuses everything.
+test fn w_RED_a_clean_routed_design_yields_no_subset_causes() -> Bool {
+  list_length(items: population_subset_causes(routed: all_eight_routed(), populated: four_active())) == 0
+}