Proves a fixed-point approximation of a publicly known architecture

The prover's model must have a "publicly known structure". Tensors are discretised by scaling and rounding ¹. The authors report perplexity changes of 0.008 to 0.09 on C4 ¹. The proof covers the quantised computation.