matters enter the Lean spine abstractly

Agent-decided, reversible. The formalization takes M : ℕ → Finset Q with two fields, monotonicity and priority (m ∈ M n → ∃ j < n, m ∈ Born j), rather than the paper's construction from roots and designations, because the theorems consume only those two facts and stating the construction would import the Designate judgment into hypotheses that do not read it. Proving the construction satisfies the fields is left as an obligation (THEOREM_MAP.md). The alternative, a concrete M, was rejected as hiding a dependency the proof-pass table was built to expose.