macroscopicLedgerTheorem
plain-language theorem explainer
A certificate that the multi-site ledger Hilbert space carries a ℂ-linear recognition update extending the single-site cyclic shift factor-wise. Gravity theorists formalizing Paper IV Track 2.A cite this to upgrade macroscopic ledger superposition from conditional to structural. The definition assembles five already-proved linearity and pure-tensor lemmas into one structure instance.
Claim. For any finite index set $\iota$, there is a macroscopic ledger certificate asserting: (1) the single-site recognition update is $\mathbb{C}$-linear on the eight-tick signal space; (2) the macroscopic update acts factor-wise on pure tensors, $\widehat{R}_{\mathrm{macro}}(\bigotimes_i \psi_i)=\bigotimes_i \widehat{R}\psi_i$; (3--4) it is additive and scalar-homogeneous; (5) it commutes with finite linear combinations of multi-site configurations.
background
Track 2.A of Gravity IV upgrades the macroscopic ledger Hilbert carrier from a conditional claim to a structural theorem. For a finite site index $\iota$, the carrier is the $\iota$-fold Pi tensor product over $\mathbb{C}$ of single-site eight-tick signal factors: $\mathrm{MacroscopicLedger}=\bigotimes[\mathbb{C}]_{i:\iota}\mathrm{Signal8}$.
The single-site recognition update is the cyclic shift on the eight-tick octave, packaged as a $\mathbb{C}$-linear endomorphism (linearity from the Schrödinger-derivation additivity and scalar-homogeneity lemmas). The macroscopic update is the factor-wise Pi-tensor map of that endomorphism; by the universal property it is automatically linear and sends pure tensors to pure tensors of shifted factors.
The certificate structure packages five clauses: single-site linearity, pure-tensor action, additivity, scalar homogeneity, and finite superposition (the update commuting with finite linear combinations of multi-site states).
proof idea
One-line structure assembly. Single-site linearity is discharged by rewriting with the linear-map additivity and scalar-homogeneity of the packaged cyclic-shift endomorphism. The remaining four fields are direct assignments of prior lemmas: pure-tensor action from the Pi-tensor map-on-tprod identity; additivity and scalar homogeneity from the corresponding LinearMap projections of the macroscopic shift; finite superposition from the Finset-induction theorem that the macroscopic shift commutes with finite weighted sums.
why it matters
Paper IV's single-site ledger superposition is already unconditional. The multi-site claim (that superpositions of multi-site ledger configurations are physical and preserved by recognition) needed the same result at tensor-product level. This definition closes Track 2.A by inhabiting the five-clause certificate, converting that claim from conditional to structural (0 sorry, 0 RS-internal axiom).
Downstream, the inhabitedness theorem simply wraps this instance to give Nonempty of the certificate type. In the broader forcing chain the eight-tick single-site carrier is the T7 octave; the macroscopic extension is the Hilbert-space substrate on which multi-site recognition and gravity-side ledger dynamics act. It does not yet derive dynamics or coupling constants; it only certifies linear extension of the update.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.