Register package-owned interval replay formats

[kim-em]

Purpose

Let arbitrary function handlers own the representation formats for their proof payloads without adding a central arithmetic or function switch to the engine.

What this establishes

• the exact replay address is (RuleKey, role, payload schema);
• RuleKey.schema is the handler/theorem compatibility epoch, while payload schema is a recipe variant within that epoch;
• each handler registers immutable, cache-independent role/schema/body validators;
• registry, replay-snapshot, and invocation constructors are private;
• the session freezes through one sealed replay snapshot, so owner and validator cannot be mixed independently on the proof-producing path;
• duplicate formats are rejected during bounded registry assembly;
• executable operations, aggregate registry metadata, and replay declarations have independent caps;
• invokePlanned returns the plan together with the exact selected handler replay snapshot;
• generic arena bounds and coverage run before package body validation;
• undeclared formats and malformed bodies fail atomically;
• two unrelated opaque packages safely reuse the same numeric schema with different validators;
• all real dyadic and centered handlers declare exact empty-body schema-zero formats and run through the proof session.

These validators check representation shape only. Package-owned semantic checkers and soundness theorems are the next layer; caches and search policy remain outside replay. Compatibility of a changed callback under an existing rule epoch is explicitly a future semantic-replay obligation, not a property claimed by this layer.

Verification

• lake build HexInterval.Experiment.PackageRegistry HexInterval.Experiment.PayloadSession HexInterval.PackageRegistryConformance HexInterval.PayloadSessionConformance HexInterval.DyadicRulesConformance HexIntervalExperiment
• directly affected Propagator/StructureView/Policy/DyadicInterval conformance and scheduler bench targets
• git diff --check
• no added native_decide, axiom, or sorry

Stacked on #9038.