Nat de-fork: one Peano Nat in std.nat, realized as the host integer (binding + cut)

[gunbai-bot]

Nat de-fork (work item adhoc-62b05aa9-8ec). XL-0N superseded for std Nat by operator default, 2026-09-30 (operator escalation via neat-boar-16 / wise-dove-693, which closed on ruling A: the Peano carrier, realized as the host integer on both seed routes). The operator can still reverse this.

XL-0N escalation: approved by timeout (neat-boar-16 ruling): the escalation that superseded XL-0N for std Nat drew no reversal within its window, so ruling A stands as approved.

The binding commit is kept separate for its byte-identity receipt; the cut and the operator repair follow.

Commit 1: realization binding (no-op over the corpus)

• Binding: std.literal_elaboration KernelGrounding plus gunbc.structural_realization_bindings kernel_grounding_rows = [std.nat Nat], keyed on the carrier's DeclarationRef. The zero and successor constructors are derived from the declaration's shape, not named in the row.
• One fold: v1.compiler.infer ground_kernel_views runs at the end of typecheck_module, after inference, exhaustiveness and descent annotation. It rewrites Zero to 0, Succ { prev: e } to e + 1, a match over Nat to an if-chain on == k / >= k with the predecessor bound as n - k, and a nested closed numeral pattern to a literal pattern. The emitter and the interpreter read that one tree, so the two routes cannot disagree.
• Identity decides, spelling only pre-filters. Unsupported forms refuse with a located diagnostic: an open successor pattern nested inside another pattern, an authored guard on a Nat match, or a bound carrier that is a coproduct of the wrong shape.
• Emitter and inference support: a bound carrier's declaration renders as the kernel integer. It contributes no structural summary, is kept out of the recursive-type set, has no constructor imports, and is not judged as a concrete coproduct by the payload-versus-parent check.
• Receipt (24GB BuildBuddy runner, exact sha):
  • the seed regenerates to a fixed point (first_generation_equal=true);
  • the self-host crate emitted from v2.compiler.compile (218 files) is byte-identical to base e7a527daba5, tree sha256 cc9510cc750ba69ec4595bf1bbf3acbb10d3bcc3d85f775ce17daf9979df7ba4 on both sides.

Commit 2: the cut

