docs(r3): P1 axiom paydown — Int=AbelianGroup<Nat> shorthand corrected (Brian directive)

docs/r3-design-schedule-2026-05-06.md

@@ -37,7 +37,13 @@
 
 ### S3 — `MachineConstraint<C>` carrier design (Brian directive 2026-05-06)
 
-**Scope**: design substrate carriers for **algebra × machine-constraints interaction modeling** per Brian directive: concrete types like `i64` emerge as products of independent constraint axes (algebra `Int = AbelianGroup<Nat>` × machine `MachineWidth<64>`), NOT primary entities.
+**Scope**: design substrate carriers for **algebra × machine-constraints interaction modeling** per Brian directive: concrete types like `i64` emerge as products of independent constraint axes (algebra side × machine `MachineWidth<64>`), NOT primary entities.
+
+**P1 axiom-violation paydown (2026-05-06; Brian directive)**: prior framing `Int = AbelianGroup<Nat>` is **structurally false** — Nat is a commutative monoid under +, not the carrier of an Abelian group (no additive inverses in {0,1,2,...}). Per ratified self-correction at [gunbc#1739 issuecomment-4385432940](https://github.com/gunb-ai/gunbc/issues/1739#issuecomment-4385432940) (cross-ref: Director-side memory entry `feedback_verify_algebraic_axioms_in_ratification` logs the discipline going forward). Two mathematically sound options pending design selection (worker judgment per `feedback_compositional_not_templating`):
+- **Option A** — `Int` as canonical AbelianGroup primitive (terminal, no Nat parameter). Severs the constructive Nat→Int edge; `Int` is just-ℤ, not derived.
+- **Option B** — `Int ≡ GroupCompletion<CommutativeMonoid<Nat>>` (Grothendieck). Algebra-faithful; preserves compositional Nat→Int edge; introduces `GroupCompletion<M>` as new substrate (P1 procedure required: name second consumer beyond Int OR justify single-consumer via P1 carve-out).
+
+Prior `AbelianGroup<Nat>` references in r3-structure.md, r3-program-plan.md, this doc are **DEFERRED-shorthand** until design selection lands. **T-Numeric-Construction further dispatch HELD** (Brian directive 2026-05-06) until algebra-side selection ratified. S3 (`MachineConstraint<C>`) interaction modeling proceeds in parallel — once algebra-side resolves, the interaction `Int<N> = Int × MachineWidth<N>` semantics carries through identically under either option (Int participates as AbelianGroup carrier in both).
 
 Carriers needed: `MachineConstraint<C>` + `MachineWidth<bits>` + interaction-lookup substrate. May require additional axes (`RegisterClass<R>`, `EndianMode<E>`, alignment) per use cases.
 

docs/r3-program-plan.md

@@ -71,7 +71,7 @@ Per `r3-debt-sweep-2026-05-06.md` §Class A (line 39): *"parser/grammar surface,
 
 | Class | TestClaim gate | Representative gap-test | Lane(s) producing closure |
 |---|---|---|---|
-| 1 — parser/grammar surface | `substrate_gap_parser_grammar_closed` | v3 substrate models concrete types as the **interaction of independent constraint models** — abstract algebra × machine constraints — with concrete types emerging as consequences (per Brian directive 2026-05-06: *"these concepts should be the interaction of several constraint models i.e. abstract algebra × machine constraints — i64 would naturally emerge as a consequence"*). Refinement syntax `Type<N>` expresses the interaction, NOT a primary entity. Pass condition: substrate declares abstract algebra (e.g., `Int = AbelianGroup<Nat>`) and machine constraints (e.g., `MachineWidth<bits>`) as independent models; concrete types emerge via interaction (e.g., `Int<64>` = `Int × MachineWidth<64>`; target-language `i64` is derived artifact, NOT primary substrate entity). v3 parser handles generic interaction syntax; demonstrated against ≥3 algebra×constraint pairs — `Int<64>` (integer × 64-bit register), `Real<64>` (real × 64-bit float), `Nat<8>` (natural × 8-bit register) — without v2-fallback; gate Pass = all 3 interaction-derived programs produce 0 diagnostics + emitted artifact compiles to expected target primitive (`i64`/`f64`/`u8`) where the target primitive is consequence-of-interaction, not declared. The interaction-modeling requirement prevents single-axis (algebra-only or width-only) hard-coding. | T-V2-Retirement (parser path) + T-Numeric-Construction (algebra side) + Substrate (machine-constraint side, may require new substrate carrier `MachineConstraint<C>`) + Substrate continuation |
+| 1 — parser/grammar surface | `substrate_gap_parser_grammar_closed` | v3 substrate models concrete types as the **interaction of independent constraint models** — abstract algebra × machine constraints — with concrete types emerging as consequences (per Brian directive 2026-05-06: *"these concepts should be the interaction of several constraint models i.e. abstract algebra × machine constraints — i64 would naturally emerge as a consequence"*). Refinement syntax `Type<N>` expresses the interaction, NOT a primary entity. Pass condition: substrate declares abstract algebra (e.g., `Int` as canonical AbelianGroup carrier — Option A canonical-primitive **OR** Option B `GroupCompletion<CommutativeMonoid<Nat>>`; design selection pending per P1 axiom-violation paydown 2026-05-06 — prior `Int = AbelianGroup<Nat>` shorthand was structurally false [Nat lacks additive inverses]; ratification at [gunbc#1739 issuecomment-4385432940](https://github.com/gunb-ai/gunbc/issues/1739#issuecomment-4385432940) + memory entry `feedback_verify_algebraic_axioms_in_ratification`) and machine constraints (e.g., `MachineWidth<bits>`) as independent models; concrete types emerge via interaction (e.g., `Int<64>` = `Int × MachineWidth<64>`; target-language `i64` is derived artifact, NOT primary substrate entity). v3 parser handles generic interaction syntax; demonstrated against ≥3 algebra×constraint pairs — `Int<64>` (integer × 64-bit register), `Real<64>` (real × 64-bit float), `Nat<8>` (natural × 8-bit register) — without v2-fallback; gate Pass = all 3 interaction-derived programs produce 0 diagnostics + emitted artifact compiles to expected target primitive (`i64`/`f64`/`u8`) where the target primitive is consequence-of-interaction, not declared. The interaction-modeling requirement prevents single-axis (algebra-only or width-only) hard-coding. | T-V2-Retirement (parser path) + T-Numeric-Construction (algebra side) + Substrate (machine-constraint side, may require new substrate carrier `MachineConstraint<C>`) + Substrate continuation |
 | 2 — function-valued data | `substrate_gap_function_valued_data_closed` | `Lens<C>` instance with function-typed payload executes through evaluator | T-Lens-Application-Surface + T-E-P-Producer-Broadening — **chain-break per YELLOW chain rule** (Substrate Mgr 2026-05-06): prereq T-Lens-Application-Surface ← T-Lens-Behavioral-Parity ← Q-Lens-Behavioral-Parity-R3-Closeability (RED). Class 2 inherits RED until LBP scope-calibration resolves. See Q-Class-2-Chain-Break in §10.3. |
 | 3 — file-ingestion | `substrate_gap_file_ingestion_closed` | One `.dag` program ingests external file (e.g., timing observation set) without `include_str!` | T-Workflow-As-Data |
 | 4 — workflow/scheduling | `substrate_gap_workflow_scheduling_closed` | CI workflow modeled as `.dag` data executes through evaluator | T-Workflow-As-Data + T-Lens-Self-Application |

docs/r3-structure.md

@@ -89,7 +89,7 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine-
   - `pb_self_compile_fixed_point` (R1 gate; closes here under stronger interpretation) — v3 binary compiles `compiler.dag` and produces bit-identical stage0 Rust + bit-identical emitted artifacts. Predicate is the same R1 predicate; R3 closes it under fixed-point semantics rather than the looser "compiler can compile itself" reading
   - **Two-horizon clarification (per R1 Closure Manager review 2026-04-28):** the predicate name `pb_self_compile_fixed_point` carries TWO horizons: (i) **R1 lane gate** — Pass = current `verification.dag` + `test_runner` evaluation under the R1 acceptance discipline; this is what `#1050` + `#1074` made green at landing. (ii) **R3 thesis facet 2** — closes under the stronger interpretation (bit-identical fixed-point + SG-0 choreography per Director decisions). **R1 close does NOT wait on R3.** R1's gate Pass is whatever the current predicate evaluates to; R3's elevated bar is a separate release/thesis acceptance, not a silent rename of the R1 predicate. See `r2-structure.md` §"R1 closure criteria" for the R1-side framing.
 - **T-Numeric-Construction (REFRAMED 2026-05-01 from T-Int128).** Acceptance gates per [`docs/design-numeric-construction.md`](design-numeric-construction.md):
-  - `numeric_abstract_carriers_landed` — Magnitude (terminal), Nat (Semiring<Magnitude>), Int (AbelianGroup<Nat>), Rational (Field<Int>), Real (ApproximateField<Rational>) declared in `dsl/std/integer.dag` + `dsl/std/float.dag`
+  - `numeric_abstract_carriers_landed` — Magnitude (terminal), Nat (Semiring<Magnitude>), Int (canonical AbelianGroup primitive **OR** `GroupCompletion<CommutativeMonoid<Nat>>` — **design selection pending** per P1 axiom-violation paydown 2026-05-06; prior `Int = AbelianGroup<Nat>` shorthand is structurally false — Nat lacks additive inverses; see [gunbc#1739 issuecomment-4385432940](https://github.com/gunb-ai/gunbc/issues/1739#issuecomment-4385432940) + [`docs/design-numeric-construction.md`](design-numeric-construction.md) §3), Rational (Field<Int>), Real (ApproximateField<Rational>) declared in `dsl/std/integer.dag` + `dsl/std/float.dag`
   - `numeric_width_refinements_landed` — `Int<N>`, `Nat<N>`, `Real<N>` refinement chain resolves at compile time
   - `numeric_aliases_align_to_refinements` — `Int8`/.../`Int128`, `Float32`/`Float64`, `UInt8`/.../`UInt128` are refinements, not parallel substrate
   - `numeric_inherited_bake_ins_dissolved` — `Char`, `EpochMs`, `Duration`, `Milliseconds`, `Seconds` consume abstract `Int` (or appropriate refinement)
@@ -170,7 +170,7 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine-
   - `apply_lens_self_application_demonstrated` — `apply_lens(timing, ci_workflow, Enforce { budget: max_ns })` enforced via existing `EnforcedApplication<Output, Budget>` carrier (per T-Lens-Application-Surface §2 + §3.2); fail-closed when observation reports `Missing | Ambiguous | Stale` per timing-lens design; demonstrates that user-authored apply_lens substrate generalizes to project-self-validation use case
   - `recursive_flex_demonstration_landed` — narrative-load-bearing thesis claim cashes in worked instance: *"the compiler that compiles gunbc programs validates the workflow that produces gunbc itself."* Compiler-people read this as the categorical move that the lens framework isn't just for user code — it applies recursively to gunbc's own runtime behavior. Either emit-back-to-CI-YAML (bidirectional case via T-Workflow-As-Data) OR direct execution. <1 min CI target tracked as informational SLO; **not a closure gate** (per Director ratification 2026-05-04 — performance metric, not structural commitment)
 - **Substrate-gap-class closure** (NEW 2026-05-06; per Brian directive at [gunbc#846](https://github.com/gunb-ai/gunbc/issues/846); closure-criteria over existing lane work, NOT new separate lanes — added without expanding R3 lane count). Five class-level closure gates each closing when **both** (per [`docs/r3-program-plan.md`](r3-program-plan.md) §1.4 conjunctive predicate; Director poke-hole 2026-05-06 finding 1.3 + openai-pro 2026-05-06 finding 2.2): **(a)** representative gap-test executes through v3 cleanly per Pass condition AND **(b)** systematic enumeration of class-bridges shows count = 0 (or any survivors carry explicit Director allocation per `docs/audit/r3-debt-sweep-2026-05-06.md` §3.A STRUCTURAL exception). Single-test-pass alone is sample-of-class, NOT closure-of-class; conjunctive predicate prevents class reading "GREEN" while real bridges in that class persist unexercised by the chosen representative. Per [`docs/r3-program-plan.md`](r3-program-plan.md) §1.4 + §4.
-  - `substrate_gap_parser_grammar_closed` — v3 substrate models concrete types as the **interaction of independent constraint models** — abstract algebra × machine constraints — with concrete types emerging as consequences (per Brian directive 2026-05-06 at [gunbc#846 inline](https://github.com/gunb-ai/gunbc/pull/1808): *"these concepts should be the interaction of several constraint models i.e. abstract algebra × machine constraints — i64 would naturally emerge as a consequence"*). Refinement syntax `Type<N>` expresses the interaction, NOT a primary entity. Substrate declares abstract algebra (e.g., `Int = AbelianGroup<Nat>`) and machine constraints (e.g., `MachineWidth<bits>`) as **independent** models; concrete types emerge via interaction (e.g., `Int<64>` = `Int × MachineWidth<64>`; target-language `i64` is derived artifact, not primary substrate entity). Pass condition: ≥3 algebra×constraint pairs (`Int<64>` / `Real<64>` / `Nat<8>`) lower through stage0 emission without v2-fallback; emitted artifact compiles to expected target primitive (`i64` / `f64` / `u8`) where target primitive is consequence-of-interaction. Closes via T-V2-Retirement parser path + T-Numeric-Construction (algebra side) + Substrate continuation (machine-constraint side; may require new `MachineConstraint<C>` substrate carrier)
+  - `substrate_gap_parser_grammar_closed` — v3 substrate models concrete types as the **interaction of independent constraint models** — abstract algebra × machine constraints — with concrete types emerging as consequences (per Brian directive 2026-05-06 at [gunbc#846 inline](https://github.com/gunb-ai/gunbc/pull/1808): *"these concepts should be the interaction of several constraint models i.e. abstract algebra × machine constraints — i64 would naturally emerge as a consequence"*). Refinement syntax `Type<N>` expresses the interaction, NOT a primary entity. Substrate declares abstract algebra (e.g., `Int` as canonical AbelianGroup carrier — design selection pending Option A canonical-primitive vs Option B `GroupCompletion<CommutativeMonoid<Nat>>`; prior `Int = AbelianGroup<Nat>` shorthand was structurally false per P1 axiom paydown 2026-05-06, see [gunbc#1739 issuecomment-4385432940](https://github.com/gunb-ai/gunbc/issues/1739#issuecomment-4385432940)) and machine constraints (e.g., `MachineWidth<bits>`) as **independent** models; concrete types emerge via interaction (e.g., `Int<64>` = `Int × MachineWidth<64>`; target-language `i64` is derived artifact, not primary substrate entity). Pass condition: ≥3 algebra×constraint pairs (`Int<64>` / `Real<64>` / `Nat<8>`) lower through stage0 emission without v2-fallback; emitted artifact compiles to expected target primitive (`i64` / `f64` / `u8`) where target primitive is consequence-of-interaction. Closes via T-V2-Retirement parser path + T-Numeric-Construction (algebra side) + Substrate continuation (machine-constraint side; may require new `MachineConstraint<C>` substrate carrier)
   - `substrate_gap_function_valued_data_closed` — `Lens<C>` instance with function-typed payload executes through evaluator and produces `DimensionReport<C>` without Rust mediation. Closes via T-Lens-Application-Surface + T-E-P-Producer-Broadening
   - `substrate_gap_file_ingestion_closed` — One `.dag` program ingests external file (timing observation set, JSON config) without `include_str!`; exercises file-ingestion grammar. Closes via T-Workflow-As-Data
   - `substrate_gap_workflow_scheduling_closed` — CI workflow modeled as `.dag` data executes through evaluator + produces `DimensionReport<TimingMeasurement>`. Closes via T-Workflow-As-Data + T-Lens-Self-Application