Lane A cost valuation

dag/gunbc/non_fold_residue.dag

@@ -71,6 +71,8 @@ data nfr_reason_cost_loop_zero_body_fold: String = "C1 zero-body summation fold
 
 data nfr_reason_cost_expr_zero_absorbing_compose: String = "zero-absorbing CostExpr composition (zero-valued CostConst is the identity for sequential add and parallel max; nested wildcard arms are the non-degenerate CostAdd/CostMax construction path, not anonymous recursion) — landed with v2.lens.cost.expr cost_expr_seq/cost_expr_par for C2 ComplexitySummary composition; surfaced by whole-corpus nfr receipt on first CI run"
 
+data nfr_reason_cost_valuation_zero_annihilator: String = "Zero-annihilator discrimination in the C1 exact evaluator: the arms separate an ExactCost carrying Zero from every other CostEvaluation on BOTH operands, so the wildcard is a nested-VALUE discrimination and not a variant sweep — CostEvaluation has exactly two variants and the other two matches in this module were made exhaustive rather than rostered when this row was written. Enumerating it would mean writing the residual combine_evaluation call once per surviving shape, which is the redundancy DESIGN §2 forbids rather than the totality DESIGN §4 asks for, and it would put a duplicated expression underneath an arm ORDER that multiply_evaluations_zero_note declares load-bearing: the annihilator is checked before refusal-dominance, so refusal times zero answers exact zero. A later tidy that flattens these arms silently restores the defect the function exists to fix. Declared at landing with the two-sided annihilator fix, not surfaced by a later cold sweep, so the ratchet arms with the code."
+
 data nfr_reason_provider_terminal_absorb: String = "terminal-state absorption over the provider/worker observation coproducts: the arm names each TERMINAL variant (ProviderCompleted / ProviderFailed / ProviderEventsRefused, or WorkerProcessRunning) and gives every non-terminal variant one shared arm, because those variants reduce to the identical behaviour — enumerating them would clone the arm per variant, which is the redundancy DESIGN §2 forbids rather than the totality DESIGN §4 asks for. Landed with the Codex dispatch and recursive workflow evidence slice; declared at landing (not surfaced by a later cold sweep) so the ratchet arms with the code."
 
 data nfr_dissolve_provider_terminal_absorb: String = "ProviderExecutionState and WorkerProcessEvidence carry a DERIVED terminality projection from inhabitance (dag/std/algebra, DESIGN §3/§4 — the same move as derived equality), so these folds match on the partition rather than on the variant list, the shared arm becomes a named case instead of a wildcard, and the rows delete."
@@ -671,6 +673,11 @@ data non_fold_residue_frontier: List<FrontierRow> = [
     reason: nfr_reason_cost_expr_zero_absorbing_compose,
     trigger: TriggerProse { text: nfr_dissolve_wildcard_total },
   },
