IndisputableMonolith.Cosmology.Alcock5
Cosmology support module for an Alcock-style five-parameter certificate built from the RS cost functional. It defines a domain cost, a positive canonical threshold, and an inhabited certificate type with elementary nonnegativity facts. Cosmologists checking RS geometric bounds would cite the certificate constructors. The file is mostly definitions plus short positivity lemmas over the imported cost layer.
claimThe module introduces a domain cost $C$ on the relevant cosmological parameter domain, a canonical threshold $\theta_*>0$, and an Alcock5 certificate type asserting that the domain cost meets the threshold, together with elementary facts $C\ge 0$ and inhabitation of the certificate.
background
Recognition Science cosmology packages geometric and redshift-space tests against the same cost layer used elsewhere in the monolith. The Cost import supplies the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), the unique nonnegative generator forced by the Recognition Composition Law. Constants supplies the RS-native tick $\tau_0=1$ and related units.
Alcock–Paczynski-type comparisons ask whether angular and radial scales are consistent under a single expansion history. This module localizes that question to a domain cost on the parameter region of interest and a single positive threshold against which a certificate can be checked.
Sibling names indicate the surface API: domainCost and its evaluation and nonnegativity lemmas, canonicalThreshold with positivity, and the certificate bundle Alcock5Cert with an inhabited instance.
proof idea
Definition-heavy module, not a single deep theorem. Domain cost is introduced as a Cost-derived functional on the cosmological domain; evaluation-at-equality and nonnegativity are short lemmas from the cost axioms. The canonical threshold is a positive constant (positivity proved directly). The certificate type packages the cost-versus-threshold comparison; inhabitation is a one-line constructor once nonnegativity and threshold positivity are available.
why it matters in Recognition Science
Gives Cosmology a reusable Alcock-style certificate object tied to the RS cost rather than an ad hoc $\chi^2$. Downstream pages can import the inhabited certificate instead of re-proving cost nonnegativity and threshold positivity. No parent theorems are listed yet in the graph (used_by empty), so the module is presently a leaf API for later geometric or BAO-style claims. It sits under the Cosmology domain and inherits units and cost uniqueness from Constants and Cost, consistent with the forcing chain’s J-uniqueness (T5) without reopening that argument.
scope and limits
- Does not derive observational Alcock–Paczynski constraints from survey data.
- Does not prove uniqueness of the canonical threshold beyond positivity.
- Does not connect the certificate to BAO scale fitting or dark-energy w(z).
- Does not re-prove J-uniqueness or the Recognition Composition Law.
- Does not claim a numerical match to any published AP measurement.