Propagate provenance honesty through goal frontend; progress 20260811T171522Z

Author: kim-em

HexInterval/SPEC/hex-interval.md

@@ -1334,11 +1334,23 @@ replay.
 
 The fold is polymorphic in the fact type and contains no sine, negation, or
 other function case. Its `Context` receives the semantics/domain laws,
-prefix-stability theorem, caller program and facts, and a plain-data encoder;
-packages remain responsible for their replay schemas. The real-sine tactic is
-now a client of this module rather than the owner of the fold. Its semantic
-bridge and final proof closure still name the canary's fixed base graph and
-target; the goal reifier below begins removing that specialization.
+prefix-stability theorem, caller program, a declared base-assumption list, and
+a plain-data encoder; packages remain responsible for their replay schemas.
+It seeds caller facts by checked position in that declared list, and the caller
+hypotheses supplied to final closure discharge the same list. The reusable
+frontend 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 each instance event's fresh nodes with domain top after checking their
+lookup in the reified final program. The real-sine tactic is now a client of
+this module rather than the owner of the fold. Its semantic bridge and final
+proof closure still name the canary's fixed base graph, declared base list,
+and target; the goal reifier below begins removing that specialization.
 
 A second live vertical validates this separation with `Real.exp`. Its
 Mathlib-free package uses a distinct three-element fact lattice, contributes
@@ -1348,7 +1360,10 @@ one replay schema. The same policy session, joint package registry,
 fact-polymorphic quotation, shared structural encoder, and generic evidence
 fold produce the ordinary theorem `0 ≤ Real.exp x`. Thus both a multi-package
 graph-growing sine proof and a single-rule exponential proof pass through the
-same frontend API without a function switch.
+same frontend API without a function switch. The goal reifier below derives
+candidate context pieces from an arbitrary caller expression, but generic
+proof emission has not yet bound its recorded seed recipe to the frontend's
+declared base list.
 
 The first goal-reification experiment now derives the exponential canary's
 base program, version-zero fact array, and target fact from the actual Lean

progress/20260811T163332Z.md

@@ -2,7 +2,8 @@
 
 - Propagated the selected-schema trust correction and guarded sine theorem
   axiom report through generic base-fact and generated-node seeding.
-- Preserved the exact `CheckerInput` binding and arbitrary-node seed rules.
+- Preserved the exact `CheckerInput` base-program and target binding and the
+  arbitrary-node seed rules.
 
 # Current frontier
 

progress/20260811T170347Z.md

@@ -0,0 +1,26 @@
+# Accomplished
+
+- Corrected the generic-seed SPEC to distinguish the direct emitter's declared
+  base-assumption list from the complete checker's position-for-position
+  construction from `CheckerInput.initialFacts` and the chronological cursor's
+  separate `InitialContext` binding.
+- Kept the actual exact bindings to `CheckerInput.baseProgram` and the target
+  explicit, and recorded that caller hypotheses discharge the declared base
+  list at final closure.
+- Passed the focused cached build and repository static checks; the repair
+  changes documentation only.
+
+# Current frontier
+
+The direct emitter has generic positional seeding for its declared base list,
+but the later generic frontend must derive that list from caller input and
+carry the corresponding position-for-position relation into direct emission.
+
+# Next step
+
+Push the repaired exact head and obtain a fresh independent review and
+exact-head CI result before merging.
+
+# Blockers
+
+None.

progress/20260811T171522Z.md

@@ -0,0 +1,26 @@
+# Accomplished
+
+- Propagated the generic-seed provenance correction through the complete
+  interval proof-frontend stack from repeated instantiation to the useful
+  branch-dependent ReLU vertical.
+- Preserved the later arbitrary-chronology, modeled-goal axiom-report,
+  split-origin freshness, proof-refutation, and branch-dependent proof changes
+  while reconciling the corrected SPEC paragraph with their stronger results.
+- Ran a focused conformance build plus source, dependency-DAG, trust-surface,
+  phase-four, factor-freshness, banned-construct, and diff checks at each
+  updated branch head.
+
+# Current frontier
+
+The stacked PR bases and heads carry the same honest distinction between the
+direct emitter's declared assumption list and the complete checker's exact
+binding to `CheckerInput.initialFacts`.
+
+# Next step
+
+Obtain a fresh isolated review and exact-head CI result for the final ReLU head
+without merging the stack.
+
+# Blockers
+
+None.