Re-author the Map literal population: the open half onto PartialFunction, the finite half onto the construction route

dag/extdeps/languages/go/types.dag

@@ -33,7 +33,7 @@ data go_algebra_inhabitants: List<InhabitantDecl> = [
     import_path: none,
     is_copy: none },
 
-  { algebra: "BooleanAlgebra",
+  { algebra: "FinitePowerSet",
     template: "map[\{0\}]struct{}",
     arity: 1,
     identity_expr: "nil",
@@ -54,6 +54,13 @@ data go_algebra_inhabitants: List<InhabitantDecl> = [
     import_path: none,
     is_copy: none },
 
+  { algebra: "FinitelySupportedFunction",
+    template: "map[\{0\}]\{1\}",
+    arity: 2,
+    identity_expr: "nil",
+    import_path: none,
+    is_copy: none },
+
   { algebra: "OrderedRing",
     template: "int64",
     arity: 0,

dag/extdeps/languages/python/types.dag

@@ -32,7 +32,7 @@ data python_algebra_inhabitants: List<InhabitantDecl> = [
     import_path: none,
     is_copy: none },
 
-  { algebra: "BooleanAlgebra",
+  { algebra: "FinitePowerSet",
     template: "set[\{0\}]",
     arity: 1,
     identity_expr: "set()",
@@ -53,6 +53,13 @@ data python_algebra_inhabitants: List<InhabitantDecl> = [
     import_path: none,
     is_copy: none },
 
+  { algebra: "FinitelySupportedFunction",
+    template: "dict[\{0\}, \{1\}]",
+    arity: 2,
+    identity_expr: "{}",
+    import_path: none,
+    is_copy: none },
+
   { algebra: "OrderedRing",
     template: "int",
     arity: 0,

dag/extdeps/languages/rust/types.dag

@@ -43,7 +43,7 @@ data rust_algebra_inhabitants: List<InhabitantDecl> = [
     import_path: none,
     is_copy: false },
 
-  { algebra: "BooleanAlgebra",
+  { algebra: "FinitePowerSet",
     template: "BTreeSet<\{0\}>",
     arity: 1,
     identity_expr: "BTreeSet::new()",
@@ -64,6 +64,13 @@ data rust_algebra_inhabitants: List<InhabitantDecl> = [
     import_path: none,
     is_copy: false },
 
+  { algebra: "FinitelySupportedFunction",
+    template: "HashMap<\{0\}, \{1\}>",
+    arity: 2,
+    identity_expr: "HashMap::new()",
+    import_path: none,
+    is_copy: false },
+
   { algebra: "OrderedRing",
     template: "i64",
     arity: 0,

dag/extdeps/languages/typescript/types.dag

@@ -33,7 +33,7 @@ data ts_algebra_inhabitants: List<InhabitantDecl> = [
     import_path: none,
     is_copy: false },
 
-  { algebra: "BooleanAlgebra",
+  { algebra: "FinitePowerSet",
     template: "Set<\{0\}>",
     arity: 1,
     identity_expr: "new Set()",
@@ -54,6 +54,13 @@ data ts_algebra_inhabitants: List<InhabitantDecl> = [
     import_path: none,
     is_copy: false },
 
+  { algebra: "FinitelySupportedFunction",
+    template: "Map<\{0\}, \{1\}>",
+    arity: 2,
+    identity_expr: "new Map()",
+    import_path: none,
+    is_copy: false },
+
   { algebra: "OrderedRing",
     template: "number",
     arity: 0,

dag/gunbc/plans/representation_minimization.dag

@@ -23,7 +23,7 @@ fn representation_minimization_body() -> List<MarkdownBlock> {
     p(text: "Lever B attacks BYTES-PER-NODE; Lever C (item 2) attacks MODULES-HELD-AT-ONCE. The two axes are orthogonal and compose multiplicatively — neither blocks the other. Lever B is gated on emitter determinism (#5879) and lands in the v2/.dag realization. Lever C has no dependency on the emitter gate and is deferred to the v2 streaming-infer realization when v2 infer becomes the live path (see the Lever C disposition section; decision A3)."),
     h2(text: "Lever C (item 2) disposition — design note (2026-06-28)"),
     p(text: "Design-first investigation result. The §2 finding is real and verified by execution: the floor / claim-execution interpreter consumes only the resolved Node tree (module items + item_registry + source_indices), NEVER the per-module type_env/func_env (proven by a discriminating teeth control — evicting items/item_registry turns reflection witnesses RED, while evicting only type_env/func_env keeps the whole 1109-witness floor GREEN). The emit path (a separate process) genuinely consumes the envs and stays byte-identical."),
-    p(text: "Extend, do not fork (DESIGN §3): the v2 self-host compiler ALREADY models the consumed-core-vs-envs split — `03_resolve.dag` `ResolvedTree = Node` (env-free) versus `04_infer.dag` `InferredTree { root: Node, facts: Map<Node, InferredFacts> }`, where the facts side-map (grounding + termination descent) is v2's analog of v1's type_env/func_env. v1's monolithic `ResolvedGraph { Vec<TypedModule { type_env, func_env }> }` is the bootstrap-seed artifact that conflates what v2 already splits. No new resolve-output type is minted; Lever C aligns to the existing v2 types."),
+    p(text: "Extend, do not fork (DESIGN §3): the v2 self-host compiler ALREADY models the consumed-core-vs-envs split — `03_resolve.dag` `ResolvedTree = Node` (env-free) versus `04_infer.dag` `InferredTree { root: Node, facts: PartialFunction<Node, InferredFacts> }`, where the facts side-map (grounding + termination descent) is v2's analog of v1's type_env/func_env. v1's monolithic `ResolvedGraph { Vec<TypedModule { type_env, func_env }> }` is the bootstrap-seed artifact that conflates what v2 already splits. No new resolve-output type is minted; Lever C aligns to the existing v2 types."),
     p(text: "The v2-surviving root is a RETENTION/EVICTION POLICY, not a type and not a fact-elimination: a module's inference facts are live only while it and its DIRECT dependents are processed (typecheck reads direct imports' facts; imported types are copied by value), so a module's facts evict once the dependency frontier passes — peak bounded by frontier width, not total modules (the #5867 shared-intern_table precedent: an algorithmic single authority). v2 `00_compile` today holds `InferredTree` WHOLE across infer→lens-gates→emit/eval, so this bound is genuinely OWED at v2 `00_compile`, unrealized."),
     p(text: "Why this is a design note and not a modeled lens today (DESIGN §5/§6): v1 is hand-written bootstrap Rust that does NOT consume the .dag authority, so a .dag-modeled bound plus a hand-coded v1 frontier-evict would be parallel representation with no derivation link, and a lens asserting the bound over v2 infer would be inert (v2 infer is not the live path — no executing consumer). The bound is therefore recorded here, to be realized as v2 infer's streaming-infer when v2 becomes the live compiler. The interim bulk-eviction PR (#5886) was dropped: it trimmed only SUSTAINED interp RSS, not the per-shard resolve/infer PEAK that is the floor OOM axis (concurrency is peak-bound, #5867/CI-floor)."),
     p(text: "Decision (MEASURED 2026-06-28): A3 — frontier-evict is NOT written into the doomed v1 typecheck seed; the ~4 GiB eviction prize is captured durably by the v2 streaming-infer realization of the frontier-bounded retention bound (the resolution-strategy fact above), when v2 infer becomes the live path. This was a data-gated decision and the data resolved to A3, robustly: the post-cutover floor measurement (claim_executor per-shard VmHWM × spawn_width=2, sccache excluded as a separate process tree) is co-resident 5.98 GiB — 1.82 GiB UNDER the ~7.8 GiB safety threshold below the 8 GiB host cgroup cap, only +0.7 percent above the 5.94 GiB pre-cutover baseline (noise). The cheaper fixes already in main — the floor alloc-clamp binding concurrency to the live cgroup limit, the shared intern_table, and the spawn-width-from-budget throttle — hold the floor comfortably under cap, and the cutover does not regress it. So v1 frontier-evict is NOT forced (the acute-pain justification that would have cemented doomed-seed Rust is absent). Its residual value at this margin is throughput-headroom (a lower per-shard peak permits a higher spawn_width), which belongs to the allocation lane (`docs/plans/resource-aware-scheduler.md`), not this representation lane. Verdict metric note: co-resident = per-shard VmHWM × spawn_width is a deliberately conservative upper bound (assumes simultaneous shard peaks), the correct fail-closed bias for a hard cap; the 1.82 GiB margin makes A3 robust rather than borderline. The flip-to-A1 trigger stays documented and re-auditable: if the corpus later grows enough that the post-cutover co-resident peak reaches ~7.8 GiB, A1 re-activates — implement frontier-evict on the claim-scoped `MultiEntryIndex.typed_module_cache` (eviction predicate fail-closed: a module's typed graph is evictable only once every module that imports it has been resolved, conservative-when-uncertain), gated on a consumer-completeness design read since that cache is load-bearing floor infrastructure. UN-tripped today at the measured 1.82 GiB margin."),