Cosmology Bitkernel Shape Forcing Power Kernel Rung Condition Iff

The pinned exponent

In cosmology, the dark-energy equation of state is often written as w(z), the ratio of pressure to energy density, and a common parametrization is the CPL form w(z) = w0 + wa * z/(1+z). The question of how w(z) evolves with redshift is one of the field's central open problems. The Recognition Science framework enters here with a specific, machine-checked claim about the kernel that multiplies the deviation from -1.

The relevant declaration, powerKernel_rung_condition_iff, is a theorem in the framework's machine-checked library of formal theorems. It considers a family of power-law kernels, written powerKernel s z = (1+z)^(-s), where s is a real exponent. The theorem states that this kernel satisfies a single-rung condition, RungCondition f, meaning f(phi-1) = 1/phi, if and only if s = 1. Here phi is the golden ratio, approximately 1.618. The proof is a short argument using the injectivity of the real logarithm: the condition at one rung, where the scale factor has grown by a factor of phi, forces the exponent to be exactly one.

The consequence is that the canonical kernel K(z) = 1/(1+z), which appears throughout cosmology as the simplest redshift dependence, is not a modeling choice in this framework. It is the unique single-channel, scale-free phi-dilution law. The theorem excludes the spatial-volume competitor s = 3 and the spacetime competitor s = 4, because neither satisfies the rung condition. This is a sharp result: it pins the shape of the kernel to a single value, leaving no free parameter in the exponent.

In Recognition Science, this theorem is part of a larger derivation. The framework models the aging charge carried across rungs of cosmic scale, where each rung is a factor of phi in the scale factor. Two premises, multiplicative composition across rungs and single-rung self-similar attenuation, force the occupancy at rung n to be phi^(-n). The powerKernel_rung_condition_iff theorem then extends this from the discrete lattice of rungs to the continuum of redshifts, selecting s = 1 among all scale-free power laws. This is what the framework means by the kernel shape being forced.

The theorem does not claim that the overall amplitude of the deviation, called delta-w0, is derived. That amplitude remains an open target, bounded above by J(phi), which is less than 0.12, but not yet pinned. The theorem also does not prove that the physical universe follows this kernel; that is a hypothesis with named falsifiers, such as any confirmed phantom crossing where w(z) < -1. The theorem is a mathematical statement about a family of functions, not an empirical measurement. It says: if you accept the rung condition, the exponent is one. It says nothing about whether nature accepts that condition.

/-- **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]

/-- **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]

/-- The pinned kernel equals the canonical `DeltaWKernel` shape pointwise on
the physical redshift domain: `(1+z)^(−1) = f_canonical(z)` for `z ≥ 0`. -/
theorem powerKernel_one_eq_canonical (z : ℝ) (hz : 0 ≤ z) :
    powerKernel 1 z = f_canonical z := by
  unfold powerKernel f_canonical
  rw [if_neg (not_lt.mpr hz), Real.rpow_neg_one, one_div]

What this page does not claim

The theorem does not prove that the physical universe follows the 1/(1+z) kernel; that is a hypothesis with named falsifiers. The theorem does not derive the today-amplitude delta-w0; that remains an open target. The theorem does not make any empirical measurement or claim about observed dark-energy data.

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: