interval: replay repeated instantiations generically

[kim-em]

Summary

• carry dependent program, version, prefix, extension, and fact-proof state through the emitted chronology
• reconstruct every instantiation as an exact prefix of the quoted final graph
• use one semantics-wide stability law to lift all existing fact evidence
• seed only each event's exact fresh-node suffix
• support later, repeated, and zero-node instantiations without function cases
• keep independently carried program versions load-bearing

Experiment

A second zero-node instantiation runs after the sine and negation rules. The emitter lifts the proved negation fact through that version transition and then consumes it in equality transport. An oversized repeated instance is rejected.

The printed tacticSine term contains transparent GenericInstanceReconstruction.reconstruct? and none of the named sine previous-fact constants; the diagnostic print was removed after inspection.

Verification

• lake build HexIntervalMathlib.SineTacticConformance (1,957 targets)
• copyright, line-count, DAG, and diff checks
• changed Lean contains no native_decide, axiom, or sorry

Stack

Depends on #9205.