Skip to content

Nat fork census - #7537

Merged
briansrls merged 6 commits into
mainfrom
session/jolly-bat-372
Aug 1, 2026
Merged

briansrls merged 6 commits into
mainfrom
session/jolly-bat-372

Conversation

@briansrls

@briansrls briansrls commented Aug 1, 2026 •

Copy link
Copy Markdown
Contributor

Retroactively completed 2026-08-01: this PR merged carrying the auto-opened session title and a TODO body with unchecked attestation. The census content was substantive and correct; the handback wrapper was not. Operator ruling — worker attestation is advisory rather than admission — so this is repaired in place (same repair pattern as #7530).

Follow-up status repair landed in #7548 (BLOCKED + LAST removed after prerequisites discharged).

What this PR landed

Execution-based Nat fork census and per-concept design authority:

  • docs/plans/nat-grounding-unification-design.md — full census, fork shape, target authority (coproduct wins), worker classification, atomic wave table, §7.6 gates
  • dag/gunbc/plans/dag_v2_defork_audit.dag — nat row updated to 138 co-occurrence, grounding-cluster status
  • dag/gunbc/doc_graph_roots.dag — HandAuthoredDocBind for nat design doc
  • Resolver wall / algebra cross-ref updates

Census conclusions (execution, 2026-08-01)

The fork is representational, not nominal: std.nat.Nat = CommutativeSemiring<Magnitude> (no constructors) vs v2.std.nat.Nat = Zero | Succ (Peano coproduct). Exactly one homonym: nat_compare — live §13 ambiguity in mixed closures.

Metric Value
Floor *_test.dag entries scanned 946 (was 351)
Closures with both authorities 138 floor closures (was 4)
LIVE fail-open pair {algebra (75), nat (138)}
dag/ std.nat importers 61
src/v2/ v2.std.nat importers 37
Direct std.nat inside src/v2/ 5 modules

What 138 means: import closures where both nat authorities are reachable — a risk and closure-population measure, not 138 migration tasks. Gate unsafe facts (§7.6), not the integer.

Exclusion rule (why 61, not 63)

Importer counts use authored top-level ^import lines only. Loose grep finds 63 dag/ files mentioning std.nat; two match only inside embedded fixture strings and are excluded.

Commands run (census session)

rg '^import.*std\.nat' dag/ --glob '*.dag'   # 61 authored imports
rg '^import.*v2\.std\.nat' src/v2/ --glob '*.dag'   # 37
# Co-occurrence: floor *_test.dag import-closure scan → 138 (946 entries)

Worker attestation (retroactive)

  • Census measurements verified by execution
  • Exclusion rule documented (61 not 63)
  • Fork characterized as representational (semiring alias vs Peano coproduct)
  • Co-occurrence shift 4 → 138 recorded with semantics
  • PR body repaired post-merge (this edit)

Note: BLOCKED + LAST status on main was stale (prerequisites discharged); corrected in follow-up #7548.

Brian Searls and others added 2 commits August 1, 2026 02:18
The dag↔v2 nat fork is catalogued in a per-concept design doc (declarations,
importers, entanglements, target authority) so the grounding-cluster repoint
can proceed after algebra. Re-measured floor import closures: 138 entries
now co-import std.nat and v2.std.nat (was 4 at 351 entries in 2026-06).

Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 1, 2026 02:19
gunbc-ci-auto-heal and others added 4 commits August 1, 2026 02:25
State the census counting rule explicitly (^import line vs loose grep):
61 live dag/ std.nat importers, reconciled against parent's 63 (two
witness fixture strings). Add HandAuthoredDocBind for
nat-grounding-unification-design so doc-reachability orphan wall covers it.

Co-authored-by: Cursor <cursoragent@cursor.com>
Split is_zero into category A′ — re-express via nat_cata, not verbatim
match port. Replace file:line integer fork evidence with std.integer.Int
and v2.std.integer.Int symbols (DESIGN §3).

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Aug 1, 2026

Copy link
Copy Markdown
Contributor

Addressed review 45861 in a034e419b:

1. is_zero predicate dissolution — Removed from category A verbatim-move set. New A′ row: migration must re-express as nat_cata(n, true, fn(_) { false }) and delete the manual Zero/Succ match in v2.std.nat.is_zero; the census notes the current walker as debt, not something to copy into canonical std.nat.

2. Symbolic citations (DESIGN §3) — §5 integer-fork row now cites std.integer.Int vs v2.std.integer.Int (type bodies in prose), not file:line. Same for the walls table qualified-Nat row.

— sent from jolly-bat-372

@briansrls
briansrls merged commit 082f9df into main Aug 1, 2026
9 of 10 checks passed
@briansrls
briansrls deleted the session/jolly-bat-372 branch August 1, 2026 03:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant