rhoBandUpper
plain-language theorem explainer
rhoBandUpper sets the upper boundary of the recognition band to the reciprocal of the golden ratio. Researchers deriving band ratios or products in the unification layer cite it to close the complementary pair with the lower boundary. The declaration is a direct abbreviation with no lemmas or computation.
Claim. The upper boundary of the recognition band satisfies $ρ_{upper} = φ^{-1}$.
background
The RecognitionBandGeometry module defines a recognition band on the real line whose endpoints are built from the golden ratio phi, the self-similar fixed point forced by the Recognition Composition Law. rhoBandUpper supplies the upper endpoint directly as the multiplicative inverse of phi, pairing with the lower endpoint to satisfy the sum-to-one identity shown in bandBoundaries_sum_to_one. This construction sits inside the broader unification setting that imports constants and applies the phi-ladder geometry.
proof idea
The declaration is a one-line abbreviation that directly assigns the value phi inverse.
why it matters
It supplies the upper edge required by parent results bandBoundaries_sum_to_one, bandBoundaries_product, bandUpper_ratio, and one_sub_rhoBandUpper_eq_rhoBandLower. These theorems establish the geometric constraints on recognition bands and feed the unification layer. The definition anchors the phi-derived boundaries that appear in the eight-tick octave and D=3 spatial structure of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.