binaryPhysicalChannelLinearWitness_apply
plain-language theorem explainer
If a channel map arises as the physical response of joint substrate dynamics, it agrees pointwise with the unique ℂ-linear witness extracted from amplitude-linearity. Gravity Track 2.C cites this when replacing a bare response function by its linear map form. The proof is Classical.choose_spec applied to the binary amplitude-linearity theorem.
Claim. Let $R_J$ be a $\mathbb{C}$-linear endomorphism of the joint substrate $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$, and let $R_C : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ be a physical channel response of $R_J$ (i.e., $R_C$ arises by substrate access: probe, extract, and calibrate). Then for every channel state $\varphi$, $R_C(\varphi)$ equals the value of the $\mathbb{C}$-linear witness map forced by amplitude-linearity at $\varphi$.
background
Track 2.C closes amplitude-linearity of physical channel responses from T0–T8 substrate semantics alone. The joint carrier is JointSubstrate = Signal8 ⊗[ℂ] Signal8 (T7 eight-tick factors, matter⊗channel). Joint dynamics is a ℂ-linear endomorphism $R_J$ of that tensor product.
A map $R_C$ is a physical channel response of $R_J$ when it arises from substrate access: prepare a matter probe $\psi_0$, apply $R_J$, extract a channel coordinate, and rescale by a nonzero calibration $\chi$. That is the content of PhysicalChannelResponseOf / ArisesFromSubstrateAccess.
The binary theorem physicalChannelResponse_isAmplitudeLinear then produces a ℂ-linear endomorphism of Signal8 that agrees with $R_C$. The noncomputable def binaryPhysicalChannelLinearWitness is exactly Classical.choose of that existence proof; the present lemma is the matching choose_spec evaluation.
proof idea
One-line term proof. Apply Classical.choose_spec to the existential returned by physicalChannelResponse_isAmplitudeLinear hPhys, then evaluate at the channel state $\varphi$. No further rewriting: the witness def is defined as that same Classical.choose, so the equality is definitional on the left and right of the choose-spec identity.
why it matters
This is the apply-form bridge between the bare physical response $R_C$ and its forced linear witness. Downstream, manyBodyPhysicalChannelResponse_tprod uses it so that the many-body channel on pure tensors acts sitewise by the binary physical response: each site consumes the Track 2.C binary closure.
In the framework it sits inside the unconditional Track 2.C closure (Sessions 85–126): T0–T8 force joint linearity and substrate-local observables, hence every physical channel response is amplitude-linear. That discharges the last structural hypothesis on the density-only no-go. Landmarks in play are T7 (eight-tick Signal8 factors) and the joint tensor structure for matter–channel coupling; the result is pure substrate semantics, not a new dynamical postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.