rhoBandLower_pos
plain-language theorem explainer
The theorem shows that the lower cognitive band boundary, defined as phi inverse squared, is strictly positive. Unification researchers cite it when establishing bounds on the recognition parameter rho in band geometry. The proof is a short term-mode argument that unfolds the definition and invokes positivity after confirming the inverse of phi is positive.
Claim. Let $0 < rho_min$ where $rho_min := phi^{-2}$ and $phi$ is the self-similar fixed point.
background
The RecognitionBandGeometry module defines the cognitive band boundaries using the golden ratio phi from the forcing chain. The lower boundary is given explicitly by phi inverse squared. This construction operates inside the Unification setting where phi arises as the fixed point at step T6.
proof idea
The proof unfolds the definition of the lower boundary to phi inverse squared. It applies the inverse positivity lemma to the known positivity of phi to obtain that phi inverse is positive. The positivity tactic then concludes the square is positive.
why it matters
This result secures the lower edge of the cognitive band above zero and supports later inequalities comparing the lower and upper boundaries. It aligns with the self-similar fixed point at T6 and the positive measures required by the eight-tick octave. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.