diff --git a/src/v4/lens/synthesis.dag b/src/v4/lens/synthesis.dag
index 6cff7e6a9ec..60280864f02 100644
--- a/src/v4/lens/synthesis.dag
+++ b/src/v4/lens/synthesis.dag
@@ -15,11 +15,14 @@
 //         Diagnostic; algorithm choice is design-tier — programmer decides)
 //
 // Owns:
-//   - lens read: Node -> Set<Report>  (advisory carrier, NEVER Witness —
-//     Witness is strictly fail-closed per INVARIANTS P3/C-8; advisory
-//     Report must not overload it. Empty set = no advice; non-empty =
+//   - lens read: (Node, LowerBoundTechnique) -> Set<Report>  (advisory carrier,
+//     NEVER Witness — Witness is strictly fail-closed per INVARIANTS P3/C-8;
+//     advisory Report must not overload it. Empty set = no advice; non-empty =
 //     advisory observations, never blocking unless user opts in via
-//     apply_lens(synthesis, Enforce { ... }))
+//     apply_lens(synthesis, Enforce { ... })).
+//     The caller DECLARES which technique applies to the node's I/O relation
+//     class; synthesis_lens does NOT infer it from Node structure
+//     (DECLARED, never inferred per T-17 + Rice-undecidability dissolution).
 //   - the user's DECLARED I/O relation (the function's contract/type —
 //     DECLARED, never inferred). There is NO program-to-program
 //     equivalence: general I/O equivalence is Rice-undecidable, and
@@ -51,15 +54,225 @@
 //   - std/report.dag (advisory carrier)
 //   - lens/complexity.dag (current-complexity input for cross-algorithm comparison)
 //
-// Status: scaffold — fill per TASKS.md T-17
-// Brief: see BRIEF_TEMPLATE.md. C2 reframe (operator-ratified 2026-05-15)
-// COLLAPSES the prior research-tier risk: no undecidable equivalence
-// engine, no unbounded rule library. Risk is now bounded to encoding the
-// CLOSED LowerBoundTechnique set (≈5, fundamental) + authoring a few
-// honest worked examples (sort: decision-tree; matmul: algebraic-rank;
-// string-match: information-theoretic — see TASKS.md T-17). STOP-and-
-// escalate still applies if a relation class needs a 6th technique
-// (substrate extension = stop signal).
+// Status: T-17 filled.
 
 module v4.lens.synthesis
 
