module module moderate

`IndisputableMonolith.Gravity.QuantumChannel.MediatorUniversalityBoundary`

Module on the mediator-universality boundary for gravitational quantum channels: pure-state densities, conjugation channels, and existence of a per-update density mediator. Gravity Track 2.C cites it when upgrading amplitude-linear mediation from modeling choice to forced structure. Argument mixes definitions (density, swap bases) with short invariance and trace-preservation lemmas built on the amplitude-linear substrate dichotomy.

claimFor a pure state $|\psi\rangle$, form the density $\rho = |\psi\rangle\langle\psi|$; show phase invariance and unit trace; construct a conjugation channel that reproduces the update and preserves trace; and prove existence of a per-update density mediator, with explicit two-level swap bases as witnesses at the universality boundary.

background

Track 2.C of the quantum-gravity plan forces the amplitude-linear gravitational channel from substrate linearity rather than assuming it. The upstream module states this as the upgrade of paper IV's T2 from MODEL to THEOREM, opening with a substrate dichotomy on a single update.

This module sits at the mediator-universality boundary of that channel. It introduces the pure-state density $\rho = |\psi\rangle\langle\psi|$ (phase-invariant, unit trace, nonzero on single rays), a conjugation channel that reproduces the density update and is trace-preserving, and an existence claim for a per-update density mediator. Two-level bases and a swap matrix supply concrete finite-dimensional witnesses.

Notation is standard quantum-information: pure states, conjugation channels as completely positive maps induced by unitary conjugation, and mediators as maps that carry density data across one recognition update while respecting the amplitude-linear constraint forced upstream.

proof idea

Definition layer first: pure-state density, two basis vectors, and the swap matrix. Short lemmas then check phase invariance of the density, unit trace, and nonvanishing on a single ray. The conjugation channel is defined and shown to reproduce the intended update and to preserve trace. The existence result for a per-update density mediator assembles those facts, using the swap witnesses at the two-level boundary. No deep tactic automation; the spine is definitional plus direct algebraic checks on matrices and channels, importing the amplitude-linear forcing context from the upstream Track 2.C module.

why it matters in Recognition Science

In Recognition Science gravity, mediation must be universal across pure-state densities once amplitude-linearity is forced. This module supplies the boundary objects (densities, conjugation channel, mediator existence) that make that universality checkable in Lean rather than schematic.

It feeds the Track 2.C program opened by AmplitudeLinearForced: substrate dichotomy implies amplitude-linear channel, which in turn constrains how gravitational updates act on quantum states. Downstream parent theorems are not yet wired in this graph (used_by empty), so the module is presently a leaf that closes local scaffolding for mediator universality.

Framework link: once the channel is forced, eight-tick and $D=3$ structure from the forcing chain constrain the same update cadence the mediator must respect; this file stays at the quantum-channel layer and does not re-derive those landmarks.

scope and limits

Does not force amplitude-linearity itself; that is upstream Track 2.C.
Does not derive Newtonian or relativistic field equations from the mediator.
Does not treat mixed states beyond pure-state densities and conjugation.
Does not claim a unique mediator; only existence at the universality boundary.
Does not yet show downstream used_by edges in the dependency graph.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForced module_import

declarations in this module (17)

def densityOf L50
theorem densityOf_phase_invariant L54
theorem trace_densityOf L78
theorem densityOf_single_ne_zero L83
def conjugationChannel L92
theorem conjugationChannel_reproduces L100
theorem conjugationChannel_trace_preserving L110
theorem per_update_density_mediator_exists L120
def basis0 L130
def basis1 L133
def swap01 L136
def swapMatrix L139
theorem swapMatrix_unitary L142
theorem swapMatrix_mulVec_basis0 L146
theorem densityOf_basis0_ne_densityOf_basis1 L158
theorem no_universal_density_mediator L165
theorem mediator_universality_boundary L189