feat(HexRCF): prove acceptance at original algebraic sources

HexManual/Chapters/HexRCF/AlgebraicCells.lean

@@ -602,7 +602,9 @@ Its default proof callback, `FieldRuntime.nonnegative`, attempts routine
 nonnegativity facts and restores its state on decline. A caller can supply
 another callback returning an ordinary proof or `none`; thrown exceptions
 remain terminal. Preparation checks each supplied proof and retains one
-aggregate reflection budget across the source, coefficients and divisors:
+aggregate reflection budget across the source, coefficients and divisors.
+The source equivalence is charged during reification and again when retained
+as a private theorem for later composition:
 
 ```lean
 open Lean Meta Qq
@@ -628,6 +630,64 @@ authenticate quoted literals for the computed proposals. This preparation API
 does not install a new `rcf` handler or close the remaining frozen-context,
 literal-authentication and general source-quotation obligations.
 
+For the retained algebraic expressions, `prepared.acceptanceIff` proves an exact
+acceptance equivalence. The left side requires the actual algebraic producer
+to return a complete packet and that packet's checker to accept `true`. The
+right side contains both the original real statement and every original
+divisor's nonzero condition. Guard validity is a conclusion of acceptance,
+even when cancellation or an empty interval makes the statement trivial.
+The helper reconstructs the ordered original guard inventory from the target;
+editing both stored guard arrays cannot remove or replace an obligation.
+The existing producer completeness and domain laws prove this equivalence;
+no successful child calculation is assumed.
+
+```lean
+open Hex Lean Meta Qq
+open Hex.RCF.RealCoefficients
+open Hex.RealClosure.BaseContext
+run_meta do
+  let target : Q(Prop) :=
+    q(∀ x : ℝ, x^2 + Real.sqrt 2 > 0)
+  let .ok prepared ←
+      AlgebraicPreparation.prepare
+        target
+    | throwError "unsupported source"
+  let before := prepared.usage
+  let registry : Q(Registry) :=
+    q(fun _ => none)
+  let .ok (equivalence, usage) ←
+      prepared.acceptanceIff
+        target registry
+    | throwError
+        "source equivalence failed"
+  let auxName := mkPrivateName
+    (← getEnv)
+    (← mkFreshUserName `sourceDoc)
+  let _ ←
+    withDeclNameForAuxNaming
+      auxName do
+        Hex.RCF.checkProof
+          `sourceAcceptance
+          (← inferType equivalence)
+          equivalence
+  unless usage.proofNodes >
+      before.proofNodes do
+    throwError
+      "proof usage did not increase"
+```
+
+This proof uses the checked algebraic expressions and their source identities.
+It does not identify separately computed proposals with frozen literals,
+reconstruct provider histories, or add a tactic handler. Those authentication
+and quotation obligations remain separate. The helper continues the same
+aggregate reflection budget, returns its updated usage for later stages, and
+restores caller state on exhaustion or failure.
+Callers continue with `{prepared with usage}` when constructing further proofs.
+Both preparation and acceptance preserve a caller's lowered recursion limit.
+Fresh importing regressions check its actual theorem bodies, true and false
+sources, retained zero guards and reversed intervals, with exactly the standard
+three axioms.
+
 The automatic-input conformance uses both selected signs of √2 alongside an
 independent positive √3. It checks simultaneous conditions and a repeated zero
 root, both true and false quantified verdicts, an unused zero input, a late

adapters/HexRCF/RealCoefficients/AlgebraicCells.lean

@@ -296,4 +296,79 @@ theorem build_sound (registry : BaseContext.Registry) (generators : Fin m → Re
   cases same
   exact checked
 
+/-- Acceptance by the actual algebraic producer and its complete packet
+checker. This predicate retains the exact source tuple, indices and original
+nonzero-divisor obligations; it does not assert frozen-history quotation. -/
+@[expose] def accepts (registry : BaseContext.Registry) (generators : Fin m → RealAlgebraicNumber)
+    (indices : Fin n → Fin m) (original : List (Fin m))
+    (formula : Hex.RealFormula.QF (n+1)) (quantifier : Hex.RealFormula.Quantifier) : Prop :=
+  ∃ result, build registry generators indices original formula = .ok result ∧
+    let sources := result.1
+    let shared := result.2.1
+    let packet := result.2.2
+    CompleteReplay.check packet.family.collection.input.context.codec
+      (packet.family.collection.input.value ∘ GatherCells.values shared (coefficients sources indices)) formula
+      ((GatherCells.guards shared (guards sources original)).map packet.family.collection.input.value)
+      packet.radical quantifier packet.rootGraph packet.cells = .ok true
+
+/-- Accepted true packets are equivalent to the original domains and shared
+sentence together. Guard validity, complete roots and real samples follow
+from the producer's existing laws, without a child-success hypothesis. -/
+theorem accepts_iff (registry : BaseContext.Registry) (generators : Fin m → RealAlgebraicNumber)
+    (indices : Fin n → Fin m) (original : List (Fin m))
+    (formula : Hex.RealFormula.QF (n+1)) (quantifier : Hex.RealFormula.Quantifier) :
+    accepts registry generators indices original formula quantifier ↔
+      (∀ i ∈ original, (generators i).toReal ≠ 0) ∧
+        (Hex.RealFormula.Prenex.quant quantifier (.matrix formula)).toProp
+          (fun i => (generators (indices i)).toReal) := by
+  constructor
+  · rintro ⟨result, produced, accepted⟩
+    refine ⟨build_domains registry generators indices original formula result.1 result.2 produced, ?_⟩
+    obtain ⟨verdict, checked, meaning⟩ :=
+      build_sound registry generators indices original formula result produced quantifier
+    have same : verdict = true := Except.ok.inj (checked.symm.trans accepted)
+    exact meaning.mp same
+  · rintro ⟨domains, truth⟩
+    have nonzero : ∀ i ∈ original, generators i ≠ 0 := by
+      intro i member zero
+      apply domains i member
+      simp only [zero, RealAlgebraicNumber.zero_toReal]
+    obtain ⟨sources, shared, packet, produced, checked⟩ :=
+      build_complete registry generators indices original formula nonzero
+    obtain ⟨verdict, accepted, meaning⟩ := checked quantifier
+    have same : verdict = true := meaning.mpr truth
+    exact ⟨⟨sources, shared, packet⟩, produced, by simpa only [same] using accepted⟩
+
+/-- Coefficient and original-divisor coordinates have separate ordered
+positions in the native producer. Every divisor remains a checked domain. -/
+theorem accepts_tuple (registry : BaseContext.Registry)
+    (values : Fin n → RealAlgebraicNumber) (divisors : Fin d → RealAlgebraicNumber)
+    (formula : Hex.RealFormula.QF (n+1)) (quantifier : Hex.RealFormula.Quantifier) :
+    accepts registry (Fin.addCases values divisors) (Fin.castAdd d)
+      (List.ofFn (Fin.natAdd n)) formula quantifier ↔
+      (∀ i, (divisors i).toReal ≠ 0) ∧
+        (Hex.RealFormula.Prenex.quant quantifier (.matrix formula)).toProp
+          (fun i => (values i).toReal) := by
+  rw [accepts_iff]
+  simp
+
+/-- Checked valuation identities and the frontend's exact equivalence connect
+producer acceptance to the original proposition and every original divisor.
+The identities are ordinary proof inputs supplied by source preparation. -/
+theorem accepts_source (registry : BaseContext.Registry)
+    (values : Fin n → RealAlgebraicNumber) (divisors : Fin d → RealAlgebraicNumber)
+    (realValues : Fin n → ℝ) (realDivisors : Fin d → ℝ)
+    (formula : Hex.RealFormula.QF (n+1)) (quantifier : Hex.RealFormula.Quantifier)
+    {source : Prop}
+    (coefficientEq : (fun i => (values i).toReal) = realValues)
+    (divisorEq : (fun i => (divisors i).toReal) = realDivisors)
+    (equivalence : (Hex.RealFormula.Prenex.quant quantifier (.matrix formula)).toProp realValues ↔ source) :
+    accepts registry (Fin.addCases values divisors) (Fin.castAdd d)
+      (List.ofFn (Fin.natAdd n)) formula quantifier ↔
+      (∀ i, realDivisors i ≠ 0) ∧ source := by
+  rw [accepts_tuple, coefficientEq]
+  have domains : (∀ i, (divisors i).toReal ≠ 0) ↔ (∀ i, realDivisors i ≠ 0) := by
+    rw [← divisorEq]
+  exact and_congr domains equivalence
+
 end Hex.RCF.RealCoefficients.AlgebraicCells