pith. sign in
module module high

IndisputableMonolith.Cosmology.BITKernelFamilies

show as:
view Lean formalization →

The Cosmology.BITKernelFamilies module supplies tagged kernel families for cosmological modeling in Recognition Science. It defines the KernelFamily type together with evaluation maps for name, kernel value, and derived quantities such as effective equation of state. The module imports only the RS time quantum and consists entirely of definitions with no proofs. It tags constant and exponential kernel forms along with their positivity and bound properties.

claimDefines tagged type $K$ (KernelFamily) equipped with $name(K)$, kernel function $k(z)$, $w_{eff}(K)$, and bounds such as $0 < k(z)$ and $0 < delta_w0_max(K) < 1$.

background

Recognition Science cosmology employs kernel families to encode redshift-dependent behavior in expansion histories, resting on the imported time quantum. The upstream Constants module states: The fundamental RS time quantum (RS-native). τ₀ = 1 tick. The present module introduces KernelFamily as a tag distinguishing functional forms, including the constant kernel fixed at unity and the exponential kernel required to remain positive. It further equips each family with an effective equation-of-state function evaluated at zero redshift and a maximum deviation parameter delta_w0_max obeying strict inequalities.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies kernel structures that feed into higher-level cosmological statements within the Recognition Science forcing chain, particularly those linking the phi-ladder mass formula to the eight-tick octave and D = 3. It provides the concrete kernel instances needed for Berry creation threshold calculations at phi^{-1} and for alpha-band constraints.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (14)