bandBoundaries_sum_to_one
plain-language theorem explainer
The lower and upper boundaries of the recognition band satisfy ρ_lower + ρ_upper = 1. Researchers deriving complementary relations or normalizing measures on the phi-ladder cite this identity. The proof unfolds the explicit definitions ρ_lower = φ^{-2} and ρ_upper = φ^{-1}, invokes the golden-ratio identities φ ≠ 0 and φ² = φ + 1, then closes by field simplification and nonlinear arithmetic.
Claim. Let ρ_min = φ^{-2} and ρ_max = φ^{-1}. Then ρ_min + ρ_max = 1.
background
In the RecognitionBandGeometry module the recognition band is delimited by two real numbers expressed via the golden ratio φ. The lower boundary is defined as ρ_lower = φ^{-2} and the upper boundary as ρ_upper = φ^{-1}. These definitions rest on the phi-ladder lattice and the self-similar fixed-point property of φ. The upstream lemmas phi_ne_zero and phi_sq_eq supply φ ≠ 0 together with the defining relation φ² = φ + 1 that enables all subsequent algebraic reduction.
proof idea
The term proof first unfolds rhoBandLower and rhoBandUpper to their explicit expressions. It obtains phi_ne_zero and phi_sq_eq to license division and substitution. Field_simp clears the resulting denominators, after which nlinarith finishes the equality by invoking positivity of φ and the quadratic identity φ² = φ + 1.
why it matters
The identity is the direct premise for the two complementary theorems one_sub_rhoBandLower_eq_rhoBandUpper and one_sub_rhoBandUpper_eq_rhoBandLower, each obtained by a single linarith step. It supplies the normalization condition required for band geometry inside the unification layer, linking the phi fixed point to the eight-tick octave and the three-dimensional spatial structure. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.