pith. machine review for the scientific record. sign in
def definition def or abbrev high

voxelLength

show as:
view Lean formalization →

The voxel length is defined as the product of the speed of light and the fundamental tick duration in RS-native units. Researchers deriving discrete spacetime scales from Recognition Science cite it to fix the minimum length element above the Planck length. The definition follows at once from the convention that c equals one voxel per tick.

claimThe voxel length satisfies $l_v = c τ_0$, where $c$ is the speed of light and $τ_0$ is the duration of one fundamental tick.

background

The PlanckScale module derives Planck length, mass, and time from RS principles via the golden ratio φ. The voxel is the minimum length quantum, set larger than the Planck scale by a factor of φ³⁴. Upstream, τ₀ is the base tick duration (defined as the fundamental time unit in the constants modules) and the voxel satisfies c = 1 voxel per tick.

proof idea

One-line definition that multiplies the speed of light by the fundamental tick duration τ₀ taken from the RS-native units.

why it matters in Recognition Science

This definition supplies the base length that enters the Planck hierarchy relations in the same module. It implements the RS mechanism linking τ₀ and φ to the Planck scale, consistent with the forcing chain landmarks where D = 3 and the phi-ladder fix the discrete units. It leaves open the explicit derivation of the φ³⁴ factor, which appears in sibling declarations.

scope and limits

formal statement (Lean)

  88noncomputable def voxelLength : ℝ := c * tau0

proof body

Definition body.

  89
  90/-- **THEOREM**: The voxel length relates to Planck length by φ³⁴. -/

depends on (4)

Lean names referenced from this declaration's body.