Pith. sign in
module module moderate

IndisputableMonolith.Gravity.QuantumChannel.SubstrateLocalAccess

show as:
view Lean formalization →

Defines substrate measurement-access data: a matter probe state, a channel-side readout index, and a nonzero calibration scalar. From that data it builds the induced channel and proves every such channel is a section readout and amplitude-linear. It rules out nontrivial density-only channels under substrate access, and shows pure-tensor factorization yields substrate access. Downstream Track 2.C and BMV modules import this package as the local-access interface.

claimSubstrate access data is a triple $(\psi_0, i_0, \chi)$ with probe state $\psi_0$, readout coordinate $i_0$, and calibration $\chi \neq 0$. The induced channel $C_{\psi_0,i_0,\chi}$ is a section readout and is amplitude-linear. No nontrivial density-only channel arises from substrate access. Pure-tensor factorization implies substrate access; the recognition probe supplies a canonical instance.

background

Gravity Track 2.C studies quantum channels that mediate gravitational or recognition updates on a joint matter-geometry substrate. Earlier work forced section-readout structure under an amplitude-linear hypothesis, still carrying a pure-tensor factorization assumption in places. The upstream module AmplitudeLinearForcedSectionReadout is the first direct attack on retiring that factorization: it is a structural theorem package (0 sorry) that forces section-readout form without assuming full pure-tensor factorization.

This module supplies the concrete measurement-access interface those forcing results act on. Substrate access data packages one recognition-update probe: a matter probe state $\psi_0$, a channel-side readout coordinate $i_0$, and a nonzero calibration scalar $\chi$. The induced channel is the channel obtained by coupling that probe to the joint substrate and reading out at $i_0$ with gain $\chi$.

Sibling predicates record when a channel arises from such data, that the induced map is a section readout, and that it is amplitude-linear. A parallel thread treats density-only channels (maps depending only on the reduced density) and shows they cannot be nontrivial once substrate access is required.

proof idea

Definition-first package, then short structural lemmas. SubstrateAccessData is the triple; inducedChannel builds the channel and inducedChannel_apply unfolds it. inducedChannel_isSectionReadout and the ArisesFromSubstrateAccess predicate feed two transfer lemmas: every channel arising from substrate access is a section readout, and is amplitude-linear.

Density-only obstruction is by reduction: under substrate access the channel vanishes on density-only data, hence no nontrivial density-only channel exists with substrate access. The pure-tensor direction is a constructor: pure-tensor factorization produces substrate-access data. recognitionProbeAccess and the canonical cyclic joint-operator lemma supply the RS-native probe instance used downstream.

why it matters in Recognition Science

This module is the local-access spine for Track 2.C substrate semantics. SubstrateSemanticsUnconditional imports it to close the substrate-access thread unconditionally (sessions that retired bare amplitude-linear-channel hypotheses). BMVFalsifierBand imports it when wiring certified entanglement witnesses and the falsifier floor, even though BMV entanglement is panel-excluded from the pillar-3 discriminator (any quantum mediator predicts it).

In framework terms it turns the abstract section-readout forcing of AmplitudeLinearForcedSectionReadout into a concrete probe calculus: recognition updates are local substrate measurements with calibration $\chi$, not arbitrary CPTP maps. That is the bridge from channel axioms to the recognition-composition and eight-tick discrete-time story used elsewhere in the gravity track.

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)