T-17 lens/synthesis.dag + std/report.dag — advisory cross-algorithm complexity (LowerBoundTechnique + DecisionTree + InformationTheoretic worked cases)

src/v4/lens/synthesis.dag

@@ -51,15 +51,181 @@
 //   - 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, list_append }
+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 synthesis_lens(n: Node) -> List<Report> {
+  match complexity_lens(n: n) {
+    Violates { diagnostic: _ } => Empty
+    Holds { value: realization } =>
+      list_append(
+        left: outcome_to_reports(outcome: assess_decision_tree(n: n, realization: realization)),
+        right: outcome_to_reports(outcome: assess_information_theoretic(n: n, realization: realization))
+      )
+  }
+}
+

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
+}

src/v4/test/claim/lens_synthesis/synthesis_gap_polynomial.dag

@@ -0,0 +1,86 @@
+// 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.synthesis { 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.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))
+}
+
+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 }
+}