rhoBandLower_lt_rhoBandUpper
plain-language theorem explainer
The lower cognitive band boundary is strictly less than the upper boundary. Researchers modeling Recognition Science band geometry cite this to confirm the ordering of limits derived from the golden ratio. The proof is a short algebraic reduction that unfolds the definitions and applies standard inequalities on the inverse golden ratio.
Claim. Let $ρ_{lower} = φ^{-2}$ and $ρ_{upper} = φ^{-1}$, where $φ > 1$ is the golden ratio. Then $ρ_{lower} < ρ_{upper}$.
background
In the Recognition Band Geometry module the cognitive band is delimited by two quantities derived from the golden ratio. The lower boundary is defined as the square of the inverse golden ratio, $ρ_{lower} = φ^{-2}$, while the upper boundary is the inverse itself, $ρ_{upper} = φ^{-1}$. These arise as the endpoints of the recognition band in the unification setting.
proof idea
The proof unfolds the two definitions, invokes positivity of $φ^{-1}$ together with the fact that $φ^{-1} < 1$ (from the one_lt_phi lemma), and finishes with a nonlinear arithmetic tactic that verifies the resulting inequality.
why it matters
This result establishes the strict ordering of the band boundaries, a prerequisite for any interval-based construction in the Recognition Science framework. It sits inside the band-geometry layer of the unification module and supports later definitions that treat the interval between these limits as the cognitive band. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.