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

ComplexFalsifier

show as:
view Lean formalization →

ComplexFalsifier records candidate counterexamples to the claim that complex numbers are forced by the 8-tick phase structure. Foundations researchers would cite the record when cataloguing ruled-out alternatives such as real-only quantum mechanics. It is implemented as a two-field record definition with no proof obligations or computational content.

claimA record type consisting of a string that describes a potential falsifier of complex-number necessity together with a string that records its status.

background

The module MATH-004 derives the necessity of complex numbers from the 8-tick phase structure of the Recognition Science ledger. Each tick corresponds to a 45° rotation, which cannot be represented in one dimension and therefore requires the imaginary unit. Upstream structures such as PhiForcingDerived.of establish the J-cost minimization that underlies ledger dynamics, while SpectralEmergence.of forces the gauge content and particle generations consistent with the same 8-tick periodicity. Constants.RSNativeUnits.status confirms the native units with c = 1 and the phi-ladder, supplying the discrete setting in which phases emerge.

proof idea

The declaration is a structure definition that introduces two String fields. No tactics or lemmas are applied; it serves as a data container for the experimentalStatus list that follows.

why it matters in Recognition Science

This structure supports the experimentalStatus definition that lists ruled-out alternatives, reinforcing the MATH-004 claim that complex numbers follow from the 8-tick octave. It connects to the requirement for two spatial dimensions for rotations within the forcing chain that ultimately yields D = 3. No open questions are directly addressed here.

scope and limits

formal statement (Lean)

 267structure ComplexFalsifier where
 268  /-- Type of potential falsification. -/
 269  falsifier : String
 270  /-- Status. -/
 271  status : String
 272
 273/-- All evidence supports complex necessity. -/

used by (1)

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

depends on (10)

Lean names referenced from this declaration's body.