Externalized Certification Meaning

Abstract

One realized decision transcript can carry collapsed or independently sampled certification value.

Theorem 1.1 (Certification meaning is external to the decision transcript).

$$\begin{array}{c}\forall epsilon:\mathbb{R},m:\mathbb{N},\\ 0<epsilon<1\wedge 0<m\Rightarrow \\ \mathrm{let}(implementation:Bool\to Bool={(}_{\mapsto }false),\\ expected:Bool\to Bool=id,\\ World=(\mathrm{Fin}(m)\to \mathrm{PMF}(Bool))\times (\mathrm{Fin}(m)\to Bool),\\ transcript:World\to \mathrm{Fin}(m)\to Bool=(world\mapsto j\mapsto \mathrm{decide}(implementation(world.2(j))=expected(world.2(j)))),\\ badGreenMass:World\to \mathbb{R}=(world\mapsto \prod _j(world.1(j)(false)).toReal));\\ \exists \mu :\mathrm{PMF}(Bool),W_c,W_i:World,\\ W_c.2=W_i.2\wedge \\ (\forall j,W_c.2(j)=false)\wedge \\ transcript(W_c)=transcript(W_i)\wedge \\ (\forall j,W_c.1(j)=\mathrm{pure}(W_c.2(j)))\wedge \\ (\forall j,W_i.1(j)=\mu )\wedge \\ \sum _{input:Bool}\text{if }implementation(input)=expected(input)\text{ then }0\text{ else }(\mu (input)).toReal=\frac{1+epsilon}{2}\wedge \\ epsilon<\sum _{input:Bool}\text{if }implementation(input)=expected(input)\text{ then }0\text{ else }(\mu (input)).toReal\wedge \\ badGreenMass(W_c)=1\wedge \\ badGreenMass(W_i)={\frac{1-epsilon}{2}}^m\wedge \\ badGreenMass(W_i)\le \exp (-(epsilon\times (m:\mathbb{R})))\wedge \\ \exp (-(epsilon\times (m:\mathbb{R})))<badGreenMass(W_c)\wedge \\ W_c.1\ne W_i.1\wedge \\ \neg \mathrm{FactorsThrough}(badGreenMass,transcript)\wedge \\ \neg \mathrm{FactorsThrough}((world\mapsto \forall j,world.1(j)=\mu ),transcript).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Interpretation/ExternalizedCertificationMeaning.externalized_certification_meaning (✓ std3). ∎

Source. Repository-derived.

Commentary.

The implementation is the constant-false Boolean program and the expected behavior is the identity. The constructed deployment law gives the single failing input mass (1 + epsilon)/2, strictly above epsilon.

Both worlds realize the same all-false suite and therefore the same all-green bit transcript. In the co-selected world every coordinate law is concentrated on that realized input. In the independent world every coordinate law equals the deployment law.

The bad-green mass is the product of the coordinate pass masses. It is one under co-selection and ((1 - epsilon)/2)^m under independent sampling. The repository exponential bound gives the displayed certification envelope, while positivity of epsilon and m makes the co-selected mass strictly exceed that envelope.

The final two clauses state the information-theoretic corollary directly: neither bad-green mass nor the independent-sampling precondition factors through the transcript. The source explicitly leaves signature semantics out of scope, so no separate universal semantics of signing is invented.

References

• Truth anchor: D5/S3/ConceptDynamics/Interpretation/ExternalizedCertificationMeaning.externalized_certification_meaning
• Dependency: D5/S3/TotalVariation/IndependentSamplingExponentialBound