def Hex.RemainderStep.map {D : Type u} {E : Type v} [Zero D] [DecidableEq D] [Zero E] [DecidableEq E] (f : D → E) (hz : ∀ (x : D), f x = 0 ↔ x = 0) (s : RemainderStep D) : RemainderStep E

Apply a zero-reflecting coefficient map to the supplied scales and quotient.

Equations

• Hex.RemainderStep.map f hz s = { leftScale := f s.leftScale, quotient := Hex.DensePoly.Interpret.map f hz s.quotient, rightScale := f s.rightScale }

def Hex.SignedRemainderChain.map {D : Type u} {E : Type v} [Zero D] [DecidableEq D] [Zero E] [DecidableEq E] (f : D → E) (hz : ∀ (x : D), f x = 0 ↔ x = 0) (cert : SignedRemainderChain D) : SignedRemainderChain E

Map the supplied remainder evidence without repeating polynomial division. Stored degrees are retained; zero reflection preserves every polynomial degree.

Equations

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

theorem Hex.SignedRemainderChain.map_checkStep {D : Type u} {E : Type v} [Zero D] [DecidableEq D] [Zero E] [DecidableEq E] (f : D → E) (hz : ∀ (x : D), f x = 0 ↔ x = 0) [Add D] [Add E] [Sub D] [Sub E] [Mul D] [Mul E] (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) (sign : D → Int) (sign' : E → Int) (hsgn : ∀ (a : D), sign' (f a) = sign a) (a b c : DensePoly D) (s : RemainderStep D) : checkStep sign' (DensePoly.Interpret.map f hz a) (DensePoly.Interpret.map f hz b) (DensePoly.Interpret.map f hz c) (RemainderStep.map f hz s) = checkStep sign a b c s

Scalar operation and sign preservation transport each checked recurrence.

theorem Hex.SignedRemainderChain.map_checks {D : Type u} {E : Type v} [Zero D] [DecidableEq D] [Zero E] [DecidableEq E] (f : D → E) (hz : ∀ (x : D), f x = 0 ↔ x = 0) [Add D] [Add E] [Sub D] [Sub E] [Mul D] [Mul E] (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) (sign : D → Int) (sign' : E → Int) (hsgn : ∀ (a : D), sign' (f a) = sign a) [NatCast D] [NatCast E] (hn : ∀ (n : Nat), f ↑n = ↑n) (p g : DensePoly D) (cert : SignedRemainderChain D) (h : check sign p g cert = true) : check sign' (DensePoly.Interpret.map f hz p) (DensePoly.Interpret.map f hz g) (map f hz cert) = true

An accepted literal chain remains accepted after a zero-reflecting map preserving scalar operations and signs. The map need not be injective.

def Hex.Endpoint.map {A : Type w} {B : Type w'} (k : A → B) : Endpoint A → Endpoint B

Map finite endpoint values, retaining the two infinities.

Equations

• Hex.Endpoint.map k Hex.Endpoint.negInf = Hex.Endpoint.negInf
• Hex.Endpoint.map k (Hex.Endpoint.finite a) = Hex.Endpoint.finite (k a)
• Hex.Endpoint.map k Hex.Endpoint.posInf = Hex.Endpoint.posInf

def Hex.TarskiCertificate.map {D : Type u} {E : Type v} [Zero D] [DecidableEq D] [Zero E] [DecidableEq E] (f : D → E) (hz : ∀ (x : D), f x = 0 ↔ x = 0) {A : Type w} {B : Type w'} {Ctx : Type w''} (k : A → B) (cert : TarskiCertificate D A Ctx) : TarskiCertificate E B Ctx

Transport all literal polynomial and endpoint data in a certificate. The context, signs, variations, and query value are retained exactly.

Equations

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

theorem Hex.TarskiCertificate.map_signAt {D : Type u} {E : Type v} [Zero D] [DecidableEq D] [Zero E] [DecidableEq E] (f : D → E) (hz : ∀ (x : D), f x = 0 ↔ x = 0) {A : Type w} {B : Type w'} (k : A → B) (sign : D → Int) (sign' : E → Int) (hsgn : ∀ (a : D), sign' (f a) = sign a) (ends : EndpointSigns D A) (ends' : EndpointSigns E B) (heval : ∀ (p : DensePoly D) (a : A), ends'.evalSign (DensePoly.Interpret.map f hz p) (k a) = ends.evalSign p a) (p : DensePoly D) (a : Endpoint A) : Endpoint.signAt sign' ends' (DensePoly.Interpret.map f hz p) (Endpoint.map k a) = Endpoint.signAt sign ends p a

theorem Hex.TarskiCertificate.map_signs {D : Type u} {E : Type v} [Zero D] [DecidableEq D] [Zero E] [DecidableEq E] (f : D → E) (hz : ∀ (x : D), f x = 0 ↔ x = 0) {A : Type w} {B : Type w'} (k : A → B) (sign : D → Int) (sign' : E → Int) (hsgn : ∀ (a : D), sign' (f a) = sign a) (ends : EndpointSigns D A) (ends' : EndpointSigns E B) (heval : ∀ (p : DensePoly D) (a : A), ends'.evalSign (DensePoly.Interpret.map f hz p) (k a) = ends.evalSign p a) (chain : Array (DensePoly D)) (a : Endpoint A) : signs sign' ends' (Array.map' (DensePoly.Interpret.map f hz) chain) (Endpoint.map k a) = signs sign ends chain a

theorem Hex.TarskiCertificate.map_checks {D : Type u} {E : Type v} [Zero D] [DecidableEq D] [Zero E] [DecidableEq E] (f : D → E) (hz : ∀ (x : D), f x = 0 ↔ x = 0) {A : Type w} {B : Type w'} (k : A → B) (sign : D → Int) (sign' : E → Int) (hsgn : ∀ (a : D), sign' (f a) = sign a) (ends : EndpointSigns D A) (ends' : EndpointSigns E B) (hcmp : ∀ (a b : A), ends'.compare (k a) (k b) = ends.compare a b) (heval : ∀ (p : DensePoly D) (a : A), ends'.evalSign (DensePoly.Interpret.map f hz p) (k a) = ends.evalSign p a) [One D] [One E] [Add D] [Add E] [Sub D] [Sub E] [Mul D] [Mul E] [NatCast D] [NatCast E] (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) (h1 : f 1 = 1) (hn : ∀ (n : Nat), f ↑n = ↑n) {Ctx : Type w''} [DecidableEq Ctx] [DecidableEq A] [DecidableEq B] (context : Ctx) (p g : DensePoly D) (a b : Endpoint A) (value : Int) (cert : TarskiCertificate D A Ctx) (h : check sign ends context p g a b value cert = true) : check sign' ends' context (DensePoly.Interpret.map f hz p) (DensePoly.Interpret.map f hz g) (Endpoint.map k a) (Endpoint.map k b) value (map f hz k cert) = true

Transport acceptance, including all literal bindings, through coefficient and endpoint maps. No injectivity or producer provenance is required.