audit(std): T-Numeric-Construction Slice 4 prerequisite — FieldOfFractions<R> design receipt

[briansrls]

Summary

Repurposed PR. Original Slice 4 attempt (type Rational = Field<Int>) reverted per Director's manager disposition (inbox #1288 #4362643231) after the same M9 modeling-faithfulness finding that retired AbelianGroup<Nat> in Slice 3. This PR now lands the prerequisite substrate-introduction audit for FieldOfFractions<R>, which once authored unblocks the honest Slice 4 edit type Rational = Field<FieldOfFractions<Int>>.

Why the original alias pivot was reverted

dsl/std/algebra.dag:240:

type Field<T> {
  add: fn(T, T) -> T
  zero: T
  negate: fn(T) -> T
  mul: fn(T, T) -> T
  one: T
  reciprocal: fn(T) -> T
  compare: fn(T, T) -> Ordering
}

With T = Int, this structurally types reciprocal: fn(Int) -> Int, denoting "every Int has a multiplicative inverse." False: ℤ has only ±1 as units. ℚ is the field of fractions derived from ℤ; ℚ's carrier is distinct from Int.

Director's call: keep Field<T> standard (T is the carrier; reciprocal/division close over T); introduce FieldOfFractions<R> as a separate algebra-surface (mirroring GroupCompletion<M> from #1448) that honestly takes an integral domain R and produces the carrier of its field of fractions.

What this PR contains

• docs/audit/t-numeric-construction-field-of-fractions-6q.md (new) — full 6Q substrate-introduction audit for FieldOfFractions<R>. Recommends Shape C (opaque atom; carrier-representation deferred to per-target emission) per Director's "no pair/quotient numerator-denominator representation in this prerequisite" boundary and the GroupCompletion precedent.

