Encyclopedia Cosmology Cosmology Cosmic Zscale Law Scale Affine Forces Identity
ARTICLE 3 claims 3 theorems
Cosmology Cosmic Zscale Law Scale Affine Forces Identity
A single admissibility condition forces the dark-energy shape to be the scale factor itself, and the proof is machine-checked.
The scale-affine law
In cosmology, the scale factor a(z) describes how the universe's size changes with redshift z. Today, at z=0, the scale factor equals 1. At earlier times, when light from distant galaxies is stretched to longer wavelengths, z is positive and the scale factor is smaller, always between 0 and 1. This simple coordinate, familiar from the Friedmann equations, is the stage on which the Recognition Science result plays out.
The declaration scaleAffine_forces_identity establishes a conditional theorem. It states that if a normalized cosmic-Z history obeys a specific admissibility law, then that history must be exactly the identity map on the scale factor. The law, called the scale-affine ledger law, requires that the normalized Z-fraction preserves convex interpolation between the early endpoint a=0 and today a=1. In plain terms, no intermediate scale-factor coordinate is preferred by the ledger before any new physical input is supplied. The proof is a short, machine-checked argument in the framework's library of formal theorems.
The consequence is concrete. Under this law, the normalized Z-history is uniquely Z/Z_today = a, and the dark-energy deviation becomes δw(z) = δw₀/(1+z). The equation of state follows as w(z) = -1 + δw₀/(1+z). This is the canonical kernel that the framework's earlier work had identified as the last shape residue in the dark-energy plan. The scale-affine law closes that gap by forcing the shape, not by fitting it.
In Recognition Science, the framework models the universe as holding a discrete record of recognition events, a ledger. The scale-affine law is an admissibility condition on that ledger: it says the ledger is uniform in the scale-factor coordinate until further physical structure is introduced. The theorem does not derive this law from deeper principles. It is an assumption, named and explicit, and the result is conditional on it.
What the declaration does not claim is just as important. It does not claim that the scale-affine law is true of the actual universe. It does not claim that dark energy is explained without any input. The theorem proves a conditional: if the law holds, the shape follows. Whether the law holds is a separate question, one the framework's library does not settle here. The value of the result is that it isolates exactly what must be assumed to force the canonical dark-energy shape, and it verifies that the step from assumption to conclusion is logically airtight.
THEOREM scaleAffine_forces_identity · IndisputableMonolith/Cosmology/CosmicZScaleLaw.lean
/-- The scale-affine ledger law uniquely forces the normalized Z-fraction to be the identity
map on scale factor. -/
theorem scaleAffine_forces_identity (law : ScaleAffineZLaw) (a : ℝ) :
law.Zfrac a = a := by
have h := law.scale_affine_from_early_to_today a
simpa [law.early_zero, law.today_one] using h
THEOREM scaleAffine_forces_linearZ · IndisputableMonolith/Cosmology/CosmicZScaleLaw.lean
/-- Scale-affinity forces the redshift history to be the linear-in-scale-factor history
`Z(z)=Z_today/(1+z)`. -/
theorem scaleAffine_forces_linearZ (Zt : ℝ) (law : ScaleAffineZLaw) (z : ℝ) :
ZfromScaleLaw Zt law z = CosmicZHistory.linearZ Zt z := by
unfold ZfromScaleLaw CosmicZHistory.linearZ scaleFactor
rw [scaleAffine_forces_identity law]
rw [mul_one_div]
THEOREM scaleAffine_forces_canonical_deviation · IndisputableMonolith/Cosmology/CosmicZScaleLaw.lean
/-- Therefore scale-affinity forces the canonical BIT deviation
`δw(z)=δw₀/(1+z)`. -/
theorem scaleAffine_forces_canonical_deviation (dw0 Zt : ℝ) (law : ScaleAffineZLaw)
(z : ℝ) (hZt : Zt ≠ 0) (hz : (1 : ℝ) + z ≠ 0) :
CosmicZHistory.bitDeviation dw0 Zt (ZfromScaleLaw Zt law) z = dw0 / (1 + z) := by
have hfun : ZfromScaleLaw Zt law = CosmicZHistory.linearZ Zt := by
funext x
exact scaleAffine_forces_linearZ Zt law x
rw [hfun]
exact CosmicZHistory.linear_accumulation_forces_canonical_kernel dw0 Zt z hZt hz
What this page does not claim
The scale-affine ledger law is not derived from deeper principles in this declaration. The theorem does not assert that the actual universe obeys the scale-affine law. The result does not claim to explain dark energy without any admissibility input.
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/CosmicZScaleLaw.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:
- What physical input would justify the scale-affine ledger law from more fundamental principles?
- How does the scale-affine law relate to the observed dark-energy equation of state from supernova surveys?
- Does the scale-affine law hold at all redshifts, or only in the regime where the scale factor is between 0 and 1?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM scaleAffine_forces_identity · IndisputableMonolith/Cosmology/CosmicZScaleLaw.lean
/-- The scale-affine ledger law uniquely forces the normalized Z-fraction to be the identity map on scale factor. -/ theorem scaleAffine_forces_identity (law : ScaleAffineZLaw) (a : ℝ) : law.Zfrac a = a := by have h := law.scale_affine_from_early_to_today a simpa [law.early_zero, law.today_one] using hThe scale-affine ledger law forces the normalized Z-fraction to be the identity map on the scale factor. scaleAffine_forces_identity · IndisputableMonolith/Cosmology/CosmicZScaleLaw.leanTHEOREM scaleAffine_forces_linearZ · IndisputableMonolith/Cosmology/CosmicZScaleLaw.lean
/-- Scale-affinity forces the redshift history to be the linear-in-scale-factor history `Z(z)=Z_today/(1+z)`. -/ theorem scaleAffine_forces_linearZ (Zt : ℝ) (law : ScaleAffineZLaw) (z : ℝ) : ZfromScaleLaw Zt law z = CosmicZHistory.linearZ Zt z := by unfold ZfromScaleLaw CosmicZHistory.linearZ scaleFactor rw [scaleAffine_forces_identity law] rw [mul_one_div]Under the scale-affine law, the redshift history is forced to be Z(z) = Z_today/(1+z). scaleAffine_forces_linearZ · IndisputableMonolith/Cosmology/CosmicZScaleLaw.leanTHEOREM scaleAffine_forces_canonical_deviation · IndisputableMonolith/Cosmology/CosmicZScaleLaw.lean
/-- Therefore scale-affinity forces the canonical BIT deviation `δw(z)=δw₀/(1+z)`. -/ theorem scaleAffine_forces_canonical_deviation (dw0 Zt : ℝ) (law : ScaleAffineZLaw) (z : ℝ) (hZt : Zt ≠ 0) (hz : (1 : ℝ) + z ≠ 0) : CosmicZHistory.bitDeviation dw0 Zt (ZfromScaleLaw Zt law) z = dw0 / (1 + z) := by have hfun : ZfromScaleLaw Zt law = CosmicZHistory.linearZ Zt := by funext x exact scaleAffine_forces_linearZ Zt law x rw [hfun] exact CosmicZHistory.linear_accumulation_forces_canonical_kernel dw0 Zt z hZt hzThe scale-affine law forces the canonical dark-energy deviation δw(z) = δw₀/(1+z). scaleAffine_forces_canonical_deviation · IndisputableMonolith/Cosmology/CosmicZScaleLaw.lean