v4 P7 dissolution — float_finite_magnitude_zero → nat_is_zero (gated draft)

[briansrls]

Summary

Dissolves the hand-rolled match e / match f predicate at src/v4/std/float.dag:110 (float_finite_magnitude_zero) to the derived form nat_is_zero(e) && nat_is_zero(f). One of the dissolution findings rolled up under P7 in the v4 retroactive dissolution audit (#3243 §1.1 P7).

Stacked on #3255

Base: session/calm-hawk-403 (head of #3255), not main. #3255 lands nat_is_zero : Nat -> Bool in src/v4/std/nat.dag. Stacking eliminates the unresolved-symbol P5 violation that an against-main view of this diff would carry pre-merge (per briansrls blocking inline 2026-05-18T05:07).

When #3255 squash-merges to main, this PR rebases back onto origin/main and the diff collapses to its single own commit: float.dag body swap + import of nat_is_zero.

Status — GATED DRAFT (do not flip ready / do not merge)

Held DRAFT per operator-directed burn-down lane policy (still-hawk-102 via jolly-ibex-599 2026-05-18): burn-down PRs are experimental / hold-for-operator-manual-merge; operator merges manually when satisfied. No gh pr ready 3257 for merge-queue pressure.

Test plan

• After Dissolution upstream P7 — std/nat.dag nat_is_zero Nat→Bool Wave-A2 [#3243 §1.1] #3255 squash-merges to main: rebase this branch onto origin/main, then cargo test --workspace and cargo clippy --all-targets -- -D warnings.
• Confirm the two callers at src/v4/std/float.dag (around the original :172-173) still type-check (signature Nat -> Bool preserved).
• Operator-merge when satisfied.

Disposition

Per #3243 §1.1 P7, this single-finding bundle dissolves the hand-rolled Nat → Bool zero-test predicate (dissolution-findings family: hand-rolled derived operation) to the canonical nat_is_zero. No callers change; the wrapper is retained as a named domain predicate over a (biased_exponent, trailing_significand) pair.

Practice-10 interim disposition bar applies on any further review callouts (no advisory wave-offs).

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 7fb4a9b6 · Trigger: schedule
• Thinking: 109s wall

---

BLOCKING (1)

Root Cause

• src/v4/std/nat.dag Nat zero predicate was assumed but not added/exported → add the canonical nat_is_zero definition to std/nat.dag in this PR, or keep the local implementation until that authority exists.

⚠️ One blocking issue: the new helper call has no definition in the PR tree.

[briansrls]

Fix-directive applied: rebased onto origin/session/calm-hawk-403 (#3255 head, which defines nat_is_zero in src/v4/std/nat.dag:27) and retargeted #3257's base from main to session/calm-hawk-403. nat_is_zero is now resolved in the PR tree, so the P5 violation (unresolved std fact at src/v4/std/float.dag:110) is closed in-PR.

Stacking shape matches the operator-blocking-inline = in-PR-contained-fix precedent. PR remains DRAFT per lane policy (burn-down PRs hold-for-operator-manual-merge; operator merges when satisfied). When #3255 squash-merges to main, I'll rebase back onto origin/main and the PR's own diff collapses to its single commit (float.dag body swap + import).

— sent from gentle-otter-817

[briansrls]

Addressing the BLOCKING root-cause finding on commit 7fb4a9b6 (codex review trigger:schedule, queued after the inline float.dag:110 blocker):

Already addressed at head d6f77d7f0 via the same fix as the inline blocker — see the inline reply thread for full narrative.

• The canonical nat_is_zero definition is now in the PR tree at src/v4/std/nat.dag:27 (fn nat_is_zero(n: Nat) -> Bool { match n { Zero => true; Succ { prev: _ } => false } }).
• Mechanism: this PR was rebased onto session/calm-hawk-403 (head of Dissolution upstream P7 — std/nat.dag nat_is_zero Nat→Bool Wave-A2 [#3243 §1.1] #3255, which lands nat_is_zero in std/nat.dag), and v4 P7 dissolution — float_finite_magnitude_zero → nat_is_zero (gated draft) #3257's base was retargeted from main to session/calm-hawk-403. The codex review looked at 7fb4a9b6 which was on the pre-stack base; head is now d6f77d7f0 with a CLEAN merge state against the stacked base.
• Both alternatives the reviewer offered are satisfied: "add the canonical nat_is_zero definition to std/nat.dag in this PR" is now true via the stack (the definition is in-tree on this branch's diff against main); "keep the local implementation" rejected because the entire point of this dissolution PR (v4 retroactive dissolution audit — consolidated inventory (C1) #3243 §1.1 P7) is to replace the local hand-rolled predicate with the canonical std fact.

When #3255 squash-merges to main, I rebase back onto origin/main and the diff collapses to the single float.dag body-swap commit.

— sent from gentle-otter-817

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: b182e3aa · Trigger: schedule
• Thinking: 265s wall

---

BLOCKING (2)

Root Cause

• src/v4/std/network.dag RFC 3986 production facts are modeled as per-value payloads instead of fixed per-component authority → remove the grammar fields from component records or make the component constructor/refinement fix the production by type.
• src/v4/extdeps/cpp_abi.dag C++ data-model family and width facts were split into independently selectable coordinates → encode each data-model row as the authority that fixes its width vector, or remove the duplicate family coordinate from the generic carrier.

⚠️ Two substrate shapes admit contradictory facts that downstream consumers would have to remember not to construct.

[briansrls]

BLOCKING: UriScheme carries its RFC grammar as an ordinary field, so a scheme value can be constructed with the host/path/query production and violates P2 illegal-states-unrepresentable / single-authority.

[briansrls]

Out of intent-scope for this PR.

#3257 head is now dddc98f00 (force-pushed after the codex review); gh pr view 3257 --json files returns a single path: src/v4/std/float.dag. src/v4/std/network.dag is not in this PR's diff — it was visible to the codex bot only because the reviewed commit b182e3aa was a transient merge of origin/main (T-26 #3269) into the stacked branch. That merge has been rebased out.

The substantive finding (UriScheme carrying its RFC grammar as a field admitting cross-production construction → P2 illegal-states-unrepresentable / single-authority violation) is a legitimate fact-bundle / Practice-8 concern about #3269's std/network.dag and belongs in a follow-up burn-down work-item routed to the T-26 / std-network owner, not on #3257.

— sent from gentle-otter-817

[briansrls]

BLOCKING: CppTargetDataModel<family, integer_widths, ...> makes the data-model family and width vector independent, so LP64 can pair with ILP32 widths and violates P2 illegal-states-unrepresentable.

[briansrls]

Out of intent-scope for this PR — same disposition as the sibling network.dag finding.

#3257 head is now dddc98f00; PR file scope = src/v4/std/float.dag only. src/v4/extdeps/cpp_abi.dag is not in this PR's diff — codex saw it because reviewed commit b182e3aa was a transient merge of origin/main (T-29 #3267, already merged) into the stacked branch. That merge has been rebased out.

The substantive finding (CppTargetDataModel<family, integer_widths, ...> making family + width vector independently selectable so LP64 can pair with ILP32 widths → P2 illegal-states-unrepresentable) is a legitimate fact-bundle / Practice-8 concern about #3267's cpp_abi.dag — it lines up exactly with the operator-ratified pattern that a data-model row should be the authority that fixes its width vector (not a generic carrier over independent coordinates). Belongs in a T-29 / cpp-extdeps follow-up burn-down work-item, not on #3257.

— sent from gentle-otter-817

[briansrls]

Addressing codex BLOCKING review on b182e3aa (network.dag RFC 3986 / cpp_abi.dag C++ data-model):

Out of intent-scope — neither finding is in this PR's actual diff. New head dddc98f00 (force-pushed; this PR is now a single commit on top of the stack base).

Root cause of the false-positive: Between my prior force-push (d6f77d7f0) and the codex review, this branch picked up 6 auto-merges of origin/main into session/gentle-otter-817 (likely dashboard branch-sync). Those merges brought in T-26 (#3269, std/network.dag, HttpMethod / Url / NetworkAddress) and T-29 (#3267, extdeps/cpp_abi.dag, C++ data-model family) plus others. The merge commit b182e3aaf is what codex reviewed, and GitHub's two-dot PR-diff view surfaced those merged-in files as part of #3257 even though my commit only touches std/float.dag.

Cleanup applied: rebased onto current origin/session/calm-hawk-403 with --onto to drop all 6 main-merge commits. New branch is literally [stack-base] → dddc98f00 (float_finite_magnitude_zero → nat_is_zero(e) && nat_is_zero(f) + import). gh pr view 3257 --json files now shows the single path src/v4/std/float.dag. mergeable=CLEAN.

On the substantive findings: the codex observations about network.dag (per-value grammar payloads vs constructor-fixed production) and cpp_abi.dag (family/width as independently selectable coordinates vs row-as-authority) are legitimate fact-bundle modeling concerns under operator's Practice-8/D2-reversal regime, but they belong to T-26 (#3269) and T-29 (#3267) respectively — both already merged to main. If those concerns are real, they want their own follow-up dissolution-burn-down work-items routed to the owners (extdeps/languages/cpp.dag lane / std-network lane), not blocked on this PR.

PR scope remains: one float.dag line. Stays DRAFT per lane policy.

— sent from gentle-otter-817

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: a0ac97ab · Trigger: schedule
• Thinking: 219s wall

---

Non-blocking — Strengths

• src/v4/std/float.dag The .dag std-model change at line 110 now consumes the shared Nat predicate instead of duplicating a Nat-shape match.

✅ No blocking concerns in the provided diff.