Prove arbitrary propagator traces over caller programs

[kim-em]

Outcome

This PR proves package-owned fact, instantiation, and equality evidence into an ordinary-kernel theorem over the caller-owned base program. It also makes the SPEC primarily a design for an arbitrary-function propagator engine, rather than an endpoint-arithmetic project.

Framework contract

• opaque generic fact domains with a companion semantic boundary;
• independently assembled function packages with stable operation, rule, relation, payload, and feature schemas;
• local and arbitrary-scope applications using the same action, queue, policy, resource, and replay machinery;
• grind-shaped but engine-owned bounded structural matching, whose matches may atomically add expressions, equalities, and propagator applications;
• append-stable network/application identity and chronological replay deltas, including scope-only events;
• package-owned scope validation, causal generation, exact structural-input provenance, and resource-first policy views;
• one bounded report envelope for multi-output facts, contradiction/inner claims, retries, instantiation, refinement, and splitting;
• an atomic two-child branch transition as the next framework milestone;
• a tactic/package extension boundary that quotes only the backwards proof slice;
• verified raster graphs and certified ODE solvers as downstream applications.

The implementation experiment for dynamic arbitrary-scope instantiation is staged separately in #9081 and #9082. This replay branch records the contract that those binding/application deltas must satisfy and rejects forged identities.

Priority and open design

Rational planning, projection, conformance, and benchmarks are now a separate deferred, non-gating backend track. Before that work resumes, the framework must complete a replayed non-polynomial sine package and the atomic branch transition. The SPEC deliberately leaves physical arenas, matcher indexes/certificates, scope anchors, binding tombstones versus append-stability witnesses, branch storage, scheduling scores, and endpoint backends open to experiment.

The design does not rely on native_decide and does not plan grind integration in this phase.

Verification

lake build HexIntervalExperiment \
  HexInterval.PropagatorE2EConformance \
  HexInterval.SemanticReplayConformance \
  HexInterval.PolicySessionConformance

The 855-job target graph passes, and git diff --check is clean.

Review focus

• authority and replay completeness for dynamic applications and structural matcher inputs;
• compositional package validation under network extension;
• generic fact/claim semantics without leaking dyadic or rational assumptions;
• branch isolation, complementary-child replay, and global-bound reporting;
• whether the remaining choices are correctly left open for measurement.