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

tick

show as:
view Lean formalization →

The fundamental RS time quantum is fixed at unity in native units. Workers deriving periods, masses, or modulation patterns from the forcing chain cite this base. The definition is a direct assignment with the simp attribute attached for rewriting in later steps.

claimIn RS-native units the fundamental time quantum satisfies $τ_0 := 1$.

background

The Constants module supplies the base units for all RS derivations. The tick is the indivisible time step from which the eight-tick octave (T7) is built as octave := 8 * tick. Upstream results fix the octave ratio at 2 in MusicalScale and in UniversalForcing.Strict.Music, while RSNativeUnits re-exports the same tick for Time-typed contexts.

proof idea

The declaration is a direct definition that sets tick to the real number 1. No lemmas are invoked; the simp attribute is attached for later rewriting.

why it matters in Recognition Science

This definition anchors the entire phi-ladder and eight-tick structures used in downstream results such as FRB_period_strict_increasing and rs_pattern_window_neutral. It realizes the T7 landmark of the forcing chain, where the fundamental evolution period is eight ticks. The declaration closes the unit choice for all subsequent constants including G and hbar.

scope and limits

Lean usage

def octave : ℝ := 8 * tick

formal statement (Lean)

   8@[simp] def tick : ℝ := 1

proof body

Definition body.

   9
  10/-- Notation for fundamental tick. -/
  11abbrev τ₀ : ℝ := tick
  12
  13/-- One octave = 8 ticks: the fundamental evolution period. -/

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.