Item 1: Persistence of the certified core minimum

Containment of the core homothet is linear in the reference at fixed coefficient, so whether a declared core minimum is satisfiable at a date is one linear program (NL-SI-A2, NL-SI-A3). What is open is the infimum over dates: whether a declared minimum keeps being satisfiable as settlement contracts the region. NL-SI-A4 shows no finite family of per-date checks decides it, and NL-SI-A7 shows both outcomes occur on small instances.

Deliverable shape: lean-proved in Workspace.Normativity.Contrib, or witness-checked for the negative direction. Acceptance check: The Lean gate builds and audits clean; or the witness checker accepts the trajectory with the violates-at-least-one property.

Context: projects/normativity/consolidation-aug9/THEORY_11_SETTLEMENT_INTERFACE.md §5. A solution ships: either a proof that a positive minimum persists under stated conditions, with necessity witnesses for those conditions; or a displayed trajectory driving it to zero under conditions the interface permits.