rhoBandUpper_pos
plain-language theorem explainer
The theorem establishes positivity of the upper recognition band boundary. Researchers deriving band inequalities on the phi-ladder cite it to bound the cognitive interval from below. The proof is a one-line term reduction that unfolds the definition and invokes the inverse-positivity lemma on phi.
Claim. $0 < phi^{-1}$ where $phi$ denotes the golden-ratio fixed point of the self-similar map.
background
The RecognitionBandGeometry module defines the upper cognitive band boundary as rhoBandUpper := phi inverse. This definition participates in the unification setting that extracts spatial dimension D=3 and the eight-tick octave from the forcing chain T0-T8 together with the Recognition Composition Law. The result depends only on the upstream definition of rhoBandUpper and the already-established positivity of phi.
proof idea
The term proof first unfolds rhoBandUpper to obtain the expression phi inverse, then applies inv_pos.mpr directly to the hypothesis phi_pos.
why it matters
The positivity statement anchors the ordering of band boundaries inside the Recognition framework and is a prerequisite for the sibling inequality rhoBandLower_lt_rhoBandUpper. It aligns with the phi-ladder mass formula and the Berry creation threshold at phi inverse, closing a basic geometric fact required by downstream unification lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.