rhoBandUpper_pos
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 in Recognition Science
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.
scope and limits
- Does not compute the numerical value of the lower band boundary.
- Does not address extensions beyond the real numbers.
- Does not prove the sum-to-one identity for the two band edges.
formal statement (Lean)
24theorem rhoBandUpper_pos : 0 < rhoBandUpper := by
proof body
Term-mode proof.
25 unfold rhoBandUpper
26 exact inv_pos.mpr phi_pos
27