Pith. sign in
module module moderate

IndisputableMonolith.Physics.MicrowaveBackgroundFromPhiLadder

show as:
view Lean formalization →

Physics module that packages CMB acoustic structure on the Recognition Science phi-ladder. It defines a domain cost, a positive canonical threshold, and an inhabited CMB acoustic-ratio certificate. Cosmology workers in RS would cite the certificate objects when linking ladder rungs to peak ratios. The module is mostly definitional, with nonnegativity and positivity lemmas plus an inhabitation proof.

claimA domain cost $C$, a canonical threshold $\theta>0$, and a CMB acoustic-ratio certificate asserting that the acoustic peak ratio lies in the band fixed by the $\varphi$-ladder (with supporting identities $C$ evaluation, $C\ge 0$, and certificate inhabitation).

background

Recognition Science places scales on a discrete $\varphi$-ladder, with $\varphi$ the self-similar fixed point from the forcing chain (T6). The Cost import supplies the J-cost $J(x)=(x+x^{-1})/2-1$ obeying the Recognition Composition Law. Constants supplies the RS-native time quantum $\tau_0=1$ tick and related unit conventions ($c=1$, $\hbar=\varphi^{-5}$, etc.).

This module specializes those primitives to the microwave background. Sibling definitions introduce a domain cost (with an evaluation identity and a nonnegativity lemma), a strictly positive canonical threshold, and a certificate type for the CMB acoustic ratio, together with an inhabitation witness. The local setting is RS cosmology phenomenology rather than a re-derivation of J-uniqueness or spatial dimension.

proof idea

Definition-and-certificate module, not a long forcing argument. domainCost is introduced with an at-equality lemma and a nonnegativity proof. canonicalThreshold is a positive real, discharged by canonicalThreshold_pos. CMBAcousticRatioCert and cert package the acoustic-ratio claim; cert_inhabited shows the certificate type is inhabited. Imports stop at Constants and Cost; no deep tactic chains beyond those supporting lemmas.

why it matters in Recognition Science

Gives the Physics domain an RS-native handle on CMB acoustic peak ratios via the phi-ladder, parallel to mass-ladder and alpha-band results in the primer. Parent use sites are not yet recorded in the graph (used_by empty), so this module is an interface layer: downstream CMB phenomenology can consume the certificate and threshold rather than rebuild domain cost from J. It does not close T0-T8; it applies the already-forced $\varphi$ and cost structure to a cosmological observable class.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)