FreeC
plain-language theorem explainer
Free complex module on a finite index set: finitely supported maps from ι into ℂ, identified with the linear span of basis kets |α⟩. Gravity-channel and BMV two-qubit arguments cite it as the carrier for superpositions of definite density or gravity configurations. The declaration is a pure type synonym for Mathlib's finitely supported functions; no proof content.
Claim. For any type $\iota$ with decidable equality, $\mathrm{FreeC}(\iota)$ denotes the free $\mathbb{C}$-module on $\iota$, realized as the space of finitely supported functions $\iota\to\mathbb{C}$ (finite $\mathbb{C}$-linear combinations of basis vectors $|\alpha\rangle$, $\alpha\in\iota$).
background
The module Gravity.LedgerSuperposition anchors two load-bearing results from Gravity from Recognition IV: The Quantum Channel. T1 treats the eight-tick recognition register as a complex Hilbert carrier whose one-tick update is ℂ-linear and inner-product preserving, so coherent superpositions of ledger configurations are physical. T2 asserts cost-gradient functoriality under superposition: any classical map from definite density configurations to gravity configurations extends uniquely to a ℂ-linear operator on the free modules they generate.
FreeC is the algebraic carrier for that extension. Mathlib's type ι →₀ ℂ is the set of finitely supported functions ι → ℂ; with decidable equality on ι it is the free ℂ-module on the basis {|α⟩ : α ∈ ι}. Sibling names DensityConfig and GravityConfig supply the classical bases that get linearized. Upstream imports (RecognitionOperator, SchrodingerDerivation, ComplexStructureForcing) already force the complex structure and the linear recognition update; FreeC only names the free module they act on.
proof idea
One-line abbreviation: FreeC ι is definitionally equal to ι →₀ ℂ. No tactics, no lemmas, no axioms. All freeness and universal-property work is deferred to Mathlib's Finsupp API and to the T2 extension construction that consumes this type.
why it matters
T2 (cost-gradient functoriality) needs a precise carrier for superpositions of definite configurations. FreeC is that carrier: classical maps g : DensityConfig → GravityConfig extend uniquely along the free-module universal property to ℂ-linear maps on FreeC. The module doc states the physical reading explicitly: in any extension of the linear ledger update from matter alone to matter-plus-gravitational-channel, the cost-gradient response must be that unique linear extension, not a nonlinear classical readout. The mathematical theorem is unconditional; the physical tag is MODEL. FreeC itself introduces no new RS axioms and sits downstream of the complex-structure forcing already proved in Foundation. Without this type synonym the free-extension statement cannot even be typed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.