c
Why this theorem is linked from Prospect of Measuring the Cosmic Dipole by Strongly Lensed Gravitational Waves Associated with Galaxy Surveys unclear
Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.
d_L(z) = (1+z) r(z) with r(z) = ∫ c/H(z) dz and H(z) = H0 √[Ωm,0(1+z)^3 + ΩΛ,0]
Relation between the paper passage and the cited Recognition theorem.
plain-language theorem explainer
The declaration sets the speed of light to exactly 1 in RS-native units of voxel per tick. Researchers normalizing calculations in the Recognition Science framework cite this choice when handling light propagation or relativistic effects. It is implemented as a direct constant definition with no lemmas or computational steps.
Claim. In Recognition Science the speed of light is defined by $c = 1$ in native units where distance is measured in voxels and time in ticks.
background
The module sets the fundamental RS time quantum to τ₀ = 1 tick. This normalizes the speed of light c to the value 1 in voxel-per-tick units. Sibling definitions in the same module introduce the golden ratio φ and the discrete tick, which together support the phi-ladder scaling and the eight-tick octave structure used throughout the framework.
proof idea
The declaration is a direct assignment of the real number 1 to c. No upstream lemmas are applied and no tactics are used; the @[simp] attribute simply marks the constant for automatic simplification in later proofs.
why it matters
This definition fixes the unit system for the Recognition Science framework, allowing c = 1 to be used consistently with ħ = φ^{-5} and G = φ^5 / π. It aligns with the forcing chain landmarks by normalizing light speed, which supports the later derivation of D = 3 spatial dimensions. No open questions are addressed here, but the choice underpins all subsequent constant and mass-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Lensed GWs forecast cosmic dipole detection in 10 years
"d_L(z) = (1+z) r(z) with r(z) = ∫ c/H(z) dz and H(z) = H0 √[Ωm,0(1+z)^3 + ΩΛ,0]"