Dependency-fidelity increment 1: the FidelityVerdict spine (single-authority verdict + input-reachability surface)

docs/plans/dependency-fidelity-design.md

@@ -1,6 +1,6 @@
 # Dependency-Fidelity — making "CI green" mean *declared ≡ witnessed*
 
-Status: design draft (operator-directed, 2026-07-14). Companion to the *enforcement-intent* thread (the same "ask once, compile forever" spine, made quantitative). Reasoned serially per DESIGN.md; each section is a consequence of the ones before it.
+Status: design draft (operator-directed, 2026-07-14). Companion to the [*enforcement-intent* thread](enforcement-intent-design.md) (the same "ask once, compile forever" spine, made quantitative). Reasoned serially per DESIGN.md; each section is a consequence of the ones before it.
 
 ---
 

docs/plans/enforcement-intent-design.md

@@ -1,6 +1,6 @@
 # Enforcement intent — ask once, compile forever
 
-*Status: draft for operator review (2026-07-02). Extends the standing threads "model §1's axioms + enforce the syllogism" and the intent-linearity draft; does not supersede either.*
+*Status: draft for operator review (2026-07-02). Extends the standing threads "model §1's axioms + enforce the syllogism" and the intent-linearity draft; does not supersede either. Quantitative companion: [dependency-fidelity design](dependency-fidelity-design.md) — the same "ask once, compile forever" spine turned into a measured coverage law (CI-green ⟺ declared ≡ witnessed across an affected-set-scoped, mutation-adequate coverage set).*
 
 ## 1. The displaced cost (why this is on-dial)
 

src/v2/lens/dependency_fidelity.dag

@@ -0,0 +1,51 @@
+module v2.lens.dependency_fidelity
+
+import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import std.disposition { SingleAuthority }
+import std.algebra { Empty }
+import v2.std.algebra { is_empty, list_snoc_item }
+import v2.std.collection { List }
+import v2.std.logic { Bool }
+import v2.std.node { Node, Symbol }
+import v2.lens.unused_parameters { UnusedParameterFact, UnusedParametersFact }
+
+data law_note: String = "dependency-fidelity §2: correctness = declared dependency structure equals witnessed (by-execution) structure. This module is the single authority for the fidelity verdict; each arm reports its located discrepancies into ONE verdict lattice, and the FidelityDiscrepancy variant IS the §3 surface it lives on (UnreachedDeclaredInput = input-reachability, UnreachedDeclaredOutput = output-reachability, UnderClaimedEdge/OverClaimedCoupling = interaction fidelity). Input-reachability is consumed from v2.lens.unused_parameters (no re-mint, §3 single authority). Output-reachability and the under-claim/over-claim edge arms are staged slots (docs/plans/dependency-fidelity-design.md §5, §8)."
+
+type FidelityDiscrepancy
+  = UnreachedDeclaredInput { declaration: Node }
+  | UnreachedDeclaredOutput { arm: Symbol }
+  | UnderClaimedEdge { source: Node, dependent: Node }
+  | OverClaimedCoupling { left: Node, right: Node }
+
+type FidelityVerdict
+  = Faithful
+  | Discrepant { findings: List<FidelityDiscrepancy> }
+
+fn verdict_from_discrepancies(findings: List<FidelityDiscrepancy>) -> FidelityVerdict {
+  if is_empty(xs: findings) {
+    Faithful
+  } else {
+    Discrepant { findings: findings }
+  }
+}
+
+fn verdict_is_faithful(v: FidelityVerdict) -> Bool {
+  match v {
+    Faithful => true
+    Discrepant { findings: _ } => false
+  }
+}
+
+fn input_reachability_discrepancies(fact: UnusedParametersFact) -> List<FidelityDiscrepancy> {
+  fold(fact.unused, init: Empty, f: fn(acc, u) {
+    list_snoc_item(xs: acc, item: UnreachedDeclaredInput { declaration: u.declaration })
+  })
+}
+
+fn input_reachability_verdict(fact: UnusedParametersFact) -> FidelityVerdict {
+  verdict_from_discrepancies(findings: input_reachability_discrepancies(fact: fact))
+}
+
+data construction_justification: ConstructionJustification = ConstructionJustification {
+  class: WallAfterGrounding { dissolves_to: SingleAuthority }
+}

src/v2/lens/dependency_fidelity_test.dag

@@ -0,0 +1,29 @@
+module v2.test.lens_dependency_fidelity.dependency_fidelity_test
+
+import v2.std.logic { Bool }
+import std.algebra { Empty }
+import v2.std.algebra { list_snoc_item }
+import v2.std.node { Node, node_synthetic, TypeNode, Atom }
+import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+import v2.lens.unused_parameters { UnusedParameterFact, UnusedParametersFact }
+import v2.lens.dependency_fidelity {
+  input_reachability_verdict,
+  verdict_is_faithful
+}
+
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+fn a_synthetic_param() -> Node {
+  node_synthetic(kind: TypeNode { connective: Atom { identity: ^p } }, children: Empty)
+}
+
+test fn clean_input_surface_is_faithful() -> Bool {
+  return verdict_is_faithful(v: input_reachability_verdict(fact: UnusedParametersFact { unused: Empty }))
+}
+
+test fn one_unused_param_flips_to_discrepant() -> Bool {
+  let fact = UnusedParametersFact {
+    unused: list_snoc_item(xs: Empty, item: UnusedParameterFact { declaration: a_synthetic_param() })
+  }
+  return !verdict_is_faithful(v: input_reachability_verdict(fact: fact))
+}