rhoBandLower_lt_one
plain-language theorem explainer
The theorem shows that the lower cognitive band boundary ρ_min = φ^{-2} is strictly less than 1. Workers on recognition band geometry in the Unification module cite it to place the band inside the unit interval. The proof unfolds the definition, invokes positivity and the inverse inequality for φ > 1, then closes with linear arithmetic.
Claim. Let ρ_min = φ^{-2}. Then ρ_min < 1.
background
In the RecognitionBandGeometry module the lower cognitive band boundary is defined by ρ_min = φ^{-2} while the upper boundary is ρ_upper = φ^{-1}. The result rests on the established fact that φ > 1, proved in Constants.lean and carried forward in PhiSupport. The local setting is the geometry of the recognition band used to organize constants on the phi-ladder.
proof idea
The proof unfolds the definition of the lower boundary to reach φ^{-2} < 1. It records 0 < φ^{-1} from inverse positivity and φ^{-1} < 1 from the inverse inequality applied to φ > 1. Linear arithmetic then finishes the comparison.
why it matters
The result confirms the lower boundary lies below unity and supports the ordering and summation properties of the band boundaries. It supplies a basic inequality needed for the geometry of the recognition band in the Unification setting, consistent with the self-similar role of φ in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.