rhoBandUpper_lt_one
plain-language theorem explainer
The upper recognition band boundary satisfies rho_upper < 1. Researchers on the phi-ladder and band geometry in Recognition Science cite this to place the upper edge inside the unit interval. The proof is a term-mode wrapper that unfolds the definition rho_upper = phi inverse and applies the reciprocal inequality to the established fact one less than phi.
Claim. Let $rho_upper = phi^{-1}$. Then $rho_upper < 1$.
background
In the RecognitionBandGeometry module the upper band boundary is introduced as the definition rhoBandUpper := phi inverse, where phi is the golden ratio. This definition appears alongside the lower boundary and supports later statements that the two boundaries sum to one. The local setting is the geometry of recognition bands inside the Unification layer, which rests on the phi-ladder structure.
proof idea
The term proof first unfolds rhoBandUpper to obtain phi inverse, then applies the lemma inv_lt_one_of_one_lt0 directly to the upstream fact one_lt_phi. No further tactics are required.
why it matters
The result confirms that the upper cognitive band boundary lies strictly below unity, a prerequisite for statements such as bandBoundaries_sum_to_one. It draws on the foundational inequality one_lt_phi established in Constants and PhiSupport, reinforcing the self-similar fixed-point property of phi at step T6 of the forcing chain. The theorem therefore anchors the band geometry used in later unification arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.