XL-0N: generic LiteralElaboration/OperatorRealization authority — typed literal-to-Zero/Succ homomorphism, operator realization by exact operand structure, structural Peano Nat (no i64 row)

dag/gunbc/guarantee_rung_drop.dag

@@ -544,3 +544,54 @@ fn stall_roster_size(ss: List<GuaranteeStall>) -> Int {
     cons: fn(acc, s) { acc + 1 },
   )
 }
+
+// THE CONNECTIVE GAP, DECLARED RATHER THAN CLAIMED (DESIGN section 4b(2): a class below its ceiling
+// names its next-rung trigger). Ordering and arithmetic on a structural operand are decided by this
+// roster -- a declared comparison, or a typed refusal. The logical connectives are NOT: inference
+// constrains only the RESULT of `&&`/`||` to Bool (v1.compiler.types infer_binop_type_node), so a
+// structural operand under a connective is authorable and renders as the host token. Found by
+// review (claude/claude-opus-4-7 on gunbc#9719, 2026-08-30) reading the arm against its own prose.
+//
+// WHY THE OBVIOUS REPAIR IS THE WRONG ONE, measured before it was rejected: refusing every
+// structural operand under a connective would refuse v2.std.logic Bool, which 593 modules import as
+// their ordinary Bool -- the false-refusal cost the namespace wall's own doctrine names, and it
+// would land as a corpus-wide red rather than as a wall. The repair is one more row FAMILY of the
+// shape this roster already carries for ordering: the declaration names the operation that realizes
+// its conjunction and disjunction, connectives on a declaration with a row realize through it, and
+// only a declaration with NO row refuses -- at which point the refusal population is enumerable
+// instead of being the whole corpus.
+// TWO Nat AUTHORITIES ARE ONE NAME ANSWERING FOR TWO CONCEPTS, and this row exists because review
+// 57758 correctly refused a version of it that was narrated in prose beside one of the two nat_max
+// declarations. The fork predates this lane; what this lane changed is that the Peano side now
+// carries real operations, so the fork is load-bearing rather than latent.
+data two_nat_authorities_stall: GuaranteeStall = GuaranteeStall {
+  subject: "std.nat Nat (CommutativeSemiring<Magnitude>, realizing natively as a machine scalar) and v2.std.nat Nat (the Peano coproduct Zero | Succ) are two declarations answering for one name, so nat_add / nat_mul / nat_max / nat_compare each exist twice and a bare reference in a closure containing both modules is ambiguous",
+  current: Mitigatable,
+  ceiling: StructurallyImpossible,
+  blocker: AwaitsOneGrounding {
+    grounding: "one Nat authority: the numeric tower deciding whether the Peano coproduct IS the declaration and the semiring alias is derived from it, or the reverse -- a modeling ruling this lane cannot make from an operator-realization change",
+  },
+  population: BoundedPopulation {
+    members: [
+      "std.nat and v2.std.nat both declaring Nat, with per-operation forks (nat_add, nat_mul, nat_max, nat_compare) that no single function can serve because the two are different types",
+      "every reference site in a closure containing both modules, which must qualify the name (v2.lens.cost.valuation does) or resolve by pool precedence",
+    ],
+  },
+  next_rung_trigger: "one Nat declaration in the corpus, with the other side derived from it rather than declared beside it -- retired by that capability and by nothing less, since deleting either declaration without deriving its operations would remove the operations its consumers call rather than unify the authority"
+}
+
+data structural_connective_stall: GuaranteeStall = GuaranteeStall {
+  subject: "std.operator_realization -- a logical connective (&&, ||) applied to a STRUCTURAL operand renders as the host token, because no declared-connective row family exists to realize or refuse it",
+  current: Mitigatable,
+  ceiling: MechanicallyPreventable,
+  blocker: AwaitsOneGrounding {
+    grounding: "a StructuralConnectiveBinding row family in std.operator_realization keyed on the operand's exact DeclarationRef (the shape StructuralOrderingBinding already has), plus its rows for the declarations this corpus uses under a connective -- v2.std.logic Bool first",
+  },
+  population: BoundedPopulation {
+    members: [
+      "a connective whose operand is a structural declaration with no host realization (v2.std.logic Bool: renders as the host token today and is the corpus's ordinary conjunction)",
+      "a connective whose operand is a structural declaration that is not a Boolean algebra at all (a Peano-shaped operand: authorable because inference constrains only the result type)",
+    ],
+  },
+  next_rung_trigger: "std.operator_realization declaring StructuralConnectiveBinding and operator_realization_for routing And/Or through it -- realizing where a row exists and refusing, typed and located, where none does; retired by that capability and by nothing less, since a roster with no consumer would leave the host token exactly where it is today"
+}