+
+import v4.lens.complexity {
+  ComplexityBound,
+  SizedLinearClass,
+  SizedLinearithmicClass,
+  complexity_lens,
+  complexity_bound_class,
+  single_complexity_variable,
+  sized_complexity
+}
+import v4.lens.cost {
+  ClassLinear,
+  ClassLinearithmic,
+  SizeVariable,
+  asymptotic_class_dominates
+}
+import v4.std.algebra { Cons, Empty }
+import v4.std.collection { List }
+import v4.std.diagnostic {
+  AmbiguousIntent,
+  Diagnostic,
+  Locus,
+  Unavailable,
+  node_locus
+}
+import v4.std.node { Node, Symbol }
+import v4.std.report { Report, SynthesisGapDecisionTree, SynthesisGapInformationTheoretic }
+import v4.std.witness { Holds, Violates }
+
+
+data synthesis_no_technique_reason_symbol: Symbol = synthesis_no_technique_reason_symbol
+
+
+// 🟢 coproduct — closed set. STOP-and-escalate if a 6th variant is needed.
+type LowerBoundTechnique
+  = DecisionTree
+  | AlgebraicRank
+  | AdversaryCommunication
+  | InformationTheoretic
+  | ReductionConditional
+
+// 🟢 product — declared relation class + applicable technique.
+type DeclaredRelationBound {
+  technique: LowerBoundTechnique
+  lower_bound: ComplexityBound
+  relation_locus: Locus
+}
+
+// 🟢 coproduct — outcome of one synthesis probe.
+type SynthesisOutcome
+  = SynthesisGap {
+      realization_cost: ComplexityBound
+      lower_bound: DeclaredRelationBound
+      report: Report
+    }
+  | SynthesisOptimal {
+      realization_cost: ComplexityBound
+      lower_bound: DeclaredRelationBound
+    }
+  | SynthesisNoTechnique {
+      diagnostic: Diagnostic
+    }
+
+
+fn synthesis_no_technique_diagnostic(n: Node) -> Diagnostic {
+  Diagnostic {
+    reason: synthesis_no_technique_reason_symbol,
+    at: node_locus(node: n),
+    correction: Unavailable { reason: AmbiguousIntent }
+  }
+}
+
+fn decision_tree_declared_bound(n: Node) -> DeclaredRelationBound {
+  DeclaredRelationBound {
+    technique: DecisionTree,
+    lower_bound: sized_complexity(
+      class: SizedLinearithmicClass,
+      variables: single_complexity_variable(size_var: SizeVariable { source: n })
+    ),
+    relation_locus: node_locus(node: n)
+  }
+}
+
+fn information_theoretic_declared_bound(n: Node) -> DeclaredRelationBound {
+  DeclaredRelationBound {
+    technique: InformationTheoretic,
+    lower_bound: sized_complexity(
+      class: SizedLinearClass,
+      variables: single_complexity_variable(size_var: SizeVariable { source: n })
+    ),
+    relation_locus: node_locus(node: n)
+  }
+}
+
+// DecisionTree: realization > Θ(n log n) → gap (asymptotic_class_dominates is strict for ClassLinearithmic).
+fn assess_decision_tree(n: Node, realization: ComplexityBound) -> SynthesisOutcome {
+  if asymptotic_class_dominates(
+    a: complexity_bound_class(b: realization),
+    b: ClassLinearithmic
+  ) {
+    SynthesisGap {
+      realization_cost: realization,
+      lower_bound: decision_tree_declared_bound(n: n),
+      report: Report {
+        reason: SynthesisGapDecisionTree,
+        at: node_locus(node: n)
+      }
+    }
+  } else {
+    SynthesisOptimal {
+      realization_cost: realization,
+      lower_bound: decision_tree_declared_bound(n: n)
+    }
+  }
+}
+
+// InformationTheoretic: realization strictly > Ω(n) → gap.
+// Double-dominance: outer gate tests dominates(realization, ClassLinear) — true iff ≥ linear
+// (reflexive for ClassLinear); inner tests dominates(ClassLinear, realization) — true iff equal,
+// false iff strictly greater → gap. Avoids == in if-conditions: parser greedily parses
+// ClassLinear{...} as a struct literal when == appears, eating the if-body and leaving else dangling.
+// complexity_bound_class called twice (pure function; let-binding before if-else is also
+// rejected by the resolve-posture gate strict mode).
+fn assess_information_theoretic(n: Node, realization: ComplexityBound) -> SynthesisOutcome {
+  if asymptotic_class_dominates(
+    a: complexity_bound_class(b: realization),
+    b: ClassLinear
+  ) {
+    if asymptotic_class_dominates(
+      a: ClassLinear,
+      b: complexity_bound_class(b: realization)
+    ) {
+      SynthesisOptimal {
+        realization_cost: realization,
+        lower_bound: information_theoretic_declared_bound(n: n)
+      }
+    } else {
+      SynthesisGap {
+        realization_cost: realization,
+        lower_bound: information_theoretic_declared_bound(n: n),
+        report: Report {
+          reason: SynthesisGapInformationTheoretic,
+          at: node_locus(node: n)
+        }
+      }
+    }
+  } else {
+    // Realization is sub-linear: InformationTheoretic has no lower-bound comparison for this class.
+    SynthesisNoTechnique {
+      diagnostic: synthesis_no_technique_diagnostic(n: n)
+    }
+  }
+}
+
+fn outcome_to_reports(outcome: SynthesisOutcome) -> List<Report> {
+  match outcome {
+    SynthesisGap { realization_cost: _, lower_bound: _, report: r } =>
+      Cons { head: r, tail: Empty }
+    SynthesisOptimal { realization_cost: _, lower_bound: _ } => Empty
+    SynthesisNoTechnique { diagnostic: _ } => Empty
+  }
+}
+
+fn outcome_to_diagnostics(outcome: SynthesisOutcome) -> List<Diagnostic> {
+  match outcome {
+    SynthesisGap { realization_cost: _, lower_bound: _, report: _ } => Empty
+    SynthesisOptimal { realization_cost: _, lower_bound: _ } => Empty
+    SynthesisNoTechnique { diagnostic: d } => Cons { head: d, tail: Empty }
+  }
+}
+
+// Caller DECLARES declared_technique — the technique the caller's I/O relation class
+// is subject to. Probes only run for the declared technique; no unconditional sweep.
+// AlgebraicRank / AdversaryCommunication / ReductionConditional → SynthesisNoTechnique with
+// honest diagnostic. Terminal: no worked example is planned here; these techniques route through
+// the diagnostic channel by design. Adding a 4th worked-example technique requires a new
+// LowerBoundTechnique variant, which is STOP-and-escalate-gated (see 🟢 mark above).
+fn synthesis_lens(n: Node, declared_technique: LowerBoundTechnique) -> List<Report> {
+  match complexity_lens(n: n) {
+    Violates { diagnostic: _ } => Empty
+    Holds { value: realization } =>
+      match declared_technique {
+        DecisionTree =>
+          outcome_to_reports(outcome: assess_decision_tree(n: n, realization: realization))
+        AlgebraicRank =>
+          outcome_to_reports(outcome: SynthesisNoTechnique { diagnostic: synthesis_no_technique_diagnostic(n: n) })
+        AdversaryCommunication =>
+          outcome_to_reports(outcome: SynthesisNoTechnique { diagnostic: synthesis_no_technique_diagnostic(n: n) })
+        InformationTheoretic =>
+          outcome_to_reports(outcome: assess_information_theoretic(n: n, realization: realization))
+        ReductionConditional =>
+          outcome_to_reports(outcome: SynthesisNoTechnique { diagnostic: synthesis_no_technique_diagnostic(n: n) })
+      }
+  }
+}
+
+// Companion: surfaces diagnostics for the declared technique — both upstream complexity
+// failures and SynthesisNoTechnique cases. Complexity Violates propagates here so callers
+// do not need to call complexity_lens separately to detect upstream failure.
+fn synthesis_lens_diagnostics(n: Node, declared_technique: LowerBoundTechnique) -> List<Diagnostic> {
+  match complexity_lens(n: n) {
+    Violates { diagnostic: d } => Cons { head: d, tail: Empty }
+    Holds { value: realization } =>
+      match declared_technique {
+        DecisionTree =>
+          outcome_to_diagnostics(outcome: assess_decision_tree(n: n, realization: realization))
+        AlgebraicRank =>
+          outcome_to_diagnostics(outcome: SynthesisNoTechnique { diagnostic: synthesis_no_technique_diagnostic(n: n) })
+        AdversaryCommunication =>
+          outcome_to_diagnostics(outcome: SynthesisNoTechnique { diagnostic: synthesis_no_technique_diagnostic(n: n) })
+        InformationTheoretic =>
+          outcome_to_diagnostics(outcome: assess_information_theoretic(n: n, realization: realization))
+        ReductionConditional =>
+          outcome_to_diagnostics(outcome: SynthesisNoTechnique { diagnostic: synthesis_no_technique_diagnostic(n: n) })
+      }
+  }
+}
+
diff --git a/src/v4/std/report.dag b/src/v4/std/report.dag
index fd73cb7f1e1..568bee250cb 100644
--- a/src/v4/std/report.dag
+++ b/src/v4/std/report.dag
@@ -1,9 +1,24 @@
 // src/v4/std/report.dag
 // Scope: advisory report carrier.
 // Anchor: docs/r4-carve-out-routing.md C7.
