IndisputableMonolith.Cosmology.BITKernelFamilies
The Cosmology.BITKernelFamilies module supplies the KernelFamily type and supporting definitions for distinct kernel forms in Recognition Science cosmology models. Researchers modeling effective equations of state or w_eff would cite these tags when selecting constant versus exponential kernels. The module is purely definitional, establishing names, positivity, and zero-point evaluations without theorems.
claimThe module introduces the type $\mathsf{KernelFamily}$ equipped with $\mathsf{name}: \mathsf{KernelFamily} \to \mathbb{R}$, $\mathsf{kernel}: \mathsf{KernelFamily} \to \mathbb{R} \to \mathbb{R}$, $\mathsf{kernel\_at\_zero}$, $\mathsf{w\_eff}$, and basic lemmas establishing $\mathsf{constant\_kernel\_eq\_one}$, positivity of $\mathsf{exp\_kernel}$, and $\mathsf{w\_eff\_at\_zero}$.
background
Recognition Science cosmology employs kernel functions to encode effective dynamics on top of the fundamental time quantum $\tau_0 = 1$ tick supplied by the imported Constants module. The present module tags these kernels via the KernelFamily type so that downstream calculations can switch between constant and exponential forms while preserving required positivity and normalization properties. Sibling definitions include $\mathsf{delta_w0_max}$ and $\mathsf{inv_one_plus_z_pos}$ to support equation-of-state bounds.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the kernel families required by higher-level cosmology constructions that extend the phi-ladder and forcing chain (T0-T8). It directly supports effective-w calculations that feed into models using the Recognition Composition Law and the Berry creation threshold.
scope and limits
- Does not derive kernels from the Recognition Composition Law.
- Does not link to the eight-tick octave or spatial dimension D=3.
- Does not compute numerical values inside the alpha band.
- Does not address mass formulas or phi-ladder rungs.
depends on (1)
declarations in this module (14)
-
inductive
KernelFamily -
def
name -
def
kernel -
theorem
kernel_at_zero -
theorem
constant_kernel_eq_one -
theorem
inv_one_plus_z_pos -
theorem
exp_kernel_pos -
def
delta_w0_max -
theorem
delta_w0_max_pos -
theorem
delta_w0_max_lt_one -
def
w_eff -
theorem
w_eff_at_zero -
structure
BITKernelFamiliesCert -
def
bitKernelFamiliesCert