solar_ratio_bound
plain-language theorem explainer
Definition solar_ratio_bound supplies the conservative upper bound 5e-10 on the ratio of solar-system scale (1 AU) to the reference scale r_0 = 12 kpc. Cosmologists working on kernel corrections or causal closure in the DIF papers would cite it when quantifying power-law extrapolation tensions at planetary distances. The entry is a direct numerical assignment derived from standard astronomical conversions with no further computation.
Claim. Let $r_0 = 12$ kpc denote the reference scale. The solar-system scale ratio satisfies the conservative bound $r_0^{-1} r_1 < 5$ where $r_1$ is the solar-system scale (1 AU) and the numerical value is obtained from the conversion 1 AU $approx 4.85 times 10^{-9}$ kpc.
background
This definition sits in the CausalClosure module of the DIF papers, which examines forced causal closure under Recognition Science, including scale-dependent behaviors of the BIT kernel. It supplies a concrete numerical input for bounding the correction term $w-1 = C (r/r_0)^alpha$ when the power-law form is extrapolated from galactic to solar distances. Upstream results include the kernel definition in Cosmology.BITKernelFamilies (constant, inverse, or exponential families) and the power spectrum in PrimordialSpectrum, both of which motivate the need for an explicit solar-to-reference ratio in tension analyses.
proof idea
The definition is a direct numerical assignment of the real constant 5e-10. It follows from the astronomical conversion stated in the documentation (1 AU $approx 4.85 times 10^{-9}$ kpc divided by r_0 = 12 kpc) and rounded upward for conservatism.
why it matters
The bound formalizes the solar-system tension identified in the module documentation: the power-law kernel lacks a built-in UV suppression mechanism, so the correction remains positive at small r/r_0. It supplies the scale factor required by sibling declarations such as kernel_correction_positive and CausalClosureForced. The constant therefore anchors the framework's application of scale-free kernels to observational constraints without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.