Licensing: migrate remaining files to the dual SPDX header (MPL-2.0 + CC-BY-SA-4.0)

[hyperpolymath]

Context

PR #58 set the standard: every source file carries two SPDX lines —
SPDX-License-Identifier: MPL-2.0 and SPDX-License-Identifier: CC-BY-SA-4.0 —
with the root LICENSE (MPL-2.0) as the GitHub community-health marker. See
LICENSING.adoc and .machine_readable/licensing-policy.toml.

Done in #58 (7 files): academic/formal-verification/{agda/*.agda, coq/Phronesis.v, lean4/*.lean} and .github/workflows/{scorecard,secret-scanner}.yml.

Pending: the remaining estate-authored files still carry a single SPDX line
(~214 MPL-2.0 + ~75 CC-BY-SA-4.0 at last census). They need the second line added.

Constraints (estate guardrail — important)

• Manual / per-file / owner-directed only. No bulk sed/script/agent SPDX
  sweep (per standards LICENCE-POLICY.adoc Addendum A2 and the neurophone#99
  post-mortem). Migrate in reviewed batches.
• Preserve each file's comment syntax: # (yaml/toml/sh/ex), -- (agda/lean/sql),
  (* … *) (coq), // (rust/adoc), ;; (scheme).
• Third-party / vendored (deps/**) is excluded — never touch upstream SPDX.
• Add the second line directly beneath the existing one; do not reorder.

Suggested approach

Batch by file class (one reviewable PR each): Elixir lib/ + test/; Rust
compiler/; formal/ + spec/; academic/ prose; wiki/; docs/; root
authority docs; .machine_readable/. Update the [migration] block in
licensing-policy.toml as batches land.

Acceptance

• Every estate-authored file carries both SPDX lines.
• LICENSING.adoc migration section flips from "in transition" to "complete".
• Root LICENSE unchanged (MPL-2.0 marker).