def Hex.SignedRemainderChain.signOperands {E : Type u} [Zero E] [DecidableEq E] (cert : SignedRemainderChain E) : List E

A finite inventory of the coefficient signs used by literal chain replay. Zero is a conservative extra operand for the default-step branch of the proof. The checker itself ranges only over existing step indices. The inventory may include unused scales; it is independent of the sign function and of acceptance.

Equations

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

theorem Hex.SignedRemainderChain.checkStep_congr {E : Type u} [Zero E] [DecidableEq E] [Add E] [Sub E] [Mul E] (sign sign' : E → Int) (a b c : DensePoly E) (s : RemainderStep E) (hl : sign s.leftScale = sign' s.leftScale) (hr : sign s.rightScale = sign' s.rightScale) : checkStep sign a b c s = checkStep sign' a b c s

Replay of a recurrence depends only on its two supplied scale signs.

theorem Hex.SignedRemainderChain.check_sign_congr {E : Type u} [Zero E] [DecidableEq E] [Add E] [Sub E] [Mul E] [NatCast E] (sign sign' : E → Int) (p f : DensePoly E) (cert : SignedRemainderChain E) (h : ∀ (x : E), x ∈ cert.signOperands → sign x = sign' x) : check sign p f cert = check sign' p f cert

Agreement on the finite inventory preserves both acceptance and rejection of the actual checker, including malformed and truncated supplied chains.

def Hex.Endpoint.signOperand {E : Type u} [Zero E] [DecidableEq E] [Add E] [Mul E] (endpoint : Endpoint E) (p : DensePoly E) : E

The coefficient passed to the sign operation at this endpoint.

Equations

• (Hex.Endpoint.finite a).signOperand p = p.eval a
• endpoint.signOperand p = p.leadingCoeff

def Hex.Endpoint.orderOperands {E : Type u} [Sub E] (a b : Endpoint E) : List E

Only two finite endpoints require a coefficient sign for their order.

Equations

• (Hex.Endpoint.finite a_2).orderOperands (Hex.Endpoint.finite b_2) = [a_2 - b_2]
• a.orderOperands b = []

def Hex.Endpoint.nonvanishingOperands {E : Type u} [Zero E] [DecidableEq E] [Add E] [Mul E] (a : Endpoint E) (p : DensePoly E) : List E

Only finite endpoints require a polynomial nonvanishing sign.

Equations

• (Hex.Endpoint.finite a_1).nonvanishingOperands p = [p.eval a_1]
• a.nonvanishingOperands p = []

theorem Hex.Endpoint.signAt_congr {E : Type u} [Zero E] [DecidableEq E] [Add E] [Sub E] [Mul E] (sign sign' : E → Int) (a : Endpoint E) (p : DensePoly E) (h : sign (a.signOperand p) = sign' (a.signOperand p)) : signAt sign (EndpointSigns.ofSign sign) p a = signAt sign' (EndpointSigns.ofSign sign') p a

Equal operand signs give equal endpoint signs, including both infinities.

theorem Hex.Endpoint.lt_congr {E : Type u} [Zero E] [DecidableEq E] [Add E] [Sub E] [Mul E] (sign sign' : E → Int) (a b : Endpoint E) (h : ∀ (x : E), x ∈ a.orderOperands b → sign x = sign' x) : lt (EndpointSigns.ofSign sign) a b = lt (EndpointSigns.ofSign sign') a b

Endpoint order depends only on the finite difference, when present.

theorem Hex.Endpoint.nonvanishing_congr {E : Type u} [Zero E] [DecidableEq E] [Add E] [Sub E] [Mul E] (sign sign' : E → Int) (a : Endpoint E) (p : DensePoly E) (h : ∀ (x : E), x ∈ a.nonvanishingOperands p → sign x = sign' x) : nonvanishing (EndpointSigns.ofSign sign) p a = nonvanishing (EndpointSigns.ofSign sign') p a

The nonvanishing guard depends only on its listed finite evaluation.

def Hex.TarskiCertificate.signOperands {E : Type u} {Ctx : Type v} [Zero E] [DecidableEq E] [Add E] [Sub E] [Mul E] (p : DensePoly E) (a b : Endpoint E) (cert : TarskiCertificate E E Ctx) : List E

All coefficients whose signs can affect this supplied whole query replay. Repeated operands are retained; sharing belongs to the evidence graph.

Equations

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

theorem Hex.TarskiCertificate.signs_congr {E : Type u} [Zero E] [DecidableEq E] [Add E] [Sub E] [Mul E] (sign sign' : E → Int) (chain : Array (DensePoly E)) (a : Endpoint E) (h : ∀ (x : E), x ∈ List.map (fun (x : DensePoly E) => a.signOperand x) chain.toList → sign x = sign' x) : signs sign (EndpointSigns.ofSign sign) chain a = signs sign' (EndpointSigns.ofSign sign') chain a

A literal endpoint sign vector depends only on the listed coefficients.

theorem Hex.TarskiCertificate.check_sign_congr {E : Type u} {Ctx : Type v} [Zero E] [DecidableEq E] [Add E] [Sub E] [Mul E] [One E] [NatCast E] [DecidableEq Ctx] (sign sign' : E → Int) (context : Ctx) (p f : DensePoly E) (a b : Endpoint E) (value : Int) (cert : TarskiCertificate E E Ctx) (h : ∀ (x : E), x ∈ signOperands p a b cert → sign x = sign' x) : check sign (EndpointSigns.ofSign sign) context p f a b value cert = check sign' (EndpointSigns.ofSign sign') context p f a b value cert

Finite sign agreement preserves complete literal query replay, including all domain guards, endpoint signs, identities and rejection paths, for endpoints in the coefficient domain with EndpointSigns.ofSign. Context and integer equality and literal binding checks are unchanged. No producer is run.