Pith. sign in
module module high

IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedSectionReadout

show as:
view Lean formalization →

Defines nonzero matter-section readout: a channel response recovered by injecting a fixed matter reference into one tensor factor of a joint linear operator, applying the operator, extracting at a fixed channel coordinate, and rescaling. Weaker than global pure-tensor factorization. Proves the amplitude-linear vs density-only dichotomy still forces the channel to vanish under this section constraint, with a recognition-specialized variant and a forcing certificate. Cited by the substrate locality / measurement-access layer.

claimA channel map $R_C$ is a nonzero matter-section readout of a joint linear operator $R_J$ if there exist a fixed matter reference $\psi_0$, an index $i_0$, and a nonzero scalar $\chi$ such that $R_C(\varphi)=\chi^{-1}\bigl(\mathrm{extract}_{i_0}\circ R_J(\psi_0\otimes\varphi)\bigr)$. Under this constraint (and its recognition specialization), any channel that is both amplitude-linear and density-only must be identically zero; pure-tensor factorization implies section readout.

background

Gravity Track 2.C closes the substrate side of the quantum-channel story for Recognition gravity. Upstream work (Sessions 85–86, substrate and joint amplitude-linear forcing) established the single-factor dichotomy: a response that is both amplitude-linear and density-only is forced to zero, and the joint setting extends that pressure to operators on matter–channel tensors.

This module weakens the structural hypothesis from global pure-tensor factorization of the joint operator to an operational section. Only the readout along the slice $\psi_0\otimes\varphi$ is constrained: inject a fixed matter reference, apply $R_J$, extract the channel factor at a fixed coordinate, and divide by a nonzero scalar. That is enough to recover a channel response $R_C$ without controlling $R_J$ on every pure tensor.

A recognition-specialized section readout is introduced alongside the general joint section readout, matching the RS measurement interface used downstream. The local setting is the forced-substrate import chain, not a new dynamical law.

proof idea

The module is theorem-bearing, not a pure definition dump. It introduces the section-readout predicates (joint and recognition), then reduces the amplitude-linear / density-only vanishing theorems to the already-forced substrate lemmas by unwinding the four-step readout (inject, apply, extract, rescale).

Pure-tensor factorization is shown to imply section readout, so earlier factorization-based amplitude-linearity results transport through the weaker interface. Density-only channels with a nonzero section readout are forced to the zero channel; nontrivial density-only examples are ruled out. A compact forcing certificate packages the section-readout dichotomy for downstream import.

why it matters in Recognition Science

Section readout is the operational bridge between joint linear structure and what a local measurement can actually see. Downstream, SubstrateLocalAccess imports this module as the step beyond Session 111's section-readout retirement and builds the substrate locality / measurement-access principle on top (structural theorem, zero sorry).

In the Recognition gravity track, this keeps the amplitude-linear forcing chain alive under a hypothesis weak enough for real channel extraction, rather than demanding global pure-tensor form of the joint operator. It feeds the closure narrative of Track 2.C: once section readout forces density-only channels to vanish, local access principles can be stated without reopening the substrate dichotomy. Framework-wise it sits on the gravity/quantum-channel side of the forcing story, not on T5–T8 constants, but it is required scaffolding for any claim that RS measurement sees only amplitude-linear channel responses.

scope and limits

used by (1)

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