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

ExternalCalibration

show as:
view Lean formalization →

ExternalCalibration supplies the three positive scaling factors that convert RS-native tick, voxel, and coherence units into SI seconds, meters, and joules while enforcing exact numerical agreement with the measured speed of light. Researchers converting Recognition Science predictions to laboratory data cite this record to anchor abstract results. It is introduced as a structure whose fields directly encode the required positivity and consistency conditions.

claimA structure consisting of positive real numbers $s$ (seconds per tick), $m$ (meters per voxel), and $j$ (joules per coherence quantum) such that $m/s = 299792458$.

background

The RS-native unit system takes the tick as the fundamental time quantum and the voxel as the fundamental length quantum, with $c=1$ in these units. Coherence quantum is defined as $phi^{-5}$. ExternalCalibration provides the optional bridge to SI units. Upstream, tick is defined as the constant 1 in Constants.tick and re-exported in RSNativeUnits.tick; voxel is similarly the unit length.

proof idea

The declaration is a structure definition that bundles the three scaling parameters together with their positivity proofs and the speed-consistency equality; no further lemmas are applied.

why it matters in Recognition Science

This structure is the anchor point for all SI conversion functions in the module, including to_meters, to_seconds, to_joules, and the theorem c_in_si that recovers the exact SI value of c. It closes the loop between the internal RS-native system (where c=1 and all ratios are fixed by phi) and external measurement, as required by the module's design for optional SI anchoring. It supports the eight-tick octave and phi-ladder scaling by providing the dimensional conversion layer.

scope and limits

Lean usage

theorem c_in_si (cal : ExternalCalibration) : to_m_per_s cal c = 299792458 := by simp [to_m_per_s, c, cal.speed_consistent]

formal statement (Lean)

 292structure ExternalCalibration where
 293  /-- Seconds per tick (τ₀ in seconds). -/
 294  seconds_per_tick : ℝ
 295  /-- Meters per voxel (ℓ₀ in meters). -/
 296  meters_per_voxel : ℝ
 297  /-- Joules per coherence quantum. -/
 298  joules_per_coh : ℝ
 299  /-- All conversion factors are positive. -/
 300  seconds_pos : 0 < seconds_per_tick
 301  meters_pos : 0 < meters_per_voxel
 302  joules_pos : 0 < joules_per_coh
 303  /-- Consistency: c = ℓ₀/τ₀ must equal 299792458 m/s in SI. -/
 304  speed_consistent : meters_per_voxel / seconds_per_tick = 299792458
 305
 306/-- Convert time (in ticks) to seconds. -/

used by (21)

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

depends on (3)

Lean names referenced from this declaration's body.