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

experimentalStatus

show as:
view Lean formalization →

This definition enumerates three experimental observations that back the necessity of complex numbers from the 8-tick phase cycle in Recognition Science. A physicist working on the origin of the wavefunction or phasors would cite the list when linking empirical data to the ledger's rotational structure. The declaration is realized as a direct list construction of three ComplexFalsifier pairs with no lemmas or reductions applied.

claimThe experimental status is the list consisting of the pair (``Real QM'', ``Ruled out by Renou et al. (2021)''), the pair (``Phase in experiments'', ``Ubiquitous and essential''), and the pair (``8-tick structure'', ``Appears in spin statistics'').

background

The module MATH-004 derives the necessity of complex numbers from Recognition Science's 8-tick structure. The fundamental time quantum is the tick, defined as 1 in RS-native units. Phase is the abbreviation for Fin 8, the 8-tick phase space whose elements label rotations by multiples of 45 degrees. ComplexFalsifier is the structure that pairs a falsification type (String) with its status (String). Upstream results include the definition of tick as the fundamental RS time quantum and the Phase abbreviation for the cycle.

proof idea

This is a direct definition that constructs the list of three ComplexFalsifier instances by enumerating the strings for each entry. No lemmas are applied; it is a literal list of pairs.

why it matters in Recognition Science

This definition supplies the experimental support section for the module claim that complex numbers are forced by the 8-tick octave (T7) in the Recognition Science framework. It records the ruling out of real-only quantum mechanics and the ubiquity of phases, closing the derivation that rotations in the ledger require two dimensions. No parent theorems appear in the used-by edges.

scope and limits

formal statement (Lean)

 274def experimentalStatus : List ComplexFalsifier := [

proof body

Definition body.

 275  ⟨"Real QM", "Ruled out by Renou et al. (2021)"⟩,
 276  ⟨"Phase in experiments", "Ubiquitous and essential"⟩,
 277  ⟨"8-tick structure", "Appears in spin statistics"⟩
 278]
 279
 280end ComplexNumbers
 281end Mathematics
 282end IndisputableMonolith

depends on (10)

Lean names referenced from this declaration's body.