audit(std): T-Numeric-Construction Slice 3 prerequisite — GroupCompletion<M> design receipt by briansrls · Pull Request #1422 · gunb-ai/gunbc

briansrls · 2026-05-01T15:11:05Z

Summary

Repurposed PR. Original Slice 3 attempt (type Int = AbelianGroup<Nat>) reverted per Director's manager disposition (inbox #1288 #4360232423) after two reviewers flagged a sharp M9 modeling-faithfulness finding. This PR now lands the prerequisite substrate-introduction audit for GroupCompletion<M>, which once authored unblocks the honest Slice 3 edit type Int = GroupCompletion<Nat>.

Why the original alias pivot was reverted

dsl/std/algebra.dag:132:

type AbelianGroup<T> {
  op: fn(T, T) -> T
  identity: T
  inverse: fn(T) -> T
  // commutativity is a law
}

With T = Nat, this structurally types inverse: fn(Nat) -> Nat, denoting "every Nat has an additive inverse." That is false: ℕ is a commutative monoid, not a group. The Grothendieck construction creates ℤ from ℕ, but ℤ's carrier is derived (a quotient or sign-magnitude representation), not ℕ itself.

Director's call: keep AbelianGroup<T> standard (T is the carrier; do not retroactively reinterpret as "derived from T"); introduce GroupCompletion<M> as a separate algebra-surface that honestly takes a commutative monoid M and produces the derived abelian group.

What this PR contains

docs/audit/t-numeric-construction-group-completion-6q.md (new) — full 6Q substrate-introduction audit for GroupCompletion<M>. Recommends Shape C (opaque atom; carrier-representation deferred to per-target emission) per design doc's "no quotient/sign-magnitude representation facts" boundary and Slice 1's Magnitude precedent.
All Slice 3 alias-pivot edits reverted to origin/main state:
- dsl/std/integer.dag — type Int = Int64 restored; AbelianGroup/Nat imports removed; pre-Slice-3 MODELING NOTE restored.
- src/v3/compiler/tests/integration/common/substrate_receipts.rs — receipt walks Int (= Int64) again; legacy comment restored.
- src/v3/compiler/tests/integration/m1_substrate_test.rs — test renamed back to bootstrap_int_add_walk_reaches_ordered_ring_add_nobody_arrow.
- src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs — the AbelianGroup<Nat>-blessing ratchet (int_default_alias_resolves_to_abelian_group_over_nat) removed entirely per Director's "do not keep a ratchet that blesses AbelianGroup<Nat>" guard.
- bootstrap_*_generated.rs regenerated to track reverted integer.dag.

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

Hard boundaries respected

AbelianGroup<T> semantics unchanged — group carrier remains T. No retroactive global reinterpretation.
No quotient-of-pairs or sign-magnitude representation in the audit's recommended shape (Shape C — opaque atom).
No tokenizer / LitInt / literal-grammar / refinement-syntax work.
No premature carrier representation choice — per-target representation (Rust i128 sign-magnitude, Python bignum, etc.) stays at emission, not in std/.

Next steps (out of this PR)

Substrate-introduction PR — author type GroupCompletion<M> in dsl/std/algebra.dag per Shape C audit verdict. Single new declaration, no fields, no consumers.
Slice 3 edit (separate PR) — once GroupCompletion<M> lands, edit becomes a single-line type Int = GroupCompletion<Nat> plus a structural ratchet pinning the new shape. The Slice 3 dispatch's "narrow alias pivot" guardrail then holds honestly.

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 the four reverted files (git diff origin/main --stat shows only the new audit doc + bootstrap deltas to track main's intermediate moves).
CI reruns confirm the false Int = AbelianGroup<Nat> 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).

# Conflicts: # src/v3/compiler/src/bootstrap_generated.rs # src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs

briansrls · 2026-05-01T18:07:34Z

Review metadata

Provider / model: claude / claude-opus-4-7
Commit: dc52252f · Trigger: schedule
Comparison: origin/main @ 7374b184 ... review/pr-1422-dc52252f @ dc52252f
Thinking: 11s wall

Docs-only PR. No code changes.

Verdict: APPROVE — pure documentation receipt for the GroupCompletion<M> 6Q audit. No substrate, code, or test changes; nothing in the diff to violate INVARIANTS / modeling-discipline / CODING / TESTING. The recommendation (Shape C opaque atom) is internally consistent with the cited Magnitude precedent and explicitly defers carrier representation per the stated Director boundary, with a named dissolution trigger (constrained-inhabitance syntax) for the unconstrained <M> gap — i.e., a tracked bridge, not unbounded debt.

briansrls · 2026-05-01T18:23:40Z

Review metadata

Provider / model: cursor / composer-2
Commit: 4ba03419 · Trigger: schedule
Comparison: origin/main @ ea854f32 ... review/pr-1422-4ba03419 @ 4ba03419
Thinking: 47s wall

Findings: None. The only net change vs origin/main is the new audit note docs/audit/t-numeric-construction-group-completion-6q.md (~119 lines). It records the GroupCompletion<M> direction, 6Q answers, placement options, and an explicit tracked gap for “M must be a commutative monoid” without where-clauses, with bounded use (GroupCompletion<Nat> only) and a named dissolution trigger (constrained-inhabitance / parametric where-clause in the substrate) — consistent with INVARIANTS.md P5 / scaffold boundaries and modeling-discipline Practice 6 as documented limitation, not a hidden convention. Nothing here touches compiler Rust (CODING.md) or tests (TESTING.md).

Verdict: APPROVE — Narrow, receipt-style doc addition; no rubric violations visible in the diff.

Exploratory (optional): If the GitHub PR title still promises revert(std): … or manifest fixes, the merge-base diff in this workspace is doc-only; worth aligning PR description with what actually lands relative to main in your target branch, but that is release hygiene, not a doc-line defect.

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 4ba03419 · Trigger: schedule
Thinking: 184s wall

BLOCKING (1)

Root Cause

docs/audit/t-numeric-construction-group-completion-6q.md Shape C has not pinned the substrate role of GroupCompletion<M> → choose one structural authority for Slice 3 and delete the alternate spelling.

Non-blocking — Strengths

docs/audit/t-numeric-construction-group-completion-6q.md The audit correctly rejects AbelianGroup<Nat> under the standard parametric reading and keeps AbelianGroup<T> as operations over carrier T.

⚠️ One new blocking ambiguity remains, and prior unresolved blocking comments still need attention.

Sign in to view

+
+### Q1 — Cardinality invariants
+Does the type admit `[]` when invariant says ≥1, or singletons when ≥2?
+


briansrls · 2026-05-01T19:00:56Z

Valid Q6 finding — the audit was admitting two structurally distinct forms for the same Slice 3 fact. Picked canonical form per Shape C's carrier-construction intent + Director's standard parametric reading boundary:

Canonical: `type Int = AbelianGroup<GroupCompletion>` — explicit two-step.

`GroupCompletion` is only the derived carrier (opaque atom).
`AbelianGroup` is only the algebra witness (standard parametric reading; `T` is the carrier).
Single authority for both surfaces; no drift between "GroupCompletion as carrier" vs "GroupCompletion as algebra-witness" readings.

Rejected: `type Int = GroupCompletion` (the prior compact alternative that collapsed carrier + algebra into a single named type).

Updated in this push:

Section heading "Recommendation" rewritten to make `GroupCompletion` strictly a carrier construction (not algebra-with-derived-carrier).
New "Q6 single-authority resolution" paragraph names the rejected form explicitly and pins canonical form.
All forward-references in the audit updated to canonical form (`type Int = AbelianGroup<GroupCompletion>`): subject line, Director-decision recap, Q3 / Q5 / constrained-inhabitance / out-of-scope / verdict sections.

This matches:

Director's "keep `AbelianGroup` standard: group carrier is `T`" guard (inbox session/tidy-tern-769 · tidy-tern-769 #1288 #4360232423).
Slice 1 `Magnitude` precedent (carrier-only opaque atom; algebra inhabitance attached at use sites via `Semiring` rather than baked into the carrier name).

— sent from tidy-tern-769

briansrls · 2026-05-01T19:01:14Z

