W3.2 coercion realization (Rung 3): preservation_rule_refinement_widening + CoercionQuality::Widened — make coercion REALIZE (rust i32→python int Accepted), not just fail-closed

src/v4/extdeps/coercion_widening.dag

@@ -0,0 +1,50 @@
+// src/v4/extdeps/coercion_widening.dag
+// Scope: cross-target faithful refinement widening pair registry (MVP rust i32 → python int).
+// Anchor: ROADMAP.md coercion (i32 → arbitrary-precision int); W3.2 Leg B.
+// Status: MVP pair table lives here; std/refinement_widening_predicate proves bundle evidence (P2).
+
+
+module v4.extdeps.coercion_widening
+
+
+import v4.extdeps.languages.python { python_int_inhabitant_node }
+import v4.extdeps.languages.rust { rust_inhabitant_i32_node }
+import v4.std.coercion {
+  CoercionCandidateSet,
+  CoercionResult,
+  coercion_fold_refinement_widening
+}
+import v4.std.constraints { CanonicalGrounding }
+import v4.std.diagnostic { Outcome }
+import v4.std.find_witness {
+  PreservationPredicate,
+  TargetDeclaredPriority,
+  preservation_rule_refinement_widening
+}
+import v4.std.node { Node }
+import v4.std.refinement_widening_predicate { refinement_widening_predicate_algebra }
+
+
+fn mvp_rust_i32_python_int_refinement_widening_predicate() -> PreservationPredicate {
+  PreservationPredicate {
+    algebra: refinement_widening_predicate_algebra(
+      source: rust_inhabitant_i32_node(),
+      candidate: python_int_inhabitant_node()
+    ),
+    preservation_rule: preservation_rule_refinement_widening
+  }
+}
+
+
+fn coercion_fold_mvp_rust_i32_to_python_int_widening(
+  source: CanonicalGrounding,
+  candidates: CoercionCandidateSet,
+  priority: Node,
+) -> Outcome<CoercionResult> {
+  coercion_fold_refinement_widening(
+    source: source,
+    candidates: candidates,
+    policy: TargetDeclaredPriority { priority: priority },
+    predicate: mvp_rust_i32_python_int_refinement_widening_predicate()
+  )
+}

src/v4/std/coercion.dag

@@ -36,7 +36,8 @@ import v4.std.find_witness {
   find_witness_reason_invalid_witness,
   find_witness_reason_no_candidate,
   find_witness_reason_not_realized,
-  preservation_rule_exact_structural_equality_zip_fold
+  preservation_rule_exact_structural_equality_zip_fold,
+  preservation_rule_refinement_widening
 }
 import v4.std.node { Conj, Edge, Named, Node, Symbol, TypeNode, well_formed }
 import v4.std.witness { HomomorphismWitness, StructuralPropertyWitness }
@@ -46,6 +47,7 @@ data coercion_homomorphism_evidence_source: Symbol = coercion_homomorphism_evide
 data coercion_homomorphism_evidence_candidate: Symbol = coercion_homomorphism_evidence_candidate
 data coercion_homomorphism_evidence_find_witness: Symbol = coercion_homomorphism_evidence_find_witness
 data homomorphism_rule_exact_structural_equality: Symbol = homomorphism_rule_exact_structural_equality
+data homomorphism_rule_refinement_widening: Symbol = homomorphism_rule_refinement_widening
 data coercion_not_realized: Symbol = coercion_not_realized
 data coercion_mismatch_no_target: Symbol = coercion_mismatch_no_target
 data coercion_mismatch_ambiguous: Symbol = coercion_mismatch_ambiguous
@@ -63,6 +65,7 @@ type FindWitnessRejectionKind
 type CoercionQuality
   = Identity
   | Exact
+  | Widened
 // 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL.
 type CoercionMismatchKind
   = NoTargetCandidate
@@ -244,7 +247,7 @@ fn coercion_homomorphism_evidence(
     ]
   }
 }
-fn coercion_fold(
+fn coercion_fold_exact_structural(
   source: CanonicalGrounding,
   candidates: CoercionCandidateSet,
   policy: TargetSelectionPolicy,
@@ -280,6 +283,51 @@ fn coercion_fold(
       }
   }
 }
