module module high

`IndisputableMonolith.Unification.RecognitionBandGeometry`

The RecognitionBandGeometry module defines the lower and upper boundaries of the recognition band as ρ_min = φ^{-2} and ρ_max = 1 - φ^{-2}. It supplies the geometric interval for the load ratio ρ in unification models. Researchers analyzing critical recognition loading cite these bounds to delimit operating regimes. The module consists of direct definitions followed by algebraic verifications of positivity, ordering, and complementarity.

claim$ρ_{band,lower} = φ^{-2}$, $ρ_{band,upper} = 1 - φ^{-2}$, with $ρ_{band,lower} > 0$, $ρ_{band,upper} < 1$, $ρ_{band,lower} < ρ_{band,upper}$, and $ρ_{band,lower} + ρ_{band,upper} = 1$.

background

Recognition Science parameterizes operating points via the load ratio ρ = R_dem / R_max inside a recognition bandwidth. The imported Constants module fixes the base time quantum as τ₀ = 1 tick, anchoring the discrete structure. This module introduces the band boundaries ρ_min = φ^{-2} and ρ_max = 1 - φ^{-2}, where φ denotes the self-similar fixed point from the forcing chain.

proof idea

This is a definition module. It sets rhoBandLower to φ^{-2} and rhoBandUpper to its complement, then verifies the listed equalities and inequalities by direct substitution and elementary properties of φ.

why it matters in Recognition Science

The band geometry supplies the concrete interval for ρ inside the control theorem of CriticalRecognitionLoading. That module sketches the operating regime for recognition bandwidth and the semantic condensation gate using these bounds. It thereby connects the phi-ladder geometry to the unification control variable.

scope and limits

Does not derive φ^{-2} from a deeper axiom inside this module.
Does not treat time evolution of the load ratio.
Does not link to mass ladders or the alpha band.
Does not supply numerical approximations or simulation code.

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