xi_of_bin
plain-language theorem explainer
Modelers discretizing the global factor ξ into quintiles cite this definition to fix deterministic representatives at the bin centers 0.1, 0.3, 0.5, 0.7, and 0.9. The map from natural-number index to real value is invoked whenever ILG calculations require a uniform global-only ξ per quintile. Implementation occurs through direct case distinction on the input index with a default clause for all larger indices.
Claim. Define the map from natural numbers to reals by cases: the value at index 0 is 1 plus the square root of 0.1, at index 1 is 1 plus the square root of 0.3, at index 2 is 1 plus the square root of 0.5, at index 3 is 1 plus the square root of 0.7, and at every index 4 or larger is 1 plus the square root of 0.9.
background
The auxiliary map xi_of_u computes the threads-informed global factor ξ from any bin-center parameter u in the closed unit interval by the formula 1 plus the square root of the value of u clamped between 0 and 1. Quintile centers are the midpoints of the five equal subintervals of [0,1]. The surrounding ILG.XiBins module collects deterministic choices for the global-only component of ξ.
proof idea
The definition is supplied directly by pattern matching on the natural-number argument, returning the evaluation of xi_of_u at the corresponding quintile center for inputs 0 through 3 and defaulting to the final center for every larger input.
why it matters
The downstream monotonicity lemma xi_of_bin_mono invokes this definition to establish that the five assigned values form a non-decreasing sequence. It supplies the concrete numerical anchors required for any quintile-based discretization of the global ξ parameter inside the ILG module. The construction preserves the deterministic, threads-informed character of global factors throughout the Recognition Science development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.