complexDim
The definition assigns the natural number 2 to the dimension of the complex plane, matching D-1 for spatial dimension D=3. Researchers deriving complex analysis results from Recognition Science cite it to fix the phase-space dimension. The assignment is a direct constant definition with no computation or lemmas required.
claimThe dimension of the complex plane is defined to be $2$, which equals $D-1$ when $D=3$.
background
Complex numbers are treated as recognition phase space with amplitude and phase factors. The squared modulus satisfies |ψ|² = J(|ψ|/|ψ₀|), the recognition cost of the amplitude ratio. Five canonical theorems (Cauchy, residue, Riemann mapping, Liouville, maximum modulus) correspond to configuration dimension D=5. The complex numbers form ℝ², hence a 2-dimensional space that equals D-1 at D=3 from the forcing chain.
proof idea
Direct definition that sets the constant complexDim to the natural number 2. No lemmas or tactics are invoked; the body is a literal assignment.
why it matters in Recognition Science
This supplies the complex dimension value required by ComplexAnalysisCert to certify five theorems with complex_dim = 3-1. It closes the identification of the complex plane with D-1, using the spatial dimension D=3 fixed by T8 of the unified forcing chain. The downstream theorem complexDim_eq_Dm1 then equates the definition to 3-1 by decidable arithmetic.
scope and limits
- Does not derive the value 2 from any prior RS axiom or forcing step.
- Does not state or prove any of the five complex analysis theorems.
- Does not specify the algebraic structure of ℂ beyond its dimension over ℝ.
- Does not address the J-cost functional or recognition composition law.
Lean usage
theorem use_complex_dim : complexDim = 2 := rflformal statement (Lean)
29def complexDim : ℕ := 2