module module high

`IndisputableMonolith.Unification.RecognitionBandGeometry`

RecognitionBandGeometry fixes the lower and upper edges of the cognitive recognition band at rho_min = phi^{-2} and rho_max = 1 - phi^{-2}. These bounds delimit admissible load ratios for semantic condensation. Control theorems on recognition bandwidth cite the interval directly. The module supplies the definitions plus elementary algebraic verifications of positivity, ordering, and complementarity.

claim$0 < 1/φ² < 1 - 1/φ² < 1$ with the lower boundary $ρ_min = φ^{-2}$ and upper boundary $ρ_max = 1 - φ^{-2}$ satisfying $ρ_min + ρ_max = 1$.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants. It operates inside the Recognition Science setting where phi is the self-similar fixed point forced by the J-uniqueness relation. The recognition band is the interval of load ratios rho = R_dem / R_max inside which the semantic condensation gate is active. Sibling definitions introduce rhoBandLower as the explicit lower edge 1/φ² together with the complementary upper edge and the sum-to-one identity.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the geometric bounds required by the downstream CriticalRecognitionLoading module, which sketches the control theorem for the operating regime inside recognition bandwidth. The band geometry anchors the load-ratio variable rho used in the semantic condensation gate.

scope and limits

Does not derive the band edges from the Recognition Composition Law.
Does not link the band to the eight-tick octave or D = 3.
Does not address mass ladders or the alpha band.
Does not treat time-dependent loading or dynamics.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Unification.CriticalRecognitionLoading module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (16)

def rhoBandLower L13
def rhoBandUpper L16
theorem rhoBandLower_eq L18
theorem rhoBandUpper_eq L21
theorem rhoBandUpper_pos L24
theorem rhoBandUpper_lt_one L28
theorem rhoBandLower_pos L32
theorem rhoBandLower_lt_one L37
theorem rhoBandLower_lt_rhoBandUpper L43
theorem one_sub_phi_inv_eq_phi_inv_sq L50
theorem bandBoundaries_sum_to_one L57
theorem one_sub_rhoBandLower_eq_rhoBandUpper L64
theorem one_sub_rhoBandUpper_eq_rhoBandLower L67
theorem bandLower_ratio L71
theorem bandUpper_ratio L77
theorem bandBoundaries_product L82