pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Mathematics.ComplexAnalysisFromRS

show as:
view Lean formalization →

The module establishes that the complex plane has dimension D-1 equals 2 inside the Recognition Science framework where the forcing chain fixes D at 3. Researchers deriving complex analysis or wave functions from the phi-ladder would cite it to justify standard complex numbers. The argument proceeds by defining complexDim and proving its equality to D minus 1 via the eight-tick octave and spatial dimension result.

claim$D = 3$ spatial dimensions imply the complex plane satisfies $dim(C) = D-1 = 2$.

background

Recognition Science derives D equals 3 from the unified forcing chain T0 to T8, with T7 fixing the eight-tick octave and T8 fixing spatial dimensions. The module introduces the complex plane as the natural 2-dimensional structure complementary to these three dimensions, consistent with the Recognition Composition Law and J-uniqueness. It sits inside the Mathematics domain and imports Mathlib to host sibling definitions such as complexDim and ComplexAnalysisCert.

proof idea

This is a definition module, no proofs. It assembles definitions for complexDim, complexDim_eq_Dm1, and ComplexAnalysisCert that together encode the dimension claim.

why it matters in Recognition Science

The module supplies the complex-plane dimension required by downstream physics derivations that use wave functions or analytic continuation. It directly supports the mass formula on the phi-ladder and the alpha band by fixing the complex structure that accompanies D equals 3. No open scaffolding remains inside the supplied siblings.

scope and limits

declarations in this module (6)