n_of_r
plain-language theorem explainer
The n_of_r definition supplies the analytic radial shape factor n(r) = 1 + A(1 - exp(-(r/r0)^p)) with a positivity guard on the normalized radius. Researchers modeling density profiles or mass ladders in the ILG sector cite this for its role in monotonicity arguments under nonnegative p. The implementation is a one-line delegation to the canonical version in XiBins, inheriting the max(0,r) normalization and exponential form.
Claim. The radial shape factor is defined by $n(r) = 1 + A(1 - e^{-(x)^p})$ where $x = (max(0,r))/max(ε_r, r_0)$ and $ε_r = 10^{-12}$, for real parameters $A, r_0, p, r$.
background
In the ILG module the radial profile is built from a shape factor that keeps the argument of the exponential non-negative. The guard εr = 1e-12, defined locally as a WIP stub, prevents division by zero when r0 vanishes. Upstream results supply the active-edge count A = 1 from IntegrationGap and Anchor, the sector-dependent r0 offsets from Anchor (e.g., 62 for leptons), and the canonical arithmetic object from ArithmeticOf that anchors all realizations. The definition re-exports the expression already present in XiBins so that monotonicity lemmas can be stated once and reused.
proof idea
This is a one-line wrapper that directly invokes the canonical n_of_r from IndisputableMonolith.ILG.XiBins, inheriting its let-binding for the normalized radius x and the subsequent arithmetic expression.
why it matters
The definition feeds the monotonicity lemma n_of_r_mono_A_of_nonneg_p in the same module and is re-used inside XiBins, closing a duplication path. It supplies the radial factor required for mass-ladder constructions that rest on the φ-exponent offsets and the eight-tick octave. The declaration therefore sits at the interface between the IntegrationGap A = 1 and the downstream density or coherence-energy calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.