Add proof-producing policy sessions

[kim-em]

What changed

• adds a private-constructor policy session which owns the policy state and engine, exact heterogeneous package registry, immutable payload arena, and all limits;
• routes selected invocation and retry plans through the exact handler-owned sealed ReplaySnapshot.freeze operation and commits the arena only after policy-state admission;
• supports invocation, retry, centered instantiation, equality contraction, dismissal, and split choices without accepting separable engine, registry, or arena inputs;
• preserves the merged generic completeness invariant through shared Suggestion.affectsClosure and the engine-owned exact kept/dropped suggestion boundary;
• treats malformed evidence and package-local payload uses, atom, and schema excess as consumed failed replies which remain live and incomplete, while whole-run entries and bodyCells exhaustion is fatal.

Conformance

The policy-owned end-to-end canary instantiates the centered form, admits and contracts its equality, exercises every choice class, retains exact fact/instance/equality recipes, rolls back an engine-rejected prospective freeze, rejects malformed and undeclared formats atomically, distinguishes all five payload resource classes, and proves an empty failed frontier is incomplete rather than saturated.

Validation

• lake build HexInterval.PolicyConformance HexInterval.PolicyDriverConformance HexInterval.PolicyFrontierConformance HexInterval.PackageRegistryConformance HexInterval.PayloadArenaConformance HexInterval.PayloadSessionConformance HexInterval.DyadicIntervalConformance HexInterval.DyadicRulesConformance HexInterval.PolicySessionConformance HexIntervalExperiment
• git diff --check origin/agent/interval-package-replay
• added-line and touched-Lean scans for native_decide, axiom, and sorry

Stack

Draft stacked on #9040 (agent/interval-package-replay).