Gate the complexity lens by-execution (discoverable test fn witnesses)

src/v2/lens/complexity/algebra_receipts.dag → src/v2/lens/complexity/algebra_receipts_test.dag

@@ -110,3 +110,17 @@ fn variable_sensitive_dominance_actual() -> Bool {
     b: variable_sensitive_dominance_claim.rhs
   ) == variable_sensitive_dominance_claim.expected_dominates
 }
+
+// By-execution gate: the product of two degree-2 polynomials over distinct
+// variables projects to the declared degree-4 multidimensional bound — the
+// degree-addition and variable-merge algebra. A degree miscount goes RED.
+test fn algebra_receipts_polynomial_product_projection_holds() -> Bool {
+  polynomial_product_projected_complexity() == polynomial_product_degree_claim.expected_complexity
+}
+
+// By-execution gate: dominance is variable-sensitive — two linear bounds over
+// DIFFERENT size variables are incomparable (neither dominates). A name-blind
+// comparator that returned dominance would go RED.
+test fn algebra_receipts_variable_sensitive_dominance_holds() -> Bool {
+  variable_sensitive_dominance_actual()
+}

src/v2/lens/complexity/map_id.dag → src/v2/lens/complexity/map_id_test.dag

@@ -3,6 +3,7 @@ module v2.test.lens_complexity.map_id
 
 import v2.lens.complexity { ComplexityBound, complexity_lens, linear_complexity }
 import v2.lens.cost { LinearCost, SizeVariable, SymbolicCost, cost_lens }
+import v2.std.logic { Bool }
 import v2.std.diagnostic {
   AmbiguousIntent,
   Diagnostic,
@@ -22,7 +23,7 @@ import v2.std.node {
   TypeNode,
   SyntheticOccurrence
 }
-import v2.std.witness { Witness }
+import v2.std.witness { Holds, Violates, Witness }
 type LensComplexityClaim {
   input: Node
   expected_cost: SymbolicCost
@@ -69,3 +70,21 @@ fn map_id_actual_cost() -> Witness<SymbolicCost> {
 fn map_id_actual_complexity() -> Witness<ComplexityBound> {
   complexity_lens(n: map_id_input)
 }
+
+// By-execution gate: cost_lens projects the iterative Cardinality body to the
+// declared LinearCost; a wrong fold (e.g. constant or quadratic) goes RED.
+test fn map_id_cost_projection_holds() -> Bool {
+  match map_id_actual_cost() {
+    Holds { value: actual } => actual == map_id_claim.expected_cost
+    Violates { diagnostic: _ } => false
+  }
+}
+
+// By-execution gate: the complexity lens (asymptotic projection of cost_lens)
+// yields the declared linear bound. Discriminates a mis-projected class/variable.
+test fn map_id_complexity_projection_holds() -> Bool {
+  match map_id_actual_complexity() {
+    Holds { value: actual } => actual == map_id_claim.expected_complexity
+    Violates { diagnostic: _ } => false
+  }
+}

src/v2/lens/complexity/nested.dag → src/v2/lens/complexity/nested_test.dag

@@ -37,7 +37,8 @@ import v2.std.node {
   SyntheticOccurrence
 }
 import v2.std.nat { Zero }
-import v2.std.witness { Witness }
+import v2.std.logic { Bool }
+import v2.std.witness { Holds, Violates, Witness }
 type LensComplexityClaim {
   input: Node
   expected_cost: SymbolicCost
@@ -101,3 +102,21 @@ fn nested_actual_cost() -> Witness<SymbolicCost> {
 fn nested_actual_complexity() -> Witness<ComplexityBound> {
   complexity_lens(n: nested_input)
 }
+
+// By-execution gate: nested Cardinality folds to a product cost over the two
+// distinct size variables. A flattened single-variable fold goes RED.
+test fn nested_cost_projection_holds() -> Bool {
+  match nested_actual_cost() {
+    Holds { value: actual } => actual == nested_claim.expected_cost
+    Violates { diagnostic: _ } => false
+  }
+}
+
+// By-execution gate: the asymptotic projection of the product cost is the
+// declared multidimensional quadratic bound (degree 2, both variables).
+test fn nested_complexity_projection_holds() -> Bool {
+  match nested_actual_complexity() {
+    Holds { value: actual } => actual == nested_claim.expected_complexity
+    Violates { diagnostic: _ } => false
+  }
+}

src/v2/lens/complexity/while_external_condition.dag → src/v2/lens/complexity/while_external_condition_test.dag

@@ -25,7 +25,8 @@ import v2.std.node {
   TypeNode,
   SyntheticOccurrence
 }
-import v2.std.witness { Witness }
+import v2.std.logic { Bool }
+import v2.std.witness { Holds, Violates, Witness }
 
 type LensComplexityClaim {
   input: Node
@@ -71,3 +72,22 @@ fn while_external_condition_actual_cost() -> Witness<SymbolicCost> {
 fn while_external_condition_actual_complexity() -> Witness<ComplexityBound> {
   complexity_lens(n: while_external_condition_input)
 }
+
+// By-execution gate (§5 fail-closed): a Loop with an undeclared bound has no
+// modeled cost, so cost_lens must Violate — never fabricate a finite bound. A
+// fail-open lens that returned Holds would go RED here.
+test fn while_external_condition_cost_fails_closed_holds() -> Bool {
+  match while_external_condition_actual_cost() {
+    Holds { value: _ } => false
+    Violates { diagnostic: _ } => true
+  }
+}
+
+// By-execution gate (§5 fail-closed): the asymptotic projection propagates the
+// cost Violation rather than inventing an UnknownComplexity Holds.
+test fn while_external_condition_complexity_fails_closed_holds() -> Bool {
+  match while_external_condition_actual_complexity() {
+    Holds { value: _ } => false
+    Violates { diagnostic: _ } => true
+  }
+}