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

U

show as:
view Lean formalization →

The definition U fixes the RS-native gauge by setting the fundamental time quantum to one tick, the spatial quantum to one voxel, and the speed of light to unity. Workers in Recognition Science cite this gauge when all quantities are expressed directly on the ledger primitives without external anchors. It is assembled as a record literal whose light-cone constraint is discharged by a single simp application on the base constants.

claimThe RS-native unit system $U$ is the structure with fundamental time unit $τ_0 = 1$, fundamental length unit $ℓ_0 = 1$, and speed of light $c = 1$, satisfying the light-cone relation $c ⋅ τ_0 = ℓ_0$.

background

In the Recognition Science framework the base units are the atomic tick (duration of one ledger posting) and the voxel (distance light travels in one tick). The structure RSUnits packages these together with the speed of light and the identity that light traverses one voxel in one tick. Upstream lemmas establish that the primitive tick equals one in RS units and that the light-cone relation holds identically once the units are chosen this way.

proof idea

The definition constructs the RSUnits record by assigning the time field to the tick constant, the length field to the voxel constant, and the speed field to the native speed constant. The required light-cone field is filled by a simp tactic that reduces the identity using the definitions of tick, voxel, and c.

why it matters in Recognition Science

This gauge is the starting point for the entire Recognition Science development: every subsequent quantity (coherence energy φ^{-5}, action ħ = φ^{-5} τ_0, masses on the φ-ladder) is expressed relative to U. It is invoked by the Chain structure for atomic ticks and by aesthetic certificates that rely on J-cost measured in these units. The construction closes the base of the T0-T8 forcing chain by fixing the eight-tick octave in native units.

scope and limits

Lean usage

computeRatios U

formal statement (Lean)

  79@[simp] noncomputable def U : RSUnits :=

proof body

Definition body.

  80{ tau0 := tick
  81, ell0 := voxel
  82, c := c
  83, c_ell0_tau0 := by simp [tick, voxel, c] }
  84

used by (40)

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

… and 10 more

depends on (12)

Lean names referenced from this declaration's body.