n_of_r_mono_A_of_nonneg_p
plain-language theorem explainer
The lemma establishes that the radial shape factor n(r) is nondecreasing in amplitude A whenever the exponent p is nonnegative. ILG radial-profile modelers cite it to justify increasing A while preserving the ordering of n at every radius. The proof is a one-line wrapper that unfolds the local definition of n_of_r and invokes the canonical monotonicity result from the XiBins module.
Claim. Let $n(r; A, r_0, p) := 1 + A(1 - e^{-x^p})$ where $x = (max(0,r))/max(ε_r, r_0)$ and $ε_r > 0$ is a fixed guard. If $p ≥ 0$ and $A_1 ≤ A_2$, then $n(r; A_1, r_0, p) ≤ n(r; A_2, r_0, p)$ for all real $r$.
background
The function n_of_r supplies the analytic global radial shape factor used throughout the ILG module: n(r) = 1 + A(1 - exp(-(x)^p)) with x formed from the ratio of max(0,r) to a positive denominator guard εr. The parameter r0 is supplied externally (for example from the Masses.Anchor sector table) while A2 appears in VoxelWalks scalings. The present declaration lives in NOfRMono as a thin re-export that delegates the monotonicity claim to the explicit proof already recorded in XiBins.
proof idea
The proof is a one-line wrapper. It applies dsimp on n_of_r to expose the XiBins definition, then hands the hypotheses hp and hA12 directly to the lemma n_of_r_mono_A_of_nonneg_p already proved in XiBins.
why it matters
The result guarantees that amplitude increases cannot invert the radial profile ordering, which is required for consistent ILG constructions that later feed into XiBins.n_of_r_mono_A_of_nonneg_p. It supports the framework's use of monotonic radial factors in phi-ladder mass assignments without introducing sign changes for nonnegative exponents. No open scaffolding remains; the claim is fully discharged by the delegation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.