Rename the Connective arm Cardinality to Occupancy: one name, one meaning (re-derives #13377)

dag/gunbc/instruments/type_declaration_use_census.dag

@@ -8,7 +8,7 @@ import v2.std.logic { Bool }
 import v2.std.text { String }
 import v2.std.node {
   Edge, Authored, StructuralLabel, Positional, Node, Symbol, symbol_lexeme, node_subtree_nodes,
-  TypeNode, ComputationNode, Atom, Conj, Disj, Arrow, Cardinality, Instantiation,
+  TypeNode, ComputationNode, Atom, Conj, Disj, Arrow, Occupancy, Instantiation,
   Transform, Value, Branch, Loop, Bind, Match
 }
 import v2.std.type_binder { GenericTypeDecl, OpaqueTypeDecl, PlainTypeDecl, TypeAlias, type_decl_view, type_param_names }
@@ -190,7 +190,7 @@ fn tdc_generic_form(name: Symbol, target: Node, kinds: FreeMonoid<DeclaredTypeKi
             Conj => tdc_member_form(name: name, member: m, kinds: kinds)
             Atom { identity: _ } => FormUndecided
             Arrow => FormUndecided
-            Cardinality => FormUndecided
+            Occupancy => FormUndecided
             Instantiation => FormUndecided
           }
         ComputationNode { behavior: _ } => FormUndecided

dag/gunbc/plans/for_while_loop_sugar.dag

@@ -59,7 +59,7 @@ fn section_2_s0() -> List<MarkdownBlock> {
       li(text: "**The fold call lowers to the full fold encoding (S3).** `v2.compiler.fold_lowering` `fold_recurrence_encoding` builds the §2.3 encoding from the call's operands, and `v2.compiler.body_lowering_fold` `body_lower_fold_encoding` fills it from their lowered forms. No interpreter executes it yet (S0's interpreter half)."),
     ]),
     h3(text: "2.2 The one extension: a domain edge"),
