xi_of_u
plain-language theorem explainer
xi_of_u supplies the threads-informed global factor ξ(u) for a bin-center parameter u in the unit interval via the closed-form expression 1 plus the square root of the clamped input. It populates the quintile bin centers used throughout the ILG.XiBins module. The definition consists of a single algebraic formula with no additional lemmas or tactics required.
Claim. Define the global factor function by $ξ(u) = 1 + √(max(0, min(1, u)))$ for real $u$, which assigns the threads-informed ξ value from the bin center $u ∈ [0,1]$.
background
The XiBins module assigns deterministic values to the global factor ξ at five canonical quintile centers. The function converts a real bin-center coordinate u into the corresponding ξ by clamping u to the unit interval and adding its square root. This setup draws from the meta-realization certificate in the upstream UniversalForcingSelfReference module, which encodes the structural axioms needed for self-referential forcing.
proof idea
The definition is implemented as a direct one-line expression applying the real square root to the result of clamping u between 0 and 1.
why it matters
This definition serves as the base for xi_of_bin, which hardcodes the ξ values at quintile centers 0.1, 0.3, 0.5, 0.7, and 0.9, and for the monotonicity proof xi_of_bin_mono. It contributes the deterministic global factor assignment in the ILG framework, supporting the broader Recognition Science derivation of physical constants from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.