theorem
HexRealRootsTheory.Tarski.check_head
{D : Type u}
[Zero D]
[DecidableEq D]
[Add D]
[Sub D]
[Mul D]
[NatCast D]
(sign : D → ℤ)
(p g : Hex.DensePoly D)
(cert : Hex.SignedRemainderChain D)
(h : Hex.SignedRemainderChain.check sign p g cert = true)
:
Accepted replay retains the exact input head.
theorem
HexRealRootsTheory.Tarski.check_tail
{D : Type u}
[Zero D]
[DecidableEq D]
[Add D]
[Sub D]
[Mul D]
[NatCast D]
(sign : D → ℤ)
(p g : Hex.DensePoly D)
(cert : Hex.SignedRemainderChain D)
(h : Hex.SignedRemainderChain.check sign p g cert = true)
(hn : cert.chain.size ≠ 1)
:
A nonsingleton accepted chain has all steps and a terminal identity.
theorem
HexRealRootsTheory.Tarski.check_dvd_last
{D : Type u}
{K : Type v}
[Zero D]
[DecidableEq D]
[Add D]
[Sub D]
[Mul D]
[NatCast D]
[Field K]
[DecidableEq K]
[LinearOrder K]
[IsStrictOrderedRing K]
(f : D → K)
(hz : ∀ (a : D), f a = 0 ↔ a = 0)
(ha : ∀ (a b : D), f (a + b) = f a + f b)
(hs : ∀ (a b : D), f (a - b) = f a - f b)
(hm : ∀ (a b : D), f (a * b) = f a * f b)
(hn : ∀ (n : ℕ), f ↑n = ↑n)
(sign : D → ℤ)
(hpos : ∀ (a : D), sign a = 1 ↔ 0 < f a)
(p g : Hex.DensePoly D)
(cert : Hex.SignedRemainderChain D)
(h : Hex.SignedRemainderChain.check sign p g cert = true)
(d : Polynomial K)
:
d ∣ HexPolyTheory.Interpret.interpret f hz p ∧ d ∣ HexPolyTheory.Interpret.interpret f hz g * Polynomial.derivative (HexPolyTheory.Interpret.interpret f hz p) ↔ d ∣ HexPolyTheory.Interpret.interpret f hz (cert.chain.getD (cert.chain.size - 1) 0)
The last entry of an accepted replay has exactly the common divisors of
P and F*P' in the semantic field, including singleton chains.
theorem
HexRealRootsTheory.Tarski.check_gcd
{D : Type u}
{K : Type v}
[Zero D]
[DecidableEq D]
[Add D]
[Sub D]
[Mul D]
[NatCast D]
[Field K]
[DecidableEq K]
[LinearOrder K]
[IsStrictOrderedRing K]
(f : D → K)
(hz : ∀ (a : D), f a = 0 ↔ a = 0)
(ha : ∀ (a b : D), f (a + b) = f a + f b)
(hs : ∀ (a b : D), f (a - b) = f a - f b)
(hm : ∀ (a b : D), f (a * b) = f a * f b)
(hn : ∀ (n : ℕ), f ↑n = ↑n)
(sign : D → ℤ)
(hpos : ∀ (a : D), sign a = 1 ↔ 0 < f a)
(p g : Hex.DensePoly D)
(cert : Hex.SignedRemainderChain D)
(h : Hex.SignedRemainderChain.check sign p g cert = true)
:
Associated (HexPolyTheory.Interpret.interpret f hz (cert.chain.getD (cert.chain.size - 1) 0))
(EuclideanDomain.gcd (HexPolyTheory.Interpret.interpret f hz p)
(HexPolyTheory.Interpret.interpret f hz g * Polynomial.derivative (HexPolyTheory.Interpret.interpret f hz p)))
The terminal polynomial in an accepted query replay is associated to the semantic gcd, whether that gcd is constant or nonconstant.
theorem
HexRealRootsTheory.Tarski.lastIsConstant_iff
{D : Type u}
{K : Type v}
[Zero D]
[DecidableEq D]
[Add D]
[Sub D]
[Mul D]
[NatCast D]
[Field K]
[DecidableEq K]
(f : D → K)
(hz : ∀ (a : D), f a = 0 ↔ a = 0)
(sign : D → ℤ)
(p g : Hex.DensePoly D)
(cert : Hex.SignedRemainderChain D)
(h : Hex.SignedRemainderChain.check sign p g cert = true)
:
The replay's literal constant-tail guard means a nonzero constant after interpretation, without requiring a canonical representative of one.
theorem
HexRealRootsTheory.Tarski.check_squarefree
{D : Type u}
{K : Type v}
[Zero D]
[DecidableEq D]
[Add D]
[Sub D]
[Mul D]
[NatCast D]
[Field K]
[DecidableEq K]
[LinearOrder K]
[IsStrictOrderedRing K]
(f : D → K)
(hz : ∀ (a : D), f a = 0 ↔ a = 0)
(ha : ∀ (a b : D), f (a + b) = f a + f b)
(hs : ∀ (a b : D), f (a - b) = f a - f b)
(hm : ∀ (a b : D), f (a * b) = f a * f b)
(hn : ∀ (n : ℕ), f ↑n = ↑n)
(sign : D → ℤ)
(hpos : ∀ (a : D), sign a = 1 ↔ 0 < f a)
[One D]
(h1 : f 1 = 1)
(p : Hex.DensePoly D)
(cert : Hex.SignedRemainderChain D)
(h : Hex.SignedRemainderChain.check sign p 1 cert = true)
:
For the derivative replay, the exact constant-tail guard is equivalent to squarefreeness over the semantic ordered field.
theorem
HexRealRootsTheory.Tarski.query_isSome
{D : Type u}
{K : Type v}
[Zero D]
[DecidableEq D]
[Add D]
[Sub D]
[Mul D]
[NatCast D]
[Field K]
[DecidableEq K]
[LinearOrder K]
[IsStrictOrderedRing K]
(f : D → K)
(hz : ∀ (a : D), f a = 0 ↔ a = 0)
(ha : ∀ (a b : D), f (a + b) = f a + f b)
(hs : ∀ (a b : D), f (a - b) = f a - f b)
(hm : ∀ (a b : D), f (a * b) = f a * f b)
(hn : ∀ (n : ℕ), f ↑n = ↑n)
(sign : D → ℤ)
(hpos : ∀ (a : D), sign a = 1 ↔ 0 < f a)
[One D]
[Neg D]
(h1 : f 1 = 1)
{E : Type w}
(endpointSigns : Hex.EndpointSigns D E)
(normalize : Hex.DensePoly D → D × Hex.DensePoly D)
(hchains :
∀ (p g : Hex.DensePoly D),
p ≠ 0 → Hex.SignedRemainderChain.check sign p g (Hex.SignedRemainderChain.build sign normalize p g) = true)
(p g : Hex.DensePoly D)
(a b : Hex.Endpoint E)
:
(Hex.TarskiCertificate.query sign endpointSigns normalize p g a b).isSome = true ↔ Hex.TarskiCertificate.checkEndpoints endpointSigns p a b = true ∧ Squarefree (HexPolyTheory.Interpret.interpret f hz p)
Query production succeeds exactly when the endpoint guards and semantic
squarefreeness hold. There is no exhaustion case hidden in the Option.