Cosmology Bitkernel Shape Forcing Bit Kernel Shape One Statement

The forced kernel

In cosmology, the dark-energy equation of state is often written with a kernel K(z) that describes how dark energy's density changes with redshift z. The simplest choice, K(z) = 1/(1+z), is so common that it is called the canonical form. The Recognition Science framework's declaration bit_kernel_shape_one_statement is a machine-checked theorem that bundles the proof that this kernel is not merely a convenient choice but the unique scale-free dilution law under the framework's two-premise dilution machinery.

The theorem's content is a conjunction of five proved statements. First, at each rung of cosmic scale, the attenuation of the aging charge is forced to be (1/φ)^n, where φ is the golden ratio. Second, the only power-law kernel that satisfies the single-rung condition is the one with exponent s = 1, which excludes the spatial-volume competitor s = 3 and the spacetime competitor s = 4. Third, that power-law kernel equals the canonical form. Fourth, the resulting equation of state lies on the line w_a = -(1+w_0) in the (w_0, w_a) plane. Fifth, the equation of state never crosses the phantom divide: w(z) ≥ -1 for all redshifts. The declaration bundles these into one statement, each component proved in the framework's machine-checked library of formal theorems.

The framework's library proves these statements from two premises. The first is multiplicative composition: attenuation across m+n rungs is the product of attenuations across m and n rungs. The second is per-rung self-similar attenuation: one rung attenuates by the reciprocal self-similarity fixed point ρ = 1/(1+ρ), which forces ρ = φ⁻¹. The substrate is self-similar with ratio φ, so rung n sits at 1+z = φⁿ. Iterating gives attenuation φ⁻ⁿ at rung n, which is exactly 1/(1+z) on the rung lattice. The continuum interpolation is pinned inside the scale-free class, where every scale-free kernel is a power law (1+z)^(-s), and the per-rung value forces s = 1 exactly.

What the declaration does not claim is as important as what it proves. The physical mechanism itself, that dark energy is the aging of a recognition charge, remains a hypothesis with a named falsifier. The single-channel selection, that the aging charge dilutes through exactly one recognition channel per rung rather than three or four, is also a hypothesis. The today-amplitude δw₀, the size of the deviation from w = -1 today, is open: the shape no longer depends on it, but its value is bounded in (0, J(φ)] and not yet derived. The declaration also retires the idea that this framework explains the Planck-RS Ω_Λ gap: the correction moves the effective Ω_Λ down, away from Planck, for every admissible amplitude.

The practical consequence is a dated prediction. The framework's dark-energy equation of state is w(z) = -1 + δw₀/(1+z), which is exactly the CPL parametrization with w₀ = -1 + δw₀ and w_a = -δw₀, hence w₀ + w_a = -1. The prediction is a line segment in the (w₀, w_a) plane: w_a = -(1+w₀) with -1 < w₀ < -0.88. The falsifiers are sharp: any confirmed phantom crossing w(z) < -1 at any redshift falsifies the mechanism; a DESI Y3+/Roman/Euclid CPL posterior excluding the segment at high confidence falsifies the forced kernel; a confirmed w₀ > -0.88 falsifies the ceiling. The declaration thus turns a modeling choice into a testable prediction with named conditions for failure.

/-- **ONE-STATEMENT SUMMARY.** The BIT kernel shape is forced to
`K(z) = 1/(1+z)` by φ-rung dilution; the RS dark-energy prediction is the
CPL segment `wₐ = −(1+w₀)`, `w₀ ∈ (−1, −0.88)`, with no phantom crossing,
to be adjudicated by DESI Y3+ / Roman / Euclid. -/
theorem bit_kernel_shape_one_statement :
    (∀ (L : RungDilution) (n : ℕ), L.occ n = (1 / Constants.phi) ^ n) ∧
    (∀ s : ℝ, RungCondition (powerKernel s) ↔ s = 1) ∧
    (∀ z : ℝ, 0 ≤ z → powerKernel 1 z = f_canonical z) ∧
    (∀ dw0 : ℝ, OnThawingLine (-1 + dw0) (-dw0)) ∧
    (∀ dw0 z : ℝ, 0 ≤ dw0 → -1 < z → -1 ≤ w_RS dw0 z) :=
  ⟨fun L n => L.occ_forced n,
   powerKernel_rung_condition_iff,
   powerKernel_one_eq_canonical,
   rs_on_thawing_line,
   no_phantom⟩

/-- **EXPONENT PINNED: the power kernel satisfies the φ-rung condition iff
`s = 1`.** With the rung attenuation forced to `φ⁻¹` (§1), the unique
scale-free kernel is `K(z) = (1+z)^(−1) = 1/(1+z)`. Spatial-volume (`s=3`)
and spacetime (`s=4`) dilution are excluded. -/
theorem powerKernel_rung_condition_iff (s : ℝ) :
    RungCondition (powerKernel s) ↔ s = 1 := by
  unfold RungCondition powerKernel
  have harg : 1 + (Constants.phi - 1) = Constants.phi := by ring
  rw [harg]
  constructor
  · intro h
    -- take logs: −s·log φ = −log φ, and log φ > 0
    have hlogpos : 0 < Real.log Constants.phi := Real.log_pos one_lt_phi
    have hlhs : Real.log (Constants.phi ^ (-s)) = -s * Real.log Constants.phi :=
      Real.log_rpow phi_pos (-s)
    have hrhs : Real.log (1 / Constants.phi) = -Real.log Constants.phi := by
      rw [one_div, Real.log_inv]
    have hkey : -s * Real.log Constants.phi = -Real.log Constants.phi := by
      rw [← hlhs, ← hrhs, h]
    have := mul_right_cancel₀ (ne_of_gt hlogpos) (by linarith : -s * Real.log Constants.phi = -1 * Real.log Constants.phi)
    linarith
  · intro h
    subst h
    rw [Real.rpow_neg_one, one_div]

/-- **RS lands on the thawing line** for every amplitude `δw₀`. -/
theorem rs_on_thawing_line (dw0 : ℝ) : OnThawingLine (-1 + dw0) (-dw0) := by
  unfold OnThawingLine
  ring

/-- **F1 (sign falsifier): no phantom crossing.** Under the forced kernel
with non-negative amplitude, `w(z) ≥ −1` at every physical redshift. A
confirmed `w < −1` measurement falsifies the BIT mechanism. -/
theorem no_phantom (dw0 z : ℝ) (h0 : 0 ≤ dw0) (hz : -1 < z) :
    -1 ≤ w_RS dw0 z := by
  have h1z : (0 : ℝ) < 1 + z := by linarith
  have : 0 ≤ dw0 / (1 + z) := div_nonneg h0 h1z.le
  unfold w_RS
  linarith

What this page does not claim

The physical mechanism that dark energy is the aging of a recognition charge is not proved by this declaration; it remains a hypothesis. The today-amplitude δw₀ is not derived by this declaration; only its bounding interval is known. The declaration does not explain the Planck-RS Ω_Λ gap; that explanation is explicitly retired.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/BITKernelShapeForcing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: