Party Simulation and Fresh-Beacon Certification

Abstract

Party-simulable certificates have bounded approval, while a fresh beacon gives a product-law guarantee with an explicit total-variation charge.

Theorem 1.1 (Simulation necessity and fresh-beacon sufficiency).

$$\begin{array}{c}\forall Seed,VerifierCoin,Input,Output,Certificate,Anchor,Task:\mathrm{Type},\\ [\mathrm{MeasurableSpace}(Seed)],[\mathrm{MeasurableSpace}(VerifierCoin)],[\mathrm{MeasurableSpace}(Input)],[\mathrm{MeasurableSpace}(Output)],[\mathrm{MeasurableEq}(Output)],\\ [\mathrm{MeasurableSpace}(Certificate)],[\mathrm{MeasurableSpace}(Anchor)],[\mathrm{MeasurableSpace}(Task)],deployment:\mathrm{Measure}\left(Input\right),[\mathrm{IsProbabilityMeasure}(deployment)],\\ expected:Input\to Output,\mathrm{Measurable}\left(expected\right),\\ m:\mathbb{N},epsilon,delta:\mathbb{R},\\ seedLaw:\mathrm{Measure}\left(Seed\right),[\mathrm{IsProbabilityMeasure}(seedLaw)],\\ verifierCoinLaw:\mathrm{Measure}\left(VerifierCoin\right),[\mathrm{IsProbabilityMeasure}(verifierCoinLaw)],\\ partySuite:Seed\to \mathrm{Fin}\left(m\right)\to Input,\mathrm{Measurable}\left(partySuite\right),\\ certificate:Seed\to Certificate,\mathrm{Measurable}\left(certificate\right),\\ verifier:(\mathrm{Fin}\left(m\right)\to (Input)\times (Output))\times (Certificate)\to VerifierCoin\to Bool,\mathrm{Measurable}\left(\mathrm{uncurry}\left(verifier\right)\right),\\ coSelected:Seed\to Input\to Output,\\ taskLaw:\mathrm{Measure}\left(Task\right),[\mathrm{IsProbabilityMeasure}(taskLaw)],\\ anchorLaw:\mathrm{Measure}\left(Anchor\right),[\mathrm{IsProbabilityMeasure}(anchorLaw)],\\ suiteMap:Anchor\to \mathrm{Fin}\left(m\right)\to Input,\mathrm{Measurable}\left(suiteMap\right),\\ implementation:Task\to Input\to Output,\mathrm{Measurable}\left(\mathrm{uncurry}\left(implementation\right)\right),\\ \mathrm{let}(L:(Input\to Output)\to \mathbb{R}=(P\mapsto \mathrm{real}\left(deployment,\left\{P(x)\ne expected(x)\mid x\in Input\right\}\right)),\\ nuParty:\mathrm{Measure}\left((Seed)\times (VerifierCoin)\right)=\mathrm{prod}\left(seedLaw,verifierCoinLaw\right),\\ nuBeacon:\mathrm{Measure}\left((Task)\times (Anchor)\right)=\mathrm{prod}\left(taskLaw,anchorLaw\right),\\ partyRecord:(Seed\to Input\to Output)\to Seed\to \mathrm{Fin}\left(m\right)\to (Input)\times (Output)=(strategy\mapsto (s\mapsto (i\mapsto (partySuite(s,i),strategy(s,partySuite(s,i)))))),\\ honestRecord:Seed\to \mathrm{Fin}\left(m\right)\to (Input)\times (Output)=(s\mapsto (i\mapsto (partySuite(s,i),expected(partySuite(s,i))))),\\ muInduced:\mathrm{Measure}\left(\mathrm{Fin}\left(m\right)\to Input\right)=\mathrm{map}\left(suiteMap,anchorLaw\right),\\ muIdeal:\mathrm{Measure}\left(\mathrm{Fin}\left(m\right)\to Input\right)=\mathrm{pi}\left((i\mapsto deployment)\right));\\ ((\forall strategy:Seed\to Input\to Output,\mathrm{real}\left(nuParty,\left\{verifier((partyRecord(strategy,omega.1),certificate(omega.1)),omega.2)=true\wedge epsilon<L(strategy(omega.1))\mid omega\in (Seed)\times (VerifierCoin)\right\}\right)\le delta)\Rightarrow \\ (\forall s:Seed,i:\mathrm{Fin}\left(m\right),coSelected(s,partySuite(s,i))=expected(partySuite(s,i)))\Rightarrow \\ (\forall s:Seed,epsilon<L(coSelected(s)))\Rightarrow \\ \mathrm{real}\left(nuParty,\left\{verifier((honestRecord(omega.1),certificate(omega.1)),omega.2)=true\mid omega\in (Seed)\times (VerifierCoin)\right\}\right)\le delta\wedge 1-delta\le \mathrm{real}\left(nuParty,\left\{verifier((honestRecord(omega.1),certificate(omega.1)),omega.2)=false\mid omega\in (Seed)\times (VerifierCoin)\right\}\right))\wedge \\ (0\le epsilon\Rightarrow \\ epsilon\le 1\Rightarrow \\ (\forall t:Task,epsilon<L(implementation(t)))\Rightarrow \\ nuBeacon(\left\{\forall i:\mathrm{Fin}\left(m\right),implementation(z.1,suiteMap(z.2,i))=expected(suiteMap(z.2,i))\mid z\in (Task)\times (Anchor)\right\})\le \mathrm{ofReal}\left((1-epsilon{)}^m\right)+\mathrm{measurableTotalVariation}\left(muInduced,muIdeal\right)).\end{array}$$

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

Source. Repository-derived.

Commentary.

The first implication quantifies over arbitrary probability laws for the party seed and verifier coin, and every seed-indexed implementation. The certificate depends only on the party seed, and the co-selected bad implementation agrees with expected behavior on that same suite. Taking the suite itself as the seed, the deployment product measure as its law, and the identity suite map realizes the source sampling.

Reliability therefore applies to a verifier input identical to the honest all-green input. Approval of the fixed nontrivial tier has probability at most delta, and total Boolean output makes the trivial tier its probability complement.

The second implication lets each task select its committed implementation before the anchor. Task and anchor are governed by their product measure, the public suite map pushes the anchor law forward, and the ideal suite is the deployment product measure on the unrestricted input carrier.

For every fixed task, the independent all-pass bound is transported to the induced suite law through measurable-event total variation, then integrated over the task law. Every measurability, probability-law, map, predicate, and threshold premise is displayed explicitly in the proposition.

References

• Truth anchor: D5/S3/ConceptDynamics/Interpretation/PartySimulationFreshBeaconCertification.party_simulation_and_fresh_beacon_certification
• Dependency: D5/S3/Estimation/DataProcessing/MeasurablePostprocessingDefectContraction