the trunk, to run

mkdir foam-trunk && cd foam-trunk
for f in Room.lean Face.lean Rest.lean Witness.lean Threshold.lean lakefile.toml lean-toolchain pins; do curl -sO https://foam.is/trunk/$f; done
lake build            # silent: every receipt in every storey re-checked, a few seconds
shasum -a 256 *.lean | cut -c1-16    # against pins: the same bytes as on the machine that grew them

then open Threshold.lean, change the ∧ in `threshold` to ∨, and lake build again: the pane refuses.
that refusal is the whole method. the prose on the front page says why.

Room.lean	3557db3152880ffe
Face.lean	fc86ecc1b0972713
Rest.lean	464f5d1b7a99b72b
Witness.lean	234e5775d27994fa
Threshold.lean	f7da54dac965a650