Base-$(2-\omega)$ digit expansions and adaptive correctness for the KFLT Groth16 garbling scheme

Trust-minimised Bitcoin bridges in the BitVM lineage garble a Groth16 verifier and disclose a secret exactly when a published proof is invalid. Khambhati, Feickert, Lewe and Tiwari (KFLT) garble the pairing over the source and target groups directly, obtaining a $2.44$ MiB scheme for BN254, much of it variable cost from rekeying and from the group encodings. We replace the binary decomposition of the rekeying scalar by a base-$(2-\omega)$ expansion with digits in $\Sigma_{\mathrm{CM}}=\{0,\pm1,\pm\omega,\pm\omega^2\}$, the free endomorphisms of the $j=0$ curve, cutting the A-encoding dimension from $3053$ to $1109$ ($L\le92$ versus $254$). We prove the greedy expansion correct with length at most $\lfloor\log_7\mathrm{N}(z)\rfloor+2$ and machine-check the BN254 bound in Lean 4 via a square-root-free threshold chain. We then identify an adaptive-correctness gap: the incomplete Jacobian formulas used to realise the encodings can be steered to return $\bot$ by a garbler who chooses the proof after garbling. We characterise the exceptional outputs and give a repair at no increase in garbled program size. Costing the stacked changes brings the scheme from $2.44$ MiB to roughly $1.1$ MiB, at which point the untouched fixed cost is $80\%$ of the program.