Helper

dsdp_algebraic_correctness

Section trace_entropy_analysis

Type Lemma

Proof Lines 5

Lemma dsdp_algebraic_correctness : forall t, S t = (U1 \* V1 \+ U2 \* V2 \+ U3 \* V3) t.

The protocol correctness theorem: the sum S equals the dot product. This is proved algebraically without depending on trace structure.

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...