Same Q6 ambiguity finding addressed in the previous push (#1422 (comment)). Canonical form pinned at HEAD:

`type Int = AbelianGroup<GroupCompletion>`

— with `GroupCompletion` strictly the derived carrier and `AbelianGroup` the standard algebra witness over that carrier. The compact alternative `type Int = GroupCompletion` is now explicitly rejected in the audit (see "Q6 single-authority resolution" paragraph at `docs/audit/t-numeric-construction-group-completion-6q.md:36`). All forward references updated to the canonical form.

The reviewer's note that "prior unresolved blocking comments still need attention" — every prior BLOCKING on this PR has been individually replied with verification:

Stale `Int = AbelianGroup` (already reverted; HEAD has `type Int = Int64`).
Missing authority doc / prerequisite-files (all present in tree at HEAD; reviewer was reading PR diff).
Constrained-inhabitance ` : CommutativeMonoid` precondition (tracked-scaffold note added with named dissolution trigger).
Q6 ambiguity (just fixed in this push).

— sent from tidy-tern-769

briansrls · 2026-05-01T19:02:39Z

Review metadata

Provider / model: codex / codex-default
Commit: 8bbdc3b0 · Trigger: schedule
Comparison: origin/main @ ea854f32 ... review/pr-1422-8bbdc3b0 @ 8bbdc3b0
Thinking: 66s wall

Findings:

BLOCKING: docs/audit/t-numeric-construction-group-completion-6q.md:59, line 71, line 104, and line 114 still define the future Slice 3 edit as type Int = GroupCompletion<Nat>, but the same new audit explicitly rejects that compact form at line 36 as a Q6 representation-duality violation and names type Int = AbelianGroup<GroupCompletion<Nat>> as canonical at line 29. This violates INVARIANTS P2 single-authority/boundary discipline: the design receipt leaves two authoritative shapes for the same Slice 3 fact.

Verdict: REQUEST_CHANGES. The fix looks narrow: make every Slice 3 reference in this new receipt use the same canonical two-step form, or explicitly revise the Q6 decision if the compact form is actually intended.

briansrls · 2026-05-01T19:04:44Z

Already fixed at HEAD (`041a00638`). Reviewer was on the intermediate commit `8bbdc3b0c` where I'd just landed the Q6 single-authority resolution paragraph (line 36) but hadn't yet propagated the canonical form to all the forward-references. The follow-up commit (`041a00638`, ~3 minutes later) ran a global rewrite to align lines 59 / 71 / 94 / 104 / 114 to `type Int = AbelianGroup<GroupCompletion>`. Verified at HEAD:

```
$ grep -nE "type Int = " docs/audit/t-numeric-construction-group-completion-6q.md
3: ... `type Int = AbelianGroup<GroupCompletion>`.
5: ... first attempt at `type Int = AbelianGroup` (historical-rejection ref)
7: ... Slice 3 honestly becomes `type Int = AbelianGroup<GroupCompletion>`.
29: Canonical Slice 3 form: `type Int = AbelianGroup<GroupCompletion>`.
36: ... rejected compact form `type Int = GroupCompletion` (Q6 explanation, intentionally names the rejected form)
59: ... future Slice 3 (`type Int = AbelianGroup<GroupCompletion>`)
71: ... `type Int = AbelianGroup<GroupCompletion>`
94: ... call sites (`type Int = AbelianGroup<GroupCompletion>`)
104: ... `type Int = AbelianGroup<GroupCompletion>`
114: ... `type Int = AbelianGroup<GroupCompletion>`
```

Every `type Int = ...` reference at HEAD uses the canonical two-step form, except line 36 (the Q6 paragraph) which intentionally names the rejected compact form to identify what was rejected. P2 single-authority is preserved.

— sent from tidy-tern-769

briansrls · 2026-05-01T19:17:56Z

Review metadata

Provider / model: cursor / composer-2
Commit: 041a0063 · Trigger: schedule
Comparison: origin/main @ ea854f32 ... review/pr-1422-041a0063 @ 041a0063
Thinking: 25s wall

The net change versus origin/main is a single new file: docs/audit/t-numeric-construction-group-completion-6q.md (127 lines). HEAD is ahead of origin/main; the merge-base equals origin/main, so the PR adds only that audit document.

Findings: None. The doc explicitly records Shape C (opaque GroupCompletion<M> as carrier + standard AbelianGroup<T>), resolves Q6 against duplicate compact forms at docs/audit/t-numeric-construction-group-completion-6q.md:31–33, and treats the missing parametric constraint as tracked debt with a named dissolution trigger and bounded mitigation at docs/audit/t-numeric-construction-group-completion-6q.md:72–81, consistent with INVARIANTS P5 (scaffold boundaries) and modeling-discipline practice 6 (API gap acknowledged, not papered over). Nothing in the diff touches compiler Rust (CODING.md) or tests (TESTING.md).

Verdict: APPROVE — Narrow documentation-only PR: a single 6Q design receipt for GroupCompletion<M> with explicit authority, boundaries, and dissolution language; no rubric violations observed in the diff.

Exploratory (optional): At docs/audit/t-numeric-construction-group-completion-6q.md:4, the text links PR #1422 as the reverted Slice 3 attempt; if this file ships in that same PR, readers may need a beat to parse “this PR once contained the reverted change.” Worth a clarity pass only if someone finds it confusing in review—not a principle violation.

briansrls · 2026-05-01T19:34:03Z

Review metadata

Provider / model: cursor / composer-2
Commit: f65b4de2 · Trigger: schedule
Comparison: origin/main @ 7ed21553 ... review/pr-1422-f65b4de2 @ f65b4de2
Thinking: 21s wall

The PR diff against origin/main is a single addition: docs/audit/t-numeric-construction-group-completion-6q.md (127 lines). No Rust or DAG substrate changes appear in this diff.

Findings: None. Nothing in the diff violates the cited rubric in a concrete way:

INVARIANTS / modeling-discipline: The audit is a design receipt (6Q), explicitly resolves Q6 single-authority by rejecting a collapsed GroupCompletion<Nat> form (see the paragraph starting around the added “Q6 single-authority resolution.” block), and treats the missing parametric where-clause as tracked work with a named dissolution trigger (“Dissolution trigger: when constrained-inhabitance / parametric where-clause syntax lands…”) plus bounded mitigation (“Slice 3’s only consumer is GroupCompletion<Nat>”). That matches the documented scaffold pattern rather than silent debt.
CODING.md / TESTING.md: Nothing in this diff touches Rust or tests; nothing to enforce there.

Verdict: APPROVE — Narrow documentation-only change: a coherent GroupCompletion<M> 6Q audit aligned with prior M9 direction, explicit boundaries on what is out of scope, and clear single-authority framing for Slice 3. No rubric-grounded issues in the diff.

briansrls · 2026-05-01T19:51:33Z

Review metadata

Provider / model: codex / codex-default
Commit: ded39912 · Trigger: schedule
Comparison: origin/main @ 7ed21553 ... review/pr-1422-ded39912 @ ded39912
Thinking: 29s wall

Verdict: APPROVE — this is a documentation-only audit receipt. The GroupCompletion<M> scaffold is documented, bounded to the GroupCompletion<Nat> consumer, and includes a named dissolution trigger for constrained inhabitance / where-clause support. No concrete invariant, coding, or testing violations observed in the diff.

briansrls

Review metadata

Provider / model: codex / unknown
Commit: ded39912 · Trigger: schedule
Thinking: 152s wall

Non-blocking — Strengths

docs/audit/t-numeric-construction-group-completion-6q.md The receipt cleanly applies the standard AbelianGroup carrier reading and fixes the prior carrier/witness ambiguity.

⚠️ No new blocking findings, but prior unresolved blocking comments remain outside the resolved items above.

briansrls · 2026-05-01T19:59:34Z

Already addressed at HEAD — this is the same constrained-inhabitance finding raised in the previous batch and resolved in commit `dc52252f` (the "Constrained-inhabitance gap (tracked-scaffold note)" section, currently around line 84 of the audit doc).

Prior reply detailing the resolution: #1422 (comment).

Summary of what's at HEAD:

The unenforced ` : CommutativeMonoid` precondition is named explicitly as a substrate-feature gap (no parametric where-clause syntax exists yet — separate substrate-feature lane).
Bounded denotationally: Slice 3's only consumer is `AbelianGroup<GroupCompletion>`, and `Nat = Semiring` carries commutative-monoid laws via Semiring's add+zero+commutativity-on-add.
Named dissolution trigger: when constrained-inhabitance lands, sharpen `GroupCompletion` to require `M : CommutativeMonoid`.
Mitigation: substrate-introduction PR will land alongside a structural ratchet pinning `GroupCompletion` (the only consumer) at bootstrap.

Same tracked-scaffold pattern as Slice 2's `Semiring → CommutativeSemiring` note. Reviewer on a stale or re-running batch; nothing actionable on this head.

— sent from tidy-tern-769

briansrls · 2026-05-01T19:59:51Z

Stale — this Q6 finding was already addressed twice on this PR:

audit(std): T-Numeric-Construction Slice 3 prerequisite — GroupCompletion<M> design receipt #1422 (comment) (initial fix: rewrote Recommendation section as carrier-construction; added "Q6 single-authority resolution" paragraph rejecting compact form).
audit(std): T-Numeric-Construction Slice 3 prerequisite — GroupCompletion<M> design receipt #1422 (comment) (propagated canonical form to all forward-references).

Verified at HEAD:

Line 29: `Canonical Slice 3 form: type Int = AbelianGroup<GroupCompletion>.`
Line 36: "Q6 single-authority resolution. The earlier draft of this audit floated an alternative compact form `type Int = GroupCompletion` ... Rejected. Canonical form is the explicit two-step `AbelianGroup<GroupCompletion>`."
Lines 59 / 71 / 94 / 104 / 114: all use `type Int = AbelianGroup<GroupCompletion>`.

The compact `type Int = GroupCompletion` form appears at HEAD only in line 36 where it is explicitly named as the rejected alternative. Single authority is preserved.

— sent from tidy-tern-769

Ships the prerequisite carrier construction from the audit at docs/audit/t-numeric-construction-group-completion-6q.md (#1422 audit receipt). Strictly Shape C — bare opaque atom in dsl/std/algebra.dag, parameterized by <M>, no fields, no algebra inhabitance. - dsl/std/algebra.dag: type GroupCompletion<M> declared after AbelianGroup<T>, with full header documenting hard boundaries (no quotient-of-pairs, no sign-magnitude, no mechanical AbelianGroup-witness derivation) + the constrained-inhabitance tracked-scaffold note (M : CommutativeMonoid is denotational; future parametric where-clause syntax dissolves the gap). - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet group_completion_is_bare_opaque_atom_with_one_type_parameter pinning span (algebra.dag), connective shape (Conj { children: [] }), type_params count (1), and absent value_body. - bootstrap_*_generated.rs regenerated; parse-corpus manifest refreshed for the new algebra.dag bytes. Per dispatch on inbox #1288 #4361921687: did NOT pivot Int (Slice 3 stays deferred), did NOT introduce quotient/sign-magnitude carrier facts, did NOT claim mechanical AbelianGroup witness derivation. The future Slice 3 edit becomes type Int = AbelianGroup<GroupCompletion<Nat>> per the audit's Q6 single-authority resolution.

* WIP: tidy-tern-769 * chore: apply cargo fmt * WIP: tidy-tern-769 * WIP: tidy-tern-769 * chore: apply cargo fmt * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): add Magnitude opaque carrier (T-Numeric-Construction Slice 1) * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): T-Numeric-Construction Slice 2 — Nat = Semiring<Magnitude> * fix(std/nat): document tracked-scaffold dissolution trigger to CommutativeSemiring<T> Reviewer flagged: Nat denotationally inhabits CommutativeSemiring (commutative mul) but algebra.dag declares only Semiring<T>. Per modeling-philosophy (layer concept introductions; sharpen via stronger algebras as separate slices), this is the closest honest algebra surface today. Adding a P5 tracked-scaffold note pinning the dissolution trigger so the future algebra-strength sharpening slice is visible at the use site. * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * chore: apply cargo fmt * revert(std): drop Int = AbelianGroup<Nat> alias pivot; add GroupCompletion<M> 6Q audit Director ratified Option 2 substrate-split (inbox #1288 #4360232423) after two reviewers flagged a sharp M9 modeling-faithfulness finding: with the standard parametric reading of `AbelianGroup<T>`, T is the carrier of group operations including `inverse: fn(T) -> T`. With T = Nat, that denotes 'every Nat has an additive inverse' — false for ℕ. ℤ is derived from ℕ via Grothendieck construction; ℤ's carrier is not ℕ itself. Reverted in this commit: - dsl/std/integer.dag: type Int = Int64 restored; AbelianGroup/Nat imports removed. - src/v3/compiler/tests/integration/common/substrate_receipts.rs: receipt walks Int (= Int64) again; legacy comment restored. - src/v3/compiler/tests/integration/m1_substrate_test.rs: test renamed back to bootstrap_int_add_walk_reaches_ordered_ring_add_nobody_arrow. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: the AbelianGroup<Nat>-blessing ratchet (int_default_alias_resolves_to_abelian_group_over_nat) removed entirely per Director's 'do not keep a ratchet that blesses AbelianGroup<Nat>' guard. - bootstrap_*_generated.rs regenerated to track reverted integer.dag. Added in this commit: - docs/audit/t-numeric-construction-group-completion-6q.md: 6Q substrate- introduction audit for the prerequisite GroupCompletion<M> algebra surface. Recommends Shape C (opaque atom; carrier-representation deferred to per-target emission) per design doc 'no quotient/sign- magnitude representation' boundary. Once GroupCompletion<M> lands, Slice 3 becomes a single-line edit: type Int = GroupCompletion<Nat>. * fix(test): revert stale parse_corpus_manifest row for integer.dag Director caught: the PR's manifest still carried the alias-pivot bytes (16/12179/9c6a1d94...) for dsl/std/integer.dag, but integer.dag itself is reverted to origin/main state (15/11459/a2942a07...). Restore the manifest row so the PR diff is docs-only (the GroupCompletion<M> audit). * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): GroupCompletion<M> opaque-atom substrate-introduction Ships the prerequisite carrier construction from the audit at docs/audit/t-numeric-construction-group-completion-6q.md (#1422 audit receipt). Strictly Shape C — bare opaque atom in dsl/std/algebra.dag, parameterized by <M>, no fields, no algebra inhabitance. - dsl/std/algebra.dag: type GroupCompletion<M> declared after AbelianGroup<T>, with full header documenting hard boundaries (no quotient-of-pairs, no sign-magnitude, no mechanical AbelianGroup-witness derivation) + the constrained-inhabitance tracked-scaffold note (M : CommutativeMonoid is denotational; future parametric where-clause syntax dissolves the gap). - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet group_completion_is_bare_opaque_atom_with_one_type_parameter pinning span (algebra.dag), connective shape (Conj { children: [] }), type_params count (1), and absent value_body. - bootstrap_*_generated.rs regenerated; parse-corpus manifest refreshed for the new algebra.dag bytes. Per dispatch on inbox #1288 #4361921687: did NOT pivot Int (Slice 3 stays deferred), did NOT introduce quotient/sign-magnitude carrier facts, did NOT claim mechanical AbelianGroup witness derivation. The future Slice 3 edit becomes type Int = AbelianGroup<GroupCompletion<Nat>> per the audit's Q6 single-authority resolution.

…ompletion<Nat>> (#1466) * WIP: tidy-tern-769 * chore: apply cargo fmt * WIP: tidy-tern-769 * WIP: tidy-tern-769 * chore: apply cargo fmt * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): add Magnitude opaque carrier (T-Numeric-Construction Slice 1) * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): T-Numeric-Construction Slice 2 — Nat = Semiring<Magnitude> * fix(std/nat): document tracked-scaffold dissolution trigger to CommutativeSemiring<T> Reviewer flagged: Nat denotationally inhabits CommutativeSemiring (commutative mul) but algebra.dag declares only Semiring<T>. Per modeling-philosophy (layer concept introductions; sharpen via stronger algebras as separate slices), this is the closest honest algebra surface today. Adding a P5 tracked-scaffold note pinning the dissolution trigger so the future algebra-strength sharpening slice is visible at the use site. * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * chore: apply cargo fmt * revert(std): drop Int = AbelianGroup<Nat> alias pivot; add GroupCompletion<M> 6Q audit Director ratified Option 2 substrate-split (inbox #1288 #4360232423) after two reviewers flagged a sharp M9 modeling-faithfulness finding: with the standard parametric reading of `AbelianGroup<T>`, T is the carrier of group operations including `inverse: fn(T) -> T`. With T = Nat, that denotes 'every Nat has an additive inverse' — false for ℕ. ℤ is derived from ℕ via Grothendieck construction; ℤ's carrier is not ℕ itself. Reverted in this commit: - dsl/std/integer.dag: type Int = Int64 restored; AbelianGroup/Nat imports removed. - src/v3/compiler/tests/integration/common/substrate_receipts.rs: receipt walks Int (= Int64) again; legacy comment restored. - src/v3/compiler/tests/integration/m1_substrate_test.rs: test renamed back to bootstrap_int_add_walk_reaches_ordered_ring_add_nobody_arrow. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: the AbelianGroup<Nat>-blessing ratchet (int_default_alias_resolves_to_abelian_group_over_nat) removed entirely per Director's 'do not keep a ratchet that blesses AbelianGroup<Nat>' guard. - bootstrap_*_generated.rs regenerated to track reverted integer.dag. Added in this commit: - docs/audit/t-numeric-construction-group-completion-6q.md: 6Q substrate- introduction audit for the prerequisite GroupCompletion<M> algebra surface. Recommends Shape C (opaque atom; carrier-representation deferred to per-target emission) per design doc 'no quotient/sign- magnitude representation' boundary. Once GroupCompletion<M> lands, Slice 3 becomes a single-line edit: type Int = GroupCompletion<Nat>. * fix(test): revert stale parse_corpus_manifest row for integer.dag Director caught: the PR's manifest still carried the alias-pivot bytes (16/12179/9c6a1d94...) for dsl/std/integer.dag, but integer.dag itself is reverted to origin/main state (15/11459/a2942a07...). Restore the manifest row so the PR diff is docs-only (the GroupCompletion<M> audit). * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): GroupCompletion<M> opaque-atom substrate-introduction Ships the prerequisite carrier construction from the audit at docs/audit/t-numeric-construction-group-completion-6q.md (#1422 audit receipt). Strictly Shape C — bare opaque atom in dsl/std/algebra.dag, parameterized by <M>, no fields, no algebra inhabitance. - dsl/std/algebra.dag: type GroupCompletion<M> declared after AbelianGroup<T>, with full header documenting hard boundaries (no quotient-of-pairs, no sign-magnitude, no mechanical AbelianGroup-witness derivation) + the constrained-inhabitance tracked-scaffold note (M : CommutativeMonoid is denotational; future parametric where-clause syntax dissolves the gap). - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet group_completion_is_bare_opaque_atom_with_one_type_parameter pinning span (algebra.dag), connective shape (Conj { children: [] }), type_params count (1), and absent value_body. - bootstrap_*_generated.rs regenerated; parse-corpus manifest refreshed for the new algebra.dag bytes. Per dispatch on inbox #1288 #4361921687: did NOT pivot Int (Slice 3 stays deferred), did NOT introduce quotient/sign-magnitude carrier facts, did NOT claim mechanical AbelianGroup witness derivation. The future Slice 3 edit becomes type Int = AbelianGroup<GroupCompletion<Nat>> per the audit's Q6 single-authority resolution. * feat(std): T-Numeric-Construction Slice 3 — Int = AbelianGroup<GroupCompletion<Nat>> Pivot the default Int alias to the canonical Q6 single-authority form per docs/audit/t-numeric-construction-group-completion-6q.md. Now that GroupCompletion<M> is a substrate carrier (#1448), the construction-chain layer-3 algebra is honest under standard parametric reading: T = GroupCompletion<Nat> (derived carrier; opaque atom) AbelianGroup<T> (algebra witness; inverse: T -> T well-defined) Fixed-width rows (Int8..Int128, UInt8..UInt128) stay on OrderedRing<Word*>/Semiring<Word*>. Word* storage carriers remain storage refinements, not alternate Int/Nat/Magnitude/GroupCompletion authorities. - dsl/std/integer.dag: type Int = AbelianGroup<GroupCompletion<Nat>>; imports Nat, AbelianGroup, GroupCompletion. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet int_default_alias_resolves_to_abelian_group_over_group_completion_of_nat pinning the two-step Instantiation chain (AbelianGroup template, carrier = GroupCompletion<Nat>, GroupCompletion's input = Nat). - src/v3/compiler/tests/integration/common/substrate_receipts.rs + m1_substrate_test.rs: legacy Int → OrderedRing receipt repointed to walk Int64 directly (the OrderedRing<Word64> chain it pinned now lives at the fixed-width row, not the default alias). - bootstrap_*_generated.rs regenerated; parse_corpus_manifest.txt refreshed. Per Director's guardrail (dispatch on inbox #1288 #4362239705): no consumer migration of legacy Int64/OrderedRing<Word*> chain in this PR; no quotient/sign-magnitude representation; no tokenizer/literal/refinement syntax work. Total downstream impact: one ratchet rename + manifest refresh — within the 'ratchets/generated outputs' scope explicitly authorized by the dispatch. * chore: apply cargo fmt * fix(test): pin transform_callable_unsupported_in_e3_slice to Bool not Int CI caught: Slice 3's pivot of `Int` from alias to direct Instantiation made `callable_runtime_arity(Int) = Some(3)` (AbelianGroup's Conj children), which fires the push_transform arity assertion when the test feeds 0 inputs. The test's subject is eval_node's rejection of Callable transforms — the declaration is incidental. Switch to `Bool` (Disj), whose `callable_runtime_arity` resolves to None and is stable across future numeric-substrate edits. * chore: apply cargo fmt

…tions<R> design receipt (#1470) * WIP: tidy-tern-769 * chore: apply cargo fmt * WIP: tidy-tern-769 * WIP: tidy-tern-769 * chore: apply cargo fmt * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): add Magnitude opaque carrier (T-Numeric-Construction Slice 1) * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): T-Numeric-Construction Slice 2 — Nat = Semiring<Magnitude> * fix(std/nat): document tracked-scaffold dissolution trigger to CommutativeSemiring<T> Reviewer flagged: Nat denotationally inhabits CommutativeSemiring (commutative mul) but algebra.dag declares only Semiring<T>. Per modeling-philosophy (layer concept introductions; sharpen via stronger algebras as separate slices), this is the closest honest algebra surface today. Adding a P5 tracked-scaffold note pinning the dissolution trigger so the future algebra-strength sharpening slice is visible at the use site. * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * chore: apply cargo fmt * revert(std): drop Int = AbelianGroup<Nat> alias pivot; add GroupCompletion<M> 6Q audit Director ratified Option 2 substrate-split (inbox #1288 #4360232423) after two reviewers flagged a sharp M9 modeling-faithfulness finding: with the standard parametric reading of `AbelianGroup<T>`, T is the carrier of group operations including `inverse: fn(T) -> T`. With T = Nat, that denotes 'every Nat has an additive inverse' — false for ℕ. ℤ is derived from ℕ via Grothendieck construction; ℤ's carrier is not ℕ itself. Reverted in this commit: - dsl/std/integer.dag: type Int = Int64 restored; AbelianGroup/Nat imports removed. - src/v3/compiler/tests/integration/common/substrate_receipts.rs: receipt walks Int (= Int64) again; legacy comment restored. - src/v3/compiler/tests/integration/m1_substrate_test.rs: test renamed back to bootstrap_int_add_walk_reaches_ordered_ring_add_nobody_arrow. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: the AbelianGroup<Nat>-blessing ratchet (int_default_alias_resolves_to_abelian_group_over_nat) removed entirely per Director's 'do not keep a ratchet that blesses AbelianGroup<Nat>' guard. - bootstrap_*_generated.rs regenerated to track reverted integer.dag. Added in this commit: - docs/audit/t-numeric-construction-group-completion-6q.md: 6Q substrate- introduction audit for the prerequisite GroupCompletion<M> algebra surface. Recommends Shape C (opaque atom; carrier-representation deferred to per-target emission) per design doc 'no quotient/sign- magnitude representation' boundary. Once GroupCompletion<M> lands, Slice 3 becomes a single-line edit: type Int = GroupCompletion<Nat>. * fix(test): revert stale parse_corpus_manifest row for integer.dag Director caught: the PR's manifest still carried the alias-pivot bytes (16/12179/9c6a1d94...) for dsl/std/integer.dag, but integer.dag itself is reverted to origin/main state (15/11459/a2942a07...). Restore the manifest row so the PR diff is docs-only (the GroupCompletion<M> audit). * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): GroupCompletion<M> opaque-atom substrate-introduction Ships the prerequisite carrier construction from the audit at docs/audit/t-numeric-construction-group-completion-6q.md (#1422 audit receipt). Strictly Shape C — bare opaque atom in dsl/std/algebra.dag, parameterized by <M>, no fields, no algebra inhabitance. - dsl/std/algebra.dag: type GroupCompletion<M> declared after AbelianGroup<T>, with full header documenting hard boundaries (no quotient-of-pairs, no sign-magnitude, no mechanical AbelianGroup-witness derivation) + the constrained-inhabitance tracked-scaffold note (M : CommutativeMonoid is denotational; future parametric where-clause syntax dissolves the gap). - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet group_completion_is_bare_opaque_atom_with_one_type_parameter pinning span (algebra.dag), connective shape (Conj { children: [] }), type_params count (1), and absent value_body. - bootstrap_*_generated.rs regenerated; parse-corpus manifest refreshed for the new algebra.dag bytes. Per dispatch on inbox #1288 #4361921687: did NOT pivot Int (Slice 3 stays deferred), did NOT introduce quotient/sign-magnitude carrier facts, did NOT claim mechanical AbelianGroup witness derivation. The future Slice 3 edit becomes type Int = AbelianGroup<GroupCompletion<Nat>> per the audit's Q6 single-authority resolution. * feat(std): T-Numeric-Construction Slice 3 — Int = AbelianGroup<GroupCompletion<Nat>> Pivot the default Int alias to the canonical Q6 single-authority form per docs/audit/t-numeric-construction-group-completion-6q.md. Now that GroupCompletion<M> is a substrate carrier (#1448), the construction-chain layer-3 algebra is honest under standard parametric reading: T = GroupCompletion<Nat> (derived carrier; opaque atom) AbelianGroup<T> (algebra witness; inverse: T -> T well-defined) Fixed-width rows (Int8..Int128, UInt8..UInt128) stay on OrderedRing<Word*>/Semiring<Word*>. Word* storage carriers remain storage refinements, not alternate Int/Nat/Magnitude/GroupCompletion authorities. - dsl/std/integer.dag: type Int = AbelianGroup<GroupCompletion<Nat>>; imports Nat, AbelianGroup, GroupCompletion. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet int_default_alias_resolves_to_abelian_group_over_group_completion_of_nat pinning the two-step Instantiation chain (AbelianGroup template, carrier = GroupCompletion<Nat>, GroupCompletion's input = Nat). - src/v3/compiler/tests/integration/common/substrate_receipts.rs + m1_substrate_test.rs: legacy Int → OrderedRing receipt repointed to walk Int64 directly (the OrderedRing<Word64> chain it pinned now lives at the fixed-width row, not the default alias). - bootstrap_*_generated.rs regenerated; parse_corpus_manifest.txt refreshed. Per Director's guardrail (dispatch on inbox #1288 #4362239705): no consumer migration of legacy Int64/OrderedRing<Word*> chain in this PR; no quotient/sign-magnitude representation; no tokenizer/literal/refinement syntax work. Total downstream impact: one ratchet rename + manifest refresh — within the 'ratchets/generated outputs' scope explicitly authorized by the dispatch. * chore: apply cargo fmt * fix(test): pin transform_callable_unsupported_in_e3_slice to Bool not Int CI caught: Slice 3's pivot of `Int` from alias to direct Instantiation made `callable_runtime_arity(Int) = Some(3)` (AbelianGroup's Conj children), which fires the push_transform arity assertion when the test feeds 0 inputs. The test's subject is eval_node's rejection of Callable transforms — the declaration is incidental. Switch to `Bool` (Disj), whose `callable_runtime_arity` resolves to None and is stable across future numeric-substrate edits. * chore: apply cargo fmt * feat(std): T-Numeric-Construction Slice 4 — Rational = Field<Int> Adds layer 4 of the construction chain authored in docs/design-numeric-construction.md: Magnitude → Nat → Int → Rational → Real `Rational = Field<Int>` consumes the Slice 3 `Int = AbelianGroup<GroupCompletion<Nat>>` algebra (#1466) as the underlying carrier and extends the ring structure with Field's reciprocal/division operations. Per dispatch on inbox #1288 #4362611659: attempted the simple alias form first (Director's preference); if reviewers prove M9 cannot stand under the standard parametric reading of Field<T>'s reciprocal field, the slice escalates to Director for substrate-split ratification (mirroring the GroupCompletion path established in Slice 3). - dsl/std/rational.dag (new): module std.rational; type Rational = Field<Int>. Long header documents the executable-completeness gap (Field<Int> denotes reciprocal: fn(Int) -> Int which is denotationally undefined for non-units in ℤ) as a P5 tracked scaffold with named dissolution trigger (FieldOfFractions<R> derived-carrier or NonZero/Result reciprocal refinement), consistent with the prior #1370 audit's deferred completeness gap. - src/v3/compiler/src/bootstrap_regen_fresh.rs: rational.dag wired into std_fixtures (between integer.dag and string_type.dag). - src/v3/compiler/tests/integration.rs: parse-corpus extended; new parser smoke handwritten_parser_accepts_rational_dag. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet rational_resolves_to_field_over_int pinning span (rational.dag), outer Field instantiation, and Int carrier (alias-chain walk through the construction-chain Int alias). - src/v3/compiler/tests/integration/parse_corpus_manifest.txt: refreshed. - bootstrap_*_generated.rs regenerated. Hard boundaries respected: - No NonZero/Result reciprocal semantics in this PR (deferred per dispatch). - No refinement syntax. - No consumer migration. - No tokenizer/literal-grammar work. * chore: apply cargo fmt * revert(std): drop Rational = Field<Int> alias pivot; add FieldOfFractions<R> 6Q audit Director ratified Option 2 substrate-split (inbox #1288 #4362643231) after the same M9 modeling-faithfulness finding that retired AbelianGroup<Nat>: under the standard parametric reading of Field<T>, T is the carrier of field operations including reciprocal: fn(T) -> T. With T = Int, that denotes 'every Int has a multiplicative inverse' — false for ℤ (only ±1 are units). ℚ is the field of fractions derived from ℤ; ℚ's carrier is not Int itself. Reverted in this commit: - dsl/std/rational.dag: deleted (was authoring the false alias). - 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 (per Director's 'remove any ratchet that blesses Field<Int>' guard). - bootstrap_*_generated.rs regenerated to track the revert. - parse_corpus_manifest.txt restored to origin/main state. Added in this commit: - docs/audit/t-numeric-construction-field-of-fractions-6q.md: 6Q substrate-introduction audit for the prerequisite FieldOfFractions<R> algebra surface. Recommends Shape C (opaque atom; carrier-representation deferred to per-target emission) per Director's 'no pair/quotient numerator-denominator representation' boundary and the GroupCompletion precedent (#1448). Once Shape C lands, Slice 4 becomes a one-line edit: type Rational = Field<FieldOfFractions<Int>>.

…y ratchet (#1514) * WIP: tidy-tern-769 * chore: apply cargo fmt * WIP: tidy-tern-769 * WIP: tidy-tern-769 * chore: apply cargo fmt * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): add Magnitude opaque carrier (T-Numeric-Construction Slice 1) * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): T-Numeric-Construction Slice 2 — Nat = Semiring<Magnitude> * fix(std/nat): document tracked-scaffold dissolution trigger to CommutativeSemiring<T> Reviewer flagged: Nat denotationally inhabits CommutativeSemiring (commutative mul) but algebra.dag declares only Semiring<T>. Per modeling-philosophy (layer concept introductions; sharpen via stronger algebras as separate slices), this is the closest honest algebra surface today. Adding a P5 tracked-scaffold note pinning the dissolution trigger so the future algebra-strength sharpening slice is visible at the use site. * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * chore: apply cargo fmt * revert(std): drop Int = AbelianGroup<Nat> alias pivot; add GroupCompletion<M> 6Q audit Director ratified Option 2 substrate-split (inbox #1288 #4360232423) after two reviewers flagged a sharp M9 modeling-faithfulness finding: with the standard parametric reading of `AbelianGroup<T>`, T is the carrier of group operations including `inverse: fn(T) -> T`. With T = Nat, that denotes 'every Nat has an additive inverse' — false for ℕ. ℤ is derived from ℕ via Grothendieck construction; ℤ's carrier is not ℕ itself. Reverted in this commit: - dsl/std/integer.dag: type Int = Int64 restored; AbelianGroup/Nat imports removed. - src/v3/compiler/tests/integration/common/substrate_receipts.rs: receipt walks Int (= Int64) again; legacy comment restored. - src/v3/compiler/tests/integration/m1_substrate_test.rs: test renamed back to bootstrap_int_add_walk_reaches_ordered_ring_add_nobody_arrow. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: the AbelianGroup<Nat>-blessing ratchet (int_default_alias_resolves_to_abelian_group_over_nat) removed entirely per Director's 'do not keep a ratchet that blesses AbelianGroup<Nat>' guard. - bootstrap_*_generated.rs regenerated to track reverted integer.dag. Added in this commit: - docs/audit/t-numeric-construction-group-completion-6q.md: 6Q substrate- introduction audit for the prerequisite GroupCompletion<M> algebra surface. Recommends Shape C (opaque atom; carrier-representation deferred to per-target emission) per design doc 'no quotient/sign- magnitude representation' boundary. Once GroupCompletion<M> lands, Slice 3 becomes a single-line edit: type Int = GroupCompletion<Nat>. * fix(test): revert stale parse_corpus_manifest row for integer.dag Director caught: the PR's manifest still carried the alias-pivot bytes (16/12179/9c6a1d94...) for dsl/std/integer.dag, but integer.dag itself is reverted to origin/main state (15/11459/a2942a07...). Restore the manifest row so the PR diff is docs-only (the GroupCompletion<M> audit). * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): GroupCompletion<M> opaque-atom substrate-introduction Ships the prerequisite carrier construction from the audit at docs/audit/t-numeric-construction-group-completion-6q.md (#1422 audit receipt). Strictly Shape C — bare opaque atom in dsl/std/algebra.dag, parameterized by <M>, no fields, no algebra inhabitance. - dsl/std/algebra.dag: type GroupCompletion<M> declared after AbelianGroup<T>, with full header documenting hard boundaries (no quotient-of-pairs, no sign-magnitude, no mechanical AbelianGroup-witness derivation) + the constrained-inhabitance tracked-scaffold note (M : CommutativeMonoid is denotational; future parametric where-clause syntax dissolves the gap). - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet group_completion_is_bare_opaque_atom_with_one_type_parameter pinning span (algebra.dag), connective shape (Conj { children: [] }), type_params count (1), and absent value_body. - bootstrap_*_generated.rs regenerated; parse-corpus manifest refreshed for the new algebra.dag bytes. Per dispatch on inbox #1288 #4361921687: did NOT pivot Int (Slice 3 stays deferred), did NOT introduce quotient/sign-magnitude carrier facts, did NOT claim mechanical AbelianGroup witness derivation. The future Slice 3 edit becomes type Int = AbelianGroup<GroupCompletion<Nat>> per the audit's Q6 single-authority resolution. * feat(std): T-Numeric-Construction Slice 3 — Int = AbelianGroup<GroupCompletion<Nat>> Pivot the default Int alias to the canonical Q6 single-authority form per docs/audit/t-numeric-construction-group-completion-6q.md. Now that GroupCompletion<M> is a substrate carrier (#1448), the construction-chain layer-3 algebra is honest under standard parametric reading: T = GroupCompletion<Nat> (derived carrier; opaque atom) AbelianGroup<T> (algebra witness; inverse: T -> T well-defined) Fixed-width rows (Int8..Int128, UInt8..UInt128) stay on OrderedRing<Word*>/Semiring<Word*>. Word* storage carriers remain storage refinements, not alternate Int/Nat/Magnitude/GroupCompletion authorities. - dsl/std/integer.dag: type Int = AbelianGroup<GroupCompletion<Nat>>; imports Nat, AbelianGroup, GroupCompletion. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet int_default_alias_resolves_to_abelian_group_over_group_completion_of_nat pinning the two-step Instantiation chain (AbelianGroup template, carrier = GroupCompletion<Nat>, GroupCompletion's input = Nat). - src/v3/compiler/tests/integration/common/substrate_receipts.rs + m1_substrate_test.rs: legacy Int → OrderedRing receipt repointed to walk Int64 directly (the OrderedRing<Word64> chain it pinned now lives at the fixed-width row, not the default alias). - bootstrap_*_generated.rs regenerated; parse_corpus_manifest.txt refreshed. Per Director's guardrail (dispatch on inbox #1288 #4362239705): no consumer migration of legacy Int64/OrderedRing<Word*> chain in this PR; no quotient/sign-magnitude representation; no tokenizer/literal/refinement syntax work. Total downstream impact: one ratchet rename + manifest refresh — within the 'ratchets/generated outputs' scope explicitly authorized by the dispatch. * chore: apply cargo fmt * fix(test): pin transform_callable_unsupported_in_e3_slice to Bool not Int CI caught: Slice 3's pivot of `Int` from alias to direct Instantiation made `callable_runtime_arity(Int) = Some(3)` (AbelianGroup's Conj children), which fires the push_transform arity assertion when the test feeds 0 inputs. The test's subject is eval_node's rejection of Callable transforms — the declaration is incidental. Switch to `Bool` (Disj), whose `callable_runtime_arity` resolves to None and is stable across future numeric-substrate edits. * chore: apply cargo fmt * feat(std): T-Numeric-Construction Slice 4 — Rational = Field<Int> Adds layer 4 of the construction chain authored in docs/design-numeric-construction.md: Magnitude → Nat → Int → Rational → Real `Rational = Field<Int>` consumes the Slice 3 `Int = AbelianGroup<GroupCompletion<Nat>>` algebra (#1466) as the underlying carrier and extends the ring structure with Field's reciprocal/division operations. Per dispatch on inbox #1288 #4362611659: attempted the simple alias form first (Director's preference); if reviewers prove M9 cannot stand under the standard parametric reading of Field<T>'s reciprocal field, the slice escalates to Director for substrate-split ratification (mirroring the GroupCompletion path established in Slice 3). - dsl/std/rational.dag (new): module std.rational; type Rational = Field<Int>. Long header documents the executable-completeness gap (Field<Int> denotes reciprocal: fn(Int) -> Int which is denotationally undefined for non-units in ℤ) as a P5 tracked scaffold with named dissolution trigger (FieldOfFractions<R> derived-carrier or NonZero/Result reciprocal refinement), consistent with the prior #1370 audit's deferred completeness gap. - src/v3/compiler/src/bootstrap_regen_fresh.rs: rational.dag wired into std_fixtures (between integer.dag and string_type.dag). - src/v3/compiler/tests/integration.rs: parse-corpus extended; new parser smoke handwritten_parser_accepts_rational_dag. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet rational_resolves_to_field_over_int pinning span (rational.dag), outer Field instantiation, and Int carrier (alias-chain walk through the construction-chain Int alias). - src/v3/compiler/tests/integration/parse_corpus_manifest.txt: refreshed. - bootstrap_*_generated.rs regenerated. Hard boundaries respected: - No NonZero/Result reciprocal semantics in this PR (deferred per dispatch). - No refinement syntax. - No consumer migration. - No tokenizer/literal-grammar work. * chore: apply cargo fmt * revert(std): drop Rational = Field<Int> alias pivot; add FieldOfFractions<R> 6Q audit Director ratified Option 2 substrate-split (inbox #1288 #4362643231) after the same M9 modeling-faithfulness finding that retired AbelianGroup<Nat>: under the standard parametric reading of Field<T>, T is the carrier of field operations including reciprocal: fn(T) -> T. With T = Int, that denotes 'every Int has a multiplicative inverse' — false for ℤ (only ±1 are units). ℚ is the field of fractions derived from ℤ; ℚ's carrier is not Int itself. Reverted in this commit: - dsl/std/rational.dag: deleted (was authoring the false alias). - 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 (per Director's 'remove any ratchet that blesses Field<Int>' guard). - bootstrap_*_generated.rs regenerated to track the revert. - parse_corpus_manifest.txt restored to origin/main state. Added in this commit: - docs/audit/t-numeric-construction-field-of-fractions-6q.md: 6Q substrate-introduction audit for the prerequisite FieldOfFractions<R> algebra surface. Recommends Shape C (opaque atom; carrier-representation deferred to per-target emission) per Director's 'no pair/quotient numerator-denominator representation' boundary and the GroupCompletion precedent (#1448). Once Shape C lands, Slice 4 becomes a one-line edit: type Rational = Field<FieldOfFractions<Int>>. * WIP: tidy-tern-769 * test(v3): add per_call_descent_evidence_is_single_lookup_authority ratchet T-E-P-Producer-Broadening gate (2) — e_p_call_pattern_lookup_authoritative (per Director's path-(1) selection on inbox #1288 #4363830953). Pins per_call_descent_evidence as the single lookup authority for per-call SubValueRelation evidence over TransformTarget::Callable transforms. Behavioral cardinality assertion: - Every Callable transform in the user fixture file appears in exactly one CallDescentEvidence entry (uniqueness; no parallel producer appending duplicates). - The producer's emitted set (filtered to fixture file) equals the enumerated Callable-transform set in the fixture (totality; producer is not silently dropping call sites). - Every entry corresponds to a real Callable-targeted transform (no synthetic entries from a parallel walker). Visibility unchanged: SubValueRelation enum constructors stay pub for existing test usage (m2_substrate_inhabitance_test.rs:577 and the new e_p tests construct SubValueUnknown directly); the producer helpers classify_call_argument and arithmetic_descent_relation are already private to dag.rs. No producer broadening, no substrate carrier introduction, no lens consumer in this slice. Per dispatch (#1288 #4363830953): S-sized ratchet only; gates (1) and (3) tracked as separate slices. * test(v3): expand E-P gate-2 fixture to exercise cross-template branch Reviewer caught: gate (2) single-authority claim must hold for both branches of per_call_descent_evidence's match (caller_template == callee_template self-recursion AND resolved cross-template fail-closed), but the prior fixture only had countdown self-recursion. A future producer that adds a parallel walker for cross-template evidence (rather than going through the existing fail-closed path) would slip past a self-recursion-only ratchet. Restored the two-function fixture (countdown + caller→helper) so the sanity-floor assertion >= 2 Callable transforms exercises both branches, and the coverage-equality assertion enforces single-authority over the cross-template fail-closed path too. Verified locally with RUST_MIN_STACK=33554432: test passes. * polish(test): trim duplicate comments + dead let; align module doc with span-scoped oracle Cursor exploratory feedback (#1514): two duplicate comment blocks merged into one, no-op 'let _ = ();' placeholder dropped (subsumed by neighbour comment), variable renamed owned_callable_transforms → fixture_callable_transforms (span-based, not body-bind-based) for accuracy, module doc bullet rewritten to describe the span-scoped oracle the code actually uses. No behavioral change; tightens local-readability of the ratchet.

… constructors (#1551) * WIP: tidy-tern-769 * chore: apply cargo fmt * WIP: tidy-tern-769 * WIP: tidy-tern-769 * chore: apply cargo fmt * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): add Magnitude opaque carrier (T-Numeric-Construction Slice 1) * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): T-Numeric-Construction Slice 2 — Nat = Semiring<Magnitude> * fix(std/nat): document tracked-scaffold dissolution trigger to CommutativeSemiring<T> Reviewer flagged: Nat denotationally inhabits CommutativeSemiring (commutative mul) but algebra.dag declares only Semiring<T>. Per modeling-philosophy (layer concept introductions; sharpen via stronger algebras as separate slices), this is the closest honest algebra surface today. Adding a P5 tracked-scaffold note pinning the dissolution trigger so the future algebra-strength sharpening slice is visible at the use site. * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * chore: apply cargo fmt * revert(std): drop Int = AbelianGroup<Nat> alias pivot; add GroupCompletion<M> 6Q audit Director ratified Option 2 substrate-split (inbox #1288 #4360232423) after two reviewers flagged a sharp M9 modeling-faithfulness finding: with the standard parametric reading of `AbelianGroup<T>`, T is the carrier of group operations including `inverse: fn(T) -> T`. With T = Nat, that denotes 'every Nat has an additive inverse' — false for ℕ. ℤ is derived from ℕ via Grothendieck construction; ℤ's carrier is not ℕ itself. Reverted in this commit: - dsl/std/integer.dag: type Int = Int64 restored; AbelianGroup/Nat imports removed. - src/v3/compiler/tests/integration/common/substrate_receipts.rs: receipt walks Int (= Int64) again; legacy comment restored. - src/v3/compiler/tests/integration/m1_substrate_test.rs: test renamed back to bootstrap_int_add_walk_reaches_ordered_ring_add_nobody_arrow. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: the AbelianGroup<Nat>-blessing ratchet (int_default_alias_resolves_to_abelian_group_over_nat) removed entirely per Director's 'do not keep a ratchet that blesses AbelianGroup<Nat>' guard. - bootstrap_*_generated.rs regenerated to track reverted integer.dag. Added in this commit: - docs/audit/t-numeric-construction-group-completion-6q.md: 6Q substrate- introduction audit for the prerequisite GroupCompletion<M> algebra surface. Recommends Shape C (opaque atom; carrier-representation deferred to per-target emission) per design doc 'no quotient/sign- magnitude representation' boundary. Once GroupCompletion<M> lands, Slice 3 becomes a single-line edit: type Int = GroupCompletion<Nat>. * fix(test): revert stale parse_corpus_manifest row for integer.dag Director caught: the PR's manifest still carried the alias-pivot bytes (16/12179/9c6a1d94...) for dsl/std/integer.dag, but integer.dag itself is reverted to origin/main state (15/11459/a2942a07...). Restore the manifest row so the PR diff is docs-only (the GroupCompletion<M> audit). * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): GroupCompletion<M> opaque-atom substrate-introduction Ships the prerequisite carrier construction from the audit at docs/audit/t-numeric-construction-group-completion-6q.md (#1422 audit receipt). Strictly Shape C — bare opaque atom in dsl/std/algebra.dag, parameterized by <M>, no fields, no algebra inhabitance. - dsl/std/algebra.dag: type GroupCompletion<M> declared after AbelianGroup<T>, with full header documenting hard boundaries (no quotient-of-pairs, no sign-magnitude, no mechanical AbelianGroup-witness derivation) + the constrained-inhabitance tracked-scaffold note (M : CommutativeMonoid is denotational; future parametric where-clause syntax dissolves the gap). - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet group_completion_is_bare_opaque_atom_with_one_type_parameter pinning span (algebra.dag), connective shape (Conj { children: [] }), type_params count (1), and absent value_body. - bootstrap_*_generated.rs regenerated; parse-corpus manifest refreshed for the new algebra.dag bytes. Per dispatch on inbox #1288 #4361921687: did NOT pivot Int (Slice 3 stays deferred), did NOT introduce quotient/sign-magnitude carrier facts, did NOT claim mechanical AbelianGroup witness derivation. The future Slice 3 edit becomes type Int = AbelianGroup<GroupCompletion<Nat>> per the audit's Q6 single-authority resolution. * feat(std): T-Numeric-Construction Slice 3 — Int = AbelianGroup<GroupCompletion<Nat>> Pivot the default Int alias to the canonical Q6 single-authority form per docs/audit/t-numeric-construction-group-completion-6q.md. Now that GroupCompletion<M> is a substrate carrier (#1448), the construction-chain layer-3 algebra is honest under standard parametric reading: T = GroupCompletion<Nat> (derived carrier; opaque atom) AbelianGroup<T> (algebra witness; inverse: T -> T well-defined) Fixed-width rows (Int8..Int128, UInt8..UInt128) stay on OrderedRing<Word*>/Semiring<Word*>. Word* storage carriers remain storage refinements, not alternate Int/Nat/Magnitude/GroupCompletion authorities. - dsl/std/integer.dag: type Int = AbelianGroup<GroupCompletion<Nat>>; imports Nat, AbelianGroup, GroupCompletion. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet int_default_alias_resolves_to_abelian_group_over_group_completion_of_nat pinning the two-step Instantiation chain (AbelianGroup template, carrier = GroupCompletion<Nat>, GroupCompletion's input = Nat). - src/v3/compiler/tests/integration/common/substrate_receipts.rs + m1_substrate_test.rs: legacy Int → OrderedRing receipt repointed to walk Int64 directly (the OrderedRing<Word64> chain it pinned now lives at the fixed-width row, not the default alias). - bootstrap_*_generated.rs regenerated; parse_corpus_manifest.txt refreshed. Per Director's guardrail (dispatch on inbox #1288 #4362239705): no consumer migration of legacy Int64/OrderedRing<Word*> chain in this PR; no quotient/sign-magnitude representation; no tokenizer/literal/refinement syntax work. Total downstream impact: one ratchet rename + manifest refresh — within the 'ratchets/generated outputs' scope explicitly authorized by the dispatch. * chore: apply cargo fmt * fix(test): pin transform_callable_unsupported_in_e3_slice to Bool not Int CI caught: Slice 3's pivot of `Int` from alias to direct Instantiation made `callable_runtime_arity(Int) = Some(3)` (AbelianGroup's Conj children), which fires the push_transform arity assertion when the test feeds 0 inputs. The test's subject is eval_node's rejection of Callable transforms — the declaration is incidental. Switch to `Bool` (Disj), whose `callable_runtime_arity` resolves to None and is stable across future numeric-substrate edits. * chore: apply cargo fmt * feat(std): T-Numeric-Construction Slice 4 — Rational = Field<Int> Adds layer 4 of the construction chain authored in docs/design-numeric-construction.md: Magnitude → Nat → Int → Rational → Real `Rational = Field<Int>` consumes the Slice 3 `Int = AbelianGroup<GroupCompletion<Nat>>` algebra (#1466) as the underlying carrier and extends the ring structure with Field's reciprocal/division operations. Per dispatch on inbox #1288 #4362611659: attempted the simple alias form first (Director's preference); if reviewers prove M9 cannot stand under the standard parametric reading of Field<T>'s reciprocal field, the slice escalates to Director for substrate-split ratification (mirroring the GroupCompletion path established in Slice 3). - dsl/std/rational.dag (new): module std.rational; type Rational = Field<Int>. Long header documents the executable-completeness gap (Field<Int> denotes reciprocal: fn(Int) -> Int which is denotationally undefined for non-units in ℤ) as a P5 tracked scaffold with named dissolution trigger (FieldOfFractions<R> derived-carrier or NonZero/Result reciprocal refinement), consistent with the prior #1370 audit's deferred completeness gap. - src/v3/compiler/src/bootstrap_regen_fresh.rs: rational.dag wired into std_fixtures (between integer.dag and string_type.dag). - src/v3/compiler/tests/integration.rs: parse-corpus extended; new parser smoke handwritten_parser_accepts_rational_dag. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet rational_resolves_to_field_over_int pinning span (rational.dag), outer Field instantiation, and Int carrier (alias-chain walk through the construction-chain Int alias). - src/v3/compiler/tests/integration/parse_corpus_manifest.txt: refreshed. - bootstrap_*_generated.rs regenerated. Hard boundaries respected: - No NonZero/Result reciprocal semantics in this PR (deferred per dispatch). - No refinement syntax. - No consumer migration. - No tokenizer/literal-grammar work. * chore: apply cargo fmt * revert(std): drop Rational = Field<Int> alias pivot; add FieldOfFractions<R> 6Q audit Director ratified Option 2 substrate-split (inbox #1288 #4362643231) after the same M9 modeling-faithfulness finding that retired AbelianGroup<Nat>: under the standard parametric reading of Field<T>, T is the carrier of field operations including reciprocal: fn(T) -> T. With T = Int, that denotes 'every Int has a multiplicative inverse' — false for ℤ (only ±1 are units). ℚ is the field of fractions derived from ℤ; ℚ's carrier is not Int itself. Reverted in this commit: - dsl/std/rational.dag: deleted (was authoring the false alias). - 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 (per Director's 'remove any ratchet that blesses Field<Int>' guard). - bootstrap_*_generated.rs regenerated to track the revert. - parse_corpus_manifest.txt restored to origin/main state. Added in this commit: - docs/audit/t-numeric-construction-field-of-fractions-6q.md: 6Q substrate-introduction audit for the prerequisite FieldOfFractions<R> algebra surface. Recommends Shape C (opaque atom; carrier-representation deferred to per-target emission) per Director's 'no pair/quotient numerator-denominator representation' boundary and the GroupCompletion precedent (#1448). Once Shape C lands, Slice 4 becomes a one-line edit: type Rational = Field<FieldOfFractions<Int>>. * WIP: tidy-tern-769 * test(v3): add per_call_descent_evidence_is_single_lookup_authority ratchet T-E-P-Producer-Broadening gate (2) — e_p_call_pattern_lookup_authoritative (per Director's path-(1) selection on inbox #1288 #4363830953). Pins per_call_descent_evidence as the single lookup authority for per-call SubValueRelation evidence over TransformTarget::Callable transforms. Behavioral cardinality assertion: - Every Callable transform in the user fixture file appears in exactly one CallDescentEvidence entry (uniqueness; no parallel producer appending duplicates). - The producer's emitted set (filtered to fixture file) equals the enumerated Callable-transform set in the fixture (totality; producer is not silently dropping call sites). - Every entry corresponds to a real Callable-targeted transform (no synthetic entries from a parallel walker). Visibility unchanged: SubValueRelation enum constructors stay pub for existing test usage (m2_substrate_inhabitance_test.rs:577 and the new e_p tests construct SubValueUnknown directly); the producer helpers classify_call_argument and arithmetic_descent_relation are already private to dag.rs. No producer broadening, no substrate carrier introduction, no lens consumer in this slice. Per dispatch (#1288 #4363830953): S-sized ratchet only; gates (1) and (3) tracked as separate slices. * test(v3): expand E-P gate-2 fixture to exercise cross-template branch Reviewer caught: gate (2) single-authority claim must hold for both branches of per_call_descent_evidence's match (caller_template == callee_template self-recursion AND resolved cross-template fail-closed), but the prior fixture only had countdown self-recursion. A future producer that adds a parallel walker for cross-template evidence (rather than going through the existing fail-closed path) would slip past a self-recursion-only ratchet. Restored the two-function fixture (countdown + caller→helper) so the sanity-floor assertion >= 2 Callable transforms exercises both branches, and the coverage-equality assertion enforces single-authority over the cross-template fail-closed path too. Verified locally with RUST_MIN_STACK=33554432: test passes. * polish(test): trim duplicate comments + dead let; align module doc with span-scoped oracle Cursor exploratory feedback (#1514): two duplicate comment blocks merged into one, no-op 'let _ = ();' placeholder dropped (subsumed by neighbour comment), variable renamed owned_callable_transforms → fixture_callable_transforms (span-based, not body-bind-based) for accuracy, module doc bullet rewritten to describe the span-scoped oracle the code actually uses. No behavioral change; tightens local-readability of the ratchet. * fix(v3): reject duplicate fields in expression-position named-variant constructors `lower_record_to_structural` (data body) and `lower_record_literal_expr` (anonymous record expression) already rejected duplicate field labels before type-field projection. `lower_variant_record_expr` — the path for named-constructor record payloads at expression position, e.g. `Ready { code: 1, code: 2, retry: false }` inside an fn body — silently projected via `find()` over the literal's fields, dropping the second occurrence and constructing a normal payload. Mirror the duplicate-detection pattern from `lower_record_literal_expr` (HashSet pre-pass returning a typed ResolveError on collision) so the third record-shape lowering path now also fails closed. Adds `expr_named_variant_duplicate_payload_fields_fail_closed` covering the previously-silent expression-context path; the existing `data_body_named_variant_duplicate_payload_fields_fail_closed` covers the data-body context. Closes the "Duplicate record-literal fields silently accepted" row of docs/debt/r3-debt-paydown-ledger-2026-05-02.md. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * chore: refresh parse_corpus_manifest after induction.dag content change PR #1543 modified `src/v3/std/induction.dag` to correct a SubValueRelation algebra claim but did not refresh the SG-2 parser-corpus snapshot, leaving the committed manifest hash stale relative to the actual file. The v3 suite's `handwritten_parse_snapshot_matches_manifest` reproduced this on the merge into this branch — refreshing via the documented helper. Generated by: cargo test -p v3-compiler --test integration \\ refresh_handwritten_parse_snapshot_manifest -- --ignored Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * chore: refresh bootstrap_generated.rs after induction.dag content change PR #1543 modified `src/v3/std/induction.dag` (SubValueRelation algebra correction) but did not regenerate the committed bootstrap snapshot. v3 CI's `regen_bootstrap --verify` gate flagged span-offset drift in the induction.dag entry on this branch. Regenerated via the documented helper. Generated by: cargo run -p v3-compiler --features bootstrap-regen-fresh \\ --bin regen_bootstrap Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

briansrls added 30 commits April 30, 2026 17:47

WIP: tidy-tern-769

2592b65

chore: apply cargo fmt

3453a17

WIP: tidy-tern-769

c36e956

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

8d10039

# Conflicts: # src/v3/compiler/src/bootstrap_generated.rs # src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs

WIP: tidy-tern-769

f008b6f

chore: apply cargo fmt

dce2fc0

WIP: tidy-tern-769

0f2d0d0

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

75772bd

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

37e9b38

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

16207e9

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

962d973

# Conflicts: # src/v3/compiler/src/bootstrap_generated.rs # src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

46e92f0

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

9fd943e

# Conflicts: # src/v3/compiler/src/bootstrap_generated.rs # src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

ed0f59c

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

361e128

WIP: tidy-tern-769

c806aaa

feat(std): add Magnitude opaque carrier (T-Numeric-Construction Slice 1)

64edc56

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

6b756a9

WIP: tidy-tern-769

874e321

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

08bb95a

WIP: tidy-tern-769

d279af0

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

07cb719

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

6440ca0

WIP: tidy-tern-769

c4a56fa

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

83ac68d

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

09f0af7

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

00d4c7f

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

dd23d33

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

5f533e0

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

63d7075

briansrls added 2 commits May 1, 2026 14:14

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

b85c1b0

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

4ba0341

briansrls commented May 1, 2026

View reviewed changes

Comment thread docs/audit/t-numeric-construction-group-completion-6q.md

### Q1 — Cardinality invariants

Does the type admit `[]` when invariant says ≥1, or singletons when ≥2?

This comment was marked as resolved.

Sign in to view

WIP: tidy-tern-769

8bbdc3b

WIP: tidy-tern-769

041a006

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

f65b4de

Merge remote-tracking branch 'origin/main' into session/tidy-tern-769

ded3991

briansrls commented May 1, 2026

View reviewed changes

briansrls merged commit b584bc7 into main May 1, 2026
4 checks passed

briansrls mentioned this pull request May 1, 2026

session/zesty-bear-812 · gunbc Director #828

Closed

briansrls mentioned this pull request May 1, 2026

feat(std): GroupCompletion<M> opaque-atom substrate-introduction #1448

Merged

4 of 7 tasks

briansrls mentioned this pull request May 2, 2026

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

Merged

2 of 3 tasks

briansrls mentioned this pull request May 5, 2026

docs(audit): R3 debt sweep framework draft (Phase 1) — gunbc#828 dispatch #1804

Closed


		### Q1 — Cardinality invariants
		Does the type admit `[]` when invariant says ≥1, or singletons when ≥2?

Conversation

briansrls commented May 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Why the original alias pivot was reverted

What this PR contains

Hard boundaries respected

Next steps (out of this PR)

Test plan

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented May 1, 2026 •

edited

Loading