cert
plain-language theorem explainer
Packages three elementary properties of the Alcock–Paczynski domain cost into a single certificate: diagonal vanishing, non-negativity off the diagonal, and a strictly positive canonical threshold. Cosmologists citing the RS AP distortion ratio use this as the structural witness that the cost is a genuine defect. The definition is a pure structure inhabitant wiring three already-proved lemmas.
Claim. There exists a certificate asserting: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the Alcock–Paczynski (AP) geometric distortion $\alpha_\perp/\alpha_\parallel$ as a J-cost defect. In Recognition Science the predicted ratio is $\phi^{J(\phi)/D}=\phi^{0.118/3}=\phi^{0.039}\approx 1.064$, obtained structurally from the unique cost $J$ and $D=3$.
The domain cost compares a model scale $m$ to an expected scale $e$. The certificate structure Alcock5Cert records the three minimal analytic properties any such cost must satisfy before it can serve as an AP witness: it vanishes on the diagonal (perfect match costs nothing), it is nonnegative for positive arguments, and a fixed positive threshold exists against which residual cost can be compared.
Upstream, non-negativity of recognition cost is already forced by $J$-cost non-negativity on positive states (cost_nonneg in ObserverForcing).
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further reasoning occurs at this declaration.
why it matters
Gives a single named witness that the AP domain cost is a legitimate defect functional. The module is marked STRUCTURAL THEOREM (0 sorry, 0 axiom) and sits in the cosmology layer that derives the AP ratio $\phi^{J(\phi)/D}$ from the forcing chain (T5 J-uniqueness, T8 $D=3$). No downstream consumers are recorded yet; the certificate is the local packaging step that later AP comparison lemmas are expected to consume when closing the geometric-distortion claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.