band
plain-language theorem explainer
The band definition supplies arithmetic conjunction on stable states by multiplying their 0/1 bits. Researchers working on Recognition Science aesthetics and acoustics invoke it when composing pre-logical configurations. The construction refines the StableState structure and exhausts the four bit cases to confirm the product remains 0 or 1.
Claim. For stable states $a$ and $b$ whose bits lie in the set $0,1$, the conjunction band$(a,b)$ is the stable state whose bit equals the product $a_0 b_0$.
background
StableState is the structure whose field bit : ℝ is witnessed by is_bit : bit = 0 ∨ bit = 1. The module PreLogicalCost treats these objects as the elementary pre-logical values constrained to the unit interval. Band is the first of the boolean operations defined on this carrier; its upstream dependency is exactly the StableState structure itself.
proof idea
The definition uses refine to build a new StableState from the product of the input bits together with a fresh proof obligation. It then applies rcases twice to split the two is_bit disjunctions and finishes with simp on the four resulting arithmetic identities.
why it matters
Band is referenced by forty downstream declarations, among them optimalT60 (which sets reverberation time to phi), acceptanceBandRatio_eq, beautyScore_at_phi, and the photobiomodulation band checks. It supplies the multiplicative fragment of the boolean algebra on stable states that precedes J-cost and the phi-ladder. No open scaffolding remains at this layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.