Real finrank of a compatible complex module

This file records the tower-law dimension formula for a complex module whose real scalar structure is the ambient one. It is the linear-algebra input for almost-complex even-dimensionality results, but has no symplectic hypotheses.

theorem TauCeti.finrank_real_eq_two_mul_finrank_complex {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] : Module.finrank ℝ V = 2 * Module.finrank ℂ V

A compatible complex module structure forces the real dimension to be twice the complex dimension. This is the ambient-real-structure form of Mathlib's finrank_real_of_complex: that lemma fixes the real structure to be the one induced by restricting scalars (Module.complexToReal), whereas here V already carries an ambient Module ℝ V made compatible via IsScalarTower ℝ ℂ V (the situation produced by an almost complex structure).