xi_of_bin_mono
plain-language theorem explainer
Monotonicity of the global factor ξ holds across the five canonical quintile bin centers 0.1, 0.3, 0.5, 0.7, 0.9 in the ILG framework. Modelers validating deterministic bin assignments for global-only ξ would reference this result when ensuring ordered assignments. The proof first derives monotonicity of the underlying u-function from square-root monotonicity after clamping to [0,1], then chains the inequalities for the specific increasing bin centers via explicit numerical bounds.
Claim. Let $ξ(u) = 1 + √(max(0, min(1, u)))$. Then $ξ(0.1) ≤ ξ(0.3) ≤ ξ(0.5) ≤ ξ(0.7) ≤ ξ(0.9)$.
background
The ILG.XiBins module supplies deterministic quintile centers for the global factor ξ. The bin mapping sends natural numbers 0 through 4 to evaluations of the u-function at the fixed centers 0.1, 0.3, 0.5, 0.7 and 0.9. The u-function itself returns 1 plus the square root of its argument after clamping into the unit interval, encoding a threads-informed global scaling factor.
proof idea
The tactic proof first introduces a monotonicity claim for the u-function: the clamped argument is nondecreasing, Real.sqrt_le_sqrt_iff transfers the order, and adding 1 preserves it. It then uses norm_num to obtain the five consecutive inequalities 0.1 ≤ 0.3, 0.3 ≤ 0.5, 0.5 ≤ 0.7 and 0.7 ≤ 0.9. Each is fed to the monotonicity fact, the results are dsimplified at the bin mapping, and combined with nested And.intro.
why it matters
The declaration secures ordered global factor values for the five bins that support global-only assignments inside the ILG framework. It underpins empirical program checks and simplicial ledger constructions even though the current dependency graph shows no direct used_by edges. In the Recognition Science setting it reinforces the deterministic binning convention that aligns with the eight-tick octave periodicity by guaranteeing consistent ordering of the global factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.