IndisputableMonolith.Astrophysics.RS_Astro_Module_003
Astrophysics module defining a domain cost functional, its nonnegativity and evaluation identity, and a positive canonical threshold, packaged as an inhabited certificate RSAstro003Cert. Observers of RS galactic or halo scaling arguments would cite the cost and threshold lemmas. The module is mostly definitional with short positivity and equality proofs over the imported J-cost.
claimThe module introduces a domain cost $C_{\mathrm{dom}}$ built from the Recognition cost $J$, proves $C_{\mathrm{dom}}\ge 0$ and an evaluation identity at a reference point, and fixes a canonical threshold $\theta>0$. These are bundled into an inhabited certificate record for RS astrophysics module 003.
background
Recognition Science measures mismatch with the cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), imported here via the Cost layer. Constants supplies the RS-native tick $\tau_0=1$. In the astrophysics domain one needs a scalar domain cost that scores how far a configuration sits from the self-similar $\phi$-ladder equilibrium, together with a positive cutoff that marks when the cost is large enough to count as a resolved structure.
This module is the third RS astrophysics certificate block. Sibling names indicate a domain cost, its pointwise evaluation lemma, nonnegativity, a canonical threshold with positivity, and a certificate type with an inhabited instance. No external physics data enter; the objects are pure RS-cost constructions.
proof idea
Definition-first module. domainCost is introduced from the imported Cost primitives; domainCost_at_eq is an evaluation identity; domainCost_nonneg follows from nonnegativity of $J$. canonicalThreshold is a positive constant (canonicalThreshold_pos). RSAstro003Cert packages these facts; cert and cert_inhabited supply a concrete witness so downstream code can assume the bundle without reconstructing it.
why it matters in Recognition Science
Gives the astrophysics layer a reusable cost-and-threshold certificate rather than ad-hoc scalars. Downstream used_by edges are empty in the graph snapshot, so this module currently stands as a leaf package: later halo, rotation-curve, or mass-ladder arguments can import the inhabited cert instead of re-proving $C_{\mathrm{dom}}\ge 0$ and $\theta>0$. It sits under the broader RS forcing chain only indirectly, via $J$ uniqueness (T5) and the $\phi$ fixed point (T6) already fixed in Cost and Constants. No paper proposition number is attached in the supplied docs.
scope and limits
- Does not derive galactic rotation curves or mass models from data.
- Does not fix numerical astrophysical units beyond RS-native cost.
- Does not prove uniqueness of the canonical threshold among all positive cutoffs.
- Does not connect domainCost to the eight-tick octave or $D=3$ forcing steps.
- Does not supply observational falsifiers or survey comparisons.