Pith. sign in
module module moderate

IndisputableMonolith.Gravity.MacroscopicLedger

show as:
view Lean formalization →

Defines the macroscopic ledger as a tensor-product lift of the eight-tick recognition carrier, together with the induced macroscopic cyclic shift. Gravity workers cite it when promoting single-tick ledger linearity to multi-copy dynamics. The module is mostly structure: Signal8 alias, linear-map wrappers for the cyclic shift, and the macroscopic shift on tensor products.

claimThe eight-tick analytic signal carrier $S_8$ is identified with the canonical complex recognition state space. The one-tick update is the cyclic shift $C$ on $S_8$, extended as a $\mathbb{C}$-linear map. A macroscopic ledger is a finite tensor product of copies of $S_8$; the macroscopic shift $C_{\mathrm{mac}}$ acts factorwise by $C$ and is $\mathbb{C}$-linear.

background

Recognition Gravity IV treats the recognition state space as an eight-tick complex Hilbert carrier (the octave forced by T7). Upstream Ledger Superposition records that this carrier admits a one-tick cyclic update that is $\mathbb{C}$-linear, anchoring Theorem 1 (ledger superposition) and the cost-gradient functoriality of Theorem 2.

This module packages that carrier under a local alias and builds the multi-copy object needed for macroscopic gravity statements: a finite tensor product of eight-tick signals. The macroscopic shift is the tensor product of the single-tick cyclic shifts. Linearity lemmas (additivity and scalar homogeneity) are recorded so later dynamical and channel arguments can treat the macroscopic update as a genuine linear operator on the multi-copy ledger.

proof idea

Definition-and-wrapper module, not a deep proof development. Signal8 is a local abbreviation for the foundation eight-tick carrier. The single-tick cyclic shift is re-exported and packaged as a linear map, with apply, additivity, and smul lemmas. MacroscopicLedger is the tensor-product construction; MacroscopicShift is defined on pure tensors by applying the cyclic shift factorwise, then extended by linearity, with the corresponding map_add and map_smul facts.

why it matters in Recognition Science

Supplies the multi-copy ledger substrate that later gravity tracks import. PageCurveDynamical uses it to replace a kinematic triangular Page-curve ansatz by Schmidt-balanced ledger dynamics on the macroscopic shift. AmplitudeLinearForcedSubstrate imports it on the quantum-channel side when closing the substrate dichotomy between amplitude-linear and density-only evolution. In the RS chain this sits downstream of T7 (eight-tick octave) and of Ledger Superposition Theorems 1–2, and upstream of dynamical Page-curve and forced-amplitude channel results.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (16)