ComplexAnalysisCert
plain-language theorem explainer
The ComplexAnalysisCert structure records that the set of recognized complex analysis theorems has cardinality five and that the complex plane dimension equals two. A researcher tracing the emergence of complex analysis from the RS forcing chain would cite it to confirm the D-1 reduction at spatial dimension three. It is realized as a direct record type whose fields simply assert the enumerated theorem count and the dimension equality.
Claim. A structure asserting that the cardinality of the set of complex analysis theorems equals 5 and that the dimension of the complex plane equals 2, where the theorems are the five cases Cauchy, Residue, Riemann mapping, Liouville, and Maximum modulus.
background
In the Recognition Science module on complex analysis, complex numbers are treated as recognition phase space whose squared modulus equals the J-cost of the amplitude. The five canonical theorems (Cauchy, Residue, Riemann mapping, Liouville, Maximum modulus) are identified with configuration dimension D=5, while the complex plane itself is identified with ℝ² and therefore carries dimension D-1 when D=3. The upstream definition complexDim fixes this value at 2, and the inductive type ComplexTheoremRS enumerates the five theorems with Fintype instance.
proof idea
The declaration is a structure definition containing two fields. The first field states that Fintype.card of ComplexTheoremRS equals 5. The second field states that complexDim equals 3-1. No lemmas or tactics are invoked; the structure simply packages the two equalities.
why it matters
The structure supplies the two invariants required to build the complexAnalysisCert instance that closes the module. It thereby confirms that complex analysis appears with exactly five theorems once the forcing chain reaches T8 and fixes D=3, consistent with the eight-tick octave and the reduction of the complex plane to D-1. It leaves open the derivation of the analytic content of those theorems from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.