promotion to the specification layer: `J`, `E ⊨ J`, `L_t`, the fidelity interface, `V_J` and `S_J` (R9)

Maintainer ruling, landed by the phase-2 round and closing the phase-1 queue's promotion entry. The specification layer gains lean/Workspace/Deference/Spec/Headline.lean (recorded in tests/spec_shape.json): the allocation of authority with its licensed acts, effective realization with the control surface and the shortfall, legitimacy L_t in general form on GateIsLegitimacy.Segment, the fidelity interface as an abstract count (zero exactly on faithful histories, the part recognized in advance marked; counts on one history add; the frame's violations instantiated; no composite model), the evaluator and the fidelity score per decision and per history. Agent-decided, reversible: promotion is by re-declaration under the promoted names with instantiation theorems, the landed originals unchanged — moving them would rename landed declarations and break the axiom audit's baseline. Everything else stays in contribution namespaces. Rejected alternative: moving the landed declarations physically.