dag/gunbc/stage0/stage0_crate_partition_generated.dag

@@ -71,6 +71,8 @@ data generated_partition_crate_rows: List<GeneratedPartitionCrateRow> = [
         "std_occurrence_identity",
         "std_source_annotation",
         "std_target_representation",
+        "std_literal_elaboration",
+        "std_operator_realization",
         "v1_std_core"
       ],
       reexport_packages: [
@@ -147,6 +149,7 @@ data generated_partition_crate_rows: List<GeneratedPartitionCrateRow> = [
       kind: GeneratedLayeredCoreCrate,
       modules: [
         "gunbc_rust_source_type_bindings",
+        "gunbc_structural_realization_bindings",
         "v1_compiler_coercion",
         "v1_compiler_infer_emit_info",
         "v1_compiler_infer_env",

dag/gunbc/structural_realization_bindings.dag

@@ -0,0 +1,64 @@
+module gunbc.structural_realization_bindings
+
+import std.types { List, String, Bool, NonEmptyStr }
+import std.decl_ref { DeclarationRef, decl_ref }
+import std.literal_elaboration { LiteralHomomorphism, LiteralSourceKind, KernelIntLiteral, KernelBoolLiteral, LiteralUnfolding, PeanoUnfold, BooleanUnfold }
+import std.operator_realization { StructuralOrderingBinding }
+
+// THE CORPUS'S HALF OF LITERAL ELABORATION AND OPERATOR REALIZATION (std.literal_elaboration,
+// std.operator_realization): which of THIS corpus's structural declarations supply a kernel literal,
+// and through which of their own constructors; and which declare an ordering, and by which
+// comparison. Keyed on the exact declaration, never on a spelling: std.nat Nat (a native-realizing
+// semiring alias) and v2.std.nat Nat (the Peano coproduct) share a spelling and only the second is
+// a row here. The sibling gunbc.rust_source_type_bindings answers the OTHER question -- which
+// declarations realize natively on the Rust target -- and a declaration is never in both: a native
+// realization takes the kernel literal directly and the host operator directly.
+//
+// A ROW MAY ONLY STATE A HOMOMORPHISM THAT IS ALREADY TRUE OF THE DESTINATION, never be added to
+// make a failing site compile (the same discipline gunbc.rust_source_type_bindings and
+// v1.compiler.coercion numeric_realization_roster_extension_note hold for the native roster). The
+// Peano row is true by the definition of the naturals: n maps to succ^n(zero), and that map is the
+// unique semiring homomorphism from the kernel integers restricted to the nonnegatives.
+
+fn peano_literal_homomorphism(module_path: String, nat: String, zero: String, succ: String, prev_field: String) -> LiteralHomomorphism {
+  LiteralHomomorphism {
+    source_kind: KernelIntLiteral,
+    destination: decl_ref(module_path: module_path, decl_name: nat),
+    producer: PeanoUnfold {
+      zero: decl_ref(module_path: module_path, decl_name: zero),
+      succ: decl_ref(module_path: module_path, decl_name: succ),
+      prev_field: prev_field as NonEmptyStr
+    }
+  }
+}
+
+fn boolean_literal_homomorphism(module_path: String, bool_decl: String, true_variant: String, false_variant: String) -> LiteralHomomorphism {
+  LiteralHomomorphism {
+    source_kind: KernelBoolLiteral,
+    destination: decl_ref(module_path: module_path, decl_name: bool_decl),
+    producer: BooleanUnfold {
+      true_variant: decl_ref(module_path: module_path, decl_name: true_variant),
+      false_variant: decl_ref(module_path: module_path, decl_name: false_variant)
+    }
+  }
+}
+
+// v2.std.logic Bool = True | False is gated structural on purpose (v1.compiler.coercion
+// structural_declaration_modules_for); the corpus-wide prelude std.types Bool realizes natively and
+// is NOT a row -- a kernel true/false at that boundary stays the host bool.
+data literal_homomorphism_rows: List<LiteralHomomorphism> = [
+  peano_literal_homomorphism(module_path: "v2.std.nat", nat: "Nat", zero: "Zero", succ: "Succ", prev_field: "prev"),
+  boolean_literal_homomorphism(module_path: "v2.std.logic", bool_decl: "Bool", true_variant: "True", false_variant: "False")
+]
+
+fn structural_ordering_binding(carrier_module: String, carrier: String, compare_module: String, compare: String, ordering_module: String, ordering: String) -> StructuralOrderingBinding {
+  StructuralOrderingBinding {
+    carrier: decl_ref(module_path: carrier_module, decl_name: carrier),
+    compare: decl_ref(module_path: compare_module, decl_name: compare),
+    ordering: decl_ref(module_path: ordering_module, decl_name: ordering)
+  }
+}
+
+data structural_ordering_rows: List<StructuralOrderingBinding> = [
+  structural_ordering_binding(carrier_module: "v2.std.nat", carrier: "Nat", compare_module: "v2.std.nat", compare: "nat_compare", ordering_module: "std.algebra", ordering: "Ordering")
+]

dag/std/literal_elaboration.dag

@@ -0,0 +1,167 @@
+module std.literal_elaboration
+
+import std.types { List, String, Bool, Int, NonEmptyStr }
+import std.decl_ref { DeclarationRef, declaration_ref_eq }
+import std.syntax { LiteralValue, LitStr, LitInt, LitFloat, LitBool, LitNull, LitSymbol }
+
+// THE EXPECTED-TYPE-DIRECTED LITERAL INTRODUCTION JUDGMENT, as a model (DESIGN section 4: one
+// decision procedure, emission and ingestion are the same homomorphism check read in two directions).
+//
+// A kernel literal (`0`, `"x"`, `true`, `^s`) is a value of the KERNEL type the parser mints for it.
+// When such a literal reaches a typed boundary -- a call argument, a declared return, a record
+// field, a data initializer, an annotated let, the other operand of a binary operator -- the
+// boundary names a DESTINATION declaration. Three things can be true of that pair, and they are
+// three outcomes, never one row with a flag:
+//   DirectLiteral     the destination realizes the kernel type itself (a host numeric, the kernel
+//                     type, a native-realizing alias): the literal is already its own value.
+//   ViaHomomorphism   the destination is a STRUCTURAL declaration that SUPPLIES the literal: one
+//                     declared homomorphism from the kernel value into the destination's own
+//                     constructors (a Peano numeral into Zero/Succ, a text into a FreeMonoid of
+//                     scalars). The typed tree carries the destination and the homomorphism at the
+//                     occurrence; emission renders the image and never re-decides from spelling.
+//   Refused           the roster is defective at this key (two rows for one destination).
+// A destination with NO row and no native realization is not refused HERE: whether a kernel
+// numeral inhabits such a declaration is the inhabitance judgment's question and it already owns
+// that refusal (v1.compiler.infer declared_type_inhabitance). Answering it twice would be the two-
+// authority state DESIGN section 3 forbids; this judgment introduces values, it does not police them.
+//
+// GENERIC BY CONSTRUCTION. The judgment is keyed on (source kind, exact destination DeclarationRef)
+// and the image is produced by a closed roster of UNFOLDINGS, one arm per structural shape a kernel
+// value can be unfolded into. A consumer that needs a new destination adds one ROW to the corpus
+// roster (gunbc.structural_realization_bindings) and, if its destination's shape is new, one
+// unfolding ARM here -- never a second elaboration fold and never a per-destination special case
+// in inference or emission. The Peano arm is the first inhabitant; the FreeMonoid-of-scalars arm
+// is the structural-text lane's (XL-0T) to add beside it.
+//
+// WHY A NEGATIVE-VALUE REFUSAL IS ABSENT ON PURPOSE (DESIGN section 4b: ask whether the RED is
+// authorable before writing the check). A kernel integer literal is never negative -- `-3` parses
+// as a unary negation applied to the literal `3`, and the negation is an ordinary expression that
+// reaches inference through its own arm, not through this judgment. A ValueOutsideHomomorphismDomain
+// arm for the Peano unfolding would therefore be permanently green and would be cited as coverage.
+
+type LiteralSourceKind
+  = KernelIntLiteral
+  | KernelStringLiteral
+  | KernelFloatLiteral
+  | KernelBoolLiteral
+  | KernelSymbolLiteral
+  | KernelNullLiteral
+
+fn literal_source_kind_of(value: LiteralValue) -> LiteralSourceKind {
+  match value {
+    LitInt { value: _ } => KernelIntLiteral
+    LitStr { value: _ } => KernelStringLiteral
+    LitFloat { value: _ } => KernelFloatLiteral
+    LitBool { value: _ } => KernelBoolLiteral
+    LitSymbol { value: _ } => KernelSymbolLiteral
+    LitNull => KernelNullLiteral
+  }
+}
+
+fn literal_source_kind_label(kind: LiteralSourceKind) -> String {
+  match kind {
+    KernelIntLiteral => "kernel_int_literal"
+    KernelStringLiteral => "kernel_string_literal"
+    KernelFloatLiteral => "kernel_float_literal"
+    KernelBoolLiteral => "kernel_bool_literal"
+    KernelSymbolLiteral => "kernel_symbol_literal"
+    KernelNullLiteral => "kernel_null_literal"
+  }
+}
+
+fn literal_source_kind_eq(a: LiteralSourceKind, b: LiteralSourceKind) -> Bool {
+  literal_source_kind_label(kind: a) == literal_source_kind_label(kind: b)
+}
+
+// HOW A KERNEL VALUE IS UNFOLDED INTO A DESTINATION'S CONSTRUCTORS. Each arm names the destination's
+// own constructors by exact DeclarationRef -- the unfolding is a fact about the destination, so a
+// renamed variant is a changed row, never a stale spelling inside the compiler.
+//   PeanoUnfold    a nonnegative integer n unfolds to succ^n(zero): `succ { prev_field: ... }` nested
+//                  n deep around the nullary `zero`.
+//   BooleanUnfold  a kernel bool unfolds to the destination's nullary true or false constructor
+//                  (v2.std.logic Bool = True | False, declared structural on purpose).
+type LiteralUnfolding
+  = PeanoUnfold { zero: DeclarationRef, succ: DeclarationRef, prev_field: NonEmptyStr }
+  | BooleanUnfold { true_variant: DeclarationRef, false_variant: DeclarationRef }
+
+type LiteralHomomorphism {
+  source_kind: LiteralSourceKind
+  destination: DeclarationRef
+  producer: LiteralUnfolding
+}
+
+type LiteralHomomorphismLookup
+  = LiteralHomomorphismFound { row: LiteralHomomorphism }
+  | LiteralHomomorphismAbsent
+  | LiteralHomomorphismAmbiguous { row_count: Int }
+
+fn literal_homomorphism_for(
+  rows: List<LiteralHomomorphism>,
+  source_kind: LiteralSourceKind,
+  destination: DeclarationRef
+) -> LiteralHomomorphismLookup {
+  let matching = rows |> filter(r =>
+    literal_source_kind_eq(a: r.source_kind, b: source_kind)
+      && declaration_ref_eq(a: r.destination, b: destination))
+  let n = matching |> count
+  if n == 0 {
+    LiteralHomomorphismAbsent
+  } else if n == 1 {
+    match matching |> first {
+      Present { value: row } => LiteralHomomorphismFound { row: row }
+      Absent => LiteralHomomorphismAbsent
+    }
+  } else {
+    LiteralHomomorphismAmbiguous { row_count: n }
+  }
+}
+
+type LiteralElaborationRefusal
+  = HomomorphismDuplicated { source_kind: LiteralSourceKind, destination: DeclarationRef, row_count: Int }
+
+fn literal_elaboration_refusal_message(cause: LiteralElaborationRefusal) -> String {
+  match cause {
+    HomomorphismDuplicated { source_kind: k, destination: d, row_count: n } =>
+      concat(
+        "literal elaboration: ", literal_source_kind_label(kind: k), " into ",
+        d.module_path as String, ".", d.decl_name as String,
+        " has more than one declared homomorphism (gunbc.structural_realization_bindings authoring defect)"
+      )
+  }
+}
+
+// THE DECISION. `destination_realizes_natively` is the caller's answer to "does this declaration
+// realize the kernel type itself" (v1.compiler.coercion decl_file_realizes_natively / the exact
+// Rust binding), passed in rather than re-derived so this module stays target-agnostic.
+type LiteralElaborationOutcome
+  = DirectLiteral
+  | ViaHomomorphism { homomorphism: LiteralHomomorphism }
+  | LiteralElaborationRefused { cause: LiteralElaborationRefusal }
+
+fn elaborate_literal_at(
+  rows: List<LiteralHomomorphism>,
+  source_kind: LiteralSourceKind,
+  destination: DeclarationRef,
+  destination_realizes_natively: Bool
+) -> LiteralElaborationOutcome {
+  if destination_realizes_natively {
+    DirectLiteral
+  } else {
+    match literal_homomorphism_for(rows: rows, source_kind: source_kind, destination: destination) {
+      LiteralHomomorphismFound { row: row } => ViaHomomorphism { homomorphism: row }
+      LiteralHomomorphismAbsent => DirectLiteral
+      LiteralHomomorphismAmbiguous { row_count: n } =>
+        LiteralElaborationRefused { cause: HomomorphismDuplicated { source_kind: source_kind, destination: destination, row_count: n } }
+    }
+  }
+}
+
+// WHAT THE TYPED TREE CARRIES at an elaborated occurrence: the source kind, the exact destination,
+// and the homomorphism selected. The occurrence itself is the node this record sits on (its
+// occurrence identity), so it is not duplicated here. Only ViaHomomorphism occurrences carry a
+// record -- a DirectLiteral is the ordinary literal node and needs nothing said about it.
+type LiteralElaboration {
+  source_kind: LiteralSourceKind
+  destination: DeclarationRef
+  homomorphism: LiteralHomomorphism
+}