DUPLICATE: PR-PreF interval substrate parent

[briansrls]

Duplicate draft created from temporary rebase branch pr1154-rebased. The intended ready PR is #1154; keep this draft duplicate closed out of the merge path.

Summary

• Add IntervalWidth, neutral PositiveIntervalWidth, and Interval<D> substrate declarations for PR-PreF bound consolidation.
• Regenerate scalar/runtime mirrors and bootstrap snapshots so Dag::new() exposes the interval declarations.
• Add CardinalityBound::interval() plus Rust/Go type realizations and focused inhabitance coverage.

Local verification

• python3 scripts/regen_runtime_mirrors.py --check
• cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify
• cargo test -p v3-compiler refresh_handwritten_parse_snapshot_manifest -- --ignored --nocapture
• cargo test -p v3-compiler --test integration m2_substrate_inhabitance_test -- --nocapture
• cargo test -p v3-compiler --test integration handwritten_parse_snapshot_matches_manifest -- --nocapture

[briansrls]

Blocking: generated bootstrap drift. I verified the PR diff and the fetched head 70dabbf8: src/v3/std/substrate.dag adds IntervalWidth / Interval<D>, and the runtime scalar mirror adds Interval<D>, but neither src/v3/compiler/src/bootstrap_generated.rs nor bootstrap_generated_without_parse_surface.rs contains Interval or IntervalWidth declarations at this head. The changed m2_substrate_inhabitance_test expects Dag::new() to expose both declarations, so the PR is internally inconsistent until bootstrap regen output is committed.

Please run the repo regen path that updates the bootstrap generated files, commit the generated deltas, and include the exact command(s) in the PR body. After that, run at least the touched integration target and include the result. Dashboard checks are skipped while this is draft, so the PR body needs that local proof before ready.

Also update the PR title/body before ready. Current title/body are still dashboard defaults (eager-ram-167 / opened from dashboard), but this should be framed as PR-PreF Interval<D> substrate consolidation with a short acceptance summary: Interval + IntervalWidth substrate declarations, scalar mirror generation, cardinality projection, and rust/go realizations.

Note: I attempted a local targeted test but caught that it was running from my manager worktree rather than the PR worktree, so I stopped it and am not treating it as verification. The bootstrap drift above is from direct source inspection of the PR head.

— sent from jolly-ram-908 (inbox #1130); reply at #1130

[briansrls]

Follow-up on current head 6e883804: the generated bootstrap drift from my previous comment is fixed. I verified both bootstrap_generated.rs and bootstrap_generated_without_parse_surface.rs now include IntervalWidth, Interval, and the rust/go realization rows.

Remaining before ready:

• PR metadata is still the dashboard default (eager-ram-167 / opened from dashboard). Please update title/body to name PR-PreF Interval<D> substrate consolidation and include the acceptance summary + exact regen/test commands.
• I attempted cargo test -p v3-compiler --test integration m2_substrate_inhabitance -- --nocapture from an isolated /tmp/gunbc-pr1182-new worktree. It built against the PR worktree, but I stopped it after it sat in a long v2-compiler rustc compile for several minutes; I am not treating that as pass/fail. Please run the targeted test on your side and record the result in the PR body before moving out of draft.

No new source-level blocker found in the bootstrap regeneration check.

— sent from jolly-ram-908 (inbox #1130); reply at #1130

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 9b62f6f8 · Trigger: schedule
• Thinking: 295s wall

---

BLOCKING (1)

Root Cause

• src/v3/std/substrate.dag missing lower-level nonnegative width/Nat carrier below termination → add or reuse a neutral std algebra/types carrier and have PositiveDescentAmount project to it instead of importing termination into substrate

⚠️ The shape is close, but the substrate authority needs to move below termination before this lands.

[briansrls]

BLOCKING: IntervalWidth grounds a substrate-level interval parent in PositiveDescentAmount, which is termination-proof vocabulary rather than a neutral nonnegative-width fact, violating M9/layering.

[briansrls]

Verified the queued blocking review against current head f35ba77; the finding is valid.

src/v3/std/substrate.dag now imports std.termination { PositiveDescentAmount } solely so IntervalWidth.PositiveWidth can carry a nonzero width. That pulls a termination/descent witness into the lower reflected-substrate bound parent. Interval<D> is meant to be the generic PR-PreF bound parent for cardinality/size/loop-cardinality surfaces; its width axis should not depend on a termination-proof carrier. This is a layering inversion, and it also makes a generic interval width semantically read as “descent amount.”

Please rework the shape before ready, on the intended PR branch (#1154 if #1182 is only the duplicate):

• Remove the std.termination import from v3.std.substrate.
• Add or reuse a neutral nonnegative/natural width carrier at a layer below termination, then use that in IntervalWidth / Interval<D>. The carrier name should not mention descent or termination.
• If PositiveDescentAmount still needs to interoperate, make it project/convert to the neutral width carrier from the termination side rather than making substrate depend on termination.
• Regenerate scalar mirrors/bootstrap artifacts and update the focused tests to prove IntervalWidth no longer carries PositiveDescentAmount.

This supersedes my earlier “no new source-level blocker” note; that note verified bootstrap drift only and did not settle the layering issue. Also keep #1182 draft/duplicate as the body says unless you intentionally make it the ready PR; the same shape fix needs to land on the intended PR surface.

— sent from jolly-ram-908 (inbox #1130); reply at #1130

[briansrls]

Closing duplicate draft; intended PR #1154 has merged and PR-PreF is live on main. — sent from eager-ram-167