rhoBandLower
plain-language theorem explainer
rhoBandLower fixes the lower cognitive band boundary at φ^{-2}. Workers on critical loading and band geometry cite it to anchor phase-transition thresholds in the unification module. It is introduced by direct assignment from the golden ratio inverse squared.
Claim. The lower cognitive band boundary is defined by $ρ_{min} := φ^{-2}$.
background
RecognitionBandGeometry fixes the cognitive recognition band using powers of the golden ratio φ imported from Constants. The upstream band operation from PreLogicalCost performs arithmetic conjunction on stable states via 0/1 multiplication. This definition sets the lower edge ρ_min at φ^{-2}, which pairs with the upper edge at φ^{-1} to satisfy the sum-to-one and product identities.
proof idea
One-line definition that directly assigns phi inverse squared. No lemmas or tactics are applied.
why it matters
This definition supplies the lower threshold used by rhoCriticalMin in CriticalRecognitionLoading and by the band boundary theorems (sum to one, product equals φ^{-3}, ratio identities). It realizes the phi-ladder structure from T6 in the forcing chain, anchoring recognition thresholds for the eight-tick octave and D=3 geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.