Cosmology Dark Energy Scale Affinity Derivation No Hidden Scale Coordinate

The no-hidden-coordinate rule

Cosmologists describe the expanding universe with a scale factor, a number that grows as space stretches. Convention sets it to zero at the Big Bang and to one today. The question is what happens in between: does the universe's behavior follow a simple, smooth progression, or does something special occur at some intermediate moment? The Recognition Science framework's ledger, a discrete record of cosmic events, takes a firm position: no hidden intermediate moment may be inserted.

The declaration NoHiddenScaleCoordinate formalizes this as a mathematical condition. It states that a normalized fraction of the ledger's accumulated value, written as a function of the scale factor, must preserve a straight-line interpolation between the two endpoints. In symbols, for any scale factor a between 0 and 1, the fraction at a must equal a itself. This is not a physical observation; it is an admissibility gate, a stated rule about what counts as an acceptable cosmic history.

From this single rule, the framework's machine-checked library of formal theorems derives a chain of results. The normalized fraction becomes the scale factor itself. The redshift history takes the form Z(z) = Z_today / (1 + z). The dark-energy equation of state, a measure of how dark energy's pressure relates to its density, becomes w = -1 + δw₀/(1+z), where δw₀ is a constant. These are the standard forms cosmologists already use; the framework's contribution is showing that the no-hidden-coordinate rule forces them.

The declaration does not claim that the no-hidden-coordinate rule is itself derived from deeper principles. It is stated as an assumption, a gate that selects which histories are admissible. The framework's own documentation notes that deriving this rule from the universal forcing layer remains an open target. Nor does the declaration make contact with measured values; it is a structural result about what follows from the rule, not a prediction that any particular constant has a specific number.

What the declaration changes is the status of the standard dark-energy shape. Within the framework, that shape is not one choice among many; it is the unique consequence of refusing to add hidden structure. The rule is simple, but its consequence is a complete cosmological history.

/-- The no-hidden-scale-coordinate condition forces normalized Z-fraction to be the scale
factor itself. -/
theorem noHidden_forces_identity (H : NoHiddenScaleCoordinate) (a : ℝ) :
    H.Zfrac a = a := by
  exact CosmicZScaleLaw.scaleAffine_forces_identity (noHidden_to_scaleAffine H) a

/-- The no-hidden-scale-coordinate condition forces the redshift history
`Z(z)=Z_today/(1+z)`. -/
theorem noHidden_forces_linearZ (Zt : ℝ) (H : NoHiddenScaleCoordinate) (z : ℝ) :
    CosmicZScaleLaw.ZfromScaleLaw Zt (noHidden_to_scaleAffine H) z =
      CosmicZHistory.linearZ Zt z :=
  CosmicZScaleLaw.scaleAffine_forces_linearZ Zt (noHidden_to_scaleAffine H) z

/-- The no-hidden-scale-coordinate condition forces the canonical equation of state. -/
theorem noHidden_forces_canonical_kernel (dw0 Zt : ℝ)
    (H : NoHiddenScaleCoordinate) (z : ℝ)
    (hZt : Zt ≠ 0) (hz : (1 : ℝ) + z ≠ 0) :
    CosmicZHistory.bitKernel dw0 Zt
        (CosmicZScaleLaw.ZfromScaleLaw Zt (noHidden_to_scaleAffine H)) z =
      -1 + dw0 / (1 + z) :=
  CosmicZScaleLaw.scaleAffine_forces_canonical_kernel
    dw0 Zt (noHidden_to_scaleAffine H) z hZt hz

/-- The lower admissibility condition behind `ScaleAffineZLaw`.

Interpretation: with only the early endpoint `a=0` and today endpoint `a=1` available, a
normalized ledger fraction cannot choose a nonlinear coordinate without adding extra
structure. Therefore it preserves endpoint interpolation. -/
structure NoHiddenScaleCoordinate where
  /-- Normalized Z-fraction as a function of scale factor. -/
  Zfrac : ℝ → ℝ
  /-- Early endpoint: no accumulated cosmic Z at `a=0`. -/
  early_zero : Zfrac 0 = 0
  /-- Today endpoint: normalized accumulated cosmic Z is `1` at `a=1`. -/
  today_one : Zfrac 1 = 1
  /-- No hidden coordinate: endpoint convex interpolation is preserved. -/
  no_hidden_coordinate :
    ∀ a : ℝ, Zfrac ((1 - a) * 0 + a * 1) = (1 - a) * Zfrac 0 + a * Zfrac 1

What this page does not claim

No claim that the no-hidden-coordinate rule is derived from deeper principles. No claim that any measured dark-energy value is predicted by the declaration. No claim that the declaration is a physical observation rather than a mathematical admissibility 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/DarkEnergyScaleAffinityDerivation.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: