n_of_r
plain-language theorem explainer
The definition supplies the closed-form radial profile n(r) = 1 + A(1 − exp(−(max(0,r)/max(εr,r0))^p)) employed in ILG coherence models. Researchers fitting mass ladders or density profiles cite this expression for its saturation behavior. The body evaluates the scaled radius and applies the exponential directly.
Claim. $n(r) = 1 + A(1 - e^{-(max(0,r)/max(ε_r,r_0))^p})$ for real parameters $A,r_0,p,r$, where $ε_r>0$ is a fixed numerical guard.
background
The ILG.XiBins module defines radial shape factors for the Integration Gap framework. Here A is the active edge count per fundamental tick, equal to 1 from the foundation. The parameter r0 comes from sector-specific phi-exponent offsets in the mass anchor. The guard εr prevents division by zero in the scaled radius x = max(0,r) / max(εr, r0). This form is the canonical analytic expression reused by monotonicity results in sibling modules.
proof idea
The definition computes the scaled radius x as the ratio of the nonnegative part of r to the positive denominator max(εr, r0), then substitutes into the saturation formula 1 + A(1 − exp(−x^p)). No lemmas are invoked; it is a direct term definition.
why it matters
This supplies the primitive radial function for ILG analysis, directly supporting the monotonicity lemma n_of_r_mono_A_of_nonneg_p that appears in both NOfRMono and XiBins. It encodes the global shape needed for the phi-ladder mass formulas at D = 3. The definition remains open for sector-specific calibration of r0 and p.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.