-    p(text: "Pointwise iteration needs something to iterate. No existing structure instantiates a body once per member: `Cardinality` and `Instantiation` are *type* connectives, not computations. So the choice is between a seventh behavior and one more named edge on `Loop`. A seventh behavior would break the closed vocabulary of DESIGN §4, so the answer is the edge:"),
+    p(text: "Pointwise iteration needs something to iterate. No existing structure instantiates a body once per member: `Occupancy` and `Instantiation` are *type* connectives, not computations. So the choice is between a seventh behavior and one more named edge on `Loop`. A seventh behavior would break the closed vocabulary of DESIGN §4, so the answer is the edge:"),
     ul(items: [
       li(text: "**`^loop_domain_edge`** (new, optional, at most one): its target is the value being iterated. Its presence is what makes a `Loop` iterate members rather than evaluate once."),
       li(text: "**`^loop_realized_declaration_edge`** (added with S3, optional, at most one): its target is the AUTHORED callee occurrence of a desugared recurrence, such as the `fold` in `fold(xs, init, step)`. Resolve must bind it to the declaration whose recurrence the `Loop` realizes, or refuse at the head (`v2.compiler.resolve` `resolve_realized_declaration`). For the collection `fold`, that is the operation `std.algebra` `collection_fold_shape`, which binds only when nothing in the lookup chain binds the spelling. For `fold_list`, it is the declaration the chain must bind exactly. **Why it exists:** desugaring runs before resolve and is keyed on the callee's spelling. Without this edge, a user's own `fold` would be silently rewritten as the collection operation, and the authored head would be dropped from the tree. It is named for its role, not for fold. `for`, `while` and unary `loop` never carry it, because the language fixes their meaning and they name no declaration."),

dag/gunbc/recurring_failure_mode/argument_type_obligation_absent_while_the_route_advances.dag

@@ -15,7 +15,7 @@ data argument_type_obligation_absent_while_the_route_advances: RecurringFailureM
 
     "RECOGNITION RULE: an application whose argument type is derived and a distinct constructor from the formal is Accepted. The discriminating RED is v2.test.claim.compiler.infer_application_argument_inhabitance_witness_test infer_incompatible_argument_refuses_holds (Bool at an Int formal). Positive control: infer_compatible_argument_admits_holds.",
 
-    "RUNG FOUND AT, source to interpretation (v2.compiler.infer consuming declared_type_inhabitance): mechanically preventable for a structurally unequal pair of derived type nodes (Bool at Int refuses with application_argument_does_not_inhabit). Unjudgeable applications that infer reaches (ArgumentTypeNotDerived, FormalUnresolved, GenericFormal) are InhabitanceUndecidable on the Accepted path, counted, not silent. Since 2026-09-27 GenericFormal means a formal that MENTIONS one of the callee's declared type variables (DeclaredTypeObligation.type_variables, read off the Arrow by v2.std.type_binder type_param_names); an Instantiation whose constructor and arguments are all established is decided by the same structural zip, so a `List<Int>` formal is judged rather than counted (a product argument at it now refuses, inhabitance_product_produced_at_a_collection_formal_refuses_holds). The declared side is read at its denotation (v2.extdeps.languages.dag dag_binding_denotation over each atom), and a bare declared atom that join does not denote is counted FormalUnresolved. The same relation now has a second producer, PositionDeclaredReturn: v2.compiler.infer infer_arrow_declared_return_check judges each Arrow body at its declared return and REPLACED the inline equality check #12379 had put on arrow introduction (infer_arrow_body_inhabits_declared_return, deleted; its reason arrow_body_does_not_inhabit_declared_return is kept, located at the body). Before the replacement a return that join did not denote was admitted with no diagnostic; it is now counted. Witnesses: v2.test.claim.compiler.infer_declared_return_inhabitance_witness_test (RED declared_return_int_with_a_bool_body_refuses_holds, controls declared_return_int_with_an_int_body_admits_holds and declared_return_bool_with_a_bool_body_admits_holds) and v2.test.claim.compiler.infer_arrow_elimination_witness_test. OptionalCarrier is enrolled on v2.std.inhabitance inhabitance_node_undecidable_reason (inhabitance_cardinality_type_is_optional_carrier_holds). A TypeNode Cardinality formal reaches that counted frontier on infer: connective_multiplicity maps Cardinality to Bounded (a type node owes only its structural fold; repetition enters only through Loop), so the application is judged and counted as OptionalCarrier on the Accepted path (infer_optional_formal_reaches_optional_carrier_frontier_holds). That is not inhabitance-by-widening and not 'every reached application is judged'.",
+    "RUNG FOUND AT, source to interpretation (v2.compiler.infer consuming declared_type_inhabitance): mechanically preventable for a structurally unequal pair of derived type nodes (Bool at Int refuses with application_argument_does_not_inhabit). Unjudgeable applications that infer reaches (ArgumentTypeNotDerived, FormalUnresolved, GenericFormal) are InhabitanceUndecidable on the Accepted path, counted, not silent. Since 2026-09-27 GenericFormal means a formal that MENTIONS one of the callee's declared type variables (DeclaredTypeObligation.type_variables, read off the Arrow by v2.std.type_binder type_param_names); an Instantiation whose constructor and arguments are all established is decided by the same structural zip, so a `List<Int>` formal is judged rather than counted (a product argument at it now refuses, inhabitance_product_produced_at_a_collection_formal_refuses_holds). The declared side is read at its denotation (v2.extdeps.languages.dag dag_binding_denotation over each atom), and a bare declared atom that join does not denote is counted FormalUnresolved. The same relation now has a second producer, PositionDeclaredReturn: v2.compiler.infer infer_arrow_declared_return_check judges each Arrow body at its declared return and REPLACED the inline equality check #12379 had put on arrow introduction (infer_arrow_body_inhabits_declared_return, deleted; its reason arrow_body_does_not_inhabit_declared_return is kept, located at the body). Before the replacement a return that join did not denote was admitted with no diagnostic; it is now counted. Witnesses: v2.test.claim.compiler.infer_declared_return_inhabitance_witness_test (RED declared_return_int_with_a_bool_body_refuses_holds, controls declared_return_int_with_an_int_body_admits_holds and declared_return_bool_with_a_bool_body_admits_holds) and v2.test.claim.compiler.infer_arrow_elimination_witness_test. OptionalCarrier is enrolled on v2.std.inhabitance inhabitance_node_undecidable_reason (inhabitance_occupancy_type_is_optional_carrier_holds). A TypeNode Occupancy formal reaches that counted frontier on infer: connective_multiplicity maps Occupancy to Bounded (a type node owes only its structural fold; repetition enters only through Loop), so the application is judged and counted as OptionalCarrier on the Accepted path (infer_optional_formal_reaches_optional_carrier_frontier_holds). That is not inhabitance-by-widening and not 'every reached application is judged'.",
 
     "RUNG FOUND AT, source to native emission: unclaimed. Native emission stays a declared frontier until v2.std.inhabitance is in the native 04_infer closure and infer_incompatible_argument_refuses_holds refuses on the emitted binary.",
 

dag/gunbc/recurring_failure_mode/generic_formal_containing_a_type_variable_unjudged.dag

@@ -14,7 +14,7 @@ data generic_formal_containing_a_type_variable_unjudged: RecurringFailureMode =
 
     "REPAIR (climb): v2.compiler.infer infer_judge_generic_formal matches the formal first-order against the argument's derived type (infer_match_generic_formal: same constructor and arity, recursing pairwise; a bare variable binds its first instance through the existing TypeVariableInstance list), instantiates the formal (infer_type_instantiated), and hands it to the SAME declared-position judge every formal uses. A constructor or arity mismatch refuses there with application_argument_does_not_inhabit, located at the application. No second inhabitance relation is introduced. Controls: v2.test.claim.compiler.generic_formal_instantiation (three REDs that were accepted at the base, two accepted controls).",
 
-    "RUNG FOUND AT: below the floor (silently admitted). RUNG NOW: structurally guaranteed for a formal whose type variables sit inside Instantiations. RESIDUE, STATED: a type variable inside a shape this match does not open -- an Arrow (`f: fn(T) -> T`), an optional (`T?`), a type variable in constructor-head position -- still reaches the judge mentioning a variable and stays UndecidableGenericFormal, admitted with the counted advisory. CEILING: structurally guaranteed (decidable over modeled types). NEXT-RUNG TRIGGER, NAMED AS A CAPABILITY: first-order matching of a generic formal through every type connective v2 infer derives (Arrow domains and codomains, Cardinality), sufficient for every generic formal whose argument type is derived to be judged rather than admitted.",
+    "RUNG FOUND AT: below the floor (silently admitted). RUNG NOW: structurally guaranteed for a formal whose type variables sit inside Instantiations. RESIDUE, STATED: a type variable inside a shape this match does not open -- an Arrow (`f: fn(T) -> T`), an optional (`T?`), a type variable in constructor-head position -- still reaches the judge mentioning a variable and stays UndecidableGenericFormal, admitted with the counted advisory. CEILING: structurally guaranteed (decidable over modeled types). NEXT-RUNG TRIGGER, NAMED AS A CAPABILITY: first-order matching of a generic formal through every type connective v2 infer derives (Arrow domains and codomains, Occupancy), sufficient for every generic formal whose argument type is derived to be judged rather than admitted.",
   ],
 
   evidence: [

dag/gunbc/recurring_failure_mode/optional_admitted_where_a_required_value_is_declared.dag

@@ -17,7 +17,7 @@ data optional_admitted_where_a_required_value_is_declared: RecurringFailureMode
     "POPULATION OF THE SECOND LANDING (the whole-root compile differential; the instrument is named on gunbc.rung_drop.compiler_change_refusals_land_outside_every_compiled_closure, `gunbc compile --source-root dag --source-root src/v2 --target dag --repository gunbc --measured-root-demands tools/whole_corpus_compile_measured_root_demands.json`, base and head run sequentially on one frozen tree and joined on verbatim message plus location). Every newly refused identity is listed on the change that filed this receipt, each repaired or dispositioned there; the counts are that join's and are not restated here. The shapes: `.first()` / `.last()` / `first(..)` consumed as the element behind a length guard (the large majority, as in the first landing); `parse_int` into an Int field twice more, the exact specimen; a `T?` policy field read as `T`; and one explicit `Present { .. }` wrapper returned where the coproduct itself was declared. SCOPE, stated because it is narrower than WHOLE CORPUS: the join covers the dag-primary population only. A src/v2-primary whole-root compile refuses at admission with WholeCorpusCompileUnmeasuredRoot, so src/v2 modules are covered only where the dag root reaches them, and the modules that compile enters in the name census only are not covered at all. Both are UNMEASURED populations, not zeros: nothing here says they hold no optional at a required position.",
     "THE INDEX CARVE-OUT WAS A DECLARED RESIDUAL OF SIX MEASURED MEMBERS AND IS DISCHARGED. v1.tokenize source_code_point and code_point_at (declared returns) and gunbc.floor_cost_distribution parse_claim_cost_line (four record-literal fields) stood admitted by v1.compiler.infer expr_value_is_index_access while the Rust realization of `xs[i]` was the bare element. Its trigger, typing and realization agreeing, landed on the Rust target (gunbc.recurring_failure_mode list_index_typed_optional_but_realized_as_the_bare_element, CLIMB): the predicate is deleted, code_point_at is deleted, source_code_point answers `Int?`, and the floor-cost fields are bound by a match. ENROLLED: test.claim.optional_at_required_position_witness_test an_index_access_at_a_required_position_refuses, flipped from the admission it used to pin.",
     "RESIDUALS, named. (1) The index population above. (2) Arguments of BUILTIN and method calls: the direct-call seam judges declared functions, so `parse_int(s: lines.first())` and join's receiver are unjudged. (3) A list literal whose HEAD element is optional elects List<T?>. (4) The five DeclaredTypePosition members with no producer (map value, variant payload, cast target, parameter default, callable return). (5) The interpreter's String-context rendering of a variant, unchanged from the first landing. (6) The v2 judge: v2.std.inhabitance answers UndecidableOptionalCarrier for a cardinality node on EITHER side and v2.compiler.infer admits that verdict, so v2 admits an optional at a required position; read from source, not executed, and reported to the owning lane rather than repaired here.",
-    "THE V2 ROUTE, a separate path with its own rung (2026-09-30). v2.std.inhabitance declared_type_inhabitance carried the same misfiling: inhabitance_node_undecidable_reason answered UndecidableOptionalCarrier for a Cardinality type node on EITHER side, so a produced T? at a declared required type was admitted with an advisory. It was not reachable from source until gunbc#12777, because infer refused any tree carrying a Cardinality node for descent first (measured on main and on gunbc#12566: infer_descent_not_derived for `fn f(x: Int?) -> Int { x }`); with that change the program was ACCEPTED. The relation now refuses the pair by its own reason, inhabitance_optional_produced_at_required_declared. CURRENT RUNG on the v2 resolve-to-infer route: structurally guaranteed where the declared type is a kernel value type (an atom the judge denotes), at a declared return and at a record field, both executed from source text by v2.test.claim.compiler.infer_optional_at_required_witness_test. COUNTED, NOT REFUSED: a produced optional at a declared declaration reference, a declared Instantiation or a declared type variable, because the relation unfolds no alias and cannot know those are required (`type Maybe = Int?` is a declaration reference); trigger: the relation reads a declared type's resolved declaration, the capability gunbc#12726 PR2 provides. NOT YET ON THE ROUTE: a direct-call argument, because a named call's callee is not typed by its declaration (gunbc#12506); the relation refuses the pair, and the route claim is owed when that lands.",
+    "THE V2 ROUTE, a separate path with its own rung (2026-09-30). v2.std.inhabitance declared_type_inhabitance carried the same misfiling: inhabitance_node_undecidable_reason answered UndecidableOptionalCarrier for an Occupancy type node on EITHER side, so a produced T? at a declared required type was admitted with an advisory. It was not reachable from source until gunbc#12777, because infer refused any tree carrying an Occupancy node for descent first (measured on main and on gunbc#12566: infer_descent_not_derived for `fn f(x: Int?) -> Int { x }`); with that change the program was ACCEPTED. The relation now refuses the pair by its own reason, inhabitance_optional_produced_at_required_declared. CURRENT RUNG on the v2 resolve-to-infer route: structurally guaranteed where the declared type is a kernel value type (an atom the judge denotes), at a declared return and at a record field, both executed from source text by v2.test.claim.compiler.infer_optional_at_required_witness_test. COUNTED, NOT REFUSED: a produced optional at a declared declaration reference, a declared Instantiation or a declared type variable, because the relation unfolds no alias and cannot know those are required (`type Maybe = Int?` is a declaration reference); trigger: the relation reads a declared type's resolved declaration, the capability gunbc#12726 PR2 provides. NOT YET ON THE ROUTE: a direct-call argument, because a named call's callee is not typed by its declaration (gunbc#12506); the relation refuses the pair, and the route claim is owed when that lands.",
     "HARM: silent wrongness, outside the ladder -- the output is plausible bytes, not a crash, and it was committed as a fixture by an automated heal.",
     "RUNG FOUND AT: silent, below the floor. CURRENT RUNG, at the grain of source to v1 acceptance: structurally guaranteed for a non-index optional value at the direct-call argument, declared list element, undeclared list-literal member, record-literal field, declared return (trailing expression and early return), let annotation and data initializer -- DeclaredTypeNotInhabited naming position, subject, declared and produced types with cardinality. Silent at the residual positions above, so the class as a whole is not at that rung and this row does not claim it. CEILING: structurally guaranteed (typecheck refusal); decidable from the two resolved types.",
     "NEXT-RUNG TRIGGERS, as capabilities. FIRST (discharged on the Rust target, see the carve-out receipt above): the index model and its realization agree. SECOND: variant-reference election consults the declared coproduct, sufficient to delete the by-name-only exclusion. THIRD: builtin and method call arguments raise a DeclaredTypeObligation. FOURTH: the four cardinality-only positions hand their obligation to declared_type_obligation_diags, deleting their older chains. Fixtures: test.claim.optional_at_required_position_witness_test.",