inductive Hex.Endpoint (E : Type u) : Type u

An exact endpoint, including both infinities.

• negInf {E : Type u} : Endpoint E
• finite {E : Type u} (value : E) : Endpoint E
• posInf {E : Type u} : Endpoint E

@[instance_reducible]

instance Hex.instDecidableEqEndpoint {E : Type u_1} [DecidableEq E] : DecidableEq (Endpoint E)

Constructor comparison is exposed for ordinary-kernel literal replay.

Equations

• One or more equations did not get rendered due to their size.
• Hex.instDecidableEqEndpoint Hex.Endpoint.negInf Hex.Endpoint.negInf = isTrue ⋯
• Hex.instDecidableEqEndpoint Hex.Endpoint.posInf Hex.Endpoint.posInf = isTrue ⋯
• Hex.instDecidableEqEndpoint Hex.Endpoint.negInf (Hex.Endpoint.finite value) = isFalse ⋯
• Hex.instDecidableEqEndpoint Hex.Endpoint.negInf Hex.Endpoint.posInf = isFalse ⋯
• Hex.instDecidableEqEndpoint (Hex.Endpoint.finite value) Hex.Endpoint.negInf = isFalse ⋯
• Hex.instDecidableEqEndpoint (Hex.Endpoint.finite value) Hex.Endpoint.posInf = isFalse ⋯
• Hex.instDecidableEqEndpoint Hex.Endpoint.posInf Hex.Endpoint.negInf = isFalse ⋯
• Hex.instDecidableEqEndpoint Hex.Endpoint.posInf (Hex.Endpoint.finite value) = isFalse ⋯

structure Hex.EndpointSigns (D : Type u) (E : Type v) [Zero D] [DecidableEq D] : Type (max u v)

Exact finite comparison and evaluation signs. Endpoint values may belong to an ordered extension of the coefficient domain, as for integer/dyadic queries.

• compare : E → E → Int
• evalSign : DensePoly D → E → Int

def Hex.EndpointSigns.ofSign {E : Type u} [Zero E] [DecidableEq E] [Sub E] [Add E] [Mul E] (sign : E → Int) : EndpointSigns E E

Compare and evaluate finite endpoints using a supplied coefficient sign.

Equations

• Hex.EndpointSigns.ofSign sign = { compare := fun (a b : E) => sign (a - b), evalSign := fun (p : Hex.DensePoly E) (a : E) => sign (p.eval a) }

def Hex.Endpoint.lt {D : Type u_1} {E : Type u_2} [Zero D] [DecidableEq D] (endpointSigns : EndpointSigns D E) : Endpoint E → Endpoint E → Bool

Equations

• Hex.Endpoint.lt endpointSigns Hex.Endpoint.negInf (Hex.Endpoint.finite value) = true
• Hex.Endpoint.lt endpointSigns Hex.Endpoint.negInf Hex.Endpoint.posInf = true
• Hex.Endpoint.lt endpointSigns (Hex.Endpoint.finite value) Hex.Endpoint.posInf = true
• Hex.Endpoint.lt endpointSigns (Hex.Endpoint.finite a) (Hex.Endpoint.finite b) = decide (endpointSigns.compare a b < 0)
• Hex.Endpoint.lt endpointSigns x✝¹ x✝ = false

def Hex.Endpoint.signAt {D : Type u_1} {E : Type u_2} [Zero D] [DecidableEq D] (sign : D → Int) (endpointSigns : EndpointSigns D E) (p : DensePoly D) : Endpoint E → Int

Equations

• Hex.Endpoint.signAt sign endpointSigns p Hex.Endpoint.negInf = sign p.leadingCoeff * if p.natDegree % 2 = 1 then -1 else 1
• Hex.Endpoint.signAt sign endpointSigns p (Hex.Endpoint.finite a) = endpointSigns.evalSign p a
• Hex.Endpoint.signAt sign endpointSigns p Hex.Endpoint.posInf = sign p.leadingCoeff

def Hex.Endpoint.nonvanishing {D : Type u_1} {E : Type u_2} [Zero D] [DecidableEq D] (endpointSigns : EndpointSigns D E) (p : DensePoly D) : Endpoint E → Bool

Equations

• Hex.Endpoint.nonvanishing endpointSigns p (Hex.Endpoint.finite a) = (endpointSigns.evalSign p a != 0)
• Hex.Endpoint.nonvanishing endpointSigns p x✝ = true

structure Hex.TarskiCertificate (D : Type u) (E : Type v) (Ctx : Type w) [Zero D] [DecidableEq D] : Type (max (max u v) w)

