complexTheoremCount
plain-language theorem explainer
The finite type enumerating five canonical complex analysis theorems has cardinality five. A researcher verifying the RS derivation of complex analysis would cite this result to confirm the dimension count. The proof reduces to a decision procedure on the inductive type's constructors.
Claim. The cardinality of the finite type enumerating the Cauchy integral theorem, residue theorem, Riemann mapping theorem, Liouville theorem, and maximum modulus principle equals 5.
background
The module interprets complex numbers as recognition phase space with amplitude and phase, where the squared modulus equals the J-cost of the normalized amplitude. It defines an inductive type whose five constructors are the Cauchy integral theorem, residue theorem, Riemann mapping theorem, Liouville theorem, and maximum modulus principle. This count is asserted to match configuration dimension D equals 5, with the complex plane supplying two dimensions equal to D minus one at spatial dimension D equals three.
proof idea
The proof is a term-mode application of the decide tactic to the goal that the Fintype cardinality of the inductive type equals 5. The tactic directly evaluates the number of constructors in the inductive definition and returns the integer 5.
why it matters
This theorem supplies the five_theorems field inside the complexAnalysisCert definition that certifies the complex analysis component. It implements the module claim that five theorems correspond to configDim D equals 5 and aligns with the complex plane dimension D minus one equals 2 when spatial dimension is fixed at three. The formalization carries zero sorry statements or extra axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.