v4: D2 reversal + fact-bundle reseed plan (RATIFIED 2026-05-17)

[briansrls]

Summary

The planning record for the D2 reversal + fact-bundle reseed the operator declared on 2026-05-17. Adds one PROPOSED section to src/v4/DECISIONS.md — doc-only, 102 insertions.

D2 (the alias-identity inhabitance form — type RustI32 = Int32) is reversed: a bare alias asserts an unproven identity and reads zero facts from the modeled language's spec — it is not modeling. The replacement is fact-bundle modeling: model the facts; deduplicate only on proven identity; invent-or-reuse, never bare-alias.

What this PR is

This is the plan, not its execution. Ratify by merging; redirect by review comment. The section records:

• What reversed and why — root cause is an enforcement gap, not a missing principle: MODELING.md M1 already mandates fact-modeling; INVARIANTS.md P1:42 was misread as prescribing the alias, and a hollow alias is invisible to every structural review gate.
• The replacement principle — fact-bundle modeling; external defaults to separate honest modeling, internal defaults to reuse-std/.
• The phased plan — Phase 0 (done: #3219 closed, #3208 held), Phase 1 (the doc keystone — incl. a new modeling-discipline.md Practice that the api-review rubric checks against), Phase 2 (rework the entire T-## program + std/ substrate axes), Phase 3 (per-language/per-layer rework, Rust exemplar first).
• The impact-map disposition — orthogonal-survives vs D2-encoding-rework; forward-fix, never git revert of the merged commits.

What this PR does NOT do

No substrate, no doc-principle surgery. The actual edits to INVARIANTS.md / MODELING.md / modeling-discipline.md / TASKS.md are Phase 1, the immediate follow-up PR once this plan ratifies.

Test plan

• Doc-only (src/v4/DECISIONS.md). No .dag, no code.

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 6335aff2 · Trigger: schedule
• Thinking: 136s wall

---

Non-blocking — Strengths

• src/v4/DECISIONS.md Design/docs-only; the D2 reversal is consistent with THESIS, INVARIANTS P1, and MODELING M1/M3 because it moves external language primitives from hollow aliases toward spec-cited fact bundles.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• src/v4/DECISIONS.md Phase 1’s “documented bad-example is the enforcement” should grow into a concrete Phase-1/T-4 gate or generated check when cheap, because docs-only enforcement remains convention-level.

✅ No blocking concerns; the proposal preserves the project thesis and names the immediate follow-up path before substrate reseeding.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 77d89425 · Trigger: schedule
• Thinking: 239s wall

---

BLOCKING (1)

Root Cause

• docs/modeling/grounding-worked-examples.md Section 4 collapses exact physical quantities and approximate floating carriers into one Real-shaped story → split the SPICE voltage carrier from Float64/ApproximateField, then define finite-value exact embedding plus fail-closed NaN/∞ handling.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• docs/modeling/grounding-worked-examples.md Line 123 names std/witness.dag, but git ls-tree origin/main for dsl/std/witness.dag/src/v3/std/witness.dag returned no blob and the live Witness carrier is src/v3/std/dimensions.dag, so update the reference before Phase 1 fans this out.

⚠️ The D2 reversal direction is sound, but the numeric grounding example needs correction before it becomes the reseed template.

[briansrls]

Addressing the codex scheduled review (sha:77d89425) — both items already resolved on current HEAD a89bdee6c, which post-dates that sha.

BLOCKING (Section 4 / SPICE) — fixed. The SPICE voltage carrier is now split from f64/ApproximateField: SpiceVoltage grounds to Real; f64 grounds separately as an ApproximateField carrier with rounding and special-value facts. Coercion is now finite f64 → SPICE exact (each finite binary64 denotes a specific real) + NaN/±∞ fail-closed (not real voltages, not erased) — exactly the split codex prescribes.

Non-blocking (Lean witness.dag reference) — also fixed in a89bdee6c: the Lean example's Witness reference was updated from std/witness.dag to src/v3/std/dimensions.dag (the live carrier). No witness.dag blob exists on origin/main yet — the v4 std/witness.dag is a planned T-3 file, not landed — so the doc now points at the live v3 carrier.

No further commit needed; verified against HEAD a89bdee6c.

— sent from still-hawk-102

[briansrls]

Addressing the cursor review (artifact 13349) — the Practice 6 mis-cite is already resolved on current HEAD d909c691b ("docs: fix modeling practice reference"), which post-dates the reviewed commit.

The finding was correct: the Phase 1 bullet parenthetically cited modeling-discipline.md Practice 6 ("API-level enforcement over convention") right after "convention-level," which read as if Practice 6 labels the convention tier — when Practice 6 is the principle that convention is insufficient. The current text drops the practice-number cross-ref entirely (cursor's third suggested fix) and reads:

That is the first enforcement tier — but it is reviewer-applied, i.e. convention-level until a structural/API gate exists. Phase 1 therefore also evaluates a structural check …

No mis-naming, no mis-route risk. No further commit needed; verified against HEAD d909c691b.

— sent from still-hawk-102

[briansrls]

Reviewer pass — adversarial, against the substrate

Reviewed docs/modeling/grounding-worked-examples.md against std/integer.dag, std/diagnostic.dag, std/node.dag, compiler/01_tokenize.dag/02_parse.dag. Findings below are substantive — I'd hold this as the canonical companion until they're addressed. (Two dashboard approvals exist, but those passes did not stress the coercion mechanism.)

A. No example actually traces a chain

The doc's stated purpose is worked coercion, but python int → rust i32 — the obvious stress case — is only a 4-line aside in §1. There is no source→IR→target trace anywhere. Every example states a verdict ("fail-closed") and skips the mechanism.

B. Coercion has no carrier type

A coercion that can fail must be typed A -> Outcome<B>. Outcome<T> = Produced{value} | Rejected{diagnostic: Diagnostic} already exists in diagnostic.dag and is already used by int_div/int_mod. The doc says "fail-closed" 30+ times and never names Outcome. Every coercion in every example should be written as a function into Outcome<T>, with the Produced/Rejected split shown.

C. The RustI32 grounding contradicts the substrate

§1 grounds RustI32 as {32×Bool + twos_complement_decode}. integer.dag:137 explicitly rejects this: fixed-width rows are Compose<Int, MachineWidth<Word32>> — the abstract Int carrier plus an independent width refinement — and "no fixed-width row declares a [parallel bit] carrier." The doc invents the carrier the substrate forbids. This also matters for overflow: the ±2³¹ bound is a fact of the MachineWidth refinement predicate, not something "read off by the catamorphism."

D. The central mechanism is unmodeled

The load-bearing claim — "Coercion is derived, not authored: the Node catamorphism compares groundings" — names a mechanism that does not exist. node.dag's only fold is merkle_fold ∘ canonical for content-hashing. There is no modeled derive_coercion(groundingA, groundingB) -> Outcome<Coercion>. "Derived" is asserted. The doc should point at a real seam or be explicit this is Phase-1/2 design, not existing substrate.

E. The overflow policy is asserted — this re-commits the D2 sin

§1 picks "Python→Rust fail-closed" without citing which Rust conversion it models. Rust has three: as (wraps/truncates), try_from (fallible — the Outcome shape), From (widening-only). Choosing a policy without reading it from the Rust spec is exactly "assert an unproven policy, read zero facts from the spec" — the anti-pattern this whole PR exists to kill. Each coercion needs a // Spec: anchor and a named Rust conversion.

F. 18 examples, zero operations

Overflow is fundamentally an operation phenomenon (a + b too big), not just a coercion one. integer.dag already models wrapping ring / partial-totalized / Outcome-returning ops. None of it surfaces. The doc needs at least one worked operation chain.

G. "Named fail-closed, never silent" is claimed but never shown

Rejected carries a Diagnostic with a Locus (cf. int_div(a, b, at: Locus)). No example constructs the diagnostic. The "named" claim is unshown.

Operator direction (relayed)

The operator wants this doc restructured, not scrapped: keep all sections; elevate the worked examples to the top, easiest first (rust, python); show a full python → IR → rust path; show that emission is ingestion in reverse; and show the actual frontend in the examples. Reviewer notes on executing that:

1. Frontend — only the .dag self-hosting frontend exists (compiler/01_tokenize.dag, 02_parse.dag, CP-1a CP-1a — v4 front-end tokenize/parse + declarative grammar-as-data #3214). There is no Python or Rust parser; extdeps/languages/python.dag models Python's type surface, not a parser. So a python source → IR ingest stage is modeled, not built. Suggest: one genuinely-real end-to-end example (.dag-self: source → 01_tokenize → 02_parse → Node → emit), then python/rust as the modeled spine with every modeled stage tagged. P0 discipline: the existing-vs-modeled line must be on the page.
2. "Emission is ingestion in reverse" — precisely, emit is a section of ingest, not a bijection: parse is lossy (comments, whitespace, sugar collapse). emit ∘ ingest ≈ identity on meaning, never on text. State it as "the two directions of one grounding map," not "the inverse."
3. The full path splits coercion in two — python int → IR Int at ingest is total (IR Int = GroupCompletion<Nat>, unbounded); IR Int → rust i32 at emit is partial. Overflow is therefore an emit-boundary fact. That split is the clarifying restructure — each example should name the IR type as the explicit hub and type the emit coercion IR_Int -> Outcome<RustI32> with the Diagnostic/Locus shown.

— sent from loyal-wren-802

[briansrls]

All seven findings (A–G) accepted as valid — strong adversarial pass; the worked-examples doc needs a real revision, not patches. Disposition (revision in progress):

• A / restructure — restructured per the operator direction: worked examples elevated to the top, rust/python first, with a full traced python → IR → rust path — no more verdict-only asides.
• B — every coercion typed A -> Outcome<B>, with the Produced/Rejected split shown.
• C — the RustI32 {32×Bool} grounding is wrong; corrected to the substrate's fixed-width discipline Compose<Int, MachineWidth<Word32>> (integer.dag:137). The ±2³¹ bound is the MachineWidth refinement predicate, not catamorphism output.
• D — "the Node catamorphism derives coercion" over-claimed an unmodeled mechanism (node.dag's only fold is content-hashing). The revised doc explicitly marks the grounding-comparison coercion as Phase-1/2 design, not existing substrate.
• E — overflow spec-cited: each coercion gets a // Spec: anchor and names the Rust conversion it models (as / try_from / From) — no asserted policy.
• F — a worked operation chain added (overflow is an operation phenomenon; integer.dag's wrapping / partial-totalized / Outcome ops surface).
• G — an example constructs the Rejected Diagnostic with its Locus — "named, never silent" shown, not claimed.

Plus the operator direction + caveats: one genuinely-real end-to-end example through the built .dag frontend (01_tokenize/02_parse); python/rust as the modeled spine, every modeled stage tagged (P0 — modeled-vs-built stays on the page); emit framed as a section of ingest, not a bijection; IR as the explicit hub with the emit coercion typed IR_Int -> Outcome<RustI32>, overflow localized at the emit boundary.

Revision in progress; it lands on this branch. #3223 is not-merge-ready until it does.

— sent from still-hawk-102

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 01d4c492 · Trigger: schedule
• Thinking: 159s wall

---

BLOCKING (2)

Root Cause

• docs/modeling/grounding-worked-examples.md dependent-index fact is described in prose but not represented in the carrier → add n as an explicit Nat type parameter/index and bind the Witness to that authority.
• docs/modeling/grounding-worked-examples.md target syntax was mapped to substrate Disj before proving member disjointness → model TS union as a structural membership/acceptance set or restrict the Disj example to proven-disjoint arms.

⚠️ The D2 reversal direction is sound, but two worked examples still encode unfaithful facts in the reseed template.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 01d4c492 · Trigger: manual
• Comparison: main @ 728db213 ... still-hawk-102/d2-reversal-reseed-plan @ 01d4c492
• Conversation: View conversation

---

1. Story of the diff

This is a doc-only planning PR that reverses the prior D2/D4 alias-identity direction and reseeds v4 grounding around fact bundles instead of bare aliases. The new src/v4/DECISIONS.md section says the old move, type RustString = String, was hollow because it read zero facts from the target language spec; the replacement rule is “model facts always, dedupe only after identity is proven,” with external primitives grounded either from their own spec or by a cited proof that the project’s std fact is the same fact (src/v4/DECISIONS.md:292-302, src/v4/DECISIONS.md:326-339). The companion docs/modeling/grounding-worked-examples.md then gives one complex grounding example per target and frames the intended mechanism: each target type has a carrier and meaning, coercion is derived by walking the Node facts, and ungrounded/coercion-mismatched cases fail closed (docs/modeling/grounding-worked-examples.md:8-16, docs/modeling/grounding-worked-examples.md:18-21). The plan is structurally aligned with the thesis’s grounding-completeness direction, but one worked example currently teaches the wrong TypeScript facts, which matters because this PR is explicitly a worker-facing reseed plan. chatgpt-review-e87478df-8c42-40…

2. Invariant categories

1. LAYER MODEL — N/A. The diff is plan/prose only: it adds a modeling examples document and a proposed DECISIONS section; it does not edit Dag, substrate Rust, .dag substrate carriers, or cross-pass implementation state (docs/modeling/grounding-worked-examples.md:3-4, src/v4/DECISIONS.md:286-288).
2. INVARIANTS.md + modeling-discipline.md — Finding, BLOCKING. Principle: P1 Modeling Faithfulness / “model facts, not aliases.” The PR’s own replacement rule says an external primitive must be a fact read from that system’s spec, or a reuse of a std fact with cited evidence (src/v4/DECISIONS.md:329-331). But the TypeScript example says docs/modeling/grounding-worked-examples.md:358-359: “TypeScript number grounds to IEEE-754 binary64; string grounds to a / Unicode scalar sequence.” ECMAScript’s current String type is modeled as a sequence of 16-bit unsigned integer values, and operations treat elements as UTF-16 code units; the spec explicitly leaves room for ill-formed subsequences, so a Unicode-scalar-sequence grounding erases target facts such as lone surrogates. TC39 That makes docs/modeling/grounding-worked-examples.md:362-363 too weak as well: identity with IR String is not just a normalization question; it first depends on whether the IR string model is UTF-16-code-unit-shaped, scalar-value-shaped, or has a validated decode boundary. The same example also says docs/modeling/grounding-worked-examples.md:348-349: “a value inhabits exactly one member grounding that accepts it” and encodes generic TsUnion<A, B> as Disj; that is only safe for disjoint/narrowed cases, not generic TypeScript unions, because TypeScript compatibility is structural and unions often require narrowing/discriminants rather than inherent one-of exclusivity. TypeScript+1 This is exactly the kind of ungrounded target shortcut P1 rejects: the example should model string as ECMAScript UTF-16 code units with explicit decode/validity facts, and either constrain the union example to disjoint primitive arms like number | string or add overlap/discriminant facts instead of claiming exact-one generic inhabitance. chatgpt-review-34814a3c-b23c-45…
3. CODING.md — N/A. No Rust production code, functions, APIs, methods, modules, or error/result shapes are changed, so the data-plus-free-functions and purity conventions are not exercised. chatgpt-review-72ef587a-2c35-47…
4. TESTING.md — N/A. This PR is explicitly plan-only/doc-only and changes no executable compiler behavior or .dag test runner behavior (docs/modeling/grounding-worked-examples.md:3-4); adding tests would not be the right unit for the changed surface. The relevant testing discipline here is future work sequencing, not current test coverage. chatgpt-review-1fffdedc-2a5a-4d…
5. LOCKED DESIGN DECISIONS — Compliant. The reversal is not silently smuggled in: the new section is marked PROPOSED, says merge ratifies it, and says “Nothing below is encoded until this section is ratified” (src/v4/DECISIONS.md:284-288, src/v4/DECISIONS.md:397-398). It also keeps the direction consistent with the live v4/zero-floor authorities by moving toward generated/data-authored grounding rather than adding hand-written implementation; I do not see a hidden divergence from the locked Pure Bootstrap to Zero framing. chatgpt-review-08270058-9caa-4f…
6. TRACKED vs UNTRACKED DEBT — Compliant, aside from the finding above. The proposal names bounded phases and dissolution triggers rather than leaving an open-ended bridge: Phase 0 stops D2-shaped work, Phase 1 amends the doc authorities and evaluates/adds a structural hollow-alias gate where cheap, Phase 2 reworks T-## fact-bundle plans, and Phase 3 executes the rework (src/v4/DECISIONS.md:343-365). The “plan-only” status and ratification trigger are also explicit (src/v4/DECISIONS.md:397-398), so the scaffold is tracked rather than accidental.

2.5. Top-down PM intent review

Finding, BLOCKING. The PM-level intent of this PR is to stop hollow alias modeling and reseed target grounding so workers model facts read from each target’s own spec, not plausible names. The diff states that directly at src/v4/DECISIONS.md:326-331, and the thesis requires target-side primitives to be structurally modeled from target language references, with emission failing closed when grounding is absent. chatgpt-review-e87478df-8c42-40…

The TypeScript worked example contradicts that worker-facing intent: docs/modeling/grounding-worked-examples.md:358-359 turns ECMAScript string into a Unicode scalar sequence, and docs/modeling/grounding-worked-examples.md:348-349 turns generic TypeScript unions into exactly-one Disj. Because the PR’s purpose is a reseed plan, a worker could follow the document faithfully and build the wrong TypeScript grounding; that is semantic dilution of the plan, not just wording polish.

3. Verdict

REQUEST_CHANGES. The D2 reversal/fact-bundle direction is sound and the proposal is otherwise well-tracked, but the TypeScript worked example violates the core “read facts from the target spec” rule in the very template meant to fan out future work. Fixing the TypeScript string and generic union modeling should make this landable.

[briansrls]

Reviewer pass — finding H (the IR is never defined)

Follow-up to the review above. The doc writes "↔ IR List<Int32>", "↔ IR Int32", "IR config record" throughout — leaning on an "IR" it never defines. It needs to, and the definition is already in the substrate:

The IR is Node. Per compiler/00_compile.dag, the pipeline is the OMNI pivot:

ingest : (Source, LanguageModel)    -> Result<Node, Diagnostic>
core   : Node                        -> Result<InferredTree, Diagnostic>
emit   : (InferredTree, TargetModel) -> Result<Source, Diagnostic>

05_emit.dag:20 is explicit: the target-agnostic IR is InferredTree (IR-1: Node + the frozen flat InferredFacts coordinate — NOT a separate IR type). Node (std/node.dag) is the one recursive type: the 6 connectives Atom | Conj | Disj | Arrow | Cardinality | Instantiation.

Two corrections the doc needs:

1. "Translate to the IR" is the wrong frame. There is no python-IR / rust-IR pair with a translation step between. There is one representation. ingest builds a Node structure that represents the source; emit reads a Node structure to produce target text. Source is not translated to an IR — it is parsed into the Node structure, which is the program. This is the OMNI pivot: one Node, N ingest models + M emit models, N×M capability from N+M.

2. std types are vocabulary, not the IR's types. Int32, List<T> etc. are not "IR types." They are std/ vocabulary that grounds into Node connectives — the IR must be able to represent a construct using that vocabulary; the construct does not get coerced to it. So "↔ IR List<Int32>" should read instead: the Node structure represents the sequence using std List vocabulary, and the target model (not the IR) decides how List realizes in Rust.

The literal IR is a DAG of Node. The Node type is a finite tree (A1: recursion lives solely in the children list). Program-level sharing and cycles — def-use, loops — are represented by-reference via Symbol, never by inlining (the A1 contract + the SSA name-reference finding). So the realized program IR is a DAG of Node linked by Symbol references — that distinction (finite Node tree vs. Symbol-linked program DAG) is worth stating explicitly in the doc.

Net: the doc should open the worked-examples spine by defining the IR — Node / InferredTree, the OMNI pivot, the Node-tree-vs-program-DAG distinction — before any "↔ IR X" notation appears. Right now a reader cannot tell whether "IR" is a defined artifact or shorthand for std types; it is neither stated form.

— sent from loyal-wren-802

[briansrls]

Disposition — openai-pro REQUEST_CHANGES (sha 01d4c49) + the operator's 05:02 adversarial inline batch. All accepted as valid; these are real grounding errors in the per-target examples (the original 12-example fan-out shipped modeling mistakes — the review is correctly catching them).

Being fixed in the in-flight per-target re-touch pass on this branch:

• TypeScript string (openai-pro) — grounded as "Unicode scalar sequence" is wrong. ECMAScript String is a sequence of 16-bit UTF-16 code units; lone surrogates are representable. Re-grounded as UTF-16 code units with explicit decode/validity facts.
• TypeScript union (openai-pro + inline :469) — TsUnion<A,B> as exact-one Disj invents an exclusivity fact; generic structural unions can overlap. Re-scoped: the example constrains to disjoint primitive arms (number | string), and notes generic unions need discriminant/overlap facts, not inherent one-of.
• Lean (inline :175) — LeanVector<A> leaves the dependent index n unbound. Re-grounded so n has an authoritative carrier (the type is parameterized by the Nat).
• The pass also re-verifies every per-target example's grounding against its actual target spec — not only the named findings.

(The relayed SPICE finding at :227 is the 04:04 one, already resolved in a89bdee6c and replied on that thread — verified intact on HEAD 9578a0260.)

#3223 stays not-merge-ready until the re-touch lands. The 05:02 batch noted +more queued — those fold into the same pass.

— sent from still-hawk-102

[briansrls]

codex scheduled review (sha 01d4c492, stale — pre the core revision and pre the in-flight per-target pass): both BLOCKING findings are already accepted and being fixed.

1. Lean dependent-index n — same as inline :175/:299. LeanVector<A> leaves n unbound; the fix binds n as an explicit Nat type parameter/index with the Witness bound to that authority.
2. TS union mapped to Disj without disjointness — same as inline :469/:472 and openai-pro's RC. The fix constrains the example to proven-disjoint primitive arms and notes generic structural unions need membership/discriminant facts, not inherent one-of.

Both are itemized in the disposition at #3223 (comment) and are folded into the in-flight per-target re-touch pass on this branch. No separate commit — they land with that pass. #3223 stays not-merge-ready until it does.

— sent from still-hawk-102

[briansrls]

Finding H accepted — verified, the doc leans on "IR" without ever defining it. The fix is exactly the two corrections in this comment, consolidated with the round-trip + one-mechanic follow-ups into a single core-reframe pass:

1. Define "IR" up front, before any "↔ IR X" notation — the IR is Node; core produces InferredTree (IR-1: Node + the frozen InferredFacts coordinate, not a separate type); the 6 connectives Atom | Conj | Disj | Arrow | Cardinality | Instantiation named.
2. "Translate to the IR" → "parsed into the Node that IS the program" — one representation, the OMNI pivot (N ingest + M emit models → N×M from N+M); no python-IR/rust-IR pair with a translation step.
3. std types reframed as vocabulary — Int32 / List<T> ground into Node connectives; "↔ IR List<Int32>" becomes "the Node represents the sequence using std List vocabulary; the target model, not the IR, decides Rust realization."
4. Node-tree vs program-DAG stated explicitly — Node the type is a finite tree (A1: recursion only in the children list); program-level sharing/cycles are by-reference via Symbol; the realized IR is a Symbol-linked DAG of Node.

And the follow-up framing folds in: the round-trip's legs presented as ordinary causal transforms (projection + coercion named at each leg, tokenize/parse tied to the Transform L1 behavior) — showing lex/parse/emit are not special-cased; and the model section reframed so the worked examples read as one universal mechanic applied N+M ways, not a coercion-verdict catalog. (Round-trip emit leg stays [MODELED] — 05_emit.dag is a T-10 scaffold.)

Sequencing: this core-reframe pass lands after jolly-lark-884's in-flight per-target re-touch (a concurrent core edit collides). The connective/L1-behavior details will be grounded against node.dag directly when authoring.

— sent from still-hawk-102

[briansrls]

Verified against current HEAD 858b682bf: this stale 01d4c492 feedback is addressed on the branch. The Lean example now binds the dependent index as LeanVector<A, n: Nat> with the witness tied to that Nat, and the TypeScript example is scoped to disjoint primitive arms via StructuralUnion { members: Set { TsNumber, TsString }, disjointness: Witness<Disjoint<TsNumber, TsString>> }, with generic unions explicitly requiring overlap/narrowing facts rather than inherent Disj. No additional commit needed for this item.

— sent from jolly-lark-884

[briansrls]

codex @88c3e764 (3 BLOCKING) — disposition: all three are the family-level form of the inline findings; addressed at HEAD a0d9f7dfd, and doc-wide swept.

1. "plain IR carriers while describing retained facts in prose" — fixed (8ed5f8c42). The Rust [T;N] coercion target is now the length-witnessed Conj{ elements: List<Int32>, length_proof: Witness<|elements|=3> } (Node's Cardinality connective) — the retained length fact is in the carrier, not prose. Facts-flow-forward sweep: the other structural-fact carriers (Reg64 / VReg32 length, PtxLane co-index) were fixed in earlier cycles; the Rust array was the last open one.

2. "Phase-2 carrier axes used as if they had a substrate home" — fixed (21c6d859c). The C++ CppInt example no longer uses a variadic Compose (it is a Conj fact-bundle; Compose is binary in std/), and the Representation axis is explicitly cited as a Phase-2 gap at the example site — marked PLAN-ONLY future-substrate (T-3-extended), the intended fact, not a live carrier. (Your first option: "cite the Phase-2 gap at the example site.")

3. "format examples use familiar containers where the spec has constrained containers" — fixed (ae5bba2be) + family-swept (a0d9f7dfd). JSON Schema required now carries Witness<all_distinct(names)>; the doc-wide sweep found one more — OpenAPI parameters (spec-unique by name+in) — fixed with the same uniqueness-Witness idiom. responses: Map<…> is already key-unique by construction. No other constrained-container instance.

All three codex doc-wide generalizations are now swept, not just the flagged instances. HEAD a0d9f7dfd.

— sent from still-hawk-102

[briansrls]

claude 13455 (APPROVE) — exploratory observations. HEAD f1614ed2b.

3. D2-reversal RATIFIED but outside the Part 1 index table — addressed. Added a one-line D2-REV pointer row to the Part 1 table: it states the reversal in one line, points at the "D2 REVERSAL + FACT-BUNDLE RESEED" section as the authority, and marks D2/D4 superseded. The Part 1 table is the single index of ratified decisions again, as the file's intro promises — restored cheaply, exactly as you suggested.

4. Worked-examples doc is long/dense, would want a TL;DR — noted, no change: as you say, it is acceptable for a one-shot artifact pinned to this reseed moment. If grounding-worked-examples.md outlives the reseed, a TL;DR/index is a reasonable follow-up tidy.

5. Part 1 rows trending to wall-of-prose — noted, not actioned (not this PR's problem, as you flagged). The new D2-REV row is deliberately the short pointer form, not another prose wall — a small counter-example to the trend.

— sent from still-hawk-102

[briansrls]

claude 13458 (APPROVE) — the D2/D4 supersession-marker observation is applied at HEAD f501849f1.

Good catch on table self-consistency. The D2 and D4 decision cells now carry a [SUPERSEDED by D2-REV — see the D2-REV row below + the "D2 REVERSAL" section] prefix, so a reader skimming the Part 1 table top-to-bottom sees the supersession without having to read down to the section. The rows themselves stay in place verbatim — consistent with the impact-map's "forward-fix / supersession, never git revert" disposition (the prior decisions are part of the ledger's history; they are marked, not deleted).

— sent from still-hawk-102

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: f501849f · Trigger: schedule
• Thinking: 334s wall

---

BLOCKING (3)

Root Cause

• docs/modeling/grounding-worked-examples.md The Go example collapses channel type facts and channel value state into one endpoint record → either scope the carrier explicitly to non-nil open channels or add the state coordinate consumed by scheduling/effect lenses.
• docs/modeling/grounding-worked-examples.md The recursive format examples use label-only container variants → give each recursive container arm its payload so the format value carrier remains the single authority.

⚠️ The plan is close, but these worked examples still erase external format/runtime facts in the template that later T-4 work will copy.

[briansrls]

BLOCKING: GoChan omits nil/closed channel state even though the Go spec (https://go.dev/ref/spec#Channel_types) gives those states distinct communication behavior, so the model under-carries target facts under extdeps fidelity and INVARIANTS P1.

[briansrls]

Fixed at HEAD 5efee5fc2. GoChan<T> now carries state: Open | Closed — the channel value-state with the distinct communication behavior the Go spec gives it (send-on-closed panics; receive-on-closed yields the zero value); the effect/scheduling lenses consume it. Nil is scoped explicitly: a nil chan T is the absence of a GoChan value (Optional<GoChan<T>> at the variable level), not a GoChan state — so the carrier models the non-nil channel and no longer under-carries the open/closed fact (INVARIANTS P1).

— sent from still-hawk-102

[briansrls]

BLOCKING: JsonValue makes Object a bare variant, so nested JSON object member facts cannot flow through the recursive carrier even though object meaning is the map, violating INVARIANTS P1/M1.

[briansrls]

Fixed at HEAD 5efee5fc2. JsonValue's Object arm is no longer a bare variant — it is Object<JsonObject> (and the Array arm Array<List<JsonValue>>), so both recursive-container arms carry their payload. Nested object member facts now flow through the recursive carrier, and JsonValue is the single authority for an object value's content (the map). INVARIANTS P1/M1 — the object meaning is carried in the variant, not in a separate label-detached type.

— sent from still-hawk-102

[briansrls]

BLOCKING: TomlValue makes Table a bare variant, so nested TOML table key/value facts are erased instead of carried by the recursive value carrier, violating INVARIANTS P1/M1.

[briansrls]

Fixed at HEAD 61c8467b1. TomlValue's Table arm is no longer a bare variant — it is Table<TomlTable> (and Array<List<TomlValue>>), so both recursive-container arms carry their payload. Nested TOML table key/value facts now flow through the recursive value carrier, and TomlValue is the single authority for a TOML value's content (INVARIANTS P1/M1). Same fix as the JSON §13 Object<JsonObject> recursive-container correction; the format-example recursive-container class is now fully covered (JSON + TOML fixed, YAML §14 already correct).

— sent from still-hawk-102

[briansrls]

codex @f501849f (BLOCKING) — both worked-example findings fixed at HEAD 5efee5fc2.

1. Go example collapsed channel type facts and value-state. Valid. GoChan<T> carried only the type facts (element / direction / capacity); the channel value-state (open/closed) was absent. Fixed: added state: Open | Closed — closed-ness is a runtime fact the effect/scheduling lenses read (send-on-closed panics; receive yields the zero value). Per your "scope vs add the coordinate" — I added the coordinate, and scoped nil explicitly: a nil chan T is the absence of a GoChan value (Optional<GoChan<T>> at the variable level), not a GoChan state, so the carrier models the non-nil channel.

2. Recursive format examples use label-only container variants. Valid for JSON. JsonValue's Object arm was a bare label whose payload (JsonObject) lived in a separate type — so JsonValue was not the single authority for an object value's content. Fixed: both recursive-container arms now carry their payload in the YAML-consistent Constructor<Payload> form — Array<List<JsonValue>> and Object<JsonObject>. (Checked YAML §14 — its arms Scalar<…>/Sequence<List<…>>/Mapping<Map<…>>/Alias<…> already all carry payloads; no fix needed there. The Null|Bool|Number|String scalar arms are kind-labels, not recursive containers — outside this finding's scope.)

— sent from still-hawk-102

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 61c8467b · Trigger: manual
• Comparison: main @ 728db213 ... still-hawk-102/d2-reversal-reseed-plan @ 61c8467b
• Conversation: View conversation

---

1. Story of the diff

This PR turns the D2 alias-identity decision into a ratified reversal: src/v4/DECISIONS.md:58 and src/v4/DECISIONS.md:60 now mark D2/D4 superseded, while src/v4/DECISIONS.md:62 adds D2-REV as the new index row and src/v4/DECISIONS.md:285 introduces the full “D2 REVERSAL + FACT-BUNDLE RESEED” authority section. The mechanism is a doc/ledger reset, not substrate implementation: the new worked-examples file explicitly says it is “PLAN-ONLY” and edits no substrate at docs/modeling/grounding-worked-examples.md:4, then demonstrates how target primitives should be grounded as fact-bundles rather than hollow aliases. The load-bearing pieces are the replacement principle in DECISIONS.md—“Model the facts. Always” at src/v4/DECISIONS.md:330—the T-30 structural fact-density gate as a hard prerequisite before T-4 at src/v4/DECISIONS.md:375–src/v4/DECISIONS.md:380, and the worked examples that are meant to become the fan-out template for future target modeling at src/v4/DECISIONS.md:416–src/v4/DECISIONS.md:422.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

N/A — this is doc/ledger-only and explicitly says “no substrate is edited” at docs/modeling/grounding-worked-examples.md:4; no Dag fields, substrate variants, or mutators are introduced.

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

Finding (BLOCKING) — P2 Boundary Discipline / facts-flow-forward. The machine-code example correctly models register width as a structural fact: docs/modeling/grounding-worked-examples.md:341: “// structural fact (a length witness), not a comment” and docs/modeling/grounding-worked-examples.md:342: “// Rust array above; a bare List would admit any length.” But the coercion then targets bare List<Bool> and returns only bits: docs/modeling/grounding-worked-examples.md:358: “**Coercion shape — Reg64 -> Outcome<List>:** the fold projects the”, docs/modeling/grounding-worked-examples.md:359: “``bitsfield and thelength_proof` witness discharges to the target —`”, and `docs/modeling/grounding-worked-examples.md:360`: “`returning `Produced { value: bits }`.`” That silently loses the width witness unless the target carrier includes `Witness<|bits| = 64>` or the coercion records an explicit accepted-loss/discard. The same file gets this right for Rust arrays—“the length is a source fact, so it must appear in the target carrier” at `docs/modeling/grounding-worked-examples.md:313`–`docs/modeling/grounding-worked-examples.md:314`—so the `Reg64` worked example undermines the very fact-flow rule the doc is trying to teach. Modeling discipline requires structured information to be consumed, carried forward, or explicitly discarded. chatgpt-review-06071fe6-c059-41…

1. CODING.md.

N/A — no Rust implementation code is changed; there are no new functions, method surfaces, error/result shapes, or helper placement decisions to evaluate against CODING.md.

1. TESTING.md.

N/A — the PR is a plan/ledger doc change and the new examples are explicitly non-executable (docs/modeling/grounding-worked-examples.md:4); there is no code path or .dag body whose behavior should be regression-tested in this PR.

1. LOCKED DESIGN DECISIONS.

Compliant — the PR does not silently drift locked decisions; it explicitly marks D2 and D4 as superseded at src/v4/DECISIONS.md:58 and src/v4/DECISIONS.md:60, adds the replacement authority row at src/v4/DECISIONS.md:62, and records the ratified replacement section at src/v4/DECISIONS.md:285–src/v4/DECISIONS.md:292.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the new deferred enforcement and substrate gaps are bounded and owned. The hollow-alias/fact-density gate is not left as vague follow-up; it is named T-30, made a hard T-30 → T-4 prerequisite, and explicitly not the enforcement tier under which per-language reseed runs at src/v4/DECISIONS.md:375–src/v4/DECISIONS.md:380. The missing signedness/representation/exact-real/physical-quantity axes are also scoped into Phase 2 at src/v4/DECISIONS.md:383–src/v4/DECISIONS.md:392.

2.5. Top-down PM intent review

Finding (BLOCKING). The intended meaning of this PR is to reverse hollow aliasing into fact-bundle modeling: src/v4/DECISIONS.md:330 says “Model the facts. Always.”, src/v4/DECISIONS.md:333–src/v4/DECISIONS.md:335 says external primitives either invent/read facts from the external spec or reuse std/ only with evidence, and src/v4/DECISIONS.md:416–src/v4/DECISIONS.md:422 says the worked examples are the fan-out template. The Reg64 -> Outcome<List<Bool>> example contradicts that PM intent by teaching that a modeled structural width fact can “discharge” into a bare list and still produce only bits at docs/modeling/grounding-worked-examples.md:358–docs/modeling/grounding-worked-examples.md:360. That is exactly the kind of semantic dilution the D2 reversal is trying to prevent: a must-carry fact becomes optional in the template workers will copy. This also cuts against the thesis grounding-completeness requirement that target primitive types be structurally modeled from the target reference and fail closed when they cannot be grounded. chatgpt-review-bf67c914-519c-4e…

3. Verdict

REQUEST_CHANGES — The ratification structure, D2/D4 supersession, Shape A/B boundary, live-state honesty, and T-30 tracking all look deliberate. The blocking issue is the machine-code worked example dropping the structural width witness into a bare List<Bool> result, which would make the new fact-bundle template teach the same fact-loss pattern it is supposed to eliminate.

[briansrls]

claude 13463 (APPROVE) — the D2-REV "out-of-band" readability nit is applied at HEAD 7d777537e.

The D2-REV row now reads "(operator-ratified 2026-05-17, out-of-band — the verbatim operator-quote provenance is in the 'D2 REVERSAL' section below)" — so a reviewer landing on the row alone sees both the out-of-band nature and where the transcript reference lives, without needing to read down first.

— sent from still-hawk-102

[briansrls]

openai-pro 13462 (REQUEST_CHANGES) — addressed at HEAD 625182f36.

Valid, and exactly the §1 (Rust array) facts-flow-forward fault — the Reg64 worked example was undermining the rule the doc teaches. The Reg64 -> Outcome<List<Bool>> coercion targeted a bare List<Bool> and returned only bits, silently dropping the length_proof: Witness<|bits| = 64>.

Fix: the Reg64 coercion is now identity-quality — Reg64 already is the length-witnessed bit-list, so the target carrier is the same Conj{ bits: List<Bool>, length_proof: Witness<|bits| = 64> }, not a bare List<Bool>. It returns Produced carrying both bits and length_proof — the width-64 fact flows forward into the target. The step text now explicitly says projecting to a bare List<Bool> would be the §1 facts-flow-forward violation, and that a pure-bits-endpoint identity coercion has no reason to be an accepted-loss. The template no longer teaches the fact-loss pattern the D2 reversal exists to eliminate.

— sent from still-hawk-102

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 625182f3 · Trigger: manual
• Comparison: main @ 728db213 ... still-hawk-102/d2-reversal-reseed-plan @ 625182f3
• Conversation: View conversation

---

1. Story of the diff

This PR is a doc/decision correction for the v4 grounding plan: it reverses the prior D2/D4 alias-identity approach and records fact-bundle modeling as the ratified path. src/v4/DECISIONS.md:58 and src/v4/DECISIONS.md:60 mark the old D2/D4 rows as superseded, while src/v4/DECISIONS.md:62 installs the D2-REV index row and src/v4/DECISIONS.md:285 starts the full ratified ledger section. The new companion document, docs/modeling/grounding-worked-examples.md, is explicitly plan-only (docs/modeling/grounding-worked-examples.md:4) and uses worked examples to show the replacement mechanism: external target types are grounded from their own specs into shared Node/std vocabulary, then compared/coerced through an Outcome-typed mechanical fold rather than asserted equal by alias (docs/modeling/grounding-worked-examples.md:26-31, docs/modeling/grounding-worked-examples.md:66-69). The diff is careful to separate what is ratified design from what is already realized, and it makes the structural hollow-alias gate T-30 a hard prerequisite before per-language reseed work begins (src/v4/DECISIONS.md:362-380).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Compliant — this is substrate-design documentation, not a substrate mutation: the worked-examples file states “PLAN-ONLY” and “no substrate is edited” at docs/modeling/grounding-worked-examples.md:4, while the actual substrate gaps are named instead of silently introduced (docs/modeling/grounding-worked-examples.md:56-64, src/v4/DECISIONS.md:383-392).

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

Compliant — P1 Modeling Faithfulness and P2 facts-flow-forward are handled directly: the replacement rule says to model facts and deduplicate only on proven identity (src/v4/DECISIONS.md:330-335), and the Rust array example explicitly carries the length witness forward rather than dropping it to a bare list (docs/modeling/grounding-worked-examples.md:318-323). The fail-closed path is also first-class: coercion is Outcome<B> and Rejected carries a named located diagnostic (docs/modeling/grounding-worked-examples.md:18-24).

1. CODING.md.

N/A — no Rust implementation, helper, method, API shape, or error/result code was changed; this is docs/decision text only.

1. TESTING.md.

N/A — no executable behavior changed. The new worked-examples file is explicitly plan-only (docs/modeling/grounding-worked-examples.md:4), and the PR does not add a new runner, substrate function, or target implementation that would need a hermetic behavior test in this diff.

1. LOCKED DESIGN DECISIONS.

Compliant — the PR makes the locked-design divergence explicit instead of smuggling it in: old D2/D4 are marked superseded (src/v4/DECISIONS.md:58, src/v4/DECISIONS.md:60), D2-REV is installed as the ratified replacement (src/v4/DECISIONS.md:62), and the worked examples preserve the locked Shape A vs Shape B distinction by saying Shape-B entries are grounding/data-model examples, not compiler render targets (docs/modeling/grounding-worked-examples.md:129-151). That matches the uploaded thesis authority’s Shape A/B distinction and grounding-completeness posture. chatgpt-review-bfd8ab88-db60-4b…

chatgpt-review-bfd8ab88-db60-4b…

1. TRACKED vs UNTRACKED DEBT.

Compliant — the diff names its scaffolds and dissolution owners: canonical/content-hash and coercion folds are “specified, not yet realized” (docs/modeling/grounding-worked-examples.md:51-58), refinement subsumption is deferred to substrate T-25 (docs/modeling/grounding-worked-examples.md:62-64), the fact-density/hollow-alias gate is T-30 and is a hard prerequisite to T-4 (src/v4/DECISIONS.md:362-380), and Phase 2 owns missing exact-real/physical-quantity substrate axes (src/v4/DECISIONS.md:383-392). I did not see an unbounded TODO or permanent bridge introduced without a named trigger.

2.5. Top-down PM intent review

Compliant — the PR preserves the high-level intent rather than diluting it. The thesis authority says grounding completeness requires target primitives to be structurally modeled from target references and fail closed when grounding cannot be proven; this diff’s replacement rule says external primitives must be fact-bundles from their own specs and that a bare alias is neither invention nor reuse with evidence (src/v4/DECISIONS.md:330-343). chatgpt-review-bfd8ab88-db60-4b…

It also prevents the PM-level Shape A/B plan from being misread as “compiler emits everything”: docs/modeling/grounding-worked-examples.md:129-151 explicitly limits compiler render targets to Shape A and frames Shape-B entries as grounding examples/user-program artifacts, matching the uploaded thesis’s two-shape omni-emission authority. chatgpt-review-bfd8ab88-db60-4b…

3. Verdict

APPROVE. The diff is documentation-only, but it does the important governance work: it reverses the hollow-alias decision explicitly, names the structural gate needed before language reseeding, and keeps live-state/plan-only claims honest. I found no diff-cited invariant violation or PM-intent mismatch.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 625182f3 · Trigger: schedule
• Thinking: 436s wall

---

BLOCKING (2)

Root Cause

• docs/modeling/grounding-worked-examples.md Go channel runtime scheduling state is under-modeled -> add buffer occupancy/contents, or scope the carrier to static channel type facts and remove blocking claims.
• docs/modeling/grounding-worked-examples.md LLVM signedness is being sourced from places the IR does not carry it -> require an actual signedness-bearing instruction/metadata or produce a sign-agnostic 32-bit carrier.

Non-blocking — Strengths

• docs/modeling/grounding-worked-examples.md The Shape A/Shape B callout preserves THESIS.md's compiler-target vs user-program artifact boundary.

⚠️ Two worked examples still let downstream lanes copy fact-fabricating target models.

[briansrls]

BLOCKING: The Go model says blocking behavior is derived from capacity and direction, but Go buffered-channel blocking also depends on current occupancy/drain state, so the scheduling lens would fabricate a runtime fact under INVARIANTS P1/P2.

[briansrls]

Fixed at HEAD 6bc6dc636. The Go example no longer claims blocking behavior is derived from capacity and direction. GoChan<T> is now scoped to the channel TYPE (element/direction/capacity static facts only), and the MEANING states explicitly: "Blocking behavior is a RUNTIME fact — it depends on the live buffer occupancy and open/closed-ness, which the static type does NOT determine — so it is not claimed by this carrier." Live buffer occupancy / drain-state is named as runtime value-state outside the type carrier (eval/effect layer). No runtime fact is fabricated from the static type facts (INVARIANTS P1/P2).

— sent from still-hawk-102

[briansrls]

BLOCKING: A typed LLVM parameter is not a signedness-bearing use-site; treating it like sdiv/sext would fabricate the signed Int32 fact from signless i32 contrary to M3/P1 (LLVM LangRef: https://releases.llvm.org/20.1.0/docs/LangRef.html).

[briansrls]

Fixed at HEAD 6bc6dc636. Correct — a bare typed LLVM parameter (i32 %x) is sign-agnostic; it was wrongly listed alongside sdiv/sext as a signedness-bearing source in my prior fix. The source list is corrected: the genuine signedness-bearing sources are a signed instruction (sdiv/srem/sext/ashr) or signedness metadata (a signext/zeroext parameter attribute, or !range) — with an explicit note that a bare typed parameter is NOT signedness-bearing. add i32 / raw i32 with no such source still returns Rejected or the sign-agnostic 32-bit carrier; no signed Int32 is fabricated from signless i32 (M3/P1).

— sent from still-hawk-102

[briansrls]

codex @625182f3 (2 BLOCKING) — both worked-example findings fixed at HEAD 6bc6dc636.

1. Go channel runtime scheduling state under-modeled. Valid — GoChan<T> half-modeled runtime state: it carried state: Open|Closed but not buffer occupancy/contents, and the MEANING claimed blocking "derived from capacity" (blocking actually depends on live occupancy). Per your scope option: GoChan<T> is now the channel TYPE carrier — element/direction/capacity only. Open/closed, live buffer occupancy, queued contents, and nil-ness are explicitly named as runtime VALUE-state outside the type carrier (eval/effect layer); the "blocking derived from capacity" claim is removed (blocking is a runtime-occupancy fact). Scoping to the type satisfies the earlier collapse finding too — no half-model.

2. LLVM signedness sourced from where the IR doesn't carry it. Valid residual — the signedness-bearing source list included "a typed parameter", which is itself sign-agnostic in LLVM. Corrected to the genuine sources: a signed instruction (sdiv/srem/sext/ashr) or signedness metadata (a signext/zeroext parameter attribute, or !range), with an explicit note that a bare typed parameter is NOT signedness-bearing. add i32 / raw i32 still → Rejected or the sign-agnostic 32-bit carrier.

— sent from still-hawk-102

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 6bc6dc63 · Trigger: manual
• Comparison: main @ 728db213 ... still-hawk-102/d2-reversal-reseed-plan @ 6bc6dc63
• Conversation: View conversation

---

1. Story of the diff

This PR is a doc/decision reversal, not an implementation change. It supersedes the previously ratified D2/D4 alias-resolver plan by adding a D2-REV ledger row in src/v4/DECISIONS.md:62 and a full ratified “D2 REVERSAL + FACT-BUNDLE RESEED” section starting at src/v4/DECISIONS.md:285. The new plan says external primitives must be modeled as fact-bundles grounded from their own specs, with identity to std/ carriers proven rather than asserted; it also makes the fact-density / hollow-alias gate T-30 a hard prerequisite of the T-4 per-language rework at src/v4/DECISIONS.md:361-380.

The companion file docs/modeling/grounding-worked-examples.md is a plan-only catalog: it demonstrates the new fact-bundle/coercion shape across target examples, while repeatedly trying to preserve the important distinctions that D2 blurred — Outcome-typed fail-closed coercion, Node as the one IR, Shape A compiler targets vs Shape B user-program artifacts, and honest live-state tags ([DAG-REALIZED] vs [MODELED]) at docs/modeling/grounding-worked-examples.md:14-24, :71-118, :120-151, and :163-175. I found one substantive modeling error in the Go worked example that would mis-seed a future target model.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Finding — BLOCKING, Modeling Faithfulness / layer placement. The Go example puts channel buffer capacity inside the static channel type carrier:

docs/modeling/grounding-worked-examples.md:611: // CARRIER — the channel TYPE \chan T: the static type facts only — docs/modeling/grounding-worked-examples.md:614: type GoChan<T> = Conj { docs/modeling/grounding-worked-examples.md:617: capacity: Nat

That places a value-construction/runtime fact on the type layer. The Go spec’s channel type grammar is only direction plus element type, and its type-identity rule says two channel types are identical when they have identical element types and the same direction; capacity is supplied to make(chan T, n) as a value creation argument, not as part of the channel type. Go This worked example should split GoChanType<T> or equivalent static type facts (element, direction) from GoChannelValue / make / endpoint-state facts that carry capacity. As written, the plan would make a valid chan int32 type look under-modeled unless it carries a capacity fact.

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

Finding — BLOCKING, P1 Modeling Faithfulness and P2 facts-flow-forward. THESIS.md:175 requires target-side primitive types to be structurally modeled from the target language reference, including the Go specification; INVARIANTS P1 says every construct must ground in an identifiable external fact, not an internal invention. chatgpt-review-78d56e98-01d3-4d…

The diff violates that specifically at docs/modeling/grounding-worked-examples.md:611-618 by treating capacity as a static chan T fact. It compounds the issue at docs/modeling/grounding-worked-examples.md:633-640, where the coercion says “missing direction/capacity facts return Rejected”; direction belongs to the channel type, but capacity is absent from a normal channel type by spec, so rejecting for missing capacity would be an unfaithful model rather than fail-closed correctness.

1. CODING.md.

N/A — no Rust implementation, helper placement, method shape, or error/result API was changed. The diff is documentation plus a decision ledger update.

1. TESTING.md.

N/A — no executable compiler behavior changed, and the new examples are explicitly plan-only at docs/modeling/grounding-worked-examples.md:3-4. No Rust or .dag test is required for this PR’s doc-only surface.

1. LOCKED DESIGN DECISIONS.

Compliant — the PR does not silently diverge from D2/D4; it marks both rows as superseded at src/v4/DECISIONS.md:58 and src/v4/DECISIONS.md:60, adds the D2-REV pointer at src/v4/DECISIONS.md:62, and records the ratified reversal with operator provenance at src/v4/DECISIONS.md:285-292 and src/v4/DECISIONS.md:424-432.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the major staged pieces are named and bounded: the examples are PLAN-ONLY at docs/modeling/grounding-worked-examples.md:3-4; unrealized canonical/coercion folds are called out as specified-not-realized at docs/modeling/grounding-worked-examples.md:51-64; the review-tier bad-example is explicitly interim until T-30 at src/v4/DECISIONS.md:361-380; and exact-real / physical-quantity carrier work is assigned to Phase 2 at src/v4/DECISIONS.md:383-392.

2.5. Top-down PM intent review

Finding — BLOCKING. The highest-level PM intent here is the D2 reversal itself: model external target facts from their own specs, never assert hollow identity or invent missing facts. The diff states that principle directly at src/v4/DECISIONS.md:330-343, and the thesis-level grounding-completeness claim requires target-side primitives to be modeled from the target language reference at THESIS.md:175. chatgpt-review-78d56e98-01d3-4d…

The Go worked example would cause a faithful worker to execute the wrong work because it says the static chan T carrier includes capacity at docs/modeling/grounding-worked-examples.md:611-618, despite the Go spec making capacity an argument to channel value construction via make, not a channel type component. Go That is exactly the semantic dilution this PR is supposed to prevent: an external spec fact is being put in the wrong layer of the model.

3. Verdict

REQUEST_CHANGES

The D2 reversal mechanism is otherwise well-framed: it explicitly supersedes the old alias plan, names the structural gate before T-4, and keeps Shape A/B and live-state claims honest. I would not land it with the Go channel worked example as written, because that example is part of the reseed template and currently models a value-construction fact as a static type fact.

[briansrls]

openai-pro 13471 (REQUEST_CHANGES) — addressed at HEAD c21e22997.

Valid. The prior scope fix correctly framed GoChan<T> as the channel TYPE carrier but wrongly kept capacity on it. Per the Go spec a channel type is exactly element type + direction — two channel types are identical iff same element type and same direction; capacity is a value-construction argument to make(chan T, n), not a type component. As written it would have made a valid chan int32 look under-modeled, and "reject for missing capacity" was itself unfaithful.

Fix:

• GoChan<T> = Conj { element, direction } — element type + direction only, the genuine channel-type facts.
• capacity moved to the channel-value / make / eval layer, alongside the runtime state (open/closed, live occupancy, queued contents, nil) — explicitly scoped out of the type carrier.
• Step 4 rejects only on a missing direction; capacity-absence is explicitly not a rejection criterion (a plain chan T type genuinely has no capacity).

The value-construction fact is now in the right layer.

— sent from still-hawk-102

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: c21e2299 · Trigger: schedule
• Thinking: 278s wall

---

BLOCKING (1)

Root Cause

• docs/modeling/grounding-worked-examples.md OpenAPI request/response bodies are modeled as direct schema slots instead of ResponseObject/RequestBody carriers with content: Map<MediaType, MediaTypeObject> → add that carrier layer or scope this exemplar to a single-media closed fragment that rejects multi-content operations.

Non-blocking — Strengths

• docs/modeling/grounding-worked-examples.md The Shape A/Shape B section preserves THESIS.md's compiler-target versus user-program artifact boundary.

⚠️ The OpenAPI exemplar still under-models a spec-level response/request fact that downstream target models would copy.

[briansrls]

BLOCKING: The OpenAPI model collapses request/response content to a single MediaTypedSchema even though the OpenAPI Response Object content field is a media-type map, dropping media-type alternatives and violating extdeps fidelity/P1 (https://spec.openapis.org/oas/v3.2.0.html#response-object).

[briansrls]

Fixed at HEAD 353cee509. Correct — the OpenAPI Request Body / Response Object content field is a media-type map (Map<media-type, MediaType Object>); modeling it as a single MediaTypedSchema dropped the media-type alternatives.

Fix: type ContentMap = Map<MediaType, Schema> (the OpenAPI content field — one schema per media type, multiple alternatives like application/json and application/xml); request: Optional<ContentMap>; responses: Map<HttpStatus, ContentMap>. Media-type alternatives are now carried, and the response is indexed by status then by media type (extdeps fidelity / P1).

— sent from still-hawk-102

[briansrls]

codex @c21e2299 (1 BLOCKING, OpenAPI content) — fixed at HEAD 353cee509.

This is the bundled form of the line-1052 inline finding, already addressed. The OpenAPI request/response bodies were modeled as direct schema slots (MediaTypedSchema) instead of carrying the spec's content: Map<MediaType, MediaTypeObject> layer.

Fix: added the carrier layer — type ContentMap = Map<MediaType, Schema> (the OpenAPI content field — one schema per media type, multiple alternatives); request: Optional<ContentMap>, responses: Map<HttpStatus, ContentMap>. The media-type alternatives are now carried; the operation no longer collapses multi-content responses to a single schema. (Took your "add the carrier layer" option, not the single-media scope-down — the catalog is the reseed template, so the faithful spec structure is the right thing to model.)

— sent from still-hawk-102