Literal inputs/context and finite query evidence. Ctx is the caller's full literal context data, not a hash. A derivative-chain replay proves the squarefree guard without running a gcd search in the checker.

• context : Ctx
• head : DensePoly D
• queryPoly : DensePoly D
• lower : Endpoint E
• upper : Endpoint E
• squarefree : SignedRemainderChain D
• remainders : SignedRemainderChain D
• lowerSigns : Array Int
• upperSigns : Array Int
• lowerVariations : Nat
• upperVariations : Nat
• value : Int

@[instance_reducible]

instance Hex.instDecidableEqTarskiCertificate {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] [DecidableEq E] [DecidableEq Ctx] : DecidableEq (TarskiCertificate D E Ctx)

Equations

• One or more equations did not get rendered due to their size.

def Hex.SignedRemainderChain.lastIsConstant {D : Type u_1} [Zero D] [DecidableEq D] (chain : SignedRemainderChain D) : Bool

A nonzero constant terminal gcd is the squarefree criterion; its stored leading coefficient need not be literal one.

Equations

• chain.lastIsConstant = ((chain.chain.getD (chain.chain.size - 1) 0).size == 1)

def Hex.TarskiCertificate.signs {D : Type u} {E : Type v} [Zero D] [DecidableEq D] (sign : D → Int) (endpointSigns : EndpointSigns D E) (chain : Array (DensePoly D)) (endpoint : Endpoint E) : Array Int

Exact signs of a literal chain at a finite or infinite endpoint.

Equations

• Hex.TarskiCertificate.signs sign endpointSigns chain endpoint = Hex.Array.map' (fun (p : Hex.DensePoly D) => Hex.Endpoint.signAt sign endpointSigns p endpoint) chain

def Hex.TarskiCertificate.checkEndpoints {D : Type u} {E : Type v} [Zero D] [DecidableEq D] (endpointSigns : EndpointSigns D E) (p : DensePoly D) (a b : Endpoint E) : Bool

Nonzero input, strictly ordered endpoints and finite endpoint nonvanishing. These guards precede all constant and zero-query shortcuts.

Equations

• One or more equations did not get rendered due to their size.

def Hex.TarskiCertificate.fromChains {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] (sign : D → Int) (endpointSigns : EndpointSigns D E) (context : Ctx) (p f : DensePoly D) (a b : Endpoint E) (squarefree remainders : SignedRemainderChain D) : TarskiCertificate D E Ctx

Attach exact endpoint signs and variations to supplied producer chains. This is shared by ordinary and prepared-domain frontends.

Equations

• One or more equations did not get rendered due to their size.

def Hex.TarskiCertificate.certify {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] [Neg D] (sign : D → Int) (endpointSigns : EndpointSigns D E) (normalize : DensePoly D → D × DensePoly D) (context : Ctx) (p f : DensePoly D) (a b : Endpoint E) : Option (TarskiCertificate D E Ctx)

Produce a finite query certificate using the one shared signed-remainder kernel. The normalizer is a total positive-content backend; field callers may use SignedRemainderChain.normalizeId. No root search or isolation is performed.

Equations

• One or more equations did not get rendered due to their size.

def Hex.TarskiCertificate.query {D : Type u} {E : Type v} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] [Neg D] (sign : D → Int) (endpointSigns : EndpointSigns D E) (normalize : DensePoly D → D × DensePoly D) (p f : DensePoly D) (a b : Endpoint E) : Option Int

The query value of the shared producer. Negative values are retained.

Equations

• Hex.TarskiCertificate.query sign endpointSigns normalize p f a b = Option.map Hex.TarskiCertificate.value (Hex.TarskiCertificate.certify sign endpointSigns normalize () p f a b)

def Hex.TarskiCertificate.checkBindings {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] [DecidableEq E] [DecidableEq Ctx] (context : Ctx) (p f : DensePoly D) (a b : Endpoint E) (value : Int) (cert : TarskiCertificate D E Ctx) : Bool

Bind every literal query input and claimed value before checking evidence.

Equations

• One or more equations did not get rendered due to their size.

def Hex.TarskiCertificate.checkDomain {D : Type u} {E : Type v} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] (sign : D → Int) (endpointSigns : EndpointSigns D E) (p : DensePoly D) (a b : Endpoint E) (squarefree : SignedRemainderChain D) : Bool

The domain part of finite replay, independent of the query polynomial. This checks supplied witnesses and never invokes a producer or gcd search.

Equations

• One or more equations did not get rendered due to their size.

def Hex.TarskiCertificate.checkQuery {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] [Add D] [Sub D] [Mul D] [NatCast D] (sign : D → Int) (endpointSigns : EndpointSigns D E) (p f : DensePoly D) (a b : Endpoint E) (value : Int) (cert : TarskiCertificate D E Ctx) : Bool

The query-dependent part of finite replay. Domain and literal input bindings are checked separately by the complete checker.

Equations

• One or more equations did not get rendered due to their size.

def Hex.TarskiCertificate.check {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] [DecidableEq E] [DecidableEq Ctx] (sign : D → Int) (endpointSigns : EndpointSigns D E) (context : Ctx) (p f : DensePoly D) (a b : Endpoint E) (value : Int) (cert : TarskiCertificate D E Ctx) : Bool

Check full literal bindings, both chain replays, exact endpoint signs and variations. Arithmetic equations use zero differences; input and context bindings use literal equality. The checker never calls a producer.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.TarskiCertificate.check_eq {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] [DecidableEq E] [DecidableEq Ctx] (sign : D → Int) (endpointSigns : EndpointSigns D E) (context : Ctx) (p f : DensePoly D) (a b : Endpoint E) (value : Int) (cert : TarskiCertificate D E Ctx) : check sign endpointSigns context p f a b value cert = (((decide (cert.context = context) && decide (cert.head = p) && decide (cert.queryPoly = f) && decide (cert.lower = a) && decide (cert.upper = b) && decide (cert.value = value) && checkEndpoints endpointSigns p a b && SignedRemainderChain.check sign p 1 cert.squarefree && cert.squarefree.lastIsConstant && SignedRemainderChain.check sign p f cert.remainders && decide (cert.lowerSigns = signs sign endpointSigns cert.remainders.chain a) && decide (cert.upperSigns = signs sign endpointSigns cert.remainders.chain b) && cert.lowerSigns.all fun (s : Int) => decide (-1 ≤ s) && decide (s ≤ 1)) && cert.upperSigns.all fun (s : Int) => decide (-1 ≤ s) && decide (s ≤ 1)) && decide (cert.lowerVariations = signVar cert.lowerSigns.toList) && decide (cert.upperVariations = signVar cert.upperSigns.toList) && decide (value = ↑cert.lowerVariations - ↑cert.upperVariations))

Expanded finite replay contract. Factoring the domain and query checks preserves the Boolean result for every supplied certificate.

def Hex.EndpointSigns.intDyadic : EndpointSigns Int Dyadic

Exact dyadic endpoints for integer coefficients.

Equations

• Hex.EndpointSigns.intDyadic = { compare := fun (a b : Dyadic) => Hex.dyadicSign (a - b), evalSign := fun (p : Hex.DensePoly Int) (a : Dyadic) => Hex.dyadicSign (Hex.ZPoly.evalDyadic p a) }

def Hex.ZPoly.normalizeContent (p : ZPoly) : Int × ZPoly

Positive integer content normalization; the producer calls it only on a nonzero remainder. It never changes the input head or makes entries monic.

Equations

• p.normalizeContent = (Hex.DensePoly.content p, Hex.DensePoly.primitivePart p)

def Hex.ZPoly.tarskiQuery (p f : ZPoly) (I : DyadicInterval) : Option Int

The signed sum at roots in the open interval, with nonzero squarefree input and root-free endpoints. Invalid mathematical inputs return none.

Equations

• p.tarskiQuery f I = Hex.TarskiCertificate.query Int.sign Hex.EndpointSigns.intDyadic Hex.ZPoly.normalizeContent p f (Hex.Endpoint.finite I.lower) (Hex.Endpoint.finite I.upper)

@[reducible, inline]

abbrev Hex.IntTarskiCertificate : Type

The integer/dyadic specialization of the shared literal replay.

Equations

• Hex.IntTarskiCertificate = Hex.TarskiCertificate Int Dyadic Unit

def Hex.IntTarskiCertificate.certify (p f : ZPoly) (I : DyadicInterval) : Option IntTarskiCertificate

Equations

• One or more equations did not get rendered due to their size.

def Hex.IntTarskiCertificate.check (p f : ZPoly) (I : DyadicInterval) (value : Int) (cert : IntTarskiCertificate) : Bool

Equations

• Hex.IntTarskiCertificate.check p f I value cert = Hex.TarskiCertificate.check Int.sign Hex.EndpointSigns.intDyadic () p f (Hex.Endpoint.finite I.lower) (Hex.Endpoint.finite I.upper) value cert