bandLower_ratio
The theorem shows that at the lower recognition band boundary the ratio of density to its complement equals the inverse golden ratio. Workers on Recognition Science band geometry cite it to close the lower-boundary case in the phi-ladder setup. The proof is a short algebraic reduction that rewrites the complement via the sum-to-one relation, substitutes the explicit power definitions, and cancels using the nonzero property of phi.
claimLet the lower band boundary be given by $ρ = φ^{-2}$. Then $ρ/(1-ρ) = φ^{-1}$.
background
The RecognitionBandGeometry module introduces the cognitive recognition band whose lower edge is the definition rhoBandLower = φ^{-2} and whose upper edge is rhoBandUpper = φ^{-1}. These two quantities are shown to sum to one by the sibling theorem bandBoundaries_sum_to_one, which immediately yields the auxiliary equality 1 - rhoBandLower = rhoBandUpper. The present result therefore supplies the complementary ratio identity at the lower edge once the upper-edge ratio (equal to φ) is already known.
proof idea
The term proof rewrites the denominator 1 - rhoBandLower by the equality one_sub_rhoBandLower_eq_rhoBandUpper, unfolds both rhoBandLower and rhoBandUpper to their explicit powers of φ^{-1}, and finishes with field_simp using the lemma phi_ne_zero.
why it matters in Recognition Science
The declaration supplies the missing lower-boundary ratio that pairs with the upper-boundary statement ρ/(1-ρ) = φ. Together they fix the geometry of the recognition band inside the unification module and rest on the phi-ladder definitions imported from PhiLadderLattice. No downstream use sites are recorded, indicating the result functions as a self-contained closure for the band-boundary algebra.
scope and limits
- Does not derive the band boundaries from the forcing chain.
- Does not treat the physical or cognitive interpretation of the band.
- Does not extend the ratio identity beyond the phi-ladder setting.
- Does not address higher-dimensional or non-real embeddings.
formal statement (Lean)
71theorem bandLower_ratio : rhoBandLower / (1 - rhoBandLower) = phi⁻¹ := by
proof body
Term-mode proof.
72 rw [one_sub_rhoBandLower_eq_rhoBandUpper]
73 unfold rhoBandLower rhoBandUpper
74 field_simp [phi_ne_zero]
75
76/-- At the upper boundary, `ρ/(1-ρ) = φ`. -/