• One declaration. std.nat Nat = Zero | Succ { prev: Nat }, chosen as the survivor by layer: std.integer, std.coercion's declaration-keyed rows and 562 consumer modules already point at it. The arrangement is acyclic because v2.std.nat imports std, never the reverse.
• Deletions and repoints. std.magnitude is deleted, along with its seed mirror and crate-partition rows. v2.std.nat is reduced to its node-bound law roster, and 52 consumers are repointed to std.nat.
• Operations use the host operators; nat_cata is an accumulating tail-recursive eliminator.
• Semiring by inhabitance. std.algebra gains OrderedSemiringProfile (the ordered ring's surface without negate) and a Nat carrier row. The inhabitance witness values are nat_semiring and nat_additive_commutative_monoid. Controls: add, mul, zero, one and compare derive for Nat; negate does not derive for Nat but does for Int.
• XL-0N's structural lane is re-subjected to test.fixture.structural_peano_nat StructuralNat. It uses distinct names on purpose: a second corpus type spelled Nat would re-create the bare-name fork. Its literal and ordering rows are repointed to the fixture, and both XL-0N claims are kept.
• Seed interpreter. The Numeric-tower grounding: ground Nat construction-side so native form == modeled form (§0) #5428 spelling-keyed Zero/Succ arms are deleted; a user Peano-shaped type is no longer silently turned into integers. Two small additions keep that deletion safe. A constructor pattern matched against a host integer now refuses with its location, since it could otherwise fall through to a wildcard silently. And a Peano-unfolded literal evaluates as its constructor image. Seed-growth row: gunbc.kernel_grounding_interpreter_seed_growth (reason and trigger stated in it); everything that replaces the deleted arms is .dag.
• Inference. A bound carrier admits itself and its transparent aliases (std.integer NonNegativeInt = Nat) at the inhabitance verdict and at the call-argument check. Without that, correct calls in semver.dag and citation.dag refused.
• Agreement control. test.claim.std_nat_realization_agreement_witness_test (interpreted) and the compiler test ct_std_nat_realization_agreement_test (the seed's own emitted std_nat) hold one program to the same expected values.
• Retired: gunbc.guarantee_stall.two_nat_authorities_stall, whose trigger is this cut, and the nat-grounding design-doc bind.

Commit 3: Nat operators refuse overflow again (found by the self-host diff)

• Defect: with Nat declared inductively its type reference has no checkpoint of its own, so v1.compiler.emit_rust expr_realizes_as_refusing_int answered false and Nat + - * emitted Rust's wrapping i64 operators instead of v1_rt::int_* (silent wrongness in an emitted release build). No gate caught it; the self-host diff by name did.
• Repair: the operand check consults the kernel grounding binding by the DeclarationRef the type reference carries (std.nat::Nat), the same key rust_kernel_grounded_type_decl uses. A first repair (environment lookup by name) missed call-result operands and was replaced.
• Controls: route witness test.claim.emitter_refusing_int_operator_witness_test w_nat_binary_operators_route_through_refusing_helpers (FAIL on the pre-fix seed, PASS after; Int/Float controls PASS on both). Executed: compiler test ct_std_nat_operators_refuse_overflow_test runs the seed's emitted std.realization_schedule runnable_batch_clamp_ms (a Nat product of a call result): in-range 2015; overflow refuses with v1_rt's integer overflow: text; RED on the pre-fix mirror (rustc's panic text).
• Row: gunbc.recurring_failure_mode a_representation_change_drops_the_types_realization_checkpoint.

Receipts (24GB BuildBuddy runner, exact sha)

• Review 73960 fix at c5e96922c7a: nat_difference_of_ordered deleted, its subtraction inlined into nat_sub's non-underflow arm. Control for nat_sub(3, 17) on both routes: the interpreted test.claim.std_nat_realization_agreement_witness_test (underflow_holds) and the emitted compiler test std_nat_emitted_realization_agrees_with_the_interpreted_witness (generated from v1.compiler.compiler_tests_rust ct_std_nat_realization_agreement_test into src/v1/stage0/src/compiler_tests.rs) both require NatSubtrahendExceedsMinuend, never a negative Nat. On that sha: seed fixed point; agreement witness 4/4; semiring 5/5; compiler tests std_nat_emitted_realization_agrees_with_the_interpreted_witness and std_nat_emitted_operators_refuse_overflow_through_the_runtime_helpers 2/2.
• Seed regenerates to a fixed point (first_generation_equal=true) on the merged head.
• Self-host crate (gunbc compile --entry src/v2/compiler/00_compile.dag) at 4349b1f22d9 vs main d7f4da974c7: 222 files, cargo check rc 0. Differing files: std_nat, v2_std_integer, v2_std_cardinality, v2_std_verdict, v2_lens_cost, v2_lens_fact_density, v2_extdeps_languages_llvm_ir, std_algebra, std_computation, lib.rs, emitted_population; deleted std_magnitude, v2_std_nat. One file outside the by-name list: std_measure -- all 134 changed lines are type arguments spelled Nat where main spelled i64 (pub type Nat = i64, same Rust type). Before the operator repair six further files differed; they are gone.
• Claims (earlier head, unchanged since for these subjects): agreement 4/4, semiring 5/5, structural Peano 31/31, refinement cast 17/17, equality 9/9, reference realization 9/9, alias identity 5/5, root4 5/5, checkpoint keying 1/1, carrier roster 4/4, fork census witness 6/6, guarantee stall 11/11, call-target realization 59/59; emitter refusing-operator witness 4/4 on the final seed.
• Whole corpus (srv1, neat-boar-16, gunbc compile per root, keyed (module, message) with positions stripped): base main 8a44bcb685 vs head 366b7aae70: 64 blocking errors on both, 62 distinct keys, new 0, gone 0; peak RSS 38.20 vs 38.35 GB. Advisory diff: nat_cata's two advisories moved from v2.std.nat to std.nat (not new); witness_row_cost's unlisted v2.std.nat.Nat use is gone; fact_density's new unlisted std.nat.Nat use is fixed (imports Nat). Re-run at head 4349b1f22d9 (operator repair) vs base d7f4da974c7: 64 blocking on both, new 0, gone 0; peak RSS 38.40 vs 38.48 GB; advisories 38,111 -> 38,116, exactly the nat_cata move plus three unlisted import use advisories gone. One advisory is new and is this PR's: gunbc.kernel_grounding_interpreter_seed_growth reports where-refinement unenforced: Brand on RoadmapNodeId (its roadmap-node field; advisory, deferred refinement).
• Pre-existing red, not from this change: w_literal_at_native_boundary_stays_direct (base emits the same v1_rt::int_add(a.clone(), 2)).

Specimen D (census rows the cut was to dissolve; before = base census, after = head 366b7aa)

module	declaration	before	after
gunbc.fleet_runner_connectivity	slot_indices_for_managed_width	readers disagree	still disagree (not Nat-specific)
gunbc.fleet_show_effective_read	oom_pressure_limit_converge_verdict	identity unavailable	resolves to std.nat::Nat, i64, Agrees
gunbc.fleet_show_effective_read	slice_property_memory_max_verdict	identity unavailable	resolves to std.nat::Nat, i64, Agrees
gunbc.floor_materialization	floor_typecheck_store_persist_cap_bytes	identity unavailable	resolves to std.nat::Nat, i64, Agrees
gunbc.machine_intake_host_resource_observation	has_duplicate	readers disagree	still disagree (not Nat-specific)
gunbc.runner_slot_allocation	host_fleet_slot_indices	readers disagree	still disagree (not Nat-specific)
gunbc.runner_unit_live_read	memory_limit_converge_verdict	identity unavailable	resolves to std.nat::Nat, i64, Agrees
gunbc.runner_unit_live_read	runner_unit_memory_max_drifts_against_cap	identity unavailable	resolves to std.nat::Nat, i64, Agrees
gunbc.runner_unit_live_read	runner_unit_usage_exceeds_bytes	identity unavailable	resolves to std.nat::Nat, i64, Agrees
gunbc.spark.serving_rank_observe	rank_nccl_gpu_direct_devices	readers disagree	still disagree (not Nat-specific)
gunbc.spark.v41_capacity_measurement	v41_measurement_ranks	readers disagree	still disagree (not Nat-specific)
gunbc.spark.v41_capacity_measurement	v41_staircase_concurrencies	readers disagree	still disagree (not Nat-specific)
test.claim.emission_entry_instrument_witness	emit_capture_window	identity unavailable	resolves to std.nat::Nat, i64, Agrees
test.claim.memory_scale_factor_derivation	factor_is	identity unavailable	resolves to std.nat::Nat, i64, Agrees
test.claim.realization_scale_agnostic	milli	identity unavailable	resolves to std.nat::Nat, i64, Agrees
test.claim.spark.v41_engram_file_backed_witness	w_offsets	readers disagree	still disagree (not Nat-specific)
test.claim.spark.v41_published_row_store_witness	w_candidate_layers	readers disagree	still disagree (not Nat-specific)
test.claim.spark.v41_published_row_store_witness	w_stores	readers disagree	still disagree (not Nat-specific)
test.claim.time_scale_factor_derivation	factor_is	identity unavailable	resolves to std.nat::Nat, i64, Agrees
v2.lens.fact_density	connective_spec_fact	identity unavailable	resolves to std.nat::Nat, i64, Agrees
v2.lens.fact_density	density_fact	identity unavailable	resolves to std.nat::Nat, i64, Agrees
v2.lens.fact_density	named_fact_count	identity unavailable	resolves to std.nat::Nat, i64, Agrees

13 dissolved. The 9 that persist are not Nat-specific: the declaration reader resolves the reference to the referring module itself, and the same head census has 66 rows of that shape over List, ObservationAttempt and ShowEffectiveRead.

Floor capacity (measured, not this PR's to fix)

The floor's terminal-ledger compile stalled with MemoryStallRefusedPageThrash on 4 of 6 runs (srv4-02, srv4-03, srv3-08, srv3-13) and passed on rerun. Cause is subject width: editing std.nat widens strict preparation to 4064 modules (26 min) against 2309 (10 min) on a typical PR, witness sites 10077 against 1141; the ledger then typechecks beside that resident state under a 25 GiB memory.high with no swap. Not a compiler regression: the ledger entry compiled alone peaks at 10.2 GB on main and 10.3 GB on head. Parent ruling: rerun until green; capacity routed to neat-boar-16.

Latent defects the wider floor subject surfaced (fixed here or by main)

floor_preparation_shared_build_witness_test (missing CrossClaimPureProducerWarm arm), citation_cit0_witness_test (optional selector), build_cache_placement_observation_test (ambiguous placement_verdict), build_cache_endpoint_path_test (untyped state list), llm_attempt_receipt_witness_test (TokenThroughput literal), bare Filesystem in harness_cli, harness_turn, repository_load, repository_save, bare Unit in systemd_property_directive_overlap.

Findings to review

1. Nat spells i64 or Nat by position. Same Rust type; emitted bytes change outside the by-name list (std_measure, above). Two emitted-bytes claims were updated to the new spelling with their subjects kept.
2. One claim no longer reaches its case. w_qualified_type_reference_qualifier_disambiguates_the_leaf depended on two corpus declarations spelled Nat; with one it exercises the unambiguous route only, as its comment says.
3. Open, not in this PR: the implicit Int->Nat crossing (std.coercion grounded_primitive_coproduct_identities Int->Nat row) admits a negative Int at a Nat position unchecked; Nat - Nat is typed Int (dag_subtraction_refinement), so the -1 is correct and the crossing is the defect. Rostered as the_checker_admits_a_cast_the_evaluator_refuses; follow-up work item adhoc-556faf74-a06 was scoped and closed unstarted at wind-down (admitting site v1.compiler.infer kernel_value_declared_type_mismatch_bounded via dag_can_cast; key the refusal on std.nat::Nat's DeclarationRef; keep nonnegative literals admitted).
4. Review 73899 nit, left as stated: eval_match's new host-integer refusal exempts Present/Absent/Some/None/Holds/Violates by name, so a user type with a variant spelled Some skips the new check. It only narrows a refusal main does not have (nothing is less safe than main); keying it on the optional/witness declarations is more hand-written seed growth, and gunbc.kernel_grounding_interpreter_seed_growth's trigger already forbids widening the list.
5. Separate defect, routed by wise-dove-693: the seed interpreter's eval_match never evaluates match-arm guards.

Please don't merge without the operator.

🤖 Generated with Claude Code

Landing round (swift-ram-239, 2026-10-02)

• Main integrated by merge commits only. Main's mirrors were taken on conflict, then regenerated to the fixed point in three rounds on a 24G-cgroup BuildBuddy runner (first_generation_equal=true, 161/161 adjudicated). The crate partition and the defork audit were regenerated through main_wet.
• One semantic edit came from the merge. Main's new std.algebra algebra_profile_admits_numeral had no arm for this PR's OrderedSemiringProfile, so the match was non-exhaustive and the regen refused. It now answers true: a non-negative numeral names the image of a natural under the unique semiring homomorphism out of the naturals.
• Floor non-fold residue (281 sites). All 281 sites predate this PR. The typed, diff-scoped residue check (NFR: typed, diff-scoped non-fold-residue check on the required floor (D) #12610) landed after the approved head. Its scope includes interface consumers, and this PR changes std.nat and std.algebra. All 281 match NFR census roster: #12610's joint landing (delete the text scan; roster 915 typed-census sites) #12980's roster by exact path::fn; NFR census roster: #12610's joint landing (delete the text scan; roster 915 typed-census sites) #12980 was built from the whole-corpus census at main ca5ed1724b, and it is now on main. Nat de-fork: one Peano Nat in std.nat, realized as the host integer (binding + cut) #12846 adds no roster rows.
• Review 74240. is_zero, nat_lte and nat_gte are deleted from std.nat: they were one-line nicknames for host comparisons, carried over from v2.std.nat. nat_lte's two callers (v2.lens.cost.expr, v2.lens.cost.valuation) now write <=, and the agreement witness asserts agreement_three() != 0.
• Hand-Rust receipt. The two std_nat compiler tests are generated from .dag (v1.compiler.compiler_tests_rust ct_std_nat_realization_agreement_test, ct_std_nat_operators_refuse_overflow_test); they are not hand-written Rust. The hand-written seed growth is limited to the interpreter arms rostered as gunbc.kernel_grounding_interpreter_seed_growth, which carries its reason and trigger. Deleted in exchange: std.magnitude, its std_magnitude.rs mirror and partition row, and the Numeric-tower grounding: ground Nat construction-side so native form == modeled form (§0) #5428 spelling-keyed Zero/Succ interpreter arms.
• XL-0N: the escalation is approved by timeout (neat-boar-16 ruling).

[gunbai-bot]

Review 74240 addressed in d88e267 (merged into head 78ddefc). is_zero, nat_lte and nat_gte are deleted from std.nat. A census after the latest main merge found two nat_lte callers, not one: v2.lens.cost.expr and v2.lens.cost.valuation. Both now write <=. The agreement witness asserts agreement_three() != 0. Mirrors were regenerated to the fixed point (first_generation_equal=true). On that tree the agreement witness passes 4/4 and the compiler tests std_nat_emitted_* pass 2/2. The hand-Rust receipt is in the body under "Landing round": both std_nat compiler tests are generated from v1.compiler.compiler_tests_rust, not hand-written.

— sent from swift-ram-239