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

voxel

show as:
view Lean formalization →

The voxel sets the fundamental length quantum to unity in Recognition Science native units, anchoring all spatial measures where light traverses one voxel per tick. Researchers deriving dimensionless constants or simulating discrete physics cite it to fix the base scale without external units. The definition is a direct assignment to the unit value in the real-number Length type, inheriting simp for automatic reduction.

claimThe fundamental length quantum (one voxel) satisfies $ℓ_0 := 1$ in RS-native units, where Length is the type of real numbers.

background

The RS-native system defines tick as the fundamental time quantum τ₀ = 1 and voxel as the corresponding length quantum ℓ₀, enforcing c = 1. Derived quantities include coherence energy φ^{-5} and action ħ = φ^{-5} τ₀, with all scalings organized on the φ-ladder φ^n for integer n. The module states that all physics is expressed directly in these units, with SI conversion treated as optional via ExternalCalibration.

proof idea

Direct definition that sets voxel to the constant 1 in the Length abbreviation (ℝ). The simp attribute is attached at declaration time for immediate rewriting in downstream expressions.

why it matters in Recognition Science

This definition supplies the spatial base for downstream results including alpha_not_tunable (where voxel topology fixes 103 and 102) and PosturalAxis (which uses the 8-tick cubic voxel structure). It realizes the T8 step fixing D = 3 dimensions and the c = 1 condition from the forcing chain, while leaving SI calibration as an explicit downstream interface.

scope and limits

Lean usage

theorem voxel_unit : voxel = 1 := rfl

formal statement (Lean)

  69@[simp] def voxel : Length := 1

proof body

Definition body.

  70
  71/-! ## Derived speed of light in RS-native units -/
  72
  73/-- Speed of light: c = ℓ₀/τ₀ = 1 voxel/tick. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (8)

Lean names referenced from this declaration's body.