MacroscopicLedgerTheorem
plain-language theorem explainer
Certificate structure bundling five clauses that the multi-site ledger update is the canonical ℂ-linear extension of the single-site eight-tick shift. Gravity IV Track 2.A cites it to upgrade macroscopic ledger superposition from a conditional claim to a structural theorem. The structure is a pure interface; inhabitance is assembled downstream from single-site linearity and the universal property of the finite tensor product map.
Claim. For a finite site index set $\iota$, a certificate that the macroscopic recognition update on $\bigotimes_{i\in\iota} S_8$ (the $\iota$-fold tensor product over $\mathbb{C}$ of eight-tick signal carriers) is a $\mathbb{C}$-linear extension of the single-site cyclic shift: (1) the single-site map is $\mathbb{C}$-linear; (2) on pure tensors it acts factor-wise; (3)--(4) the macroscopic map is additive and scalar-homogeneous; (5) it commutes with finite linear combinations (superposition of multi-site configurations).
background
Track 2.A of Gravity IV upgrades the macroscopic ledger Hilbert carrier from a definition or conditional claim to a structural theorem. The single-site carrier is the eight-tick analytic signal $S_8$ (identified with the forced complex structure carrier). Its one-tick recognition update is the cyclic shift, packaged as a $\mathbb{C}$-linear endomorphism via additivity and scalar homogeneity proved in the Schrödinger derivation.
Given a finite index set $\iota$ of sites, the macroscopic carrier is the $\iota$-fold PiTensorProduct over $\mathbb{C}$ of $S_8$ factors. The macroscopic update is the factor-wise map of the single-site linear shift. By the universal property of that tensor-product map, the result is automatically $\mathbb{C}$-linear and sends a pure tensor $\bigotimes_i \psi_i$ to $\bigotimes_i R(\psi_i)$.
Paper IV's single-site ledger superposition is already unconditional. The multi-site claim (that superpositions of multi-site configurations remain physical and are preserved by recognition) needs the same linearity at tensor-product level; this certificate packages exactly those clauses.
proof idea
This declaration is a structure (interface), not a proved theorem: it names five fields that any witness must supply. No proof body lives here.
Inhabitance is constructed downstream. Single-site linearity is the map_add/map_smul data of the packaged cyclic-shift endomorphism (itself from the Schrödinger-derivation add and smul lemmas). Pure-tensor action is the defining equation of the PiTensorProduct factor-wise map. Additivity, scalar homogeneity, and finite-superposition commutation are the corresponding LinearMap laws of that macroscopic map, applied to finite sums. The witness definition fills the five fields by rewriting with those map laws.
why it matters
Discharges Track 2.A of the Gravity IV master plan: the macroscopic ledger Hilbert carrier becomes a structural theorem (zero sorry, zero RS-internal axiom) rather than a definition or conditional theorem. Downstream, a concrete witness inhabits the structure for every finite $\iota$, and a Nonempty theorem records that inhabitance.
In the broader Recognition chain this is the multi-site lift of single-site ledger superposition. It sits on the eight-tick octave carrier (T7) and the forced complex structure, and it is the Hilbert-space substrate on which multi-site recognition updates act linearly. Without these five clauses, macroscopic superposition in gravity ledgers would remain a paper-level assumption.
It does not yet close dynamics, continuum limits, or coupling to the mass ladder; it only certifies that the carrier and update are the correct linear extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.