Pith. sign in
module module high

IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedJoint

show as:
view Lean formalization →

Defines the joint matter-plus-channel substrate as the binary tensor product Signal8 ⊗[ℂ] Signal8: first factor the matter ledger, second the channel ledger. Track 2.C uses this to lift the single-factor amplitude-linear dichotomy to a two-factor setting. Mostly definitions and elementary tensor lemmas (eval, insert, extract). Cited by the substrate-side closure and the Track 2.C master certificate.

claimThe joint substrate is the $\mathbb{C}$-tensor product $H_{\mathrm{joint}} := \mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$, with the first factor the matter ledger and the second the channel ledger. The module supplies evaluation at pure tensors, insertion of a vector into either factor, and extraction of either factor from a pure tensor $u \otimes v$.

background

Track 2.C of the quantum-gravity plan upgrades paper IV's T2 from a modeling assumption to a theorem: the amplitude-linear gravitational channel must be forced by substrate linearity. The upstream module AmplitudeLinearForced opens that track with the single-factor substrate dichotomy on Signal8: no nontrivial channel response is simultaneously amplitude-linear and density-only.

This module supplies the two-factor arena. Both ledgers are copies of the eight-tick signal space Signal8 (the discrete octave carrier from the forcing chain). The joint state space is their algebraic tensor product over $\mathbb{C}$. Pure tensors $u \otimes v$ represent product matter-channel configurations; the insert/extract maps move between single-factor and joint data without choosing bases beyond the tensor structure.

Notation is standard Mathlib tensor product: tmul for $\otimes$, with evaluation and factor projections stated as simp-friendly identities.

proof idea

This is a definition module, not a theorem package. It introduces JointSubstrate as the binary tensor product and a small API: evalAt on pure tensors, insertFirst/insertSecond to embed a single-factor vector, and extractFirst/extractSecond with the expected identities on tmul. Companion lemmas are one-line rfl or simp rewrites. No forcing or dichotomy is proved here; those live downstream once the joint substrate is in place.

why it matters in Recognition Science

Session 86 of Track 2.C. Downstream AmplitudeLinearForcedSubstrate records that Sessions 85 and 86 established the single-factor dichotomy and the joint binary-tensor model; the substrate-side closure then finishes the two-factor argument. The master certificate module aggregates Sessions 85–87 and treats this binary-tensor model as the ambient setting for the Track 2.C closure.

Without a clean joint substrate, the amplitude-linear forcing claim cannot be stated for matter coupled to a channel. The module therefore sits between the single-factor dichotomy and the certified forcing theorem, keeping the tensor bookkeeping out of the physics proofs. It does not itself touch T5–T8 or the RCL; it only prepares the Hilbert-space-like carrier those gravity results act on.

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 (18)