GravityConfig
plain-language theorem explainer
GravityConfig is a pure type synonym: for any type κ it is definitionally κ, used only as a named marker for the gravitational configuration space. Anyone citing Theorem 2 (cost-gradient functoriality) of Gravity from Recognition IV uses it as the codomain of classical maps from density configurations. There is no proof content; the abbrev is identity.
Claim. For an arbitrary type $\kappa$, the gravitational configuration space is identified with $\kappa$ itself: $\mathrm{GravityConfig}(\kappa) := \kappa$. The name is a notational marker, not a new construction.
background
The module Gravity.LedgerSuperposition anchors two load-bearing results from Gravity from Recognition IV: The Quantum Channel. Theorem 1 (ledger superposition) shows that the eight-tick recognition carrier is a complex Hilbert space and that the one-tick update is $\mathbb{C}$-linear and inner-product preserving, so coherent superpositions of ledger states are physical. Theorem 2 (cost-gradient functoriality) concerns classical maps from matter density configurations into a gravitational configuration space, and their unique $\mathbb{C}$-linear extensions on free modules.
GravityConfig is the named codomain of those classical maps. Sibling markers in the same file include DensityConfig (matter side) and FreeC (the free $\mathbb{C}$-module on a finite basis, identified with finitely supported functions $\iota \to_0 \mathbb{C}$). The module reuses Foundation.SchrodingerDerivation, RecognitionOperator, and ComplexStructureForcing; it introduces no new RS axioms.
proof idea
Definitional abbrev only: GravityConfig κ reduces by unfolding to κ. No tactics, no lemmas, no hypotheses. Downstream code treats the name as documentation that a type is playing the gravitational-configuration role in the T2 extension diagram.
why it matters
In the paper's Theorem 2 story, any classical map $g : \mathrm{DensityConfig} \to \mathrm{GravityConfig}$ extends uniquely to a $\mathbb{C}$-linear operator on the free modules generated by the two bases, by the universal property of free linear extension. The physical reading (tagged MODEL in the module doc) is that the cost-gradient response in any matter-plus-gravitational-channel extension of the linear ledger update must be that unique linear extension, not a nonlinear classical readout.
The abbrev earns its place by giving that codomain a stable name shared with DensityConfig and FreeC, so the functoriality statements stay readable. Downstream, the file's inhabitedness witness for the ledger-superposition theorem package sits next to the Theorem 2 section that consumes this marker. Framework-wise this is gravity-side packaging of the complex structure already forced for the recognition register (eight-tick octave, $\mathbb{C}$-linearity), not a new forcing step in T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.