Binding the primitive carrier transport to the actual cycle parameters

The geometry and support proofs live below the stage controls in ActualCarrierTransportBase. This module identifies them with the literal canonical parameter record without adding a solved-field assumption.

@[simp]

theorem NavierStokes.ActualCarrierTransport.domain_eq : ActualCarrierTransportBase.domain = ActualInitialization.geometry.domain

@[simp]

theorem NavierStokes.ActualCarrierTransport.labelCarrier_eq {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ActualCarrierTransportBase.labelCarrier l n = ActualInitialization.labelCarrier l n

theorem NavierStokes.ActualCarrierTransport.canonical_geometry {B N0 : ℕ} (l : Index B N0) (n : ℕ) : (ActualParticularStageControls.canonicalParameters (l.2, l.1)).geometry n = geometry l n

theorem NavierStokes.ActualCarrierTransport.canonical_length {B N0 : ℕ} (l : Index B N0) (n : ℕ) : (ActualParticularStageControls.canonicalParameters (l.2, l.1)).length n = referenceLength l / clock l n

theorem NavierStokes.ActualCarrierTransport.canonical_cutoff {B N0 : ℕ} (l : Index B N0) (n : ℕ) : (ActualParticularStageControls.canonicalParameters (l.2, l.1)).cutoff n = ActualGaussianCoverage.nativeCutoff CorrectionInitialization.ActualPrimary.slots.radius (referenceLength l) ⋯ ⋯ (clock l n)

theorem NavierStokes.ActualCarrierTransport.fixed_geometry {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ((ActualCycleParameters.fixedParameters B N0).particular l).geometry n = geometry l n

theorem NavierStokes.ActualCarrierTransport.fixed_length {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ((ActualCycleParameters.fixedParameters B N0).particular l).length n = referenceLength l / clock l n

theorem NavierStokes.ActualCarrierTransport.fixed_cutoff {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ((ActualCycleParameters.fixedParameters B N0).particular l).cutoff n = ActualGaussianCoverage.nativeCutoff CorrectionInitialization.ActualPrimary.slots.radius (referenceLength l) ⋯ ⋯ (clock l n)