complexAnalysisCert
plain-language theorem explainer
This definition assembles a certificate that exactly five complex analysis theorems hold in the Recognition Science setting, with the complex plane dimension fixed at D-1. A researcher deriving complex analysis from the J-cost functional would cite it to anchor the theorem count and the dimensional reduction from spatial D=3. The construction is a direct structure instantiation that substitutes two decidable equalities for the required fields.
Claim. Let ComplexAnalysisCert be the structure asserting that the cardinality of the set of complex analysis theorems equals 5 and that the complex dimension equals 3 minus 1. Then complexAnalysisCert is the instance of this structure obtained by substituting the decidable equality for the theorem count into the first field and the equality complexDim = 2 into the second field.
background
In the Recognition Science framework, complex numbers represent recognition phase space consisting of amplitude and phase, with the squared modulus given by the J-cost of the amplitude relative to a reference scale. The module states that five canonical theorems (Cauchy, residue, Riemann mapping, Liouville, maximum modulus) correspond to configuration dimension 5, while the complex plane itself is two-dimensional and equals D-1 when spatial dimension D=3.
proof idea
The definition is a one-line wrapper that populates the ComplexAnalysisCert structure by assigning the five_theorems field directly to complexTheoremCount and the complex_dim field directly to complexDim_eq_Dm1. Both source theorems are established by the decide tactic, so the construction inherits their decidability with no further reasoning steps.
why it matters
This definition completes the certification that complex analysis follows from the Recognition Science primitives, linking the five theorems to configuration dimension and the plane dimension to D-1 from the forcing chain. It supports the claim that standard complex results emerge once J-uniqueness and the eight-tick octave fix D=3. No downstream uses are recorded, leaving it as a self-contained anchor for further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.