complexDim_eq_Dm1
plain-language theorem explainer
The equality fixes the complex plane dimension at exactly 2, matching D-1 for the three spatial dimensions fixed by the forcing chain. Researchers certifying embeddings of the five canonical complex analysis theorems in Recognition Science cite this step when assembling the overall certificate. The proof is a one-line decision tactic that reduces the definition directly to the arithmetic identity.
Claim. The dimension of the complex plane equals 3 minus 1.
background
The module interprets complex numbers as recognition phase space with amplitude and phase, where the squared modulus equals the J-cost of the amplitude. Complex plane dimension is introduced as the two-dimensional real plane, set equal to D-1 once D=3 is fixed. The upstream definition states that this dimension is 2.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the arithmetic equality between the upstream definition of the complex plane dimension and 3-1.
why it matters
This equality is used inside the ComplexAnalysisCert to bundle the five theorems with the complex dimension. It supplies the concrete link between T8 (D=3) in the forcing chain and the two-dimensional complex plane required for the canonical theorems. The module doc-comment notes that complex numbers correspond to ℝ² at D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.