+fn coercion_fold(
+  source: CanonicalGrounding,
+  candidates: CoercionCandidateSet,
+  policy: TargetSelectionPolicy,
+) -> Outcome<CoercionResult> {
+  coercion_fold_exact_structural(
+    source: source,
+    candidates: candidates,
+    policy: policy
+  )
+}
+fn coercion_fold_refinement_widening(
+  source: CanonicalGrounding,
+  candidates: CoercionCandidateSet,
+  policy: TargetSelectionPolicy,
+  predicate: PreservationPredicate,
+) -> Outcome<CoercionResult> {
+  match find_witness(
+    source_facts: source.node,
+    candidates: candidates.set,
+    predicate: predicate,
+    multiplicity_policy: TargetSelection { policy: policy }
+  ) {
+    Accepted { value: fw, diagnostics: fw_d } =>
+      Accepted {
+        value: CoercionResult {
+          target: fw.candidate,
+          quality: Widened,
+          witness: CoercionWitness {
+            homomorphism: HomomorphismWitness {
+              rule: homomorphism_rule_refinement_widening,
+              evidence: coercion_homomorphism_evidence(source: source, fw: fw)
+            }
+          }
+        },
+        diagnostics: fw_d
+      }
+    Rejected { diagnostics: r } =>
+      match coercion_wrap_find_witness_rejection(source: source, upstream: r) {
+        Accepted { value: wrapped, diagnostics: _ } =>
+          Rejected { diagnostics: wrapped }
+        Rejected { diagnostics: wrap_r } => Rejected { diagnostics: wrap_r }
+      }
+  }
+}
 fn coercion_fold_with_declared_priority(
   source: CanonicalGrounding,
   candidates: CoercionCandidateSet,
@@ -291,3 +339,16 @@ fn coercion_fold_with_declared_priority(
     policy: TargetDeclaredPriority { priority: priority }
   )
 }
+fn coercion_fold_refinement_widening_with_declared_priority(
+  source: CanonicalGrounding,
+  candidates: CoercionCandidateSet,
+  priority: Node,
+  predicate: PreservationPredicate,
+) -> Outcome<CoercionResult> {
+  coercion_fold_refinement_widening(
+    source: source,
+    candidates: candidates,
+    policy: TargetDeclaredPriority { priority: priority },
+    predicate: predicate
+  )
+}

src/v4/std/find_witness.dag

@@ -25,6 +25,7 @@ import v4.std.constraint_satisfaction_predicate {
 import v4.std.exact_structural_equality_zip_fold_predicate {
   exact_structural_equality_zip_fold_preservation_holds
 }
+import v4.std.refinement_widening_predicate { refinement_widening_preservation_holds }
 import v4.std.node { Node, Symbol, well_formed }
 import v4.std.witness { StructuralPropertyWitness }
 data find_witness_reason_no_candidate: Symbol = find_witness_reason_no_candidate
@@ -33,6 +34,7 @@ data find_witness_reason_not_realized: Symbol = find_witness_reason_not_realized
 data find_witness_reason_invalid_witness: Symbol = find_witness_reason_invalid_witness
 data preservation_rule_constraint_satisfaction: Symbol = preservation_rule_constraint_satisfaction
 data preservation_rule_exact_structural_equality_zip_fold: Symbol = preservation_rule_exact_structural_equality_zip_fold
+data preservation_rule_refinement_widening: Symbol = preservation_rule_refinement_widening
 type CandidateSet {
   candidates: List<Node>
   closedness: StructuralPropertyWitness
@@ -114,6 +116,12 @@ fn preservation_predicate_holds(
         candidate: candidate,
         algebra: predicate.algebra
       )
+    preservation_rule_refinement_widening =>
+      refinement_widening_preservation_holds(
+        source_facts: source_facts,
+        candidate: candidate,
+        algebra: predicate.algebra
+      )
     _ => false
   }
 }
@@ -240,6 +248,13 @@ fn find_witness(
         predicate: predicate,
         multiplicity_policy: multiplicity_policy
       )
+    preservation_rule_refinement_widening =>
+      find_witness_realized(
+        source_facts: source_facts,
+        candidates: candidates,
+        predicate: predicate,
+        multiplicity_policy: multiplicity_policy
+      )
     _ => outcome_rejected(find_witness_not_realized_diagnostic(source_facts: source_facts))
   }
 }
