def Hex.RCF.buildIsolations? (carrier : CarrierCert) : Option IsolationCert

Run executable isolation, validate the raw intervals against the carrier's literal replay, and refine touching intervals to strict separation.

Equations

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

theorem Hex.RCF.check_buildIsolations {carrier : CarrierCert} {isolations : IsolationCert} (h : buildIsolations? carrier = some isolations) : IsolationCert.checkStrict carrier.replay isolations = true

Every emitted isolation array passes the generalized strict checker.

def Hex.RCF.buildIocCmps? (carrier : CarrierCert) (isolations : IsolationCert) (a b : Dyadic) : Option (IocCmps isolations.intervals.size)

Build both size-indexed endpoint-comparison vectors and retain them only after the endpoint checker accepts every position.

Equations

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

theorem Hex.RCF.check_buildIocCmps {carrier : CarrierCert} {isolations : IsolationCert} {a b : Dyadic} {cmps : IocCmps isolations.intervals.size} (h : buildIocCmps? carrier isolations a b = some cmps) : IocCmps.check carrier.carrier carrier.replay isolations a b cmps = true

Every emitted endpoint package passes its positional checker.

def Hex.RCF.buildSignMatrix? (s : Sentence) (carrier : CarrierCert) : Option SignMatrixCert

Wrap the aligned common-root list as a sign-matrix certificate, retaining it only after the sign-matrix alignment checker accepts it.

Equations

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

theorem Hex.RCF.check_buildSignMatrix {s : Sentence} {carrier : CarrierCert} {signs : SignMatrixCert} (h : buildSignMatrix? s carrier = some signs) : SignMatrixCert.check s carrier signs = true

Every emitted sign-matrix package passes its alignment checker.

structure Hex.RCF.BuildResult : Type

A compiled build result retains the certificate that produced its diagnostic or proof-producing verdict.

• certificate : Certificate

  The certificate accepted by three-valued replay.

• verdict : Bool

  The replay verdict. false remains diagnostic only.

def Hex.RCF.build? (s : Sentence) : Option BuildResult

Assemble a certificate and reject it if replay finds malformed evidence.

Equations

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

theorem Hex.RCF.replay_build {s : Sentence} {result : BuildResult} (h : build? s = some result) : Certificate.replay? s result.certificate = some result.verdict

A retained build result records exactly the certificate's replay verdict.

def Hex.RCF.decide (s : Sentence) : Option Bool

Compiled convenience decision. False is diagnostic. True is returned only after the kernel-facing Boolean checker accepts the retained certificate.

Equations

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

theorem Hex.RCF.exists_cert_of_decide {s : Sentence} (h : decide s = some true) : ∃ (cert : Certificate), Certificate.check s cert = true

A true compiled verdict exposes a certificate accepted by the checker.