IndisputableMonolith.ILG.NOfRMono
The ILG.NOfRMono module supplies an internal numerical guard ε_r together with the analytic global radial shape factor in the ILG setting. It depends on ParamsKernel to enforce well-formed parameters. Sibling declarations address the function n_of_r and its monotonicity when the parameter A is non-negative. The module is marked as a WIP stub with no completed proofs.
claim$\epsilon_r := 10^{-12}$ (square-root guard); $n(r)$ the analytic global radial shape factor, monotonic for non-negative parameters.
background
The module imports ParamsKernel, whose verification predicate requires parameters to be well-formed. It introduces the noncomputable real ε_r as an internal guard to keep square-root expressions defined and reuses the canonical definition of the analytic global radial shape factor. The local setting is the ILG domain focused on radial functions and their monotonicity properties.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies supporting definitions for n_of_r and its monotonicity inside the ILG parameter kernel verification. It has no listed downstream uses in the used_by edges.
scope and limits
- Does not complete any monotonicity proof for n_of_r.
- Does not supply the explicit form of the radial shape factor beyond the stub.