@@ -250,7 +265,8 @@ fn find_witness_realized(
   multiplicity_policy: MultiplicityPolicy
 ) -> Outcome<FindWitnessResult> {
   if (predicate.preservation_rule != preservation_rule_constraint_satisfaction)
-    && (predicate.preservation_rule != preservation_rule_exact_structural_equality_zip_fold) {
+    && (predicate.preservation_rule != preservation_rule_exact_structural_equality_zip_fold)
+    && (predicate.preservation_rule != preservation_rule_refinement_widening) {
     outcome_rejected(find_witness_not_realized_diagnostic(source_facts: source_facts))
   } else {
   let passing_count = passing_candidate_count(
@@ -316,6 +332,13 @@ fn verify_witness(
         predicate: predicate,
         witness: witness
       )
+    preservation_rule_refinement_widening =>
+      verify_witness_realized(
+        source_facts: source_facts,
+        candidate: candidate,
+        predicate: predicate,
+        witness: witness
+      )
     _ => outcome_rejected(find_witness_not_realized_diagnostic(source_facts: source_facts))
   }
 }

src/v4/std/refinement_widening_predicate.dag

@@ -0,0 +1,81 @@
+// src/v4/std/refinement_widening_predicate.dag
+// Scope: mechanical refinement-widening preservation check (leaf — no extdeps import).
+// Anchor: ROADMAP.md coercion faithful widening; design-v4-compiler-homomorphism.md Pass B.
+// Status: bundle-encoded pair evidence on PreservationPredicate.algebra; axis-general registry is forward work.
+
+
+module v4.std.refinement_widening_predicate
+
+
+import v4.std.diagnostic { Accepted, Outcome, Rejected }
+import v4.std.node { Conj, Edge, Named, Node, Symbol, TypeNode, well_formed }
+import v4.std.node_query { find_named_child }
+
+
+data refinement_widening_field_source: Symbol = refinement_widening_field_source
+data refinement_widening_field_candidate: Symbol = refinement_widening_field_candidate
+data refinement_widening_field_source_facts: Symbol = refinement_widening_field_source_facts
+
+
+fn refinement_widening_predicate_algebra(
+  source: Node,
+  candidate: Node,
+) -> Node {
+  Node {
+    kind: TypeNode { connective: Conj },
+    children: [
+      Edge {
+        label: Named { name: refinement_widening_field_source },
+        target: source
+      },
+      Edge {
+        label: Named { name: refinement_widening_field_candidate },
+        target: candidate
+      },
+      Edge {
+        label: Named { name: refinement_widening_field_source_facts },
+        target: source
+      }
+    ]
+  }
+}
+
+
+fn refinement_widening_bundle_holds(
+  source_facts: Node,
+  candidate: Node,
+  algebra: Node,
+) -> Bool {
+  match find_named_child(root: algebra, name: refinement_widening_field_source) {
+    Accepted { value: bundled_source, diagnostics: None } =>
+      match find_named_child(root: algebra, name: refinement_widening_field_candidate) {
+        Accepted { value: bundled_candidate, diagnostics: None } =>
+          match find_named_child(root: algebra, name: refinement_widening_field_source_facts) {
+            Accepted { value: bundled_source_facts, diagnostics: None } =>
+              (bundled_source == source_facts)
+                && (bundled_candidate == candidate)
+                && (bundled_source_facts == source_facts)
+                && (source_facts != candidate)
+            Rejected { diagnostics: _ } => false
+          }
+        Rejected { diagnostics: _ } => false
+      }
+    Rejected { diagnostics: _ } => false
+  }
+}
+
+
+fn refinement_widening_preservation_holds(
+  source_facts: Node,
+  candidate: Node,
+  algebra: Node,
+) -> Bool {
+  well_formed(n: source_facts)
+    && well_formed(n: algebra)
+    && well_formed(n: candidate)
+    && refinement_widening_bundle_holds(
+      source_facts: source_facts,
+      candidate: candidate,
+      algebra: algebra
+    )
+}

src/v4/test/claim/manual/find_witness_distinct_node_zip_fold.dag

@@ -195,6 +195,7 @@ fn quality_is_exact(q: CoercionQuality) -> Bool {
   match q {
     Exact => true
     Identity => false
+    Widened => false
   }
 }
 data witness_find_witness_distinct_node_accepts: Bool = match find_witness(

src/v4/test/claim/manual/find_witness_identity_mvp.dag

@@ -153,6 +153,7 @@ fn quality_is_identity(q: CoercionQuality) -> Bool {
   match q {
     Identity => true
     Exact => false
+    Widened => false
   }
 }
 data witness_find_witness_identity_accepts: Bool = match find_witness(