v2 infer: an integer literal elaborates at an expected type through literal_homomorphism_rows; std.nat Peano row; -1 refused at Nat (XL-2)

[gunbai-bot]

What this does

v2 infer elaborates an integer literal at an expected type through the one declared table: std.literal_elaboration elaborate_literal_at over gunbc.structural_realization_bindings literal_homomorphism_rows, the same function and rows the seed's inference uses. It also adds std.nat Nat's Peano literal row, so g(n: 0) at a Nat parameter is accepted with the literal as written.

Stacked on #13307 (count), which is stacked on #13207. Until those land, this diff includes them.

The change

• v2.compiler.infer infer_literal_elaborates_at, one helper.
  • An integer literal whose expected type is a declaration with a literal row elaborates to that type.
  • It is read by the declared-type obligation (infer_judge_declared_position), which covers every declared position.
  • destination_realizes_natively is passed as false, and that is a decision, stated in the code. The seed answers it from kernel_grounding_rows: std.nat Nat is grounded to the kernel integer, so the seed takes DirectLiteral, which is a realization fact. v2 infer keeps Nat and Int distinct types and asks the typing question.
• A negated literal refuses at a row-backed destination. -1 lowers to a unary Transform (the - token, canonicalized to the subtraction wire) over the literal 1. Before this it reached the judge underived and was admitted at Nat (and at any type). It now refuses with infer_reason_negative_literal_has_no_image_in_destination, located at the expression.
• The std.nat Peano row in literal_homomorphism_rows. The seed never reaches it: Nat is grounded, so the seed answers DirectLiteral first. The stage0 mirrors were regenerated; the fixed point came at round 2.
• Scope, stated. Integer literals only. A string literal at the free monoid over Char stays the text-boundary lane's.

What is NOT here, and why (calm-boar-904's rulings)

• No operator-unify reader. It would change no verdict:

  • Nat carries no algebra row, so n + 1 refuses at the operator either way;
  • ==, < and - are not judged at all (RFM: comparison operands are never judged in v2 infer (below floor, measured) #13311).

  It would be an unconsumed declaration (§3c), so it is added when either trigger makes it observable. The code says so.

• count stays the stated, judged Int (option B). v2 infer does not judge a call's result when the callee returns a declared type (RFM: a call's result is unjudged in v2 infer when the callee returns a declared type (below floor; N7 next wall) #13314, measured). Flipping count to Nat would lower every count result from judged to unjudged. The departure on std.algebra algebra_count_length_name_fork_note now names both conditions: literal elaboration, met by this PR; declared-type call results judged, not met.

Controls (v2.test.claim.compiler.literal_elaboration), per DESIGN §3's witness rule

claim	kind	head
lel_route_runs_on_the_real_path: one module with a std.nat peer is assembled and inferred (0 and 3 at a declared Nat, 3 at Int, 0 + 1 an Int); on the v2 eval route, zz(Zero) and zo(Succ { prev: Zero }) with body n == 0 never answer wrongly	real path	PASS
lel_literals_elaborate_at_nat (0, 3)	supplied	PASS
lel_literal_at_int_is_not_elaborated	supplied	PASS
lel_literal_at_a_type_without_a_row_is_not_elaborated	supplied, RED	PASS
lel_negative_literal_at_nat_refuses, pinned to its reason	supplied, RED	PASS
lel_literal_of_another_kind_is_not_elaborated_at_nat (a string)	supplied, RED	PASS
lel_count_compared_with_a_literal_executes_on_the_seed	seed execution	PASS

Mutation. Deleting the std.nat Peano row turns lel_route_runs_on_the_real_path FAIL.

The eval condition. It is disjunctive and red-capable. Today v2 eval refuses both calls: the comparison is underived (#13311), and a Nat constructor argument is refused too. Refusing is not answering wrongly. Once comparisons are judged, Zero must answer true and Succ { prev: Zero } false, and any one-sided answer or wrong Bool reds.

Freeze note (tightened)

This PR adds no floor_cross_claim_pure_producers_warm rows. The real-path claim is over budget (it assembles and infers), so it becomes this module's single floor_single_claim_fill_debt member once #13043 lands.

🤖 Generated with Claude Code

N7 re-measure after the #13388 / #13487 merges (head 1ad2232 vs merge base ea9a51c)

gunbc test //v2/test/parse/expression_bodied_fn_decl_parse:all (native route, full refusal chain). Head f55c0828, base f1c46a7a.

• The bare count link CLEARS (from v2: bare count over lists binds the std.algebra collection size row, a stated Int (XL-2, N7) #13307, which this PR stacks on). At base the chain refuses count 3 times (resolve_unbound_name_is_declared_in_several_modules); at head it does not appear.
• The next link at that position is bare filter (resolve_unbound_name_is_declared_elsewhere @ v2.std.algebra.filter), which the XL-2 filter/any retirement removes.
• Every other link is identical (EmptyPattern, from_code_point, the Optional and Cardinality ambiguities), so there is no new refusal. All 8 verdicts still refuse at prepare.

The #13388 merge repointed this PR's v2.std.optional import (with optional_absent / optional_present, which std.optional exports unchanged) using tools.source_reference_repoint, and regenerated the gunbc_structural_realization_bindings mirror on a fresh seed (fixed point at round 2). The head was later advanced to bc59995 by merging #13307's head, with main and #13490 in it; this PR adds no rung-drop row, so its docs projection is #13307's.

[gunbai-bot]

Addressed review 77219 per calm-boar-904's ruling (A), at d974378.

• Partition law restored. The Peano LiteralHomomorphism row for std.nat Nat is dropped. Nat is kernel-grounded, so it carries no homomorphism row (std.literal_elaboration: a declaration is never both).
• Nat elaborates a literal through its kernel grounding, with a declared range on the grounding model:
  • KernelGrounding gains min: Int? / max: Int?, in std.types range's own vocabulary.
  • Admission is kernel_grounding_admits, which calls that range, so there is one range authority and no check inside infer.
  • Nat's row declares min: 0.
  • v2.compiler.infer infer_int_literal_value_at reads the grounding row first: the range admits → elaborated; otherwise it refuses infer_reason_literal_outside_kernel_grounding_range, so -1 at Nat refuses DERIVED from the row.
  • The homomorphism route remains for structural destinations (test.fixture.structural_peano_nat StructuralNat).
• Controls, enrolled: 0 and 3 elaborate at Nat; the -1 RED is pinned to the range reason; a new claim reads Nat's production grounding row and checks it admits 0 and 3 and not -1. The real-path claim's deletion note now names Nat's grounding row.
• Prose: the bindings header and peano_nat_structural_realization witness say Nat has no literal row and takes literals directly. That is TRUE again with the row dropped, so no rewrite was needed. The comment this PR had added above literal_homomorphism_rows, which claimed a Nat row, is deleted.
• (4) does not apply: Nat needs no Zero/Succ structural realization. It is realized as the kernel integer, and the Peano structural realization belongs to the StructuralNat fixture.

Verified on BuildBuddy at d974378 (5f0e3674):

• literal_elaboration_test 8/8.
• peano_nat_structural_realization_test 29/29.
• Mirrors regenerated (std_literal_elaboration.rs, gunbc_structural_realization_bindings.rs), fixed point at round 2.
• self_host_peano_literal_operator_realization_witness_test is 10/11. Its one failure, w_literal_at_native_boundary_stays_direct (an Int a + 2 emission expectation), fails identically on main f035b26 (e9b75e65) and at this PR's pre-rework head (95c5e3c5), so it is not introduced here.

— sent from silent-wren-814