Pith. sign in
module module high

IndisputableMonolith.Gravity.QuantumChannel.SubstrateLocalAccess

show as:
view Lean formalization →

Defines substrate measurement-access data: a matter probe state, a channel-side readout coordinate, and a nonzero calibration scalar, plus the channel they induce. Shows every channel from such access is a section-readout and amplitude-linear, and that no nontrivial density-only channel arises this way. Cited by Track 2.C substrate-semantics closure and the BMV falsifier band. Proofs reduce access data to upstream forced section-readout structure.

claimSubstrate access data is a triple $(\psi_0, i_0, \chi)$ with matter probe state $\psi_0$, channel-side readout index $i_0$, and nonzero calibration scalar $\chi$. It induces a quantum channel on the joint substrate. Any channel arising from such access is a section-readout and is amplitude-linear; no nontrivial density-only channel admits substrate access. Pure-tensor factorization and the canonical recognition probe both yield instances of this access.

background

Gravity Track 2.C studies which quantum channels on a joint matter-mediator substrate can arise from local recognition updates. The upstream module on amplitude-linear forced section-readout forces section-readout structure for amplitude-linear channels without full pure-tensor factorization; it is a structural theorem with zero sorry.

This module packages the concrete measurement-access data of one recognition-update probe: a matter probe state $\psi_0$, a channel-side readout coordinate $i_0$, and a nonzero calibration scalar $\chi$. From that triple one builds an induced channel and the predicate that a given channel arises from substrate access.

The local goal is to connect that access predicate to section-readout and amplitude-linearity, and to rule out nontrivial density-only channels under substrate access, so later modules can close the substrate-semantics thread unconditionally.

proof idea

Definition-led module with short structural lemmas. Substrate access data is a record; the induced channel applies the calibrated probe at the chosen readout coordinate. A direct check shows the induced channel is a section-readout. The arises-from-access predicate implies section-readout and amplitude-linearity by reducing to that induced form. Density-only channels from access are forced to vanish, so no nontrivial density-only channel has substrate access. Two constructors close the circle: pure-tensor factorization produces access data, and the canonical recognition probe (cyclic joint operator) arises from recognition-probe access.

why it matters in Recognition Science

Data and forcing layer for the Track 2.C substrate-access thread. Downstream, the substrate-semantics unconditional module imports it to close that thread: sessions retiring bare amplitude-linear-channel hypotheses land on the access predicate and the no-nontrivial-density-only theorem defined here. The BMV falsifier band also imports it when packaging the certified entanglement witness and falsifier floor; BMV entanglement is excluded from the pillar-3 discriminator (any quantum mediator predicts it), but substrate-access language still supplies the channel side of the witness.

In framework terms the module turns abstract section-readout forcing into an explicit recognition-update probe, the measurement interface needed before mass-ladder or eight-tick claims can be read off a gravity channel.

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)