def Hex.RCF.buildCarrier? (s : Sentence) : Option CarrierCert

Build a square-free carrier and retain it only after the kernel-facing checker accepts all multiplication identities and the generalized replay.

Equations

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

theorem Hex.RCF.check_buildCarrier {s : Sentence} {cert : CarrierCert} (h : buildCarrier? s = some cert) : CarrierCert.check s cert = true

Every carrier emitted by compiled preparation has passed its checker.

def Hex.RCF.buildCommonRoot? (atom carrier : ZPoly) : Option CommonRootCert

Build one common-root package by rational extended gcd and retain it only after all divisibility, scaled Bezout, and replay checks pass.

Equations

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

theorem Hex.RCF.check_buildCommonRoot {atom carrier : ZPoly} {cert : CommonRootCert} (h : buildCommonRoot? atom carrier = some cert) : CommonRootCert.check atom carrier cert = true

Every common-root package emitted by compiled preparation has passed its checker against the external atom and carrier.

def Hex.RCF.buildCommonRoots? (s : Sentence) (carrier : ZPoly) : Option (List CommonRootCert)

Build one checker-retained common-root package per distinct nonconstant sentence polynomial, in the exact order expected by the sign-matrix checker.

Equations

• Hex.RCF.buildCommonRoots? s carrier = Hex.RCF.buildCommonRootsFrom?✝ carrier (Hex.RCF.dedupPolys s.polys)

theorem Hex.RCF.check_buildCommonRoots {s : Sentence} {carrier : ZPoly} {commons : List CommonRootCert} (h : buildCommonRoots? s carrier = some commons) : checkCommon carrier (dedupPolys s.polys) commons = true

Every emitted common-root list passes the sign-matrix alignment checker against the recomputed distinct polynomial order.