DensityConfig
plain-language theorem explainer
Density-configuration indices are identified with an arbitrary parameter type ι: definite ledger states (mass densities) are just the points of ι. Anyone reading the cost-gradient functoriality theorem (T2) or the BMV two-mass setup cites this naming. The declaration is a pure type synonym, so equality is definitional.
Claim. For any type $\iota$, the density-configuration index type is definitionally $\iota$: definite ledger configurations (mass densities) are parameterized by $\iota$. In the BMV two-mass, two-branch setup one takes $\iota = \mathrm{Fin}\,4$, indexing the four branch states $\{\mathrm{LL},\mathrm{LR},\mathrm{RL},\mathrm{RR}\}$.
background
The module Gravity IV anchors two load-bearing results from Gravity from Recognition IV: The Quantum Channel. T1 (ledger superposition) states that the eight-tick carrier is a complex Hilbert space and that the one-tick recognition update is ℂ-linear and inner-product preserving, so coherent superpositions of definite ledger states are physical. T2 (cost-gradient functoriality) asserts that any classical map from density configurations to gravity configurations extends uniquely by free linear extension to the free ℂ-modules on those bases.
The eight-tick analytic signal carrier is the type Fin 8 → ℂ (locally abbreviated from the foundation complex-structure forcing development), equipped with its canonical Hermitian product. Definite ledger configurations are the classical basis points that get superposed inside that carrier. The present abbreviation simply names the index type of those classical density points, so that the domain of a classical cost-gradient map can be written cleanly before free linear extension.
In the Bose–Marletto–Vedral two-mass, two-branch thought experiment the index set is Fin 4, labeling the four definite branch states {LL, LR, RL, RR}. The same pattern applies to any finite (or abstract) index type of mass-density configurations.
proof idea
Pure abbreviation: the right-hand side is the parameter type itself. No tactics, no lemmas, no axioms. Unfolding is definitional equality in Lean.
why it matters
T2 is stated as unique ℂ-linear extension of a classical map g from density configurations to gravity configurations. Naming the domain type makes that statement readable and matches the paper's language (definite ledger configurations as mass densities). The module doc tags the mathematical free-extension theorem as unconditional and the physical identification (cost-gradient response must be that unique linear extension, not a nonlinear classical readout) as MODEL.
Downstream, the inhabited package for the ledger-superposition theorem sits in the same file and the T2 section opens immediately after; GravityConfig is the matching codomain synonym. The construction reuses only foundation material (recognition operator, Schrödinger derivation, complex-structure forcing) and introduces no new RS-internal axioms. Framework landmarks in view are the eight-tick octave carrier and the linear recognition update that T1 already showed preserves superpositions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.