pith. sign in
module module moderate

IndisputableMonolith.Mathematics.ComplexAnalysisFromRS

show as:
view Lean formalization →

The module establishes that the complex plane dimension equals D-1=2 inside Recognition Science. Researchers deriving complex structures from the forcing chain would cite it to link T8 spatial dimension to complex analysis. The module organizes sibling theorems that enforce the reduction without introducing new forcing steps.

claimThe complex plane satisfies $D-1=2$, where $D=3$ denotes the spatial dimension forced by the Recognition Science chain.

background

Recognition Science derives physics from one functional equation. The forcing chain reaches T8, which sets three spatial dimensions. This module introduces the complex-analysis layer by identifying the complex plane with the (D-1)-dimensional complement. It imports only Mathlib and collects the objects ComplexTheoremRS, complexDim, complexDim_eq_Dm1, and ComplexAnalysisCert.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the complex-dimension foundation that ComplexAnalysisCert and complexAnalysisCert consume. It closes the step from T8 (D=3) to the complex plane used in later RS derivations of physical constants.

declarations in this module (6)