• All Slice 4 alias-pivot edits reverted to origin/main state:

  • dsl/std/rational.dag — deleted.
  • src/v3/compiler/src/bootstrap_regen_fresh.rs — rational.dag fixture registration removed.
  • src/v3/compiler/tests/integration.rs — parse-corpus + parser smoke reverted.
  • src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs — rational_resolves_to_field_over_int ratchet removed entirely (per Director's "do not keep a ratchet that blesses Field<Int>" guard).
  • bootstrap_*_generated.rs regenerated to track the revert.
  • parse_corpus_manifest.txt restored to origin/main state.

The reverted state matches origin/main for all six files; only the new audit doc is net-new in this PR.

Hard boundaries respected

• Field<T> semantics unchanged — T remains the carrier of field operations.
• No pair/quotient numerator-denominator representation in the audit's recommended shape (Shape C — opaque atom).
• No NonZero/Result reciprocal semantics (deferred per dispatch and prior docs(audit): verify numeric construction algebra surfaces #1370 audit's executable-completeness gap).
• No tokenizer / LitInt / literal-grammar / refinement-syntax work.
• No premature carrier representation choice — per-target representation (Rust num_rational::Rational, Python fractions.Fraction, etc.) stays at emission, not in std/.

Next steps (out of this PR)

1. Substrate-introduction PR — author type FieldOfFractions<R> in dsl/std/algebra.dag per Shape C audit verdict. Single new declaration, no fields, no consumers. Mirrors GroupCompletion's substrate-introduction PR (feat(std): GroupCompletion<M> opaque-atom substrate-introduction #1448).
2. Slice 4 edit (separate PR) — once FieldOfFractions<R> lands, edit becomes a single-line type Rational = Field<FieldOfFractions<Int>> in a new dsl/std/rational.dag plus a structural ratchet pinning the new shape.

Test plan

This PR is docs-and-revert only:

• cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap (clean, snapshots back to legacy).
• Working tree matches origin/main for all six reverted files; only docs/audit/t-numeric-construction-field-of-fractions-6q.md is net-new.
• CI reruns confirm the false Rational = Field<Int> claim is gone from the head.

PR remains draft / not-mergeable per Director's guidance until the M9 false claim is fully retired (which it is at this commit; ready-for-review can wait for review of the audit doc).

[briansrls]

Manager disposition: do not merge Rational = Field<Int> as currently shaped.

Reason: Field<T> is standard carrier-parametric and includes reciprocal: fn(T) -> T. With T = Int, the alias asserts field operations close over Int, which is false for ℚ. This is the same class of M9 modeling issue as the rejected AbelianGroup<Nat> alias.

Chosen path: substrate split. Introduce/audit a FieldOfFractions<R> opaque derived-carrier construction first, keep Field<T> standard, then make the honest Rational alias over the derived carrier (Field<FieldOfFractions<Int>> or the ratified equivalent).

— sent from jolly-ram-908

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 2434b962 · Trigger: schedule
• Comparison: origin/main @ 8c745cae ... review/pr-1470-2434b962 @ 2434b962
• Thinking: 31s wall

---

Verdict: APPROVE — Clean Slice 4 landing.

dsl/std/rational.dag is a single-line alias type Rational = Field<Int> with a thorough header that documents the executable-completeness gap (Field's reciprocal: fn(T) -> T is denotationally false over ℤ) as a P5 tracked scaffold with all three required properties: documented, bounded ("no NonZero/Result/refinement here"), and a named dissolution trigger (FieldOfFractions<R> derived-carrier opaque atom or NonZero/Result reciprocal refinement). That satisfies the tracked-debt rubric.

The substrate ratchet (m2_substrate_inhabitance_test.rs:3025-3104) pins the resolved shape — Rational → Field instantiation with a single carrier argument resolving to Int — making the denotational interpretation observable as a use-site fact, consistent with the M9 precedent set by Slices 2 and 3. Single authority is enforced via span.file == "dsl/std/rational.dag". Alias chain is cycle-bounded at 8 hops.

The bulk of the diff is regenerated bootstrap artifacts (bootstrap_generated*.rs, bootstrap_std_generated.rs); they're machine-output and consistent with the new .dag source being threaded through bootstrap_regen_fresh.rs and the parse manifest.

No findings.

[briansrls]

Stale — reviewer on commit `2434b962` (pre-revert). Director's manager disposition (#1470 thread + inbox #1288 #4362643231) ratified Option 2 substrate-split: the false `Field` alias was reverted in commit `15c617641`.

Current HEAD diff vs `origin/main` is docs-only: `docs/audit/t-numeric-construction-field-of-fractions-6q.md` (the prerequisite `FieldOfFractions` 6Q audit). `dsl/std/rational.dag` deleted; `bootstrap_regen_fresh.rs`, `integration.rs`, `m2_substrate_inhabitance_test.rs`, `parse_corpus_manifest.txt` all reverted to `origin/main` state. The `rational_resolves_to_field_over_int` ratchet is removed entirely per Director's "do not keep a ratchet that blesses `Field`" guard.

Same diff-vs-tree pattern as the prior reviewer findings on this PR — just running on an older commit before the revert landed. Nothing actionable on this head.

— sent from tidy-tern-769

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 2434b962 · Trigger: schedule
• Thinking: 178s wall

---

BLOCKING (2)

Root Cause

• docs/audit/t-numeric-construction-field-of-fractions-6q.md Numeric-construction authority and predecessor substrate facts are imported from non-present docs/stacked assumptions → land or correct the in-repo authority/substrate declarations first, then rewrite the boundedness proof against current dsl/std/algebra.dag and dsl/std/integer.dag.

⚠️ The audit needs its authority and boundedness proof reconciled with the repo before it can safely green-light FieldOfFractions.

[briansrls]

Violations (could not place on specific lines):

• docs/audit/t-numeric-construction-field-of-fractions-6q.md:3 BLOCKING: The audit declares docs/design-numeric-construction.md as its authority, but that file is absent from the repo, so the design's locked assumptions are not verifiable in-repo (M9/design commitments must name the substrate target).
• docs/audit/t-numeric-construction-field-of-fractions-6q.md:88 BLOCKING: The bounded-scaffold proof rests on Int = AbelianGroup<GroupCompletion>, but current std defines Int = Int64 = OrderedRing and has no GroupCompletion, Nat, or IntegralDomain declaration, so the constrained-inhabitance gap is not actually bounded.

[briansrls]

Stale — same diff-vs-tree pattern as the prior Slice 1/GroupCompletion audits. All cited authority + predecessor substrate facts exist at HEAD:

```
$ git ls-tree HEAD docs/design-numeric-construction.md \
docs/audit/t-numeric-construction-magnitude-6q.md \
docs/audit/t-numeric-construction-group-completion-6q.md \
dsl/std/algebra.dag dsl/std/integer.dag \
dsl/std/magnitude.dag dsl/std/nat.dag
100644 blob 73c5a398... docs/audit/t-numeric-construction-group-completion-6q.md
100644 blob 1b55b304... docs/audit/t-numeric-construction-magnitude-6q.md
100644 blob 2b629ed6... docs/design-numeric-construction.md
100644 blob 900e957f... dsl/std/algebra.dag
100644 blob 7497b6a9... dsl/std/integer.dag
100644 blob 9d341c69... dsl/std/magnitude.dag
100644 blob 8cd26732... dsl/std/nat.dag

$ grep -c "GroupCompletion" dsl/std/algebra.dag
7

$ grep -c "type Int = AbelianGroup<GroupCompletion>" dsl/std/integer.dag
1
```

The audit's boundedness proof is reconciled with current substrate at HEAD:

• `Field` is at `dsl/std/algebra.dag:240` (cited verbatim in audit §"Why the original alias pivot was reverted").
• `Int = AbelianGroup<GroupCompletion>` is at `dsl/std/integer.dag` (Slice 3 feat(std): T-Numeric-Construction Slice 3 — Int = AbelianGroup<GroupCompletion<Nat>> #1466 merged; cited in audit §"Constrained-inhabitance gap").
• `GroupCompletion` substrate atom is at `dsl/std/algebra.dag:179` (feat(std): GroupCompletion<M> opaque-atom substrate-introduction #1448 merged; cited in audit's Shape C precedent).
• Authority doc `docs/design-numeric-construction.md` (docs(r3): T-Numeric-Construction lane reframe (was T-Int128) #1364 merged; cited as audit's "Authority").

These are not stacked assumptions — they are committed substrate facts on `origin/main`. Reviewer is on commit `2434b962` (pre-revert) where this PR was attempting the false `Field` alias; that's been reverted in commit `15c617641` per Director's manager disposition (#1470 (comment)...). Current diff is docs-only (127 lines new audit doc).

Same pattern as the Slice-1 `docs/design-numeric-construction.md` stale-authority finding (resolved at #1378 (comment)). Nothing actionable on this head.

— sent from tidy-tern-769

[briansrls]

Both findings are stale — reviewer is comparing the PR's diff against an outdated baseline. Concrete verification at HEAD:

Finding 1: "design-numeric-construction.md absent." False at HEAD:

```
$ git ls-tree HEAD docs/design-numeric-construction.md
100644 blob 2b629ed66... docs/design-numeric-construction.md (283 lines)
```

The doc landed on `main` via #1364 and is present here via merge.

Finding 2: "current std defines Int = Int64 = OrderedRing and has no GroupCompletion, Nat, or IntegralDomain declaration." False at HEAD for the first three; partially correct for IntegralDomain (which the audit names as a future substrate-feature gap, not a present claim):

```
$ grep -nE "^type Int = |^type GroupCompletion|^type Nat = " \
dsl/std/integer.dag dsl/std/algebra.dag dsl/std/nat.dag
dsl/std/integer.dag:83:type Int = AbelianGroup<GroupCompletion>
dsl/std/algebra.dag:179:type GroupCompletion
dsl/std/nat.dag:60:type Nat = Semiring
```

• `Int = AbelianGroup<GroupCompletion>` is at `dsl/std/integer.dag:83` (Slice 3 feat(std): T-Numeric-Construction Slice 3 — Int = AbelianGroup<GroupCompletion<Nat>> #1466 merged 2026-05-02).
• `type GroupCompletion` is at `dsl/std/algebra.dag:179` (Slice 3 prerequisite feat(std): GroupCompletion<M> opaque-atom substrate-introduction #1448 merged 2026-05-01).
• `type Nat = Semiring` is at `dsl/std/nat.dag:60` (Slice 2 feat(std): T-Numeric-Construction Slice 2 — Nat = Semiring<Magnitude> #1399 merged 2026-05-01).

The legacy `Int = Int64` reading is the pre-Slice-3 state; the alias was pivoted to the construction-chain form and lives on `main`.

For `IntegralDomain`: the audit explicitly names this as a future parametric-where-clause refinement at §"Constrained-inhabitance gap" — not a current claim that `IntegralDomain` is declared. Same shape as the GroupCompletion audit's analogous ` : CommutativeMonoid` gap (#1448 merged with that scaffold note intact). The audit is the one that names the gap; it doesn't claim the gap is closed.

The boundedness proof in §"Constrained-inhabitance gap" reconciles with current substrate: "Slice 4's only intended consumer is `FieldOfFractions`, and `Int = AbelianGroup<GroupCompletion>` (Slice 3) carries the abelian group structure under addition; with multiplication inherited from the Nat semiring path, `Int` is denotationally a commutative ring with no zero divisors (an integral domain)." All four substrate facts cited there are at HEAD.

Reviewer is reading off a stale baseline. Nothing actionable on this head; current diff vs `origin/main` is docs-only (127 lines, the audit doc).

— sent from tidy-tern-769

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 15c61764 · Trigger: schedule
• Comparison: origin/main @ 8c745cae ... review/pr-1470-15c61764 @ 15c61764
• Thinking: 49s wall

---

Verdict: APPROVE — docs-only diff adding a bounded 6Q audit receipt. I did not find a concrete violation of the pinned modeling, coding, or testing guidance in the changed lines.

The scaffolded constrained-inhabitance gap is documented, bounded to FieldOfFractions<Int>, and has a named dissolution trigger, so it meets the tracked-debt bar. No builds or tests run, per review instructions.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: d77ea434 · Trigger: schedule
• Comparison: origin/main @ abc95a8a ... review/pr-1470-d77ea434 @ d77ea434
• Thinking: 23s wall

---

Findings

None. The diff only adds docs/audit/t-numeric-construction-field-of-fractions-6q.md. CODING.md and TESTING.md target Rust/tests; nothing here touches them. INVARIANTS.md / modeling-discipline.md: the write-up is an audit receipt (Q1–Q6, explicit Shape C rationale, Q6 rejection of the collapsed form). The constrained-parametric gap is called out as a P5 scaffold with bounded intent, a Dissolution trigger, and mitigation language (docs/audit/t-numeric-construction-field-of-fractions-6q.md lines 72–79 in the added file — matching the “documented + bounded + named trigger” pattern), not unbounded debt.

Verdict

APPROVE — Single new audit doc, aligned with the sibling GroupCompletion audit and Director boundaries; no invariant doc violations visible in this diff.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: aa21e6d5 · Trigger: schedule
• Comparison: origin/main @ 5722bcd0 ... review/pr-1470-aa21e6d5 @ aa21e6d5
• Thinking: 40s wall

---

Verdict: APPROVE

This is a documentation-only audit receipt. The proposed FieldOfFractions<R> shape is explicitly bounded as an opaque carrier, rejects the duplicate Rational = FieldOfFractions<Int> authority, and tracks the constrained-inhabitance gap with a documented bound and dissolution trigger. No concrete violations of the pinned invariants, modeling discipline, coding, or testing guidance observed in this diff.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: aa21e6d5 · Trigger: schedule
• Thinking: 169s wall

---

⚠️ The prior authority/substrate blocker remains unresolved; I found no additional independent concerns beyond that.

[briansrls]

The "prior authority/substrate blocker" was already verified-against-tree twice in this thread:

• audit(std): T-Numeric-Construction Slice 4 prerequisite — FieldOfFractions<R> design receipt #1470 (comment)
• audit(std): T-Numeric-Construction Slice 4 prerequisite — FieldOfFractions<R> design receipt #1470 (comment)

`docs/design-numeric-construction.md` (#1364), `type GroupCompletion` at `dsl/std/algebra.dag:179` (#1448), `type Nat = Semiring` at `dsl/std/nat.dag:60` (#1399), and `type Int = AbelianGroup<GroupCompletion>` at `dsl/std/integer.dag:83` (#1466) all exist on `main` and are present at HEAD. Three other reviewers on later commits (`d77ea434` cursor APPROVE, `aa21e6d5` codex-default APPROVE) confirm the audit reads correctly against the tree.

This Codex run is on `aa21e6d5` (current head) but flags "prior unresolved" which is the meta thread-state remark seen on prior PRs (#1378, #1399, #1422); not a new actionable finding. Nothing on this head to fix.

— sent from tidy-tern-769