interval: replay repeated instantiations generically

HexInterval/Experiment/ProofEmitter.lean

@@ -152,6 +152,44 @@ def assumedAt {Fact : Type} {semantics : Semantics Fact} (program : Program)
     Evidence (semantics.Entails program base fact) :=
   assumed (memOfGet? base index fact found)
 
+/-- The node of a caller fact selected by `assumedAt` is within the current
+program whenever the complete base list is. -/
+theorem factWithinAt {Fact : Type} (program : Program)
+    (base : List (NodeFact Fact)) (within : FactsWithin program base)
+    (index : Nat) (fact : NodeFact Fact) (found : base[index]? = some fact) :
+    fact.node.index < program.nodes.size :=
+  within fact (memOfGet? base index fact found)
+
+/-- A successful exact node lookup proves the corresponding size bound. -/
+theorem nodeWithin (program : Program) (node : NodeId) (instruction : Node)
+    (found : program.node? node = some instruction) :
+    node.index < program.nodes.size := by
+  by_cases within : node.index < program.nodes.size
+  · exact within
+  · simp [Program.node?, within] at found
+
+/-- Old node membership remains valid across an append-only prefix. -/
+theorem liftNode {before after : Program} (step : ProgramPrefix before after)
+    {node : NodeId} (within : node.index < before.nodes.size) :
+    node.index < after.nodes.size :=
+  Nat.lt_of_lt_of_le within step.nodeSize
+
+/-- A complete base context remains within every append-only program. -/
+theorem liftFacts {Fact : Type} {before after : Program}
+    (step : ProgramPrefix before after) {facts : List (NodeFact Fact)}
+    (within : FactsWithin before facts) : FactsWithin after facts :=
+  fun fact member => liftNode step (within fact member)
+
+/-- Transport one table entry to an enlarged program. -/
+def liftFact {Fact : Type} {semantics : Semantics Fact}
+    {before after : Program} {base : List (NodeFact Fact)}
+    {fact : NodeFact Fact} (step : StableStep semantics before after)
+    (baseWithin : FactsWithin before base)
+    (sound : Evidence (semantics.Entails before base fact))
+    (factWithin : fact.node.index < before.nodes.size) :
+    Evidence (semantics.Entails after base fact) :=
+  liftEntails step baseWithin factWithin sound
+
 /-- Prove the domain's top fact for any exactly checked node.  The chronology
 emitter uses this theorem to seed generated nodes at version zero; that
 generated/version condition belongs to its evidence-table discipline, not to

HexInterval/SPEC/hex-interval.md

@@ -1248,9 +1248,13 @@ central case split over function keys. The transparent
 the exact prefix of the retained final node array selected by
 `event.newNodes`, keeps the operation table fixed, and obtains stability from
 one semantics-wide prefix-locality law. It covers both ordinary node appends and
-zero-node version-only instances. Integrating this arm into `TraceReplay` and
-comparing it with package-dispatched reconstruction remains experimental.
-Neither arm may introduce a central enumeration of functions.
+zero-node version-only instances. The direct proof emitter now uses this arm
+at every quoted instantiation event: it replays the owning package's
+conservative-extension theorem, lifts every retained fact proof through the
+semantics-wide stability law, and seeds exactly the event's fresh nodes with
+top. Integrating the same arm into runtime `TraceReplay` and comparing it with
+package-dispatched reconstruction remains experimental. Neither arm may
+introduce a central enumeration of functions.
 
 The private chronological cursor is indexed by its exact program version and
 program value. Its instance transition requires the originating action to
@@ -1316,45 +1320,50 @@ yet the general tactic. Its elaborator walks the arbitrary quoted event list
 and maintains an exact `(node, version)` evidence table. Rule and transport
 steps obtain their previous facts and ordered dependencies from this table,
 select their package schemas solely by replay address, and insert their proved
-result versions. The fold carries the program version established by the
-instance event rather than trusting each later fact event's claimed version.
-Reordering negation before the sine result it consumes, or mutating a
-transport to a different program version, fails before replay. This event fold
-contains no sine, negation, or other function case. It seeds caller facts by
-checked position in the emitter's declared base-assumption list; the caller
-hypotheses supplied to final closure discharge that same list. This direct
-emitter does not yet construct the `InitialContext` witness that relates the
-declared list position-for-position to `CheckerInput.initialFacts`. The
-complete `TraceReplay` checker already constructs its `initialBase`
-position-for-position from `CheckerInput.initialFacts`; separately,
+result versions. The same fold accepts instantiation events at arbitrary
+chronology positions. It reconstructs each intermediate graph as the exact
+prefix of the reified final program, carries the independently established
+program version, transports the complete evidence table across stability, and
+then seeds the new-node suffix. A second zero-node instance can therefore
+advance the version after the sine and negation rules while preserving the
+negation evidence needed by a later equality transport. Reordering negation
+before the sine result it consumes, or claiming the wrong program version,
+fails before replay. This event fold contains no sine, negation, or other
+function case. It seeds caller facts by checked position in the emitter's
+declared base-assumption list; the caller hypotheses supplied to final closure
+discharge that same list. This direct emitter does not yet construct the
+`InitialContext` witness that relates the declared list position-for-position
+to `CheckerInput.initialFacts`. The complete `TraceReplay` checker already
+constructs its `initialBase` position-for-position from
+`CheckerInput.initialFacts`; separately,
 `ChronologicalReplay.Cursor.startInput` consumes `InitialContext` for cursor
 replay. The later generic frontend must carry the corresponding binding into
 direct emission. The current replay applications and final closure remain
 indexed by the exact `CheckerInput.baseProgram` and target. The emitter also
