Joint-Law Certification Value Separation

Abstract

The same complete decision transcript can carry separated certification values under co-selected and independently sampled joint laws.

Theorem 1.1 (Certification value is not a function of the decision transcript).

$$\begin{array}{c}\forall epsilon:\mathbb{R},m:\mathbb{N},\\ 0<epsilon\wedge epsilon<1\wedge 0<m\Rightarrow \\ \mathrm{let}(implementation:Bool\to Bool={(}_{\mapsto }false),\\ expected:Bool\to Bool=id,\\ World=(\mathrm{Measure}(\mathrm{Fin}(m)\to Bool))\times (\mathrm{Fin}(m)\to Bool),\\ transcript:World\to (\mathrm{Fin}(m)\to Bool)\times (\mathrm{Fin}(m)\to Bool)=(world\mapsto (world.2,(j\mapsto \mathrm{decide}(implementation(world.2(j))=expected(world.2(j)))))),\\ certificationValue:World\to \mathbb{R}=(world\mapsto \mathrm{badGreenMass}(implementation,expected,world.1)));\\ \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 \\ W_c.1=\mathrm{dirac}(W_c.2)\wedge \\ W_i.1=\mathrm{pi}(j\mapsto \mathrm{toMeasure}(\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 \\ certificationValue(W_c)=1\wedge \\ certificationValue(W_i)={\frac{1-epsilon}{2}}^m\wedge \\ certificationValue(W_i)\le \exp (-(epsilon\times (m:\mathbb{R})))\wedge \\ \exp (-(epsilon\times (m:\mathbb{R})))<certificationValue(W_c)\wedge \\ W_c.1\ne W_i.1\wedge \\ \neg \mathrm{FactorsThrough}(certificationValue,transcript)\wedge \\ \neg \mathrm{FactorsThrough}((world\mapsto world.1=\mathrm{pi}(j\mapsto \mathrm{toMeasure}(\mu ))),transcript).\end{array}$$

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

Source. Repository-derived.

Commentary.

For a threshold strictly between zero and one and a positive suite budget, the implementation is the constant-false Boolean program and the expected behavior is the identity.

The two worlds realize the same suite and the same complete suite-and-verdict transcript. The co-selected world has the Dirac law at that suite, while the independent world has the finite product of the deployment law.

Deployment loss is strictly above epsilon. The co-selected bad-green mass is one, while the independent mass is the displayed product and lies below the exponential envelope; positive budget makes the separation strict.

The final clauses state directly that neither certification value nor the independent-product-law status factors through the transcript.

References

• Truth anchor: D5/S3/ConceptDynamics/Interpretation/JointLawCertificationValueSeparation.joint_law_certification_value_separation
• Dependency: D5/S3/ConceptDynamics/Interpretation/JointLawExternalizedCertificationMeaning