one_sub_rhoBandLower_eq_rhoBandUpper
plain-language theorem explainer
The lower and upper boundaries of the cognitive band satisfy 1 minus the lower boundary equals the upper boundary. Researchers deriving ratio identities in recognition band geometry cite this relation. The proof is a one-line wrapper applying linear arithmetic directly to the theorem that the two boundaries sum to one.
Claim. $1 - rho_min = rho_max$, where $rho_min = phi^{-2}$ is the lower cognitive band boundary and $rho_max = phi^{-1}$ is the upper cognitive band boundary.
background
The module introduces the lower cognitive band boundary as the square of the inverse golden ratio, $rho_min = phi^{-2}$, and the upper boundary as $rho_max = phi^{-1}$. The key upstream result is the theorem that these two boundaries sum to one, established by unfolding the definitions, applying field simplification with the relation $phi^2 = phi + 1$, and invoking nlinarith together with positivity of phi. The local setting is the unification of recognition band geometry, which builds on constants from the Recognition Science framework where phi serves as the self-similar fixed point.
proof idea
This is a one-line wrapper that applies the linarith tactic to the bandBoundaries_sum_to_one theorem asserting that the lower and upper boundaries add to one. No unfolding of definitions or additional lemmas beyond that sum identity is required.
why it matters
This identity feeds directly into the bandLower_ratio theorem establishing that at the lower boundary the ratio of rho over one minus rho equals the inverse of phi. It supplies an algebraic step in recognition band geometry that connects to the phi-ladder and self-similarity properties in the Recognition Science framework, specifically the forcing of phi as the self-similar fixed point. No open questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.