Cosmology Bitkernel Shape Forcing F Canonical Rung Scaling

The forced rung law

The declaration f_canonical_rungScaling states a precise scaling law for the function f(z) = 1/(1+z), which in cosmology measures how a quantity attenuates with redshift z. The law says two things. First, at redshift zero, f(0) = 1, meaning no attenuation today. Second, for any non-negative redshift z, the function satisfies f(φ(1+z) − 1) = f(z)/φ, where φ is the golden ratio. This is a self-similarity condition: scaling the argument by φ reduces the value by exactly φ. The theorem proves that the canonical kernel, the function 1/(1+z), obeys this law.

The significance is that this law is not assumed but derived. The framework's library proves that any function satisfying the rung scaling law must take the values (1/φ)^n at the points φ^n − 1, which are the rungs of a cosmic scale ladder. This lattice uniqueness is a theorem. Also, within the class of scale-free functions, which are power laws (1+z)^(−s), the condition that one rung attenuates by 1/φ forces the exponent s to be exactly 1. The proof uses the injectivity of the real logarithm. This pins the canonical kernel uniquely, excluding the spatial-volume competitor s = 3 and the spacetime competitor s = 4.

In Recognition Science, the framework models cosmic aging as a discrete process. The ledger, a discrete record of recognition events, carries an aging charge that dilutes across scale rungs. The two premises are: composition across rungs (attenuation over m+n rungs is the product of the two sub-attenuations) and single-rung self-similar attenuation (one rung attenuates by ρ = 1/(1+ρ), forcing ρ = 1/φ). These are the same premises that force the dark-energy occupancy θ = φ⁻⁴. The framework proves that the canonical kernel is the unique single-channel scale-free φ-dilution law.

The derived shape leads to a one-parameter family for the dark-energy equation of state: w(z) = −1 + δw₀/(1+z). This is exactly the CPL parametrization with w₀ = −1 + δw₀ and wₐ = −δw₀, implying w₀ + wₐ = −1. The framework proves that w(z) never goes below −1 (no phantom crossing) and that w₀ lies in the interval (−1, −0.88), given the amplitude bound. This yields a testable prediction: a line segment in the (w₀, wₐ) plane. A confirmed phantom crossing or a CPL posterior excluding this segment would falsify the mechanism.

What the declaration does not claim is equally important. It does not derive the today-amplitude δw₀; that remains an open problem, bounded but not fixed. It does not prove the physical selection of exactly one temporal channel per rung; that is a hypothesis with a named falsifier. And it does not explain the Ω_Λ gap; that explanation is retired. The scaling law is a theorem about a function, not a complete cosmological model.

/-- The canonical kernel satisfies the rung-scaling law. -/
theorem f_canonical_rungScaling : RungScalingLaw f_canonical := by
  refine ⟨f_canonical_today, ?_⟩
  intro z hz
  have h1z : (0 : ℝ) < 1 + z := by linarith
  have hphi : (0 : ℝ) < Constants.phi := phi_pos
  have harg : (0 : ℝ) ≤ Constants.phi * (1 + z) - 1 := by nlinarith [one_lt_phi]
  unfold f_canonical
  rw [if_neg (not_lt.mpr harg), if_neg (not_lt.mpr hz)]
  have h2 : 1 + (Constants.phi * (1 + z) - 1) = Constants.phi * (1 + z) := by ring
  rw [h2]
  field_simp

/-- **LATTICE UNIQUENESS.** Any kernel satisfying the rung-scaling law
equals `φ⁻ⁿ = 1/(1+z)` at every rung `z = φⁿ − 1` of the scale lattice. -/
theorem rungScaling_forces_lattice {f : ℝ → ℝ} (hf : RungScalingLaw f) :
    ∀ n : ℕ, f (Constants.phi ^ n - 1) = (1 / Constants.phi) ^ n := by
  intro n
  induction n with
  | zero => simpa using hf.1
  | succ k ih =>
      have hpow : (0 : ℝ) ≤ Constants.phi ^ k - 1 := by
        have : (1 : ℝ) ≤ Constants.phi ^ k := one_le_pow₀ one_lt_phi.le
        linarith
      have harg : Constants.phi ^ (k + 1) - 1
          = Constants.phi * (1 + (Constants.phi ^ k - 1)) - 1 := by ring
      rw [harg, hf.2 _ hpow, ih]
      field_simp
      ring

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

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

/-- **The today-value band.** For any positive amplitude up to the
phantom-Carnot ceiling, `w₀ ∈ (−1, −0.88)`. -/
theorem w0_band (dw0 : ℝ) (h0 : 0 < dw0) (hJ : dw0 ≤ Cost.Jcost Constants.phi) :
    -1 < -1 + dw0 ∧ -1 + dw0 < -0.88 := by
  have := jcost_phi_lt_012
  constructor <;> linarith

What this page does not claim

The today-amplitude δw₀ is not derived; it remains an open parameter bounded by the Carnot ceiling. The physical selection of one temporal channel per rung is a hypothesis, not a theorem. The framework does not claim to explain the Planck-RS Ω_Λ gap; that explanation is retired. The declaration does not prove the golden ratio is the only self-similar ratio for all possible scaling laws, only for this specific rung condition.

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: