even-money — 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 even-money.lean prints nothing when every receipt passes

import Room
open Room
set_option autoImplicit false

#guard ((perms [1, 2, 3]).filter (firstOf Nat.beq 1 2)).length == 3
#guard (perms [1, 2, 3]).length == 6
#guard ((perms [1, 2, 3, 4]).filter (firstOf Nat.beq 1 2)).length == 12
#guard (perms [1, 2, 3, 4]).length == 24
#guard trade Nat.beq 1 2 1 == 2
#guard trade Nat.beq 1 2 3 == 3

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