rhoBandLower_eq
plain-language theorem explainer
The equality fixes the lower cognitive band boundary at the square of the inverse golden ratio. Researchers deriving critical loading thresholds in the Recognition Science unification cite this result to anchor the minimum control parameter. The proof is a direct reflexivity step that follows immediately from the definition of the lower band boundary.
Claim. The lower cognitive band boundary satisfies $ρ_{min} = φ^{-2}$.
background
In the RecognitionBandGeometry module the lower band boundary is introduced as the real number defined by the explicit expression involving the inverse golden ratio. The golden ratio φ is the self-similar fixed point forced at step T6 of the unified forcing chain. This sets the lower edge of the recognition band used for cognitive operations in the unification setting.
proof idea
The proof is a one-line wrapper that applies the reflexivity tactic. The definition of rhoBandLower is exactly φ inverse squared, so the claimed equality holds by direct substitution with no additional lemmas required.
why it matters
This result supplies the explicit value imported by the downstream theorem rhoCriticalMin_eq that fixes the control band for the runtime. It anchors the phi-ladder rung for band boundaries inside the Recognition Science framework and is consistent with the eight-tick octave and the forcing chain steps T5 through T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.