+  FrontierRow {
+    subject: PathSubject { path: "src/v2/lens/cost/valuation.dag::multiply_evaluations" },
+    reason: nfr_reason_cost_valuation_zero_annihilator,
+    trigger: TriggerProse { text: nfr_dissolve_wildcard_total },
+  },
   FrontierRow {
     subject: PathSubject { path: "src/v2/lens/fact_density.dag::connective_is_kernel_ambient_atom" },
     reason: nfr_reason_mint_era,

dag/std/algebra.dag

@@ -122,6 +122,11 @@ type FreeMonoid<T>
   = Empty
   | Cons { head: T, tail: FreeMonoid<T> }
 
+type FreeSemigroup<T> {
+  head: T
+  tail: FreeMonoid<T>
+}
+
 type PartialFunction<K, V> {
   lookup: fn(K) -> V?
   empty: PartialFunction<K, V>

dag/test/claim/realization_schedule_critical_path_test.dag

@@ -42,7 +42,7 @@ test fn witness_measured_total_uses_critical_path_basis() -> Bool {
 
 test fn witness_nat_ordering_supports_max() -> Bool {
   match std.nat.nat_compare(a: 7, b: 3) {
-    Greater => nat_max(a: 7, b: 3) == 7
+    Greater => std.nat.nat_max(a: 7, b: 3) == 7
     _ => false
   }
 }

src/v1/stage0/src/std_algebra.rs

@@ -228,6 +228,13 @@ pub struct PointwisePower<T> {
 
 pub type FreeMonoid<T> = Vec<T>;
 
+#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
+pub struct FreeSemigroup<T: Clone> {
+    pub head: T,
+    pub tail: Rc<Vec<T>>,
+    pub _phantom: std::marker::PhantomData<T>,
+}
+
 #[derive(Clone)]
 pub struct PartialFunction<K, V> {
     pub lookup: Rc<dyn Fn(K) -> Option<V>>,

src/v2/compiler/self_host/frontier_probe_types.dag

@@ -42,9 +42,9 @@ import v2.std.optional { Absent, Optional, Present }
 import v2.std.qualified_name { QualifiedName }
 import v2.std.text { String }
 
-data frontier_nonempty_carrier_pattern_note: String = "NonEmptySymbolChain and NonEmptyGrammarChoiceAmbiguityRows join NonEmptyDiagnostics and NonEmptyProcessNodeIds as hand-rolled nonempty carriers beside the generic NonEmptyList refinement (fixture-only today). Counted here so the pattern is visible rather than silently repeated. Dissolve triggers: non_empty_symbol_chain_dissolve_trigger (this module); NonEmptyGrammarChoiceAmbiguityRows trigger on v2.std.grammar_choice_ambiguity."
+data frontier_nonempty_carrier_pattern_note: String = "NonEmptySymbolChain and NonEmptyGrammarChoiceAmbiguityRows join NonEmptyDiagnostics, NonEmptyProcessNodeIds and v2.std.collection FiniteSet as hand-rolled nonempty carriers. The generic carrier is NO LONGER fixture-only: std.algebra FreeSemigroup is a real construction wall in the tree, so this count is now migration debt with a reachable destination rather than a pattern with nowhere to go. Counted here so the pattern is visible rather than silently repeated. Dissolve triggers: non_empty_symbol_chain_dissolve_trigger (this module); NonEmptyGrammarChoiceAmbiguityRows trigger on v2.std.grammar_choice_ambiguity. NonEmptyDiagnostics, NonEmptyProcessNodeIds and FiniteSet carry NO trigger and are untracked stalls owed one - see std.algebra free_semigroup_grounding_note, which names them at the grain a grep decides."
 
-data non_empty_symbol_chain_dissolve_trigger: String = "migrate_when_nonempty_list_refinement_promoted — NonEmptySymbolChain dissolves into NonEmptyList<Symbol> when the refinement is promoted from v2.test.claim.manual.refinement_nonempty_list to std."
+data non_empty_symbol_chain_dissolve_trigger: String = "migrate_when_free_semigroup_available — NonEmptySymbolChain dissolves into std.algebra FreeSemigroup<Symbol>. RETARGETED: this trigger previously named the promotion of the manual Refined<List<T>> fixture to std, and the generic carrier that landed is a record with a head field rather than that refinement, with the NonEmptyList alias deliberately withheld while the fixture lives - so the event as previously spelled will not occur and this row would have stalled untracked. The construction wall is now available; see std.algebra free_semigroup_grounding_note."
 
 data frontier_fixture_cemented_producer_note: String = "FixtureCemented is forward-declared for the fixture-free self-host bar; inhabited by the behavioral-equivalence probe when it detects injected fixtures cementing greens (e.g. add_arrow_eval_allocate_literal, pick-lit hardcoding) — not by frontier_classify_rejection_reason (assemble/emit stage only)."
 

src/v2/lens/cost.dag

@@ -233,17 +233,25 @@ fn symbolic_sequential(a: SymbolicCost, b: SymbolicCost) -> SymbolicCost {
   }
 }
 
+data symbolic_product_zero_absorption_note: String = "Zero is checked on BOTH operands before anything else, and the order is the whole point. An earlier revision matched a's arms first - including UnknownCost - and only then inspected b, so zero times unknown absorbed to zero while unknown times ZERO returned unknown. Multiplication is commutative, so an operand order that changes the answer is a defect on its face, not a stylistic asymmetry: the authority absorbed zero only when zero happened to be written on the left. Found by comparing this authority against v2.lens.cost.valuation, whose exact evaluator has the same obligation - a zero multiplicity means the other factor is never executed, so its work is zero whatever that factor is and however little is known about it. Both paths now answer zero for both orders, so the two agree completely rather than agreeing in one direction and diverging in the other. The scope of that claim is CLASSIFICATION, not provenance, and saying so here is what stops a later reader from concluding the function is symmetric in every respect and then being surprised. One asymmetry survives deliberately: unknown times unknown returns the LEFT operand's diagnostic, so the reverse order returns the right one and the other is dropped. That is a lesser class than what this change fixed - before it, the operand order changed the KIND of the answer, and now it changes only which of two equally valid diagnostics is carried - and it is not introduced here: symbolic_sequential carries the identical left-biased drop, so it is a module-wide pattern of UnknownCost holding exactly one diagnostic. Closing it means widening UnknownCost to carry several, which is a real change with its own witnesses and does not belong on the annihilator fix."
+
 fn symbolic_product(a: SymbolicCost, b: SymbolicCost) -> SymbolicCost {
   match a {
     ConstantCost { value: Zero } => zero_cost()
-    ConstantCost { value: Succ { prev: Zero } } => b
-    UnknownCost { diagnostic: _ } => a
     _ =>
       match b {
         ConstantCost { value: Zero } => zero_cost()
-        ConstantCost { value: Succ { prev: Zero } } => a
-        UnknownCost { diagnostic: _ } => b
-        _ => ProductCost { lhs: a, rhs: b }
+        _ =>
+          match a {
+            ConstantCost { value: Succ { prev: Zero } } => b
+            UnknownCost { diagnostic: _ } => a
+            _ =>
+              match b {
+                ConstantCost { value: Succ { prev: Zero } } => a
+                UnknownCost { diagnostic: _ } => b
+                _ => ProductCost { lhs: a, rhs: b }
+              }
+          }
       }
   }
 }