-seeds the instance event's fresh nodes with domain top after checking their
+seeds each instance event's fresh nodes with domain top after checking their
 lookup in the reified final program; named sine-specific previous-fact proofs
 are absent from the tactic term. The next frontend experiment must derive the
 base program, declared base-assumption list and its caller-input binding,
-semantic bridge, and final target for an arbitrary caller expression, and
-reconstruct intermediate programs for later or repeated instantiations,
-instead of naming this canary's fixed contexts.
+semantic bridge, and final target for an arbitrary caller expression instead
+of naming this canary's fixed contexts.
 
 The fixed canary also requires a live session with no dropped work and an exact
 proof history of one instance, one equality, three fact events, and the
 expected interleaving before it reads historical values through
 `Engine.factAt?`. This exact trace-shape gate is not a claim that
 `Session.complete` holds. The values are quoted as data, while their proofs
 come from caller assumptions, top soundness, or an earlier emitted replay
-result. A future arbitrary-trace emitter must likewise
-obtain evidence from its chronological proof table; a successful full-history
+result. A future arbitrary-trace emitter must likewise obtain evidence from
+its chronological proof table; a successful full-history
 lookup is never evidence that the dependency was available at the required
 earlier step.
+
 The quotation walker consumes arbitrary `HistoryEvent` lists, requires
 sequential role-local indices, and rejects omitted or duplicated fact or
 instance records through final exhaustion. Proof emission then folds the
-resulting fact events through its evidence state. The present fold permits one
-leading instance event; supporting later or repeated instantiations requires
-updating the checked program and seeding each new node at the corresponding
+resulting fact and instance events through its dependent program/evidence
+state. Repeated and zero-node instantiations update the checked program,
+version, prefix, extension theorem, fact bounds, and fact proofs at the exact
 chronology position.
 
 A general direct emitter maintains a table from each already-established fact

HexIntervalMathlib/Experiment/SineSign.lean

@@ -9,6 +9,7 @@ module
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 public import Mathlib.Tactic.Linarith
 public import HexInterval.Experiment.ProofEmitter
+public import HexInterval.Experiment.GenericInstanceReconstruction
 public import HexInterval.Experiment.SineSign
 
 @[expose] public section
@@ -25,6 +26,7 @@ negation propagator, and generic equality transport.
 namespace Hex.Interval.Experiment.SineSign
 
 open Propagator SemanticReplay ChronologicalReplay ProofEmitter
+open GenericInstanceReconstruction
 
 /-! ## Real interpretation -/
 
@@ -213,6 +215,41 @@ def stable : StableStep semantics baseProgram extendedProgram :=
         Contains fact.fact (newValue fact.node)
       rw [agreement fact.node within] }
 
+theorem nodeAtPrefix {before after : Program}
+    (stepPrefix : ProgramPrefix before after) (target : NodeId)
+    (instruction : Node)
+    (found : before.node? target = some instruction) :
+    after.node? target = some instruction := by
+  have within : target.index < before.nodes.size := by
+    by_contra outside
+    have notWithin : ¬target.index < before.nodes.size := by omega
+    simp [Program.node?, notWithin] at found
+  rw [Program.node?, stepPrefix.nodeAt target.index within]
+  exact found
+
+/-- Node-local real semantics is stable across every checked, fixed-operation
+program prefix.  This law is independent of the sine oddness instantiator and
+can therefore drive generic reconstruction of repeated instance events. -/
+def stableLaw : StableLaw semantics :=
+  { stable := by
+      intro before after _ _ stepPrefix _
+      refine
+        { programPrefix := stepPrefix
+          modelsBefore := ?_
+          holdsOld := ?_ }
+      · intro valuation model
+        change Models after valuation at model
+        change Models before valuation
+        exact
+          ⟨fun found => model.1 (nodeAtPrefix stepPrefix _ _ found),
+           fun found => model.2.1 (nodeAtPrefix stepPrefix _ _ found),
+           fun found => model.2.2.1 (nodeAtPrefix stepPrefix _ _ found),
+           fun found => model.2.2.2 (nodeAtPrefix stepPrefix _ _ found)⟩
+      · intro oldValue newValue fact within _ _ agreement
+        change Contains fact.fact (oldValue fact.node) ↔
+          Contains fact.fact (newValue fact.node)
+        rw [agreement fact.node within] }
+
 theorem oddnessEntails :
     semantics.EntailsEq extendedProgram [] (node 2) (node 4) := by
   change ∀ valuation : NodeId -> ℝ, Models extendedProgram valuation ->