binaryPhysicalChannelLinearWitness
plain-language theorem explainer
Given a physical channel response arising from substrate access of any ℂ-linear joint dynamics on the binary matter-channel substrate, this definition extracts a ℂ-linear endomorphism of the eight-tick signal space that realizes the response pointwise. Gravity-track authors cite it when they need the linear-map object rather than mere existence. The body is a one-line Classical.choose on the unconditional amplitude-linearity theorem.
Claim. Given a $\mathbb{C}$-linear joint dynamics $R_J$ on the binary joint substrate $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$ and a map $R_C : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ that is a physical channel response of $R_J$ (arising from substrate access via a matter probe, a channel coordinate, and a nonzero calibration scalar), produce a $\mathbb{C}$-linear endomorphism $L : \mathrm{Signal}_8 \to_{\ell} \mathrm{Signal}_8$ witnessing amplitude-linearity of $R_C$.
background
Track 2.C closes amplitude-linearity of physical channel responses from T0-T8 substrate semantics alone, with no remaining RS-internal axioms. The joint carrier is the binary tensor product $\mathrm{JointSubstrate} = \mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$: first factor matter ledger, second factor channel ledger, each an eight-tick signal space forced by T7.
A function $R_C$ is a physical channel response of a $\mathbb{C}$-linear joint map $R_J$ when it arises from substrate access: there exist a matter probe $\psi_0$, a channel coordinate $i_0$, and a nonzero calibration $\chi$ such that $R_C\varphi = \chi^{-1}\cdot\mathrm{extractSecond}_{i_0}(R_J(\mathrm{insertFirst},\psi_0,\varphi))$. That is the substrate-semantic content of operational channel observables.
Upstream, every such $R_C$ is amplitude-linear: there exists a $\mathbb{C}$-linear endomorphism of $\mathrm{Signal}_8$ equal to $R_C$ pointwise. The proof composes joint linearity (the $\mathrm{LinearMap}$ signature, substrate-semantic Schrödinger linearity) with the access factorization into linear maps.
proof idea
One-line wrapper. Apply the unconditional theorem that every physical channel response is amplitude-linear, then take Classical.choose on the resulting existence witness. No further algebraic work: the chosen object is already a Signal8 →ₗ[ℂ] Signal8 equal to $R_C$ on all inputs (the equality is packaged in the choose-spec, used by the sibling apply lemma).
why it matters
This is the extractable linear object behind Track 2.C's unconditional closure. Downstream, the apply lemma states $R_C\varphi$ equals the witness applied to $\varphi$, turning existence into a usable identity. The many-body construction builds a sitewise $\mathbb{C}$-linear map on the macroscopic channel ledger by consuming one binary witness per site: each local physical response is replaced by its linear endomorphism.
Framework landmarks: T7 forces the eight-tick factors; joint linearity lifts Schrödinger linearity to the tensor substrate; substrate-locality of observables forces the access composite to be linear, hence amplitude-linear. The module status is full theorem closure (zero sorry). The definition itself is not a new force; it packages the forced linear map for gravity-channel and many-body consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.