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

[briansrls]

Summary

Pre-existing parallel-authority fix surfaced by codex BLOCKING inline finding on (closed) PR #2198 (gunbc#2198 #pullrequestreview at 2026-05-08T02:28:36Z). Symmetric to the Div-cap fix that PR attempted but for Sub:

• lower.rs::is_strictly_smaller's Sub arm accepts any positive integer literal (*v > 0)
• The per-call descent producer's dag.rs::positive_amount_from_i64 only materializes PositiveDescentAmount for 1..=MAX_PEANO_MATERIALIZATION (256)
• f(n - 257) therefore passes the termination prover but the producer falls back to SubValueUnknown — parallel-authority split-brain

Same single-authority discipline Slice 3 (#2182) established for descent_provable / ClusterDescentChecker. The discipline pattern Slices 1-5 have been holding the lane to.

Provenance

This issue predates Slices 1-5. Sub was the only ArithmeticOp the prover accepted before Slice 5 attempted Div, and its acceptance boundary was never tightened to match the producer's materialization range. Closed PR #2198 attempted the symmetric Div cap; codex caught the asymmetric Sub gap during that review. PR #2198 was closed independently because v3's / returns Result<T, DivError> (binary-halving recursion is unreachable at the v3 surface), so the Div cap was inert. The Sub cap is real and live.

Mechanism

let rhs_in_descent_range = matches!(
    &args[1],
    SurfaceExpr::Literal {
        value: SurfaceLiteral::Int(v), ..
    } if (1..=MAX_PEANO_MATERIALIZATION).contains(v)
);

Same MAX_PEANO_MATERIALIZATION import pattern (now used). Both authorities share the same acceptance boundary on param - k.

ClusterDescentChecker automatically inherits the change because its descent gate routes through the same is_strictly_smaller predicate (single-authority discipline preserved per Slice 3's BLOCKING-fix lesson).

Tests

New: e_p_per_call_descent_evidence_constant_descent_termination_matches_producer_acceptance_boundary — compiles f(n - 257) and asserts termination rejection. Symmetric tripwire to what closed PR #2198's boundary test established for Div.

If either authority shifts the range (prover widens, producer narrows), the divergence surfaces immediately at this test.

Cross-slice invariants

• ✓ No new CallPattern variant
• ✓ No new SubValueRelation kind
• ✓ No TransformNode widening
• ✓ Same fail-closed discipline (cap matches producer's materialization range)
• ✓ No INVARIANTS.md P1 substrate-fact-introduction trigger
• ✓ ClusterDescentChecker inherits via the shared predicate (P2 single-authority)

Authority

• Codex BLOCKING finding on closed Substrate T-E-P P1 follow-up: proportional arithmetic descent termination #2198 at 2026-05-08T02:28:36Z (lower.rs:8788)
• T-E-P P1 lane single-authority discipline established by Slice 3 (Substrate T-E-P P1 Slice 3: nested-match scrutinee + termination #2182)
• Continuation under standing-authority criteria (clean+green CI + 30min sit + no BLOCKING)

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 52e01e1f · Trigger: schedule
• Comparison: origin/main @ 027fa6bd ... review/pr-2201-52e01e1f @ 52e01e1f
• Thinking: 49s wall

---

Verdict: APPROVE

Diff is small and clean. The lower.rs change removes a real parallel-authority mismatch by making the termination gate use the same MAX_PEANO_MATERIALIZATION boundary as the descent-evidence producer, and the added regression test in src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs pins that fail-closed behavior at the compiler boundary. I did not find a concrete violation of INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md in the touched lines.

[briansrls]

Approved under standing-authority — narrow +50/-4 scope; same single-authority discipline (is_strictly_smaller ↔ producer's positive_amount_from_i64 materialization range) Slice 3 #2182 established for descent_provable / ClusterDescentChecker. Pattern: when termination prover and per-call descent producer disagree on a value range, the disagreement is a parallel-authority bug, not a feature. Capping the prover at producer's materialization range is the structurally honest fix.

The f(n - 257) test fixture pinning split-brain-rejection is exactly the right shape — same tripwire-discipline as Slices 4 + 6 cementing.

Standing CI + sit-window applies; no Mgr review needed before merge.

— sent from warm-wolf-698

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 52e01e1f · Trigger: schedule
• Thinking: 136s wall

---

✅ The change aligns the recursive termination prover with the producer’s bounded Peano materialization range and adds focused coverage for the former split-brain case.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 52e01e1f · Trigger: manual
• Comparison: main @ 027fa6bd ... fix-sub-descent-prover-cap @ 52e01e1f
• Conversation: View conversation

---

1. Story of the diff

This PR closes a mismatch between the subtractive termination prover and the descent-evidence producer. Previously, is_strictly_smaller treated any positive literal in param - k as proof of strict descent; this meant f(n - 257) could be accepted as terminating even though the producer’s PositiveDescentAmount materialization range only covers 1..=MAX_PEANO_MATERIALIZATION. The fix imports that same cap from dag at src/v3/compiler/src/lower.rs:33 and changes the predicate to require (1..=MAX_PEANO_MATERIALIZATION).contains(v) at src/v3/compiler/src/lower.rs:8771, so the proof path and evidence-production path now share the same boundary. The added integration regression constructs the oversize recursive subtractor and asserts it is rejected with semantic diagnostics, pinning the false-positive case this PR is meant to remove at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:963 through src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:981.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Compliant — this is implementation-side lowering/prover logic, not a new substrate type or Dag schema change; the implementation explicitly reads the existing materialization authority via MAX_PEANO_MATERIALIZATION at src/v3/compiler/src/lower.rs:33 and applies it at src/v3/compiler/src/lower.rs:8771.

1. INVARIANTS.md + modeling-discipline.md.

Compliant — single-authority / fail-closed are handled by replacing the independent “positive integer” rule with the producer’s exact materialization range: src/v3/compiler/src/lower.rs:8759 through src/v3/compiler/src/lower.rs:8766 document the split-brain failure mode, and src/v3/compiler/src/lower.rs:8771 enforces the shared cap rather than fabricating a termination proof the producer cannot materialize.

1. CODING.md.

Compliant — the change stays in a small pure predicate: the local name changes from “positive” to the more precise rhs_in_descent_range at src/v3/compiler/src/lower.rs:8767, and the function continues to return the boolean composition directly at src/v3/compiler/src/lower.rs:8773 without introducing hidden state, object-style API growth, or an extra helper with broader dependencies.

1. TESTING.md.

Compliant — the PR adds a focused regression test for the actual failure mode: the fixture uses n - 257 at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:965 through src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:968, expects compilation rejection at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:970, and checks for semantic diagnostics naming the rejected recursive function at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:974 through src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:981. Integration-level compile_to_dag is appropriate here because the contract under test is the compile-time termination/lowering boundary, not a narrow accessor.

1. LOCKED DESIGN DECISIONS.

N/A — the diff does not add, remove, or alter any marked locked design decision; it aligns an implementation predicate with an existing materialization cap.

1. TRACKED vs UNTRACKED DEBT.

N/A — no new TODO, scaffold, bridge, temporary representation, or debt marker is introduced. The new comments at src/v3/compiler/src/lower.rs:8759 through src/v3/compiler/src/lower.rs:8766 and src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:949 through src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:962 explain the invariant being protected rather than creating a deferred work item.

3. Verdict

APPROVE

The patch fixes the false-positive termination proof by making the subtractive prover consume the same bounded materialization authority as the descent producer, and it adds a targeted regression for the previously accepted oversize subtractor. I did not find a diff-line-backed invariant, coding-style, testing, locked-design, or debt issue.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: bcf11989 · Trigger: schedule
• Comparison: origin/main @ 23e8320b ... review/pr-2201-bcf11989 @ bcf11989
• Thinking: 28s wall

---

Findings: None. The change uses the same MAX_PEANO_MATERIALIZATION / 1..=… range as positive_amount_from_i64 in dag.rs (shared constant, not a second source of truth), which supports P2: Boundary Discipline and modeling discipline §5 (single-authority metadata) instead of violating them. The new test’s Diagnostic::ResolveError + name.contains(...) style matches the same file’s existing pattern (e.g. the X1.b test around m2_substrate_inhabitance_test.rs:985–989), so it does not newly introduce C-5-style “string as authority” in a way that departs from established integration tests there; it is a pipeline/contract test, which TESTING.md allows for compile_to_dag.

Verdict: APPROVE — Small, targeted fix: cap is_strictly_smaller’s subtractive literal check to the producer’s materialization range, with a regression that would catch prover/producer drift. No invariant or testing-discipline issues grounded in this diff.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: bcf11989 · Trigger: manual
• Comparison: main @ 23e8320b ... fix-sub-descent-prover-cap @ bcf11989
• Conversation: View conversation

---

1. Story of the diff

This PR fixes a split between two termination authorities for subtractive recursion. Before the change, is_strictly_smaller treated any positive literal in param - k as descent evidence, while the per-call descent producer can only materialize PositiveDescentAmount inside 1..=MAX_PEANO_MATERIALIZATION; the patch imports that shared bound at src/v3/compiler/src/lower.rs:33 and applies it directly at src/v3/compiler/src/lower.rs:8771. The practical effect is fail-closed: f(n - 257) is no longer accepted as a strict descent proof when the producer would later degrade the same edge to SubValueUnknown, and the new integration regression pins that rejection through compile_to_dag(...).expect_err(...) at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:1030-1037.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Compliant — the diff does not introduce or mutate Dag-resident substrate types, fields, or variants; it is an implementation-side lowering/prover change that reads the existing materialization authority via MAX_PEANO_MATERIALIZATION at src/v3/compiler/src/lower.rs:33 and uses it at src/v3/compiler/src/lower.rs:8771.

1. INVARIANTS.md + modeling-discipline.md.

Compliant — fail-closed and single-authority are handled correctly: is_strictly_smaller now accepts subtractive descent only when the literal is inside the same producer range, (1..=MAX_PEANO_MATERIALIZATION).contains(v), rather than fabricating a proof for all positive literals at src/v3/compiler/src/lower.rs:8771; the test explicitly targets the prior split-brain case at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:1021-1024.

1. CODING.md.

Compliant — the implementation stays as a small pure helper decision: the local boolean is renamed to the more precise rhs_in_descent_range at src/v3/compiler/src/lower.rs:8767, and the function remains an input-to-bool predicate with no hidden state, builder shape, object method expansion, or new error carrier.

1. TESTING.md.

Compliant — the PR adds a focused regression test for the behavioral bug: a minimal recursive fixture containing ep_oversize_subtractor(n - 257) is compiled at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:1030-1037, then the test asserts the compile fails semantically and surfaces a termination-related diagnostic at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:1038-1048. Integration level is appropriate here because the contract being pinned is compile-time termination rejection, not a narrow accessor.

1. LOCKED DESIGN DECISIONS.

N/A — the diff does not alter thesis/design documents or introduce a divergence from a locked design decision; it aligns an implementation helper to an existing materialization bound.

1. TRACKED vs UNTRACKED DEBT.

N/A — no new TODOs, temporary scaffolds, compatibility bridges, or staged alternate representations are introduced in the diff.

3. Verdict

APPROVE

The patch is small and directly addresses the bug at the authority boundary: the prover now uses the producer’s existing materialization cap instead of independently accepting all positive subtractive literals. The regression test pins the oversize case that would previously have produced a false termination proof.