From 7516528d33ee1e770af478caa7189ae0f90261dc Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Tue, 11 Aug 2026 20:32:55 +0000
Subject: [PATCH 1/7] feat(interval): prove a mixed sine-exp tactic path

Add progress/20260811T203239Z.md with the mixed-function frontier.
---
 HexInterval/Experiment/MixedFunctions.lean    | 209 +++++++++++
 HexInterval/SPEC/hex-interval.md              |  32 ++
 .../Experiment/MixedFunctions.lean            | 207 +++++++++++
 .../MixedFunctionsConformance.lean            | 329 ++++++++++++++++++
 lakefile.lean                                 |   7 +-
 progress/20260811T203239Z.md                  |  36 ++
 .../bench/proof_only_runtime_exemptions.json  |   6 +
 7 files changed, 824 insertions(+), 2 deletions(-)
 create mode 100644 HexInterval/Experiment/MixedFunctions.lean
 create mode 100644 HexIntervalMathlib/Experiment/MixedFunctions.lean
 create mode 100644 conformance/HexIntervalMathlib/MixedFunctionsConformance.lean
 create mode 100644 progress/20260811T203239Z.md

diff --git a/HexInterval/Experiment/MixedFunctions.lean b/HexInterval/Experiment/MixedFunctions.lean
new file mode 100644
index 000000000..cb01f74e4
--- /dev/null
+++ b/HexInterval/Experiment/MixedFunctions.lean
@@ -0,0 +1,209 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import HexInterval.Experiment.PolicySession
+
+@[expose] public section
+
+/-!
+# A Mathlib-free mixed-function propagation canary
+
+This experiment puts two unrelated opaque unary functions in one package
+registry.  The first establishes a unit-range fact; the second consumes that
+fact to establish an upper bound.  Mathematical interpretations and replay
+theorems belong to the companion module.
+-/
+
+namespace Hex.Interval.Experiment.MixedFunctions
+
+open Propagator PayloadArena
+
+/-- The smallest fact lattice needed to test a non-vacuous function chain. -/
+inductive Bound where
+  | all
+  | unit
+  | atMostThree
+  | empty
+  deriving DecidableEq, Repr
+
+namespace Bound
+
+def meet : Bound → Bound → Bound
+  | .empty, _ | _, .empty => .empty
+  | .all, right => right
+  | left, .all => left
+  | .unit, .unit => .unit
+  | .atMostThree, .atMostThree => .atMostThree
+  | .unit, .atMostThree | .atMostThree, .unit => .unit
+
+def code : Bound → Nat
+  | .all => 0
+  | .unit => 1
+  | .atMostThree => 2
+  | .empty => 3
+
+def ofCode? : Nat → Option Bound
+  | 0 => some .all
+  | 1 => some .unit
+  | 2 => some .atMostThree
+  | 3 => some .empty
+  | _ => none
+
+end Bound
+
+def factDomain : FactDomain Bound where
+  top _ := .all
+  narrow _ current proposed :=
+    let installed := current.meet proposed
+    if installed == current then .noChange
+    else if installed == .empty then .contradiction installed
+    else .improved installed
+
+def real : DomainId := { index := 0 }
+
+def sourceKey : OpKey := { name := "mixed-functions.source" }
+def sineKey : OpKey := { name := "mixed-functions.sine" }
+def expKey : OpKey := { name := "mixed-functions.exp" }
+
+def sineRuleKey : RuleKey := { name := "mixed-functions.sine.unit" }
+def expRuleKey : RuleKey := { name := "mixed-functions.exp.at-most-three" }
+
+def sourceOperation : Operation :=
+  { key := sourceKey, inputs := [], output := real }
+
+def sineOperation : Operation :=
+  { key := sineKey, inputs := [real], output := real }
+
+def expOperation : Operation :=
+  { key := expKey, inputs := [real], output := real }
+
+def operations : Array Operation :=
+  #[sourceOperation, sineOperation, expOperation]
+
+def sineRule : Registration :=
+  { key := sineRuleKey
+    head := sineKey
+    kind := .forward
+    watches := [.argument 0]
+    writes := [.result] }
+
+def expRule : Registration :=
+  { key := expRuleKey
+    head := expKey
+    kind := .forward
+    watches := [.argument 0]
+    writes := [.result] }
+
+def factFormat : ReplayFormat :=
+  { role := .fact
+    schema := 1
+    validateBody := fun body =>
+      match body with
+      | [code] => (Bound.ofCode? code).isSome
+      | _ => false }
+
+def sinePlan (request : RuleRequest Bound) : Plan Bound :=
+  match request.inputs, request.writes with
+  | [_], [target] =>
+      { outcome :=
+          .success
+            [{ node := target, fact := .unit, payload := { index := 0 } }]
+            [] {}
+        drafts :=
+          [{ label := { index := 0 }
+             role := .fact
+             schema := 1
+             body := [Bound.unit.code] }] }
+  | _, _ => { outcome := .failed 1, drafts := [] }
+
+/-- Exponential propagation deliberately requires the sine package's exact
+unit-range fact.  This makes the mixed-function chronology non-vacuous. -/
+def expPlan (request : RuleRequest Bound) : Plan Bound :=
+  match request.inputs, request.writes with
+  | [input], [target] =>
+      if input.fact == .unit then
+        { outcome :=
+            .success
+              [{ node := target, fact := .atMostThree, payload := { index := 0 } }]
+              [] {}
+          drafts :=
+            [{ label := { index := 0 }
+               role := .fact
+               schema := 1
+               body := [Bound.atMostThree.code] }] }
+      else
+        { outcome := .failed 2, drafts := [] }
+  | _, _ => { outcome := .failed 3, drafts := [] }
+
+def sourcePackage : Package Bound :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation]
+    handlers := #[] }
+
+def sinePackage : Package Bound :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sineOperation]
+    handlers := #[Handler.statelessPlanned sineRule sinePlan #[factFormat]] }
+
+def expPackage : Package Bound :=
+  { Cache := Unit
+    cache := ()
+    operations := #[expOperation]
+    handlers := #[Handler.statelessPlanned expRule expPlan #[factFormat]] }
+
+def packages : Array (Package Bound) :=
+  #[sourcePackage, sinePackage, expPackage]
+
+def engineLimits : Propagator.Limits :=
+  { maxOperations := 3
+    maxNodes := 8
+    maxRules := 2
+    maxRegistryEntries := 16
+    maxReplayFormats := 4
+    maxArity := 1
+    maxScopeNodes := 1
+    maxApplications := 8
+    maxQueueEntries := 24
+    maxActions := 16
+    maxMatcherVisits := 16
+    matcherBatchSize := 8
+    maxAcceptedFacts := 8
+    maxRetainedSuggestions := 1
+    maxEffort := 1
+    maxObservationValue := 16
+    maxDiagnosticValue := 300
+    maxOutcomeCandidates := 1
+    maxOutcomeSuggestions := 1
+    maxProposalItems := 4
+    maxInstances := 1
+    maxGeneration := 1
+    maxNodeDepth := 4
+    maxEqualities := 1
+    splitEndpointLimit :=
+      { maxEndpointHeight := 8, maxAlignmentShift := 4 } }
+
+def policyLimits : Propagator.Policy.Limits :=
+  { maxDecisions := 24
+    maxTraversal := 256
+    maxLiveOffers := 24 }
+
+def arenaLimits : PayloadArena.Limits :=
+  { maxEntries := 16
+    maxBodyCells := 32
+    maxDrafts := 8
+    maxDraftCells := 8
+    maxAtom := 32
+    maxSchema := 1
+    maxUses := 8 }
+
+def limits : PolicySession.Limits :=
+  { engine := engineLimits, policy := policyLimits, arena := arenaLimits }
+
+end Hex.Interval.Experiment.MixedFunctions
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 8e1ec3357..f9358ec6e 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -1765,6 +1765,38 @@ reified facts, checks every seeded lookup definitionally, proves the recorded
 hypothesis recipes, and supplies the resulting premise to closure. A reusable
 `InitialContext`-style constructor remains future API work.
 
+A mixed-function vertical tests the stronger requirement that independently
+registered function packages cooperate in one search, rather than merely use
+the same generic API in separate examples. The existing sine and exponential
+canaries cannot soundly be concatenated: they instantiate different fact
+types and hence different `Semantics`, fact-domain laws, and proof registries.
+The mixed canary supplies the smallest shared range lattice needed to expose
+that alignment requirement. A sine package unconditionally proves
+`sin x ∈ [-1,1]`; a distinct exponential package is inapplicable until it sees
+that exact input fact, then proves `exp (sin x) ≤ 3`. Its package theorem uses
+the sine bound together with monotonicity of `Real.exp` and
+`Real.exp_one_lt_three`. Thus the retained exponential event has the sine
+event as an actual proof dependency, not merely an unrelated earlier
+improvement. The structural goal reifier selects source, sine, and exponential
+packages recursively from `Real.exp (Real.sin x)`, and the generic scheduler,
+chronology quotation, and proof frontend remain free of function cases. The
+result is the ordinary theorem `Real.exp (Real.sin x) ≤ 3`, without
+`native_decide`. Runtime planning and the Mathlib-free packages perform no
+rational normalization; the Mathlib companion may use `norm_num` for closed
+side conditions such as `1 ≤ 3`.
+
+This experiment also identifies the intended package boundary: independently
+upgradeable operations may contribute their own syntax recognizer, executable
+propagators, mathematical relation, and replay schemas, but packages taking
+part in one run must agree on a fact representation and semantic value model.
+Future domain adapters may embed a package's private facts into a richer shared
+domain; merely joining registries with incompatible `Fact` parameters is not
+meaningful. The mixed target already exercises recursive structural discovery
+of both functions. It does not add a new expression during propagation; a
+later mixed-function acceptance case should use the existing instantiation
+protocol to introduce an auxiliary expression whose package then participates
+in the same dependent chain.
+
 The first goal-reification experiment now derives the exponential canary's
 base program, version-zero fact array, and target fact from the actual Lean
 goal before running its compiled fixture. Expression packages contribute an
diff --git a/HexIntervalMathlib/Experiment/MixedFunctions.lean b/HexIntervalMathlib/Experiment/MixedFunctions.lean
new file mode 100644
index 000000000..f5def487c
--- /dev/null
+++ b/HexIntervalMathlib/Experiment/MixedFunctions.lean
@@ -0,0 +1,207 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import Mathlib.Analysis.Complex.ExponentialBounds
+public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
+public import HexInterval.Experiment.MixedFunctions
+public import HexInterval.Experiment.ProofRegistry
+public import HexInterval.Experiment.OperationSemantics
+
+@[expose] public section
+
+/-!
+# Real semantics for the mixed sine/exponential canary
+
+The sine package first proves a unit-range fact.  The exponential package can
+only emit its upper bound when that exact fact is present, so its replay proof
+must consume the sine event reconstructed by the generic frontend.
+-/
+
+namespace Hex.Interval.Experiment.MixedFunctions
+
+open Propagator SemanticReplay ChronologicalReplay ProofEmitter ProofRegistry
+open GenericInstanceReconstruction OperationSemantics
+
+def Contains : Bound → ℝ → Prop
+  | .all, _ => True
+  | .unit, x => -1 ≤ x ∧ x ≤ 1
+  | .atMostThree, x => x ≤ 3
+  | .empty, _ => False
+
+def sourceModel : OperationSemantics.Model ℝ :=
+  { operation := sourceOperation
+    relation := fun inputs _ => inputs = [] }
+
+def sineModel : OperationSemantics.Model ℝ :=
+  { operation := sineOperation
+    relation := fun inputs output =>
+      match inputs with
+      | [input] => output = Real.sin input
+      | _ => False }
+
+def expModel : OperationSemantics.Model ℝ :=
+  { operation := expOperation
+    relation := fun inputs output =>
+      match inputs with
+      | [input] => output = Real.exp input
+      | _ => False }
+
+def operationModels : Array (OperationSemantics.Model ℝ) :=
+  #[sourceModel, sineModel, expModel]
+
+def semantics : Semantics Bound :=
+  OperationSemantics.semantics operationModels Contains
+
+theorem containsMeet (left right : Bound) (x : ℝ) :
+    Contains (left.meet right) x ↔ Contains left x ∧ Contains right x := by
+  have unitThree : (-1 ≤ x ∧ x ≤ 1) → x ≤ 3 := fun bounds =>
+    bounds.2.trans (by norm_num)
+  cases left <;> cases right <;>
+    simp_all [Bound.meet, Contains]
+
+def boundSchema : FactDomainSchema semantics :=
+  { top := fun _ => .all
+    topSound := by
+      intro _ _ _ _ _ _
+      trivial
+    proveMeet := fun _ _ previous proposed installed =>
+      if exact : installed = previous.meet proposed then
+        some
+          { proof := by
+              subst installed
+              intro valuation _
+              exact containsMeet previous proposed (valuation _) }
+      else
+        none }
+
+def laws : Laws semantics :=
+  { holdsEq := by
+      intro _ valuation left right fact _ _ values
+      change Contains fact (valuation left) ↔ Contains fact (valuation right)
+      rw [values] }
+
+def stableLaw : StableLaw semantics :=
+  OperationSemantics.stableLaw operationModels Contains
+
+theorem sineEntails (graph : Program) (assumptions : List (NodeFact Bound))
+    (output : NodeId) (instruction : Node) (input : NodeId)
+    (found : graph.node? output = some instruction)
+    (operation : instruction.op = ({ index := 1 } : OpId))
+    (arguments : instruction.args = [input]) :
+    semantics.Entails graph assumptions { node := output, fact := .unit } := by
+  intro valuation model _
+  change NodeId → ℝ at valuation
+  obtain ⟨meaning, meaningAt, related⟩ :=
+    model.2 output instruction found
+  simp [operationModels, operation] at meaningAt
+  subst meaning
+  have outputEq : valuation output = Real.sin (valuation input) := by
+    simpa [sineModel, arguments, List.map] using related
+  change -1 ≤ valuation output ∧ valuation output ≤ 1
+  rw [outputEq]
+  exact ⟨Real.neg_one_le_sin _, Real.sin_le_one _⟩
+
+theorem expEntails (graph : Program) (assumptions : List (NodeFact Bound))
+    (output : NodeId) (instruction : Node) (input : NodeId)
+    (found : graph.node? output = some instruction)
+    (operation : instruction.op = ({ index := 2 } : OpId))
+    (arguments : instruction.args = [input])
+    (exactAssumptions :
+      assumptions = [{ node := input, fact := .unit }]) :
+    semantics.Entails graph assumptions
+      { node := output, fact := .atMostThree } := by
+  intro valuation model holds
+  change NodeId → ℝ at valuation
+  obtain ⟨meaning, meaningAt, related⟩ :=
+    model.2 output instruction found
+  simp [operationModels, operation] at meaningAt
+  subst meaning
+  have outputEq : valuation output = Real.exp (valuation input) := by
+    simpa [expModel, arguments, List.map] using related
+  have inputRange : Contains .unit (valuation input) :=
+    holds { node := input, fact := .unit } (by simp [exactAssumptions])
+  change valuation output ≤ 3
+  rw [outputEq]
+  exact (Real.exp_le_exp.mpr inputRange.2).trans Real.exp_one_lt_three.le
+
+private theorem factWith (fact : NodeFact Bound) {value : Bound}
+    (equal : fact.fact = value) :
+    fact = { node := fact.node, fact := value } := by
+  cases fact
+  simp_all
+
+def sineFactSchema : PackedFactSchema semantics where
+  rule := sineRuleKey
+  schema := 1
+  Certificate := Unit
+  decode := fun body => if body == [Bound.unit.code] then some () else none
+  replay := fun _ _ context _ =>
+    if proposedFact : context.proposed.fact = .unit then
+      match found : context.program.node? context.proposed.node with
+      | some instruction =>
+          if operation : instruction.op = ({ index := 1 } : OpId) then
+            match arguments : instruction.args with
+            | [input] =>
+                some
+                  { proof := by
+                      rw [factWith context.proposed proposedFact]
+                      exact sineEntails context.program context.assumptions
+                        context.proposed.node instruction input found operation
+                        arguments }
+            | _ => none
+          else none
+      | none => none
+    else none
+
+def expFactSchema : PackedFactSchema semantics where
+  rule := expRuleKey
+  schema := 1
+  Certificate := Unit
+  decode := fun body =>
+    if body == [Bound.atMostThree.code] then some () else none
+  replay := fun _ _ context _ =>
+    if proposedFact : context.proposed.fact = .atMostThree then
+      match found : context.program.node? context.proposed.node with
+      | some instruction =>
+          if operation : instruction.op = ({ index := 2 } : OpId) then
+            match arguments : instruction.args with
+            | [input] =>
+                if exactAssumptions :
+                    context.assumptions = [{ node := input, fact := .unit }] then
+                  some
+                    { proof := by
+                        rw [factWith context.proposed proposedFact]
+                        exact expEntails context.program context.assumptions
+                          context.proposed.node instruction input found operation
+                          arguments exactAssumptions }
+                else none
+            | _ => none
+          else none
+      | none => none
+    else none
+
+def sourceProof : ProofRegistry.Package semantics Lean.Name :=
+  { semantic := { factSchemas := #[] }
+    emit := { schemas := [] } }
+
+def sineProof : ProofRegistry.Package semantics Lean.Name :=
+  { semantic := { factSchemas := #[sineFactSchema] }
+    emit :=
+      { schemas :=
+          [{ key := sineFactSchema.key, handle := ``sineFactSchema }] } }
+
+def expProof : ProofRegistry.Package semantics Lean.Name :=
+  { semantic := { factSchemas := #[expFactSchema] }
+    emit :=
+      { schemas :=
+          [{ key := expFactSchema.key, handle := ``expFactSchema }] } }
+
+def proofPackages : Array (ProofRegistry.Package semantics Lean.Name) :=
+  #[sourceProof, sineProof, expProof]
+
+end Hex.Interval.Experiment.MixedFunctions
diff --git a/conformance/HexIntervalMathlib/MixedFunctionsConformance.lean b/conformance/HexIntervalMathlib/MixedFunctionsConformance.lean
new file mode 100644
index 000000000..3332443ad
--- /dev/null
+++ b/conformance/HexIntervalMathlib/MixedFunctionsConformance.lean
@@ -0,0 +1,329 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+import HexIntervalMathlib.Experiment.MixedFunctions
+import HexInterval.Experiment.GoalFrontend
+import HexInterval.Experiment.GoalClosure
+import HexInterval.Experiment.ProofFrontend
+import HexInterval.Experiment.TargetRun
+import Mathlib.Lean.Elab.Tactic.Meta
+
+/-!
+# Mixed sine/exponential tactic conformance
+
+One generic goal reifier selects three independently registered syntax
+packages for `x`, `Real.sin x`, and `Real.exp (Real.sin x)`.  Search first
+replays sine's unit-range theorem, then exponential's upper-bound theorem.
+The generic scheduler and proof frontend contain no cases for either function.
+-/
+
+namespace Hex.IntervalMathlib.MixedFunctionsConformance
+
+open Lean Elab Tactic Meta
+open Hex.Interval.Experiment
+open Propagator PolicySession SemanticReplay ChronologicalReplay ProofEmitter
+open Frontend FrontendEncoder ProofFrontend ProofRegistry GoalFrontend GoalClosure
+open MixedFunctions
+
+private def sourceSyntax : GoalFrontend.Package :=
+  { operation := sourceOperation
+    recognize := fun expression => do
+      let type ← inferType expression
+      pure <|
+        if expression.isFVar && type == mkConst ``Real then some [] else none }
+
+private def sineSyntax : GoalFrontend.Package :=
+  { operation := sineOperation
+    recognize := fun expression =>
+      let arguments := expression.getAppArgs
+      pure <|
+        if expression.getAppFn.constName? == some ``Real.sin &&
+            arguments.size == 1 then
+          some [arguments[0]!]
+        else none }
+
+private def expSyntax : GoalFrontend.Package :=
+  { operation := expOperation
+    recognize := fun expression =>
+      let arguments := expression.getAppArgs
+      pure <|
+        if expression.getAppFn.constName? == some ``Real.exp &&
+            arguments.size == 1 then
+          some [arguments[0]!]
+        else none }
+
+private def goalRegistry? : Except String GoalFrontend.Registry :=
+  GoalFrontend.Registry.build
+    { maxPackages := 4, maxNodes := 16, maxDepth := 8 }
+    #[sourceSyntax, sineSyntax, expSyntax]
+
+private def isThree (expression : Expr) : Bool :=
+  let arguments := expression.getAppArgs
+  expression.getAppFn.constName? == some ``OfNat.ofNat &&
+    arguments.size == 3 &&
+      match arguments[1]! with
+      | .lit (.natVal 3) => true
+      | _ => false
+
+private def claimParser : GoalFrontend.Parser Bound :=
+  { parse := fun proposition => do
+      let arguments := proposition.getAppArgs
+      if proposition.getAppFn.constName? == some ``LE.le &&
+          arguments.size ≥ 2 then
+        let left := arguments[arguments.size - 2]!
+        let right := arguments[arguments.size - 1]!
+        let leftType ← inferType left
+        if isThree right && leftType == mkConst ``Real then
+          pure <| some
+            { expression := left
+              domain := real
+              fact := .atMostThree }
+        else pure none
+      else pure none }
+
+private theorem sourceAligned : sourceModel.operation = sourceOperation := rfl
+private theorem sineAligned : sineModel.operation = sineOperation := rfl
+private theorem expAligned : expModel.operation = expOperation := rfl
+
+private def sourceMeaning : GoalClosure.Package :=
+  { operation := sourceOperation
+    model := mkConst ``sourceModel
+    aligned := mkConst ``sourceAligned
+    prove := fun arguments _ => do
+      unless arguments.isEmpty do
+        throwError "interval_mixed: source meaning received arguments"
+      mkAppM ``Eq.refl #[FrontendEncoder.listExpr (mkConst ``Real) []] }
+
+private def sineMeaning : GoalClosure.Package :=
+  { operation := sineOperation
+    model := mkConst ``sineModel
+    aligned := mkConst ``sineAligned
+    prove := fun arguments output => do
+      let [input] := arguments
+        | throwError "interval_mixed: sine meaning is not unary"
+      let expected ← mkAppM ``Real.sin #[input]
+      unless ← isDefEq output expected do
+        throwError "interval_mixed: sine recognizer changed the expression"
+      mkAppM ``Eq.refl #[output] }
+
+private def expMeaning : GoalClosure.Package :=
+  { operation := expOperation
+    model := mkConst ``expModel
+    aligned := mkConst ``expAligned
+    prove := fun arguments output => do
+      let [input] := arguments
+        | throwError "interval_mixed: exponential meaning is not unary"
+      let expected ← mkAppM ``Real.exp #[input]
+      unless ← isDefEq output expected do
+        throwError "interval_mixed: exponential recognizer changed the expression"
+      mkAppM ``Eq.refl #[output] }
+
+private def meanings : Array GoalClosure.Package :=
+  #[sourceMeaning, sineMeaning, expMeaning]
+
+private meta def reifyGoal (target : Expr) : MetaM (GoalFrontend.Result Bound) := do
+  let registry ←
+    match goalRegistry? with
+    | .ok registry => pure registry
+    | .error message => throwError "interval_mixed: invalid registry: {message}"
+  let context ← getLCtx
+  let mut hypotheses := []
+  for declaration in context do
+    unless declaration.isImplementationDetail do
+      hypotheses := hypotheses.concat
+        (← instantiateMVars declaration.type, mkFVar declaration.fvarId)
+  GoalFrontend.reify registry factDomain claimParser hypotheses target
+
+private def firstOffer : TargetRun.Controller Bound Unit :=
+  { update := fun state _ => state
+    choose := fun state view =>
+      match view.offers[0]? with
+      | some offer => .select offer state
+      | none => .stop state }
+
+private structure Fixture where
+  result : TargetRun.Result Bound Unit
+  reached : TargetRun.Reached Bound
+  registry : ProofRegistry.Registry semantics Name
+
+private def runInput? (input : CheckerInput Bound) : Option Fixture := do
+  let .ok session := PolicySession.Session.start factDomain input.baseProgram
+      packages input.initialFacts limits
+    | none
+  let result := TargetRun.drive factDomain input.target.node input.target.fact
+    firstOffer limits.policy.maxDecisions session ()
+  let .target reached := result.stop | none
+  let .ok registry := ProofRegistry.build result.session.registry proofPackages
+    | none
+  some { result, reached, registry }
+
+private def node (index : Nat) : NodeId := { index }
+
+private def mixedProgram : Program :=
+  { operations
+    nodes :=
+      #[{ domain := real, op := { index := 0 }, args := [] },
+        { domain := real, op := { index := 1 }, args := [node 0] },
+        { domain := real, op := { index := 2 }, args := [node 1] }] }
+
+private def mixedInput : CheckerInput Bound :=
+  { baseProgram := mixedProgram
+    initialFacts := #[.all, .all, .all]
+    target := { node := node 2, fact := .atMostThree } }
+
+private structure MixedSummary where
+  reached : SeenVersion
+  fact : Bound
+  facts : Array Bound
+  chronology : Array HistoryEvent
+
+private def mixedSummary? : Option MixedSummary := do
+  let .ok session := PolicySession.Session.start factDomain mixedProgram
+      packages mixedInput.initialFacts limits
+    | none
+  let result := TargetRun.drive factDomain mixedInput.target.node
+    mixedInput.target.fact firstOffer limits.policy.maxDecisions session ()
+  let .target reached := result.stop | none
+  some
+    { reached := reached.seen
+      fact := reached.fact
+      facts := result.session.state.engine.facts
+      chronology := result.session.state.engine.chronology }
+
+#guard
+  mixedSummary?.any fun summary =>
+    summary.reached == ({ node := node 2, version := 1 } : SeenVersion) &&
+      summary.fact == .atMostThree &&
+      summary.facts == #[.all, .unit, .atMostThree] &&
+      summary.chronology == #[.fact 0, .fact 1]
+
+private def mixedTrace? : Option (Frontend.Trace Bound) := do
+  let .ok session := PolicySession.Session.start factDomain mixedProgram
+      packages mixedInput.initialFacts limits
+    | none
+  let result := TargetRun.drive factDomain mixedInput.target.node
+    mixedInput.target.fact firstOffer limits.policy.maxDecisions session ()
+  let .target _ := result.stop | none
+  Frontend.trace? result.session.state.engine result.session.arena
+
+#guard
+  mixedTrace?.any fun trace =>
+    match trace.events with
+    | [.rule sine, .rule exp] =>
+        sine.entry.replayKey == sineFactSchema.key &&
+          sine.assumptions == [{ node := node 0, fact := .all }] &&
+          exp.entry.replayKey == expFactSchema.key &&
+          exp.assumptions == [{ node := node 1, fact := .unit }]
+    | _ => false
+
+private def boundExpr : Bound → Expr
+  | .all => mkConst ``Bound.all
+  | .unit => mkConst ``Bound.unit
+  | .atMostThree => mkConst ``Bound.atMostThree
+  | .empty => mkConst ``Bound.empty
+
+private def boundEncoder : FrontendEncoder.Encoder Bound :=
+  FrontendEncoder.make (mkConst ``Bound) (fun fact => pure (boundExpr fact))
+
+private def factBridge : GoalClosure.FactBridge Bound :=
+  { runtime := factDomain
+    schema := mkConst ``boundSchema
+    proveAssumption := fun program valuation node fact _ proof => do
+      let expected ←
+        mkAppM ``SemanticReplay.Semantics.holds
+          #[mkConst ``semantics, program, valuation,
+            ← boundEncoder.nodeFact { node, fact }]
+      unless ← isDefEq (← inferType proof) expected do
+        throwError "interval_mixed: hypothesis does not prove its parsed fact"
+      pure proof }
+
+private def seedAssumed (graph : Program) (base : List (NodeFact Bound))
+    (index : Nat) (fact : NodeFact Bound) (found : base[index]? = some fact) :
+    Evidence (semantics.Entails graph base fact) :=
+  ProofEmitter.assumedAt graph base index fact found
+
+private def inputContext (result : GoalFrontend.Result Bound)
+    (base : GoalClosure.BaseProof) : ProofFrontend.Context Bound Name :=
+  { encoder := boundEncoder
+    resolveSchema := pure
+    semantics := mkConst ``semantics
+    domain := mkConst ``boundSchema
+    laws := mkConst ``laws
+    stableLaw := mkConst ``stableLaw
+    input := base.input
+    assumed := ``seedAssumed
+    baseFacts := result.baseFacts
+    baseFactsTerm := base.facts
+    baseProgram := result.input.baseProgram
+    baseProgramTerm := base.program
+    basePrefix := base.basePrefix
+    baseWithin := base.within
+    initialExtension := base.extension
+    finalPrefix := base.basePrefix
+    sameOperations := base.sameOperations
+    top := boundSchema.top }
+
+private meta def emitInput (result : GoalFrontend.Result Bound)
+    (base : GoalClosure.BaseProof) : MetaM Expr := do
+  let some fixture := runInput? result.input
+    | throwError "interval_mixed: search or proof registry failed"
+  let some trace := Frontend.trace? fixture.result.session.state.engine
+      fixture.result.session.arena
+    | throwError "interval_mixed: chronology quotation failed"
+  unless trace.program == result.input.baseProgram do
+    throwError "interval_mixed: propagation unexpectedly changed the graph"
+  let state ← ProofFrontend.emitTrace (inputContext result base)
+    trace.program trace.events fixture.registry.emit
+  ProofFrontend.closeTarget (inputContext result base) state fixture.reached.seen
+    fixture.reached.fact result.input.target
+
+private meta def proveMixed (target : Expr) : MetaM Expr := do
+  let result ← reifyGoal target
+  unless result.input.baseProgram.operations == operations &&
+      result.input.baseProgram.nodes.size == 3 &&
+      result.input.target.node == ({ index := 2 } : NodeId) do
+    throwError "interval_mixed: reifier produced an unexpected graph"
+  let some fallback := GoalClosure.termAt? result.terms { index := 0 }
+    | throwError "interval_mixed: source expression is missing"
+  let model ← GoalClosure.proveModel (mkConst ``Real) fallback meanings
+    boundEncoder result
+  let base ← GoalClosure.proveBase (mkConst ``Bound) (mkConst ``semantics)
+    boundEncoder result.input
+  let facts ← GoalClosure.proveFacts factBridge boundEncoder result base model
+  let evidence ← emitInput result base
+  let proof ←
+    mkAppM ``Evidence.proof #[evidence, model.valuation, model.proof, facts]
+  unless ← isDefEq (← inferType proof) target do
+    throwError "interval_mixed: emitted proof has the wrong target"
+  pure (← instantiateMVars proof)
+
+syntax (name := intervalMixedTac) "interval_mixed" : tactic
+
+@[tactic intervalMixedTac] meta def evalIntervalMixed : Tactic := fun stx => do
+  match stx with
+  | `(tactic| interval_mixed) =>
+      let goal ← getMainGoal
+      goal.withContext do
+        goal.assign (← proveMixed (← instantiateMVars (← goal.getType)))
+      replaceMainGoal []
+  | _ => throwUnsupportedSyntax
+
+/-- Both arbitrary-function packages contribute a replayed fact, and the
+exponential proof consumes the sine proof as its exact dependency. -/
+theorem mixedSinExp (x : ℝ) : Real.exp (Real.sin x) ≤ 3 := by
+  interval_mixed
+
+/--
+info: 'Hex.IntervalMathlib.MixedFunctionsConformance.mixedSinExp' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs in
+#print axioms mixedSinExp
+
+example (_x : ℝ) : True := by
+  fail_if_success interval_mixed
+  trivial
+
+end Hex.IntervalMathlib.MixedFunctionsConformance
diff --git a/lakefile.lean b/lakefile.lean
index 6f4ad627f..13aea37c3 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -369,7 +369,8 @@ lean_lib HexIntervalExperiment where
     `HexInterval.Experiment.PntBKLNWExp,
     `HexInterval.Experiment.PntBKLNWPow,
     `HexInterval.Experiment.SinTen,
-    `HexInterval.Experiment.SinTenInterval].map Glob.one
+    `HexInterval.Experiment.SinTenInterval,
+    `HexInterval.Experiment.MixedFunctions].map Glob.one
 
 lean_lib HexIntervalMathlibExperiment where
   globs := #[`HexIntervalMathlib.Experiment.Arithmetic,
@@ -407,7 +408,8 @@ lean_lib HexIntervalMathlibExperiment where
     `HexIntervalAlgebraic.Experiment.PolynomialDispatch,
     `HexIntervalAlgebraic.Experiment.PolynomialDispatchProof,
     `HexIntervalMathlib.Experiment.SinTen,
-    `HexIntervalMathlib.Experiment.SinTenInterval].map Glob.one
+    `HexIntervalMathlib.Experiment.SinTenInterval,
+    `HexIntervalMathlib.Experiment.MixedFunctions].map Glob.one
 
 @[default_target]
 lean_lib HexIntervalMathlib where
@@ -508,6 +510,7 @@ lean_lib HexConformance where
 
     ++ #[`HexInterval.PolicyFeatureConformance,
       `HexInterval.FeaturePolicyConformance,
+      `HexIntervalMathlib.MixedFunctionsConformance,
       `HexIntervalMathlib.ExactBranchConformance].map Glob.one
 
 -- The expensive complete-family Mathlib proofs are owned only by this
diff --git a/progress/20260811T203239Z.md b/progress/20260811T203239Z.md
new file mode 100644
index 000000000..f08f2f490
--- /dev/null
+++ b/progress/20260811T203239Z.md
@@ -0,0 +1,36 @@
+# Accomplished
+
+- Added a Mathlib-free mixed-function experiment with independently registered
+  source, sine, and exponential packages over one shared fact domain.
+- Made the exponential propagator inapplicable until the sine package proves
+  the exact unit-range fact, so the second replay proof genuinely consumes the
+  first rather than merely following it in the chronology.
+- Added real operation semantics and package-owned replay theorems proving
+  `Real.exp (Real.sin x) ≤ 3` from `Real.sin x ∈ [-1, 1]`, exponential
+  monotonicity, and `Real.exp_one_lt_three`.
+- Added an end-to-end tactic conformance test. The structural goal reifier
+  recursively selects both function packages; the generic scheduler quotes two
+  fact events; and the generic proof frontend emits the ordinary theorem with
+  no function cases.
+- Documented the semantic-alignment requirement for mixed package registries
+  and the remaining dynamic-instantiation experiment in the interval SPEC.
+- Built all three new modules and passed DAG, trust-surface, JSON, and diff
+  checks without `native_decide`, axioms, or sorries.
+
+# Current frontier
+
+The mixed-function tactic now demonstrates a non-vacuous dependency across two
+arbitrary non-polynomial packages. It uses recursive structural discovery of
+the nested goal expression, but does not yet introduce a previously absent
+auxiliary function expression during propagation.
+
+# Next step
+
+Use the existing instantiation protocol to add an auxiliary expression whose
+separately registered package creates a fact needed later in the same mixed
+function proof. A richer shared interval domain can then replace this minimal
+four-element alignment canary without changing the generic frontend.
+
+# Blockers
+
+None.
diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json
index d4df1aea0..e2fd48b08 100644
--- a/scripts/bench/proof_only_runtime_exemptions.json
+++ b/scripts/bench/proof_only_runtime_exemptions.json
@@ -239,6 +239,12 @@
     "current_blob": "6f4ad627fd141e71916da6a287d0743d93c30197",
     "reason": "Additionally registers the isolated Mathlib-free bounded feature-scoring policy experiment and its conformance module on top of the retained PolicyFeature, adaptive policy, exact-branch proof, subtraction replay, staged policy, complete LogTables, PNT, and public interval registrations; neither enters the factorization service target or changes its executable dependency graph."
   },
+  {
+    "path": "lakefile.lean",
+    "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
+    "current_blob": "efdad9a3533bef3735dc0474f7ca15bf2c0731df",
+    "reason": "Additionally registers the isolated mixed-function interval experiment, its proof-only real-semantics companion, and conformance module; the factorization service target and executable dependency graph are unchanged."
+  },
   {
     "path": "HexBerlekamp/FactorTacticTests.lean",
     "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",

From 4d1c11d95cd5c4daebcfa750ef578b55e2b794da Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Sat, 15 Aug 2026 00:15:58 +0000
Subject: [PATCH 2/7] docs(interval): record mixed-function reconciliation

---
 progress/20260815T001524Z.md | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 progress/20260815T001524Z.md

diff --git a/progress/20260815T001524Z.md b/progress/20260815T001524Z.md
new file mode 100644
index 000000000..66ae0fc24
--- /dev/null
+++ b/progress/20260815T001524Z.md
@@ -0,0 +1,32 @@
+# Accomplished
+
+- Replayed the mixed sine/exponential tactic feature onto exact local #9237
+  head `6aa8b4c0bfaee89c3c43255e43043c1f6b304667`, preserving all package-policy,
+  raster, Table 12, and PNT work in the stack.
+- Audited the shared fact lattice, independent runtime and proof packages,
+  recursive goal reification, exact sine-then-exponential chronology, and the
+  exponential replay theorem's use of the sine event as a real dependency.
+- Confirmed that the generic quotation and proof frontend produce an ordinary
+  theorem whose guarded axiom report contains only the expected foundational
+  axioms, with no function-specific frontend or scheduler case.
+- Preserved the honest limits: this is recursive structural discovery rather
+  than dynamic instantiation, and packages in one run currently share one fact
+  representation and semantic value model.
+- Reconciled all Lake registrations, refreshed the narrow proof-only exemption,
+  built the three mixed-function targets, and passed structural, trust,
+  freshness, PNT inventory, and banned-mechanism checks.
+
+# Current frontier
+
+Two independently registered arbitrary-function packages now cooperate in one
+live tactic proof with a load-bearing cross-package fact dependency.
+
+# Next step
+
+After #9237 lands, rebase this local feature onto its exact merge commit,
+recompute the Lake exemption, and run the final PR review and CI cycle.
+
+# Blockers
+
+None. The shared filesystem remains very full, but the exact 2,222-job focused
+build completed successfully.

From 017ff1edcab0d6becb704d55e1ad5015f2117e22 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Sat, 15 Aug 2026 02:41:01 +0000
Subject: [PATCH 3/7] test(interval): harden mixed function dependency

---
 HexInterval/SPEC/hex-interval.md              |  5 +-
 .../MixedFunctionsConformance.lean            | 54 +++++++++++++++++++
 progress/20260815T024038Z.md                  | 44 +++++++++++++++
 3 files changed, 102 insertions(+), 1 deletion(-)
 create mode 100644 progress/20260815T024038Z.md

diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index f9358ec6e..9be6a073f 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -1792,7 +1792,10 @@ part in one run must agree on a fact representation and semantic value model.
 Future domain adapters may embed a package's private facts into a richer shared
 domain; merely joining registries with incompatible `Fact` parameters is not
 meaningful. The mixed target already exercises recursive structural discovery
-of both functions. It does not add a new expression during propagation; a
+of both functions. Like the current package-composed semantics experiment, it
+still requires the operation, meaning, and proof-package arrays in one fixed
+aligned order; key-resolved package reordering remains future work. It does not
+add a new expression during propagation; a
 later mixed-function acceptance case should use the existing instantiation
 protocol to introduce an auxiliary expression whose package then participates
 in the same dependent chain.
diff --git a/conformance/HexIntervalMathlib/MixedFunctionsConformance.lean b/conformance/HexIntervalMathlib/MixedFunctionsConformance.lean
index 3332443ad..b8498e622 100644
--- a/conformance/HexIntervalMathlib/MixedFunctionsConformance.lean
+++ b/conformance/HexIntervalMathlib/MixedFunctionsConformance.lean
@@ -174,6 +174,60 @@ private def mixedInput : CheckerInput Bound :=
     initialFacts := #[.all, .all, .all]
     target := { node := node 2, fact := .atMostThree } }
 
+private def mixedView : ProgramView :=
+  { programVersion := 0
+    operations
+    nodes := mixedProgram.nodes
+    generations := #[0, 0, 0]
+    depths := #[0, 1, 2] }
+
+private def expAction : Action :=
+  { serial := 1
+    programVersion := 0
+    application := { index := 1 }
+    rule := { index := 1 }
+    key := expRuleKey
+    node := node 2
+    kind := .forward
+    effort := 0
+    inputs := [{ node := node 1, version := 1 }]
+    writes := [node 2] }
+
+private def expRequest (fact : Bound) (version : Nat) : RuleRequest Bound :=
+  { action := { expAction with inputs := [{ node := node 1, version }] }
+    program := mixedView
+    inputs := [{ node := node 1, fact, version }]
+    writes := [node 2] }
+
+/- The exponential callback is unavailable at the initial top fact and becomes
+applicable only after the exact sine fact has been installed. -/
+#guard
+  match (expPlan (expRequest .all 0)).outcome with
+  | .failed 2 => true
+  | _ => false
+
+#guard
+  match (expPlan (expRequest .unit 1)).outcome with
+  | .success [candidate] [] _ =>
+      candidate.node == node 2 && candidate.fact == .atMostThree
+  | _ => false
+
+private def expContext : RuleFactContext mixedInput expAction :=
+  { program := mixedProgram
+    basePrefix := ProgramPrefix.refl mixedProgram
+    assumptions := [{ node := node 1, fact := .unit }]
+    proposed := { node := node 2, fact := .atMostThree } }
+
+private def wrongExpFact : RuleFactContext mixedInput expAction :=
+  { expContext with assumptions := [{ node := node 1, fact := .all }] }
+
+private def bypassedSine : RuleFactContext mixedInput expAction :=
+  { expContext with assumptions := [{ node := node 0, fact := .unit }] }
+
+#guard (expFactSchema.replay mixedInput expAction expContext ()).isSome
+#guard (expFactSchema.replay mixedInput expAction wrongExpFact ()).isNone
+#guard (expFactSchema.replay mixedInput expAction bypassedSine ()).isNone
+
 private structure MixedSummary where
   reached : SeenVersion
   fact : Bound
diff --git a/progress/20260815T024038Z.md b/progress/20260815T024038Z.md
new file mode 100644
index 000000000..474608994
--- /dev/null
+++ b/progress/20260815T024038Z.md
@@ -0,0 +1,44 @@
+# Accomplished
+
+- Reconciled the #9238 mixed sine-to-exponential vertical onto exact local
+  #9237 candidate `b032d33fb9133e65552c353c2cfe709335d7e9d3`, preserving the
+  separate #9235 branch and current PNT/Table 12 registrations.
+- Audited the live runtime chain. With the initial `.all` input, `expPlan`
+  emits no candidate and reports diagnostic failure `2`; it emits the
+  `.atMostThree` candidate only after seeing the exact `.unit` sine fact.
+- Confirmed that chronology quotation records sine followed by exponential,
+  and that `expFactSchema` accepts exactly the sine node's `.unit` assumption.
+  Its theorem obtains the exponential bound from that retained assumption.
+- Added executable guards for the pre-sine planner rejection, post-sine
+  applicability, successful exact replay, and rejection of both a weakened
+  fact and a source-node substitution.
+- Re-audited recursive goal discovery, model construction, quotation, generic
+  proof emission, and ordinary theorem closure. Function-specific cases remain
+  confined to independently supplied syntax, runtime, semantic, and replay
+  packages; the shared generic frontend was unchanged.
+- Confirmed the ordinary theorem's guarded axiom report contains only
+  `propext`, `Classical.choice`, and `Quot.sound`, with no banned proof
+  mechanism. The model proof is constructed for every reified node, so the
+  package `Entails` theorems are not used through a vacuous `Models` premise.
+- Made the SPEC explicit that this canary shares one `Fact` and real-valued
+  semantic model and still requires fixed aligned operation, meaning, and
+  proof-package arrays; package reordering remains future work.
+- Built all three focused mixed-function targets and the preserved interval/PNT
+  targets, then passed structural, trust-surface, freshness, PNT inventory,
+  release, Mathlib-free bench, and static checks.
+
+# Current frontier
+
+Two function packages now participate in one ordinary proof with a
+load-bearing cross-package fact dependency. Dynamic expression instantiation,
+heterogeneous fact/value adapters, and key-resolved package reordering remain
+future work.
+
+# Next step
+
+After #9237 lands, rebase this local candidate onto its exact merge commit,
+refresh the Lake exemption, and perform the final review and CI cycle.
+
+# Blockers
+
+None.

From d5964063e02e65780e9190130ccf11b682d28a4b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Sat, 15 Aug 2026 07:42:35 +0000
Subject: [PATCH 4/7] docs(interval): record mixed function preparation

---
 progress/20260815T074216Z.md                  | 21 +++++++++++++++++++
 .../bench/proof_only_runtime_exemptions.json  |  2 +-
 2 files changed, 22 insertions(+), 1 deletion(-)
 create mode 100644 progress/20260815T074216Z.md

diff --git a/progress/20260815T074216Z.md b/progress/20260815T074216Z.md
new file mode 100644
index 000000000..22d240dc7
--- /dev/null
+++ b/progress/20260815T074216Z.md
@@ -0,0 +1,21 @@
+# Accomplished
+
+- Recovered the audited mixed sine-to-exponential experiment as `#9238` on exact prepared `#9237` head `b17cc2b6d849370258c8c5d887d9c6f5cb652fec`, preserving all earlier preparation refs and a source ref for the historical audited patch.
+- Confirmed exponential planning is inapplicable at the initial `.all` fact and requires the exact sine-produced `.unit` fact before emitting `.atMostThree`.
+- Confirmed the retained chronology is sine then exponential, and the exponential replay schema consumes exactly the sine-node `.unit` assumption; weakened-fact and source-node substitutions both fail closed.
+- Audited package-owned sine and exponential schemas, recursive package-generic goal reification, generic chronology quotation and `ProofFrontend` replay, and the nonvacuous ordinary theorem `Real.exp (Real.sin x) ≤ 3` with its exact axiom guard.
+- Confirmed all runtime packages share one `Bound` fact type and all proof packages share one `ℝ` semantic value type. The SPEC honestly retains the fixed aligned operation, meaning, and proof-package slot order and leaves key-resolved reordering as future work.
+- Recomputed the exact Lake freshness exemption for blob `bdbf6e162f63907d15e7819df8854eadce601f10`.
+- Passed the focused mixed-function and experiment builds, complete PNT conformance set, static/DAG/phase checks, trust-surface and release-manifest checks, source-pinned PNT inventory checks, unit tests, and factor-sweep freshness.
+
+# Current frontier
+
+`#9238` is a clean local-only mixed-function candidate on branch `codex/9238-prepare-current`, reconciled with FeaturePolicy and all current public arithmetic and PNT registrations.
+
+# Next step
+
+Retain the branch for the directed landing sequence; rebase and repeat exact-head review/CI only when explicitly requested.
+
+# Blockers
+
+None.
diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json
index e2fd48b08..d169f5059 100644
--- a/scripts/bench/proof_only_runtime_exemptions.json
+++ b/scripts/bench/proof_only_runtime_exemptions.json
@@ -242,7 +242,7 @@
   {
     "path": "lakefile.lean",
     "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
-    "current_blob": "efdad9a3533bef3735dc0474f7ca15bf2c0731df",
+    "current_blob": "bdbf6e162f63907d15e7819df8854eadce601f10",
     "reason": "Additionally registers the isolated mixed-function interval experiment, its proof-only real-semantics companion, and conformance module; the factorization service target and executable dependency graph are unchanged."
   },
   {

From 1c574e42369212bc98931b3fa294452e347c41ed Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Sat, 15 Aug 2026 13:22:44 +0000
Subject: [PATCH 5/7] docs(interval): record mixed function fork

---
 progress/20260815T132225Z.md                  | 36 +++++++++++++++++++
 .../bench/proof_only_runtime_exemptions.json  |  2 +-
 2 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 progress/20260815T132225Z.md

diff --git a/progress/20260815T132225Z.md b/progress/20260815T132225Z.md
new file mode 100644
index 000000000..771b972dc
--- /dev/null
+++ b/progress/20260815T132225Z.md
@@ -0,0 +1,36 @@
+# Accomplished
+
+- Replayed the mixed sine-to-exponential experiment directly onto exact #9237
+  head `a4df54c9d47319a40c036e7923d246aaa29a20cc`, preserving all earlier fork
+  refs and current public, split, precision, and PNT registrations.
+- Confirmed the exponential callback is inapplicable at the initial `.all`
+  fact and emits its proposal only after sine installs the exact `.unit` fact.
+- Confirmed the retained chronology is sine then exponential and that the
+  exponential replay schema consumes the sine node's exact `.unit` assumption;
+  weakened-fact and source-node mutations fail closed.
+- Re-audited recursive function-generic goal reification, exact chronology
+  quotation, generic `ProofFrontend` replay, model construction, and ordinary
+  theorem closure. The guarded axiom report remains limited to `propext`,
+  `Classical.choice`, and `Quot.sound`.
+- Kept the experiment's boundaries explicit: runtime packages share one
+  `Bound` fact type, proof packages share the real-valued semantics, and the
+  operation, meaning, and proof-package arrays still use fixed aligned slots.
+- Refreshed the exact Lake registration exemption, built the 2286-job focused
+  mixed-function/controller/public/PNT closure, and passed structural, trust,
+  inventory, release, freshness, and banned-mechanism checks.
+
+# Current frontier
+
+Two independently registered function packages now contribute to one
+non-vacuous ordinary proof through a generic scheduler and proof frontend.
+Dynamic graph instantiation and key-resolved package reordering remain later
+work.
+
+# Next step
+
+Retain this fork for the directed landing sequence and rebase onto the eventual
+exact predecessor merge before any remote review or CI cycle.
+
+# Blockers
+
+None.
diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json
index d169f5059..27a38f7df 100644
--- a/scripts/bench/proof_only_runtime_exemptions.json
+++ b/scripts/bench/proof_only_runtime_exemptions.json
@@ -242,7 +242,7 @@
   {
     "path": "lakefile.lean",
     "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
-    "current_blob": "bdbf6e162f63907d15e7819df8854eadce601f10",
+    "current_blob": "ed91aed063678adea53970312b08d97c268ada84",
     "reason": "Additionally registers the isolated mixed-function interval experiment, its proof-only real-semantics companion, and conformance module; the factorization service target and executable dependency graph are unchanged."
   },
   {

From 5574b6f7495bf5a342a73fb17533779838b28368 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Sun, 16 Aug 2026 01:41:26 +0000
Subject: [PATCH 6/7] docs(interval): prepare mixed function edge

---
 progress/20260816T014109Z.md                  | 27 +++++++++++++++++++
 .../bench/proof_only_runtime_exemptions.json  |  4 +--
 2 files changed, 29 insertions(+), 2 deletions(-)
 create mode 100644 progress/20260816T014109Z.md

diff --git a/progress/20260816T014109Z.md b/progress/20260816T014109Z.md
new file mode 100644
index 000000000..5f5a546fc
--- /dev/null
+++ b/progress/20260816T014109Z.md
@@ -0,0 +1,27 @@
+# Prepare mixed sine-exp path after feature policy
+
+## Accomplished
+
+- Replayed the audited mixed sine-to-exp proof path directly onto exact #9237
+  candidate `d75ee4c2a01aa3ea8a920af5d0156873e0481d33`, excluding raster #9235.
+- Preserved exp inapplicability before the exact sine `.unit` fact, exact
+  sine-to-exp chronology, schema and source-node mutation rejection, the
+  generic reifier, quotation, ProofFrontend and GoalClosure path, and the
+  nonvacuous ordinary theorem and guarded axiom surface.
+- Preserved the honest fixed aligned operation/meaning/proof-package slot
+  limitation and all current feature-policy, controller, public, and PNT
+  registrations while refreshing the exact Lake exemption.
+
+## Current frontier
+
+The local branch contains only the mixed sine-to-exp edge above #9237. Raster
+#9235 and dynamic mixed instantiation #9240 remain independent and unchanged.
+
+## Next step
+
+After #9237 merges, replay this prepared edge onto its literal merge commit and
+publish PR #9238 as a direct-main branch.
+
+## Blockers
+
+None.
diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json
index 27a38f7df..922fdb82e 100644
--- a/scripts/bench/proof_only_runtime_exemptions.json
+++ b/scripts/bench/proof_only_runtime_exemptions.json
@@ -242,8 +242,8 @@
   {
     "path": "lakefile.lean",
     "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
-    "current_blob": "ed91aed063678adea53970312b08d97c268ada84",
-    "reason": "Additionally registers the isolated mixed-function interval experiment, its proof-only real-semantics companion, and conformance module; the factorization service target and executable dependency graph are unchanged."
+    "current_blob": "13aea37c3d992ceea397993b0ff9230798ce0478",
+    "reason": "Additionally registers the isolated mixed-function interval experiment, its proof-only real-semantics companion, and conformance module on top of the retained feature policies, exact-branch proof, subtraction replay, staged policy, complete LogTables, PNT, and public interval registrations; none enters the factorization service target or changes its executable dependency graph."
   },
   {
     "path": "HexBerlekamp/FactorTacticTests.lean",

From 933a6a58c9dc54abbc77972c6550ebe6eae1d7d0 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Sun, 16 Aug 2026 02:03:58 +0000
Subject: [PATCH 7/7] docs(interval): record merged mixed-function restack

---
 progress/20260816T020347Z.md | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 progress/20260816T020347Z.md

diff --git a/progress/20260816T020347Z.md b/progress/20260816T020347Z.md
new file mode 100644
index 000000000..441159735
--- /dev/null
+++ b/progress/20260816T020347Z.md
@@ -0,0 +1,25 @@
+# Restack mixed sine-exp path onto merged feature policy
+
+## Accomplished
+
+- Replayed the prepared mixed sine-to-exp edge onto literal #9237 merge commit
+  `6075687a18f4c43ad4b93c0d5d5065625cdcc6b2`, excluding raster #9235.
+- Preserved the merged feature policies, adaptive policy, exact-branch proof,
+  subtraction replay, staged policy, complete source-pinned LogTables providers
+  and inventory, PNT examples, and current public interval registrations.
+- Confirmed that the exact combined Lake blob and narrow proof-only runtime
+  exemption remain unchanged by the merge-parent restack.
+
+## Current frontier
+
+PR #9238 is a direct-main mixed sine-to-exp proof edge. Raster #9235 and
+dynamic mixed instantiation #9240 remain independent and unchanged.
+
+## Next step
+
+Run focused mixed-function, frontend, controller, inventory, trust, freshness,
+and diff gates; then publish the direct-main PR head and monitor automatic CI.
+
+## Blockers
+
+None.