fix(v3): cap subtractive descent prover at producer's materialization range

src/v3/compiler/src/lower.rs

@@ -30,7 +30,7 @@ use crate::dag::{
     Declaration, DeclarationId, Field, FieldMap, IntraClusterCall, LiteralBits, LoopBound,
     LoopNode, MemberDescent, NodeId, NominalOpacity, NonEmptyList, NonSingletonList, Path,
     PayloadBinding, PhantomParameter, PortId, TemplateArgument, TransformNode, TransformTarget,
-    TypeConnective, ValueNode,
+    TypeConnective, ValueNode, MAX_PEANO_MATERIALIZATION,
 };
 use crate::diagnostics::{
     declaration_display_name, witness_correction_for_decl, Diagnostic, SourceSpan,
@@ -8756,13 +8756,21 @@ fn is_strictly_smaller(
         &args[0],
         SurfaceExpr::Var { name, .. } if name == first_param
     );
-    let rhs_is_positive = matches!(
+    // RHS must be a positive integer literal AND within the descent-evidence
+    // carrier's `positive_amount_from_i64` materialization range
+    // (`dag.rs:1031-1032`, `1..=MAX_PEANO_MATERIALIZATION`). Without the
+    // upper cap, the termination prover would accept `f(n - 257)` while
+    // the per-call descent producer fails to materialize a
+    // `PositiveDescentAmount` and falls back to `SubValueUnknown` —
+    // parallel-authority split-brain (the same single-authority discipline
+    // Slice 3's ClusterDescentChecker fix established).
+    let rhs_in_descent_range = matches!(
         &args[1],
         SurfaceExpr::Literal {
             value: SurfaceLiteral::Int(v), ..
-        } if *v > 0
+        } if (1..=MAX_PEANO_MATERIALIZATION).contains(v)
     );
-    lhs_is_param && rhs_is_positive
+    lhs_is_param && rhs_in_descent_range
 }
 
 fn is_structurally_smaller(

src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs

@@ -1010,6 +1010,44 @@ fn invoke(w: Wrapper, x: Int) -> Int = w.f(x)
     );
 }
 
+#[test]
+fn e_p_per_call_descent_evidence_constant_descent_termination_matches_producer_acceptance_boundary()
+{
+    // Symmetric to the proportional-descent boundary test below but for
+    // the Sub arm: the termination prover and per-call descent producer
+    // MUST share the same acceptance boundary on `param - k`.
+    // `positive_amount_from_i64` (dag.rs:1031-1032) materializes
+    // `PositiveDescentAmount` for `1..=MAX_PEANO_MATERIALIZATION`;
+    // accepting any larger literal in `is_strictly_smaller` would let
+    // `f(n - 257)` pass termination while the producer fails to
+    // materialize and emits `SubValueUnknown` — parallel-authority
+    // split-brain (the discipline Slice 3 cemented for descent_provable
+    // / ClusterDescentChecker single-authority alignment).
+    //
+    // This test pins the boundary by rejecting `n - 257` at compile
+    // time. If either authority's range shifts, this test surfaces the
+    // divergence.
+    let err = compile_to_dag(
+        "\
+fn ep_oversize_subtractor(n: Int) -> Int =
+  if n == 0 then 0 else ep_oversize_subtractor(n - 257)
+",
+        "e_p_oversize_subtractor.v3",
+    )
+    .expect_err("subtractor beyond producer's materialization range must be rejected");
+    let CompileError::Semantic(dag) = err else {
+        panic!("expected semantic diagnostics, got {err:?}");
+    };
+    let saw_termination_diagnostic = dag.diagnostics().iter().any(|(_, d)| match d {
+        Diagnostic::ResolveError { name, .. } => name.contains("ep_oversize_subtractor"),
+        _ => false,
+    });
+    assert!(
+        saw_termination_diagnostic,
+        "expected a termination diagnostic naming `ep_oversize_subtractor`"
+    );
+}
+
 #[test]
 fn e_p_per_call_descent_evidence_fails_closed_for_non_self_call() {
     let dag = compile_to_dag(