-// Owns: Report, ReportReason, ReportSuggestion.
-// Consumes: std diagnostic, std node.
-// Status: scaffold for T-17; advisory discipline in C7-REPORT.
+// Owns: Report, ReportReason.
+// Consumes: std diagnostic.
+// Status: T-17 filled.
 
 module v4.std.report
 
+
+import v4.std.diagnostic { Locus }
+
+
+// 🟢 coproduct — closed set; disjoint from Diagnostic.reason (Symbol) per T-17 brief (TASKS.md:800).
+// STOP-and-escalate before adding a variant for a new advisory lens.
+type ReportReason
+  = SynthesisGapDecisionTree
+  | SynthesisGapInformationTheoretic
+
+// 🟢 grounded — advisory carrier; never Witness (INVARIANTS P3/C-8).
+type Report {
+  reason: ReportReason
+  at: Locus
+}
diff --git a/src/v4/test/claim/lens_synthesis/synthesis_gap_information_theoretic.dag b/src/v4/test/claim/lens_synthesis/synthesis_gap_information_theoretic.dag
new file mode 100644
index 00000000000..7a5e6cba0d7
--- /dev/null
+++ b/src/v4/test/claim/lens_synthesis/synthesis_gap_information_theoretic.dag
@@ -0,0 +1,124 @@
+// src/v4/test/claim/lens_synthesis/synthesis_gap_information_theoretic.dag
+// Scope: T-17 worked claim — polynomial-cost node emits non-empty synthesis advisory
+//        when InformationTheoretic technique is declared (O(n^2) > Ω(n) lower bound).
+// Owns: claim_synthesis_gap_information_theoretic.
+// Consumes: lens synthesis, std algebra, std node, std verification.
+// Status: T-17 filled.
+
+module v4.test.claim.lens_synthesis.synthesis_gap_information_theoretic
+
+import v4.lens.complexity { ComplexityBound, complexity_lens }
+import v4.lens.synthesis {
+  InformationTheoretic,
+  SynthesisGap,
+  SynthesisNoTechnique,
+  SynthesisOptimal,
+  assess_information_theoretic,
+  synthesis_lens
+}
+import v4.std.algebra { non_empty }
+import v4.std.logic { Bool }
+import v4.std.node {
+  Atom,
+  Cardinality,
+  ComputationNode,
+  Edge,
+  Node,
+  Positional,
+  Symbol,
+  Transform,
+  TypeNode
+}
+import v4.std.report { SynthesisGapDecisionTree, SynthesisGapInformationTheoretic }
+import v4.std.verification {
+  EqualsClaim,
+  TestClaim,
+  TestClassification,
+  T19ManualAnchorAbsent,
+  Tier1,
+  Unit,
+  t19_manual_claim_anchor
+}
+import v4.std.witness { Holds, Violates }
+
+data synthesis_gap_it_atom_symbol: Symbol = synthesis_gap_it_atom_symbol
+data synthesis_gap_it_sentinel_symbol: Symbol = synthesis_gap_it_sentinel_symbol
+
+data synthesis_gap_it_leaf: Node = Node {
+  kind: TypeNode { connective: Atom { identity: synthesis_gap_it_atom_symbol } },
+  children: []
+}
+
+data synthesis_gap_it_body: Node = Node {
+  kind: ComputationNode { behavior: Transform },
+  children: [
+    Edge { label: Positional, target: synthesis_gap_it_leaf }
+  ]
+}
+
+data synthesis_gap_it_inner: Node = Node {
+  kind: TypeNode { connective: Cardinality },
+  children: [
+    Edge { label: Positional, target: synthesis_gap_it_body }
+  ]
+}
+
+// Nested Cardinality → O(n^2) > Ω(n); InformationTheoretic lower bound is Ω(n).
+data synthesis_gap_it_input: Node = Node {
+  kind: TypeNode { connective: Cardinality },
+  children: [
+    Edge { label: Positional, target: synthesis_gap_it_inner }
+  ]
+}
+
+data synthesis_gap_it_sentinel: Node = Node {
+  kind: TypeNode { connective: Atom { identity: synthesis_gap_it_sentinel_symbol } },
+  children: []
+}
+
+fn synthesis_gap_it_lens_non_empty() -> Bool {
+  non_empty(synthesis_lens(n: synthesis_gap_it_input, declared_technique: InformationTheoretic))
+}
+
+fn synthesis_gap_it_rhs() -> Node {
+  if synthesis_gap_it_lens_non_empty() {
+    synthesis_gap_it_input
+  } else {
+    synthesis_gap_it_sentinel
+  }
+}
+
+data claim_synthesis_gap_information_theoretic: TestClaim = EqualsClaim {
+  label: "lens_synthesis/synthesis_gap_it: polynomial cost emits non-empty IT synthesis advisory",
+  t19_anchor: t19_manual_claim_anchor(anchor: T19ManualAnchorAbsent),
+  lhs: synthesis_gap_it_input,
+  rhs: synthesis_gap_it_rhs(),
+  classification: TestClassification { tier: Tier1, layer: Unit }
+}
+
+// Pins the published ReportReason to SynthesisGapInformationTheoretic.
+// Bypasses List<T> to avoid bootstrap generic-T field-access limitation (same as polynomial
+// claim): calls assess_information_theoretic directly so r binds from a concrete coproduct field.
+fn synthesis_gap_it_first_reason_node() -> Node {
+  match complexity_lens(n: synthesis_gap_it_input) {
+    Violates { diagnostic: _ } => synthesis_gap_it_sentinel
+    Holds { value: realization } =>
+      match assess_information_theoretic(n: synthesis_gap_it_input, realization: realization) {
+        SynthesisGap { realization_cost: _, lower_bound: _, report: r } =>
+          match r.reason {
+            SynthesisGapDecisionTree => synthesis_gap_it_sentinel
+            SynthesisGapInformationTheoretic => synthesis_gap_it_input
+          }
+        SynthesisOptimal { realization_cost: _, lower_bound: _ } => synthesis_gap_it_sentinel
+        SynthesisNoTechnique { diagnostic: _ } => synthesis_gap_it_sentinel
+      }
+  }
+}
+
+data claim_synthesis_gap_it_reason: TestClaim = EqualsClaim {
+  label: "lens_synthesis/synthesis_gap_it: report reason is SynthesisGapInformationTheoretic",
+  t19_anchor: t19_manual_claim_anchor(anchor: T19ManualAnchorAbsent),
+  lhs: synthesis_gap_it_input,
+  rhs: synthesis_gap_it_first_reason_node(),
+  classification: TestClassification { tier: Tier1, layer: Unit }
+}
diff --git a/src/v4/test/claim/lens_synthesis/synthesis_gap_polynomial.dag b/src/v4/test/claim/lens_synthesis/synthesis_gap_polynomial.dag
new file mode 100644
index 00000000000..6bbc5828af7
--- /dev/null
+++ b/src/v4/test/claim/lens_synthesis/synthesis_gap_polynomial.dag
@@ -0,0 +1,124 @@
+// src/v4/test/claim/lens_synthesis/synthesis_gap_polynomial.dag
+// Scope: T-17 worked claim — polynomial-cost node emits non-empty synthesis advisory (DecisionTree gap).
+// Owns: claim_synthesis_gap_polynomial.
+// Consumes: lens synthesis, std algebra, std node, std verification.
+// Status: T-17 filled.
+
+module v4.test.claim.lens_synthesis.synthesis_gap_polynomial
+
+import v4.lens.complexity { ComplexityBound, complexity_lens }
+import v4.lens.synthesis {
+  DecisionTree,
+  SynthesisGap,
+  SynthesisNoTechnique,
+  SynthesisOptimal,
+  assess_decision_tree,
+  synthesis_lens
+}
+import v4.std.algebra { non_empty }
+import v4.std.logic { Bool }
+import v4.std.witness { Holds, Violates }
+import v4.std.node {
+  Atom,
+  Cardinality,
+  ComputationNode,
+  Edge,
+  Node,
+  Positional,
+  Symbol,
+  Transform,
+  TypeNode
+}
+import v4.std.report { SynthesisGapDecisionTree, SynthesisGapInformationTheoretic }
+import v4.std.verification {
+  EqualsClaim,
+  TestClaim,
+  TestClassification,
+  T19ManualAnchorAbsent,
+  Tier1,
+  Unit,
+  t19_manual_claim_anchor
+}
+
+data synthesis_gap_poly_atom_symbol: Symbol = synthesis_gap_poly_atom_symbol
+data synthesis_gap_poly_sentinel_symbol: Symbol = synthesis_gap_poly_sentinel_symbol
+
+data synthesis_gap_poly_leaf: Node = Node {
+  kind: TypeNode { connective: Atom { identity: synthesis_gap_poly_atom_symbol } },
+  children: []
+}
+
+data synthesis_gap_poly_body: Node = Node {
+  kind: ComputationNode { behavior: Transform },
+  children: [
+    Edge { label: Positional, target: synthesis_gap_poly_leaf }
+  ]
+}
+
+data synthesis_gap_poly_inner: Node = Node {
+  kind: TypeNode { connective: Cardinality },
+  children: [
+    Edge { label: Positional, target: synthesis_gap_poly_body }
+  ]
+}
+
+// Nested Cardinality → polynomial (O(n^2)) complexity; strictly dominates Θ(n log n) lower bound.
+data synthesis_gap_poly_input: Node = Node {
+  kind: TypeNode { connective: Cardinality },
+  children: [
+    Edge { label: Positional, target: synthesis_gap_poly_inner }
+  ]
+}
+
+data synthesis_gap_poly_sentinel: Node = Node {
+  kind: TypeNode { connective: Atom { identity: synthesis_gap_poly_sentinel_symbol } },
+  children: []
+}
+
+fn synthesis_gap_poly_lens_non_empty() -> Bool {
+  non_empty(synthesis_lens(n: synthesis_gap_poly_input, declared_technique: DecisionTree))
+}
+
+fn synthesis_gap_poly_rhs() -> Node {
+  if synthesis_gap_poly_lens_non_empty() {
+    synthesis_gap_poly_input
+  } else {
+    synthesis_gap_poly_sentinel
+  }
+}
+
+data claim_synthesis_gap_polynomial: TestClaim = EqualsClaim {
+  label: "lens_synthesis/synthesis_gap_polynomial: polynomial cost emits non-empty synthesis advisory",
+  t19_anchor: t19_manual_claim_anchor(anchor: T19ManualAnchorAbsent),
+  lhs: synthesis_gap_poly_input,
+  rhs: synthesis_gap_poly_rhs(),
+  classification: TestClassification { tier: Tier1, layer: Unit }
+}
+
+// Pins the published ReportReason to SynthesisGapDecisionTree.
+// Bypasses List<T> to avoid bootstrap generic-T field-access limitation: r.reason fails when r
+// is a generic lambda param T even after T=Report is established. Calls assess_decision_tree
+// directly so r is bound from a concrete coproduct field (report: Report), not generic T.
+fn synthesis_gap_poly_first_reason_node() -> Node {
+  match complexity_lens(n: synthesis_gap_poly_input) {
+    Violates { diagnostic: _ } => synthesis_gap_poly_sentinel
+    Holds { value: realization } =>
+      match assess_decision_tree(n: synthesis_gap_poly_input, realization: realization) {
+        SynthesisGap { realization_cost: _, lower_bound: _, report: r } =>
+          match r.reason {
+            SynthesisGapDecisionTree => synthesis_gap_poly_input
+            SynthesisGapInformationTheoretic => synthesis_gap_poly_sentinel
+          }
+        SynthesisOptimal { realization_cost: _, lower_bound: _ } => synthesis_gap_poly_sentinel
+        SynthesisNoTechnique { diagnostic: _ } => synthesis_gap_poly_sentinel
+      }
+  }
+}
+
+data claim_synthesis_gap_poly_decision_tree_reason: TestClaim = EqualsClaim {
+  label: "lens_synthesis/synthesis_gap_polynomial: report reason is SynthesisGapDecisionTree",
+  t19_anchor: t19_manual_claim_anchor(anchor: T19ManualAnchorAbsent),
+  lhs: synthesis_gap_poly_input,
+  rhs: synthesis_gap_poly_first_reason_node(),
+  classification: TestClassification { tier: Tier1, layer: Unit }
+}
diff --git a/src/v4/test/claim/lens_synthesis/synthesis_no_technique_diagnostic.dag b/src/v4/test/claim/lens_synthesis/synthesis_no_technique_diagnostic.dag
new file mode 100644
index 00000000000..68ed4bb4279
--- /dev/null
+++ b/src/v4/test/claim/lens_synthesis/synthesis_no_technique_diagnostic.dag
@@ -0,0 +1,87 @@
+// src/v4/test/claim/lens_synthesis/synthesis_no_technique_diagnostic.dag
+// Scope: T-17 worked claim — AlgebraicRank (non-implemented technique) emits a
+//        non-empty SynthesisNoTechnique diagnostic from synthesis_lens_diagnostics.
+// Owns: claim_synthesis_no_technique_diagnostic.
+// Consumes: lens synthesis, std algebra, std node, std verification.
+// Status: T-17 filled.
+
+module v4.test.claim.lens_synthesis.synthesis_no_technique_diagnostic
+
+import v4.lens.synthesis { AlgebraicRank, synthesis_lens_diagnostics }
+import v4.std.algebra { non_empty }
+import v4.std.logic { Bool }
+import v4.std.node {
+  Atom,
+  Cardinality,
+  ComputationNode,
+  Edge,
+  Node,
+  Positional,
+  Symbol,
+  Transform,
+  TypeNode
+}
+import v4.std.verification {
+  EqualsClaim,
+  TestClaim,
+  TestClassification,
+  T19ManualAnchorAbsent,
+  Tier1,
+  Unit,
+  t19_manual_claim_anchor
+}
+
+data synthesis_no_tech_atom_symbol: Symbol = synthesis_no_tech_atom_symbol
+data synthesis_no_tech_sentinel_symbol: Symbol = synthesis_no_tech_sentinel_symbol
+
+data synthesis_no_tech_leaf: Node = Node {
+  kind: TypeNode { connective: Atom { identity: synthesis_no_tech_atom_symbol } },
+  children: []
+}
+
+data synthesis_no_tech_body: Node = Node {
+  kind: ComputationNode { behavior: Transform },
+  children: [
+    Edge { label: Positional, target: synthesis_no_tech_leaf }
+  ]
+}
+
+data synthesis_no_tech_inner: Node = Node {
+  kind: TypeNode { connective: Cardinality },
+  children: [
+    Edge { label: Positional, target: synthesis_no_tech_body }
+  ]
+}
+
+// Polynomial node: complexity_lens gives Holds; AlgebraicRank has no worked example.
+data synthesis_no_tech_input: Node = Node {
+  kind: TypeNode { connective: Cardinality },
+  children: [
+    Edge { label: Positional, target: synthesis_no_tech_inner }
+  ]
+}
+
+data synthesis_no_tech_sentinel: Node = Node {
+  kind: TypeNode { connective: Atom { identity: synthesis_no_tech_sentinel_symbol } },
+  children: []
+}
+
+fn synthesis_no_tech_diagnostics_non_empty() -> Bool {
+  non_empty(synthesis_lens_diagnostics(n: synthesis_no_tech_input, declared_technique: AlgebraicRank))
+}
+
+fn synthesis_no_tech_rhs() -> Node {
+  if synthesis_no_tech_diagnostics_non_empty() {
+    synthesis_no_tech_input
+  } else {
+    synthesis_no_tech_sentinel
+  }
+}
+
+data claim_synthesis_no_technique_diagnostic: TestClaim = EqualsClaim {
+  label: "lens_synthesis/synthesis_no_technique_diagnostic: AlgebraicRank emits SynthesisNoTechnique diagnostic",
+  t19_anchor: t19_manual_claim_anchor(anchor: T19ManualAnchorAbsent),
+  lhs: synthesis_no_tech_input,
+  rhs: synthesis_no_tech_rhs(),
+  classification: TestClassification { tier: Tier1, layer: Unit }
+}