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

Literal domain evidence shared by queries on one head and interval. Context identity and the entire squarefree witness remain part of the stored data.

• context : Ctx
• head : DensePoly D
• lower : Endpoint E
• upper : Endpoint E
• squarefree : SignedRemainderChain D

def Hex.TarskiCertificate.domain {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] (cert : TarskiCertificate D E Ctx) : Domain D E Ctx

Extract the supplied domain literals, without validating them.

Equations

• cert.domain = { context := cert.context, head := cert.head, lower := cert.lower, upper := cert.upper, squarefree := cert.squarefree }

structure Hex.TarskiCertificate.Domain.Checked {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] (sign : D → Int) (endpointSigns : EndpointSigns D E) : Type (max (max u v) w)

A domain whose actual finite replay has succeeded under these fixed sign operations. This is independent of producer preparation or root-sum semantics.

• data : Domain D E Ctx
• accepted : checkDomain sign endpointSigns self.data.head self.data.lower self.data.upper self.data.squarefree = true

def Hex.TarskiCertificate.Domain.replay? {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] (sign : D → Int) (endpointSigns : EndpointSigns D E) (raw : Domain D E Ctx) : Option (Checked sign endpointSigns)

Validate the supplied endpoint guards and squarefree chain once. Invalid certificate evidence returns none; this is not a root-nonexistence test.

Equations

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

theorem Hex.TarskiCertificate.Domain.replay_data {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] {sign : D → Int} {endpointSigns : EndpointSigns D E} {raw : Domain D E Ctx} {d : Checked sign endpointSigns} (h : replay? sign endpointSigns raw = some d) : d.data = raw

Domain replay preserves every literal field, including context identity.

def Hex.TarskiCertificate.Domain.binds {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] [DecidableEq E] [DecidableEq Ctx] (d : Domain D E Ctx) (context : Ctx) (p : DensePoly D) (a b : Endpoint E) (squarefree : SignedRemainderChain D) : Bool

Reuse requires the caller's exact context, head, interval and squarefree witness. Equal interpretations never replace these literal bindings.

Equations

• d.binds context p a b squarefree = decide (d.context = context ∧ d.head = p ∧ d.lower = a ∧ d.upper = b ∧ d.squarefree = squarefree)

def Hex.TarskiCertificate.checkBody {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq 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

The query-dependent part of replay, including all certificate bindings. This does not check the squarefree domain witness. Complete replay must also validate that domain, as checkHit and checkCached do through checked evidence or full replay. This component alone does not certify a Tarski result.

Equations

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

def Hex.TarskiCertificate.checkHit {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) (d : Domain.Checked sign endpointSigns) (cert : TarskiCertificate D E Ctx) : Bool

Check a cache hit against an already replayed domain. A literal mismatch returns false; use checkCached for complete replay with fallback. All query bindings and query-dependent checks remain mandatory on a hit.

Equations

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

theorem Hex.TarskiCertificate.checkHit_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) (d : Domain.Checked sign endpointSigns) (cert : TarskiCertificate D E Ctx) : checkHit sign endpointSigns context p f a b value d cert = (d.data.binds context p a b cert.squarefree && check sign endpointSigns context p f a b value cert)

Shared replay is precisely full replay with an additional literal-cache binding guard. The full certificate checker is neither weakened nor bypassed.

theorem Hex.TarskiCertificate.checkHit_replay {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) (raw : Domain D E Ctx) (cert : TarskiCertificate D E Ctx) : ((Domain.replay? sign endpointSigns raw).elim false fun (d : Domain.Checked sign endpointSigns) => checkHit sign endpointSigns context p f a b value d cert) = (checkDomain sign endpointSigns raw.head raw.lower raw.upper raw.squarefree && raw.binds context p a b cert.squarefree && checkBindings context p f a b value cert && checkQuery sign endpointSigns p f a b value cert)

Boolean elimination rule for the opaque validated-domain constructor. It exposes every check performed when a raw domain is replayed and then used.

def Hex.TarskiCertificate.checkCached {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) (cache : Option (Domain.Checked sign endpointSigns)) (cert : TarskiCertificate D E Ctx) : Bool

Use a validated domain when its literals match. A different squarefree witness is replayed in full, so a cache miss cannot reject otherwise valid certificate evidence. The query-dependent checks use the same shared kernel.

Equations

• One or more equations did not get rendered due to their size.
• Hex.TarskiCertificate.checkCached sign endpointSigns context p f a b value none cert = Hex.TarskiCertificate.check sign endpointSigns context p f a b value cert

theorem Hex.TarskiCertificate.checkCached_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) (cache : Option (Domain.Checked sign endpointSigns)) (cert : TarskiCertificate D E Ctx) : checkCached sign endpointSigns context p f a b value cache cert = check sign endpointSigns context p f a b value cert

Cached replay has exactly the original Boolean result for every supplied certificate and every validated cache, including cache misses and rejections.

theorem Hex.TarskiCertificate.checkHit_checks {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} {d : Domain.Checked sign endpointSigns} {cert : TarskiCertificate D E Ctx} (h : checkHit sign endpointSigns context p f a b value d cert = true) : check sign endpointSigns context p f a b value cert = true

Arbitrary supplied query evidence accepted using a shared domain also passes the complete shared-kernel checker, regardless of producer provenance.