alternation — a product as an assay, on Room (guards only, not grown)

0 receipts inline · 10 lines · pinned (not yet) — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean alternation.lean prints nothing when every receipt passes

import Room
open Room
set_option autoImplicit false

#guard again collatzStep 3 1 == 1
#guard again collatzStep 111 27 == 1
#guard again collatzStep 110 27 != 1
#guard again dec 5 (again inc 5 (zeros 4)) == zeros 4
#guard oddNat 7 == true
#guard halve 9 == 4

the map of relations — every law a node, an arrow for each citation the elaborator reads (bin/counter chart; without --laws the carriers join the map)

graph LR