Cosmology Dark Energy Dilution From Jcost Occ Of Composes

The multiplication law

In the Recognition Science framework, dark energy is described by an occupancy, a number that measures how much of a recognition channel remains after attenuation. The framework's library of machine-checked theorems contains a declaration, occOf_composes, that proves a specific multiplication law: the occupancy through m + n independent channels equals the product of the occupancies through m and through n channels separately. In symbols, if occ(n) is the occupancy through n channels, then occ(m + n) = occ(m) * occ(n). The proof is short: the occupancy is defined as the exponential of a sum of per-channel log-costs, and exponentials turn sums into products.

This matters because an earlier derivation of dark energy dilution had assumed this multiplication law as an unproved premise, calling it the "multiplicative shadow" of log-additivity. The declaration occOf_composes removes that assumption for a specific class of occupancies: those that are uniform-weight exponential aggregates of a single per-channel survival ratio. For that class, the multiplication law is now a theorem, not an axiom. The framework's library also records a more general version, aggregate_hadamardMul, which shows that any J-cost aggregate is multiplicative over independent channels.

What the declaration does not do is equally important. It does not prove that the physical dark energy occupancy actually has this exponential aggregate form. That identification is a modeling choice, not a theorem. The declaration also leaves untouched the real physical premise: per-channel self-similar attenuation, the condition that one channel's survival ratio s satisfies s = 1/(1+s). That premise is what forces s to equal the reciprocal of the golden ratio, and it is assumed, not derived here. So the net effect is premise substitution, not premise elimination: the multiplication law is re-derived from a logically equivalent form, grounding it in the framework's cost API rather than leaving it abstract.

The practical consequence is that the framework's dark energy amplitude chain, which ends at the predicted present amplitude φ⁻⁴ · J(φ), now rests on two explicit premises instead of three. One of them, the multiplication law, is proved for the channel-aggregate class. The other two, the channel-aggregate identification and self-similar attenuation, remain as the surviving assumptions. The declaration is non-vacuous: a canonical example with s = 1/φ exists, so the theorem applies to something real.

/-- **THE `composes` PREMISE, DISCHARGED.** Occupancy across `m + n` independent
channels is the product of the block occupancies. Proof: the log-ledger is
additive over disjoint channel blocks, and `exp` turns sums into products
(`Real.exp_add`) — the multiplicative shadow of J-cost log-additivity, now a
theorem instead of an axiom. -/
theorem occOf_composes (m n : ℕ) :
    C.occOf (m + n) = C.occOf m * C.occOf n := by
  rw [occOf_eq_exp, occOf_eq_exp, occOf_eq_exp, ← Real.exp_add]
  congr 1
  push_cast
  ring

/-- Closed exponential form of the channel occupancy: `occOf n = exp(n · log s)`.
The log of the occupancy is the sum of the `n` per-channel log-costs. -/
theorem occOf_eq_exp (n : ℕ) :
    C.occOf n = Real.exp (n * Real.log C.s) := by
  unfold occOf Cost.Ndim.aggregate Cost.Ndim.dot Cost.Ndim.logVec
  simp only [one_mul, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
    nsmul_eq_mul]

/-- **The J-cost aggregate is multiplicative over independent channels.**
Log-costs add (`Cost.Ndim.dot_log_hadamardMul`), so aggregates multiply. -/
theorem aggregate_hadamardMul {n : ℕ} (α x y : Cost.Ndim.Vec n)
    (hx : ∀ i, 0 < x i) (hy : ∀ i, 0 < y i) :
    Cost.Ndim.aggregate α (Cost.Ndim.hadamardMul x y)
      = Cost.Ndim.aggregate α x * Cost.Ndim.aggregate α y := by
  unfold Cost.Ndim.aggregate
  rw [Cost.Ndim.dot_log_hadamardMul α x y hx hy, Real.exp_add]

/-- The per-channel survival ratio is forced to `φ⁻¹` by the self-similar
premise alone (via the recipShift fixed-point theorem). -/
theorem s_forced : C.s = 1 / Constants.phi :=
  DarkEnergyPhiDilutionDerivation.self_similar_attenuation_forced C.s_pos C.self_similar

What this page does not claim

The physical dark energy occupancy is a channel aggregate. The self-similar attenuation premise is derived or eliminated. The framework's dark energy amplitude is measured against astronomical 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/DarkEnergyDilutionFromJCost.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: