bandUpper_ratio
The result establishes that at the upper boundary of the recognition band the ratio of the boundary value to its complement equals the golden ratio φ. Researchers deriving scaling relations or band widths in Recognition Science unification models cite this identity. The short term proof rewrites the complement via the band sum identity then reduces the ratio by field simplification.
claim$ρ_upper / (1 - ρ_upper) = φ$ where $ρ_upper = φ^{-1}$ and $φ$ denotes the golden ratio.
background
The RecognitionBandGeometry module introduces the cognitive recognition band with explicit boundaries. The upper boundary is defined as $ρ_upper = φ^{-1}$ and the lower as $ρ_lower = φ^{-2}$. A supporting theorem states that the boundaries sum to one, so $1 - ρ_upper = ρ_lower$. This local setting rests on the non-vanishing of φ established in the Constants, PhiLadderLattice and PhiSupport modules.
proof idea
The proof rewrites the denominator using the identity $1 - ρ_upper = ρ_lower$. It unfolds the definitions of both boundaries and applies field simplification, invoking the lemma that φ is nonzero to cancel terms and obtain φ directly.
why it matters in Recognition Science
The theorem supplies the upper-boundary counterpart to the lower-boundary ratio, completing the pair of identities needed for band geometry calculations. It feeds into phi-ladder scaling and recognition composition steps in the T5-T8 forcing chain. No downstream citations appear yet, so the result functions as a basic algebraic closure for boundary arithmetic.
scope and limits
- Does not derive the numerical value of φ.
- Does not prove existence or stability of the recognition band.
- Applies only to the static boundary definitions given.
- Does not address time evolution or dynamical crossing of the band.
formal statement (Lean)
77theorem bandUpper_ratio : rhoBandUpper / (1 - rhoBandUpper) = phi := by
proof body
Term-mode proof.
78 rw [one_sub_rhoBandUpper_eq_rhoBandLower]
79 unfold rhoBandLower rhoBandUpper
80 field_simp [phi_ne_zero]
81