Records the runtime-axis dual of ownership totality (model 0008). 0008
totalises the *annotation* (own/borrow everywhere, no Implicit) but keeps
universal RC as the floor; 0009 asks the question totality makes askable
— must the runtime discipline stay universal, or can it follow the type?
Principle: RC is authored, never universal. Default `box` (affine,
refcount-free, deterministic scope-drop ≈ Box); opt-in `rc` (refcounted,
explicit `share` ≈ Rc). Motivated by the maintenance record: ~1/3 of
recent commits touch RC/ownership/drop, no bug was ever in the RC runtime
itself — all lived in the inference (uniqueness-elision, is_rc_heap_allocated,
mode-through-subst) that exists only to reconcile affine ownership with
universal RC and strip the RC it over-charges.
Soundness leans on existing law: the 0015 DAG constraints + linear-by-
default already draw the "needs-a-count" partition; `rc` only names it.
No cycle collector reappears (rc graphs stay acyclic). No `&mut` mode:
in-place mutation rides consume-and-return (move, not alias), so
constraint 3 (immutable-once-constructed) holds — `mut` is out by
principle. §5 enumerates what leaves the compiler (uniqueness-elision,
is_rc_heap_allocated term-shape predicate, over-strict lint, reuse-as,
escape-clawback) and what stays (the affine/linearity check, already
present).
Status-stamped NOT current state, per the honesty rule and the 0008
precedent; INDEX.md left untouched (exploration whitepapers are not on the
canonical spine until adopted). Composes with 0008 regime A, which already
makes transitive box-drop sound. §8 isolates the open questions (closure
capture move/share, clone-vs-share split, coupling to 0008's escape pass,
keyword spelling, sharing-heavy workloads).
Brummel
9848d4b2df