The actual signed family at its native reference bands

Each primary label retains its own prepared slow domain. The otherwise irrelevant band index in a physical reference is frozen at that label's reference band. In particular, no global ordering of a fixed native cover above all common covers is asserted.

The request uses the actual common-reference state and its torus average. Only the wave geometry is put in native coordinates: inverse-cover pullback of the entire state would in general have only subcover periodicity.

A common-torus signed request with native wave geometry

The torus-averaged signed request is independent of the free fast coordinate and angle at which it is evaluated. The common state can therefore be kept on its original torus while the primary wave uses native fast coordinates. Freezing the band index preserves every actual derivative and average.

@[reducible, inline]

abbrev NavierStokes.TorusMeanRequestRebase.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.TorusMeanRequestRebase.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

abbrev NavierStokes.TorusMeanRequestRebase.Cylinder : Type

Cylinder: an abbreviation for PhysicalSignedWave.Cylinder.

Equations

• NavierStokes.TorusMeanRequestRebase.Cylinder = NavierStokes.PhysicalSignedWave.Cylinder

@[reducible, inline]

abbrev NavierStokes.TorusMeanRequestRebase.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.TorusMeanRequestRebase.Plane = NavierStokes.TorusInverse.Plane

noncomputable def NavierStokes.TorusMeanRequestRebase.freezeStrip {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (m : ℕ) : WeightedClasses.StripData D

Freeze strip as an element of StripData D.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.TorusMeanRequestRebase.freezeTriple {D : Type} (v : MeanIncrementBounds.Triple D) (m : ℕ) : MeanIncrementBounds.Triple D

Freeze triple, given by ⟨fun _ => v.radial m, fun _ => v.angular m, fun _ => v.axial m⟩.

Equations

• NavierStokes.TorusMeanRequestRebase.freezeTriple v m = { radial := fun (x : ℕ) => v.radial m, angular := fun (x : ℕ) => v.angular m, axial := fun (x : ℕ) => v.axial m }

noncomputable def NavierStokes.TorusMeanRequestRebase.freezeContext {D : Type} (c : CorrectionState.Context D) (m : ℕ) : CorrectionState.Context D

Freeze context, bundling operators, epsilon, radialFrequency, fastCoefficient and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.TorusMeanRequestRebase.freezeState {D : Type} (u : CorrectionState.State D) (m : ℕ) : CorrectionState.State D

Freeze state, bundling mean, pressure, oscillation, oscillatoryPressure and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.TorusMeanRequestRebase.freezeWave {D : Type} (a : LinearWaveBounds.WaveCoefficients D) (m : ℕ) : LinearWaveBounds.WaveCoefficients D

Freeze wave, bundling radius, radialBase, frequencyBase, axialBase and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.TorusMeanRequestRebase.freezeDirections {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : LinearWaveBounds.GraphDirections D) (m : ℕ) : LinearWaveBounds.GraphDirections D

Freeze directions, given by { d with radialScale := fun _ => d.radialScale m, fastScale := fun _ => d.fastScale m }.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NavierStokes.TorusMeanRequestRebase.freezeStrip_domain {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (m : ℕ) : (freezeStrip s m).domain = s.domain

@[simp]

theorem NavierStokes.TorusMeanRequestRebase.freezeStrip_epsilon {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (m n : ℕ) : (freezeStrip s m).epsilon n = s.epsilon m

@[simp]

theorem NavierStokes.TorusMeanRequestRebase.freezeState_covariance {D : Type} (u : CorrectionState.State D) (m n : ℕ) (i j : Fin 3) : (freezeState u m).covariance i j n = u.covariance i j m

@[simp]

theorem NavierStokes.TorusMeanRequestRebase.freezeState_theta {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (m n : ℕ) : (freezeState u m).thetaResidual (freezeContext c m) n = u.thetaResidual c m

@[simp]

theorem NavierStokes.TorusMeanRequestRebase.freezeState_axial {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (m n : ℕ) : (freezeState u m).axialResidual (freezeContext c m) n = u.axialResidual c m

@[simp]

theorem NavierStokes.TorusMeanRequestRebase.freezeContext_frame {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (m n : ℕ) : HarmonicResidual.contextFrame (freezeContext c m) n = HarmonicResidual.contextFrame c m

theorem NavierStokes.TorusMeanRequestRebase.freezeState_coherent {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (u : CorrectionState.State D) (m n nr : ℕ) (U : Set D) : PhysicalResidualNaturality.StateOn U (ContinuousLinearEquiv.refl ℝ D) 1 1 (freezeState u m) (freezeState u m) n nr

theorem NavierStokes.TorusMeanRequestRebase.freezeContext_coherent {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (m n nr : ℕ) (U : Set D) : PhysicalResidualNaturality.ContextOn U (ContinuousLinearEquiv.refl ℝ D) 1 1 (freezeContext c m) (freezeContext c m) n nr

The evaluation point carries no torus or angle dependence

theorem NavierStokes.TorusMeanRequestRebase.fullRequest_free_variables (s : WeightedClasses.StripData Point) (P : SignedStressPrimitive.Patch) (coord : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (n : ℕ) (r : ℝ) (z Y Y' : Plane) (theta theta' : ℝ) : LocalSignedRequest.fullRequest s P coord c u n ((r, z, Y), theta) = LocalSignedRequest.fullRequest s P coord c u n ((r, z, Y'), theta')

theorem NavierStokes.TorusMeanRequestRebase.stateRequest_free_variables (s : WeightedClasses.StripData Cylinder) (P : SignedStressPrimitive.Patch) (h : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (n : ℕ) (r : ℝ) (z Y Y' : Plane) (theta theta' : ℝ) : PhysicalSignedWave.stateRequest s P h c u n ((r, z, Y), theta) = PhysicalSignedWave.stateRequest s P h c u n ((r, z, Y'), theta')

theorem NavierStokes.TorusMeanRequestRebase.stateRequest_fast_map (s : WeightedClasses.StripData Cylinder) (P : SignedStressPrimitive.Patch) (h : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (n : ℕ) (mapFast : Plane → Plane) (x : Cylinder) : PhysicalSignedWave.stateRequest s P h c u n ((x.1.1, x.1.2.1, mapFast x.1.2.2), x.2) = PhysicalSignedWave.stateRequest s P h c u n x

This changes only the evaluation point, not the state or the measure used for its torus average. The fast-coordinate map can be arbitrary.

theorem NavierStokes.TorusMeanRequestRebase.stateRequest_inverseCover (s : WeightedClasses.StripData Cylinder) (P : SignedStressPrimitive.Patch) (h : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (n gap : ℕ) (x : Cylinder) : PhysicalSignedWave.stateRequest s P h c u n ((x.1.1, x.1.2.1, (CommonCoverSolve.coverPower gap).symm x.1.2.2), x.2) = PhysicalSignedWave.stateRequest s P h c u n x

theorem NavierStokes.TorusMeanRequestRebase.stateRequest_freeze (s sr : WeightedClasses.StripData Cylinder) (P : SignedStressPrimitive.Patch) (h : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (m n : ℕ) (hepsilon : sr.epsilon n = s.epsilon m) (x : Cylinder) : PhysicalSignedWave.stateRequest sr P h (freezeContext c m) (freezeState u m) n x = PhysicalSignedWave.stateRequest s P h c u m x

Equality uses exactly the source and target epsilons. No equality of their unrelated domains, phase frames, or native backgrounds is needed.

theorem NavierStokes.TorusMeanRequestRebase.stateRequest_freeze_full (s : WeightedClasses.StripData Point) (sr : WeightedClasses.StripData Cylinder) (P : SignedStressPrimitive.Patch) (h : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (m n : ℕ) (hepsilon : sr.epsilon n = s.epsilon m) (x : Cylinder) : PhysicalSignedWave.stateRequest sr P h (freezeContext c m) (freezeState u m) n x = LocalSignedRequest.fullRequest s P (2 * h) c u m (PhysicalResidualTZ.swapCylinder x)

@[simp]

theorem NavierStokes.TorusMeanRequestRebase.stateRequest_freezeStrip (s : WeightedClasses.StripData Cylinder) (P : SignedStressPrimitive.Patch) (h : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (m n : ℕ) (x : Cylinder) : PhysicalSignedWave.stateRequest (freezeStrip s m) P h (freezeContext c m) (freezeState u m) n x = PhysicalSignedWave.stateRequest s P h c u m x

Identity band views of the native primary

theorem NavierStokes.TorusMeanRequestRebase.ratioPower_self {Q : ℝ} (hQ : 0 < Q) (a : ℝ) : PhysicalParticularWave.ratioPower Q Q a = 1

theorem NavierStokes.TorusMeanRequestRebase.slowChange_self (h : ℝ) {Q : ℝ} (hQ : 0 < Q) (z : Plane) : (PhysicalSignedWave.slowChange h Q Q) z = z

theorem NavierStokes.TorusMeanRequestRebase.requestChart_self (h : ℝ) {Q : ℝ} (hQ : 0 < Q) : PhysicalSignedWave.requestChart h hQ hQ 0 = ContinuousLinearEquiv.refl ℝ Point

noncomputable def NavierStokes.TorusMeanRequestRebase.identityViews {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (m : ℕ) (h Q : ℝ) (cover : ℕ) (hQ : 0 < Q) (hfrequency : B.base.frequency m ≠ 0) : B.Views m

The dummy band index repeats one physical scale and one native cover. Every coordinate change is the identity; the supplied primary is retained.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NavierStokes.TorusMeanRequestRebase.identityViews_map {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (m : ℕ) (h Q : ℝ) (cover : ℕ) (hQ : 0 < Q) (hfrequency : B.base.frequency m ≠ 0) (n : ℕ) (x : Cylinder) : ((identityViews B m h Q cover hQ hfrequency).map n) x = x

@[simp]

theorem NavierStokes.TorusMeanRequestRebase.identityViews_velocity {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (m : ℕ) (h Q : ℝ) (cover : ℕ) (hQ : 0 < Q) (hfrequency : B.base.frequency m ≠ 0) (n : ℕ) : (identityViews B m h Q cover hQ hfrequency).velocity n = 1

The actual common state supplies the request of these native views

noncomputable def NavierStokes.TorusMeanRequestRebase.stateData {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (m : ℕ) (h Q : ℝ) (cover : ℕ) (hQ : 0 < Q) (hfrequency : B.base.frequency m ≠ 0) (hh : 0 < h) (hh1 : h < 1 / 2) (R : LocalSignedRequest.SlowRegion (2 * h)) (P : SignedStressPrimitive.Patch) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData R P.a P.b c u) (hp : GaugeMomentBalances.MovingField R P.a P.b u.pressure) (hslow : ∀ x ∈ B.strip.domain, (x.1.2.1.2, x.1.2.1.1) ∈ R.carrier) : (identityViews B m h Q cover hQ hfrequency).StateData

Both stored states and both contexts are the same frozen common objects. Only their dummy band index is changed. The native primary is left intact. Residual regularity and periodicity are derived from the primitive data.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.TorusMeanRequestRebase.stateData_request {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (m : ℕ) (h Q : ℝ) (cover : ℕ) (hQ : 0 < Q) (hfrequency : B.base.frequency m ≠ 0) (hh : 0 < h) (hh1 : h < 1 / 2) (R : LocalSignedRequest.SlowRegion (2 * h)) (P : SignedStressPrimitive.Patch) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData R P.a P.b c u) (hp : GaugeMomentBalances.MovingField R P.a P.b u.pressure) (hslow : ∀ x ∈ B.strip.domain, (x.1.2.1.2, x.1.2.1.1) ∈ R.carrier) (s : WeightedClasses.StripData Cylinder) (n : ℕ) (hepsilon : B.strip.epsilon n = s.epsilon m) (x : Cylinder) : (stateData B m h Q cover hQ hfrequency hh hh1 R P c u H hp hslow).request n x = PhysicalSignedWave.stateRequest s P h c u m x

theorem NavierStokes.TorusMeanRequestRebase.stateData_referenceRequest {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (m : ℕ) (h Q : ℝ) (cover : ℕ) (hQ : 0 < Q) (hfrequency : B.base.frequency m ≠ 0) (hh : 0 < h) (hh1 : h < 1 / 2) (R : LocalSignedRequest.SlowRegion (2 * h)) (P : SignedStressPrimitive.Patch) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData R P.a P.b c u) (hp : GaugeMomentBalances.MovingField R P.a P.b u.pressure) (hslow : ∀ x ∈ B.strip.domain, (x.1.2.1.2, x.1.2.1.1) ∈ R.carrier) (s : WeightedClasses.StripData Cylinder) (hepsilon : B.strip.epsilon m = s.epsilon m) (x : Cylinder) : (stateData B m h Q cover hQ hfrequency hh hh1 R P c u H hp hslow).referenceRequest m x = PhysicalSignedWave.stateRequest s P h c u m x

theorem NavierStokes.TorusMeanRequestRebase.stateData_referenceRequest_full {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (m : ℕ) (h Q : ℝ) (cover : ℕ) (hQ : 0 < Q) (hfrequency : B.base.frequency m ≠ 0) (hh : 0 < h) (hh1 : h < 1 / 2) (R : LocalSignedRequest.SlowRegion (2 * h)) (P : SignedStressPrimitive.Patch) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData R P.a P.b c u) (hp : GaugeMomentBalances.MovingField R P.a P.b u.pressure) (hslow : ∀ x ∈ B.strip.domain, (x.1.2.1.2, x.1.2.1.1) ∈ R.carrier) (s : WeightedClasses.StripData Point) (hepsilon : B.strip.epsilon m = s.epsilon m) (x : Cylinder) : (stateData B m h Q cover hQ hfrequency hh hh1 R P c u H hp hslow).referenceRequest m x = LocalSignedRequest.fullRequest s P (2 * h) c u m (PhysicalResidualTZ.swapCylinder x)

Exact binding to the original common-coordinate full signed request. The swap only puts the slow coordinates into their original (time,axial) order.

theorem NavierStokes.TorusMeanRequestRebase.stateData_referenceRequest_fast {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (m : ℕ) (h Q : ℝ) (cover : ℕ) (hQ : 0 < Q) (hfrequency : B.base.frequency m ≠ 0) (hh : 0 < h) (hh1 : h < 1 / 2) (R : LocalSignedRequest.SlowRegion (2 * h)) (P : SignedStressPrimitive.Patch) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData R P.a P.b c u) (hp : GaugeMomentBalances.MovingField R P.a P.b u.pressure) (hslow : ∀ x ∈ B.strip.domain, (x.1.2.1.2, x.1.2.1.1) ∈ R.carrier) (s : WeightedClasses.StripData Point) (hepsilon : B.strip.epsilon m = s.epsilon m) (mapFast : Plane → Plane) (x : Cylinder) : (stateData B m h Q cover hQ hfrequency hh hh1 R P c u H hp hslow).referenceRequest m x = LocalSignedRequest.fullRequest s P (2 * h) c u m (PhysicalResidualTZ.swapCylinder ((x.1.1, x.1.2.1, mapFast x.1.2.2), x.2))

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalBinding.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.ActualSignedPhysicalBinding.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalBinding.Cylinder : Type

Cylinder: an abbreviation for PhysicalSignedWave.Cylinder.

Equations

• NavierStokes.ActualSignedPhysicalBinding.Cylinder = NavierStokes.PhysicalSignedWave.Cylinder

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalBinding.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.ActualSignedPhysicalBinding.Slow = NavierStokes.PhaseCalculus.Slow

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalBinding.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.ActualSignedPhysicalBinding.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalBinding.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.ActualSignedPhysicalBinding.Space = NavierStokes.ProblemStatement.Space

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalBinding.Label (B N0 : ℕ) : Type

Label: an abbreviation for ActualSignedStageControls.SignedLabel B N0 open CorrectionInitialization CorrectionInitialization.ActualPrimary.

Equations

• NavierStokes.ActualSignedPhysicalBinding.Label B N0 = NavierStokes.ActualSignedStageControls.SignedLabel B N0

noncomputable def NavierStokes.ActualSignedPhysicalBinding.reference {B N0 : ℕ} (l : Label B N0) : ℕ

Reference, given by BaseChartJets.cellBand l.1.

Equations

• NavierStokes.ActualSignedPhysicalBinding.reference l = NavierStokes.BaseChartJets.cellBand l.1

noncomputable def NavierStokes.ActualSignedPhysicalBinding.domain {B N0 : ℕ} (l : Label B N0) : PhaseJetBounds.Domain ℕ Slow

Domain, given by ActualParticularStageControls.reindexDomain (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N) (fun _ => l.1).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.pulse {B N0 : ℕ} (l : Label B N0) (j : Fin 2) : PrimaryPulseBounds.PhaseConstruction (domain l)

Pulse, given by ActualParticularStageControls.reindexConstruction (phases B N0 j) (fun _ => l.1).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.pulse_frame {B N0 : ℕ} (l : Label B N0) (j : Fin 2) (n : ℕ) : (pulse l j).frame n = (CorrectionInitialization.ActualPrimary.phases B N0 j).frame l.1

noncomputable def NavierStokes.ActualSignedPhysicalBinding.spatialLabel {B N0 : ℕ} (l : Label B N0) : SlotColoring.Label

Spatial label, given by PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label nominal l.1) l.2.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.geometry {B N0 : ℕ} (l : Label B N0) : CommonCoverSolve.Geometry

Geometry, given by ActualSignedGeometry.slotGeometry slots vectors_det (spatialLabel l) 0.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.nativeClock {B N0 : ℕ} (l : Label B N0) (Y : Plane) : ℝ

Native clock, given by PeriodicPhaseAssembly.periodicClock (geometry l) (clockWindow l.1).cutoff Y.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.toCommon {B N0 : ℕ} (l : Label B N0) : Point ≃L[ℝ] Point

Native free coordinates mapped to the actual common reference lift.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.toCommonCylinder {B N0 : ℕ} (l : Label B N0) : Cylinder ≃L[ℝ] Cylinder

To common cylinder, given by PhysicalResidualTZ.swapCylinder.toContinuousLinearEquiv.trans ((toCommon l).prodCongr (ContinuousLinearEquiv.refl ℝ ℝ)).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.toCommon_apply {B N0 : ℕ} (l : Label B N0) (x : Point) : (toCommon l) x = (x.1, x.2.1, (CommonCoverSolve.coverPower (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (reference l) - CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (reference l))).symm x.2.2)

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.toCommonCylinder_apply {B N0 : ℕ} (l : Label B N0) (x : Cylinder) : (toCommonCylinder l) x = ((x.1.1, (x.1.2.1.2, x.1.2.1.1), (CommonCoverSolve.coverPower (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (reference l) - CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (reference l))).symm x.1.2.2), x.2)

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.toCommonCylinder_symm_apply {B N0 : ℕ} (l : Label B N0) (x : Cylinder) : (toCommonCylinder l).symm x = ((x.1.1, (x.1.2.1.2, x.1.2.1.1), (CommonCoverSolve.coverPower (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (reference l) - CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (reference l))) x.1.2.2), x.2)

noncomputable def NavierStokes.ActualSignedPhysicalBinding.strip {B N0 : ℕ} (l : Label B N0) : WeightedClasses.StripData Cylinder

Strip, constructed using freezeStrip.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.base {B N0 : ℕ} (l : Label B N0) : LinearWaveBounds.WaveCoefficients Cylinder

Base, given by freezeWave (ActualReferenceRebase.pullWave (toCommonCylinder l) (chartCoefficients l.2 l.1)) (reference l).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.directions {B N0 : ℕ} (l : Label B N0) : LinearWaveBounds.GraphDirections Cylinder

Directions, constructed using freezeDirections.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.primary {B N0 : ℕ} (l : Label B N0) : PhysicalSignedWave.PrimaryData (domain l)

Actual selected primary data. Only the dummy index is repeated.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.nativeViews {B N0 : ℕ} (l : Label B N0) : (primary l).Views (reference l)

All dummy bands describe this one native physical reference.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.nativeViews_map {B N0 : ℕ} (l : Label B N0) (n : ℕ) (x : Cylinder) : ((nativeViews l).map n) x = x

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.nativeViews_velocity {B N0 : ℕ} (l : Label B N0) (n : ℕ) : (nativeViews l).velocity n = 1

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.primary_frequency {B N0 : ℕ} (l : Label B N0) (n : ℕ) : (primary l).base.frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (reference l))

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.primary_epsilon {B N0 : ℕ} (l : Label B N0) (n : ℕ) : (primary l).strip.epsilon n = ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (reference l)

theorem NavierStokes.ActualSignedPhysicalBinding.primary_matrix {B N0 : ℕ} (l : Label B N0) (n : ℕ) (x : Cylinder) : (primary l).matrix n x = CorrectionInitialization.ActualPrimary.covariance B N0 l.1 (x.1.1, x.1.2.1)

theorem NavierStokes.ActualSignedPhysicalBinding.native_change_cancel {B N0 : ℕ} (l : Label B N0) (x : Cylinder) : (PhysicalParticularWave.cylinderChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q (reference l)) (ChartScales.Q (reference l)) (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (reference l) - CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (reference l))) (PhysicalResidualTZ.swapCylinder ((toCommonCylinder l) x)) = x

theorem NavierStokes.ActualSignedPhysicalBinding.primary_phase {B N0 : ℕ} (l : Label B N0) (n : ℕ) : (primary l).base.phase n = ActualSignedGeometry.periodicPhase CorrectionInitialization.ActualPrimary.slots (spatialLabel l) 0 (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (reference l)) ((pulse l l.2).phase.p (reference l)) ((pulse l l.2).phase.pz (reference l)) ((pulse l l.2).phase.x0 (reference l)) ((pulse l l.2).phase.F (reference l)) ((pulse l l.2).phase.G (reference l))

theorem NavierStokes.ActualSignedPhysicalBinding.primary_domain {B N0 : ℕ} (l : Label B N0) (x : Cylinder) : x ∈ (primary l).strip.domain ↔ PhysicalResidualTZ.swapSlow x.1 ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain

The native record retains the exact annular domain; it is not an empty or shrinking domain chosen to make the reference data vacuous.

theorem NavierStokes.ActualSignedPhysicalBinding.primary_time_pos {B N0 : ℕ} (l : Label B N0) {x : Cylinder} (hx : x ∈ (primary l).strip.domain) : 0 < x.1.2.1.2

theorem NavierStokes.ActualSignedPhysicalBinding.primary_slow_mem {B N0 : ℕ} (l : Label B N0) {x : Cylinder} (hx : x ∈ (primary l).strip.domain) : (x.1.2.1.2, x.1.2.1.1) ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier

theorem NavierStokes.ActualSignedPhysicalBinding.primary_radial {B N0 : ℕ} (l : Label B N0) (n : ℕ) : (primary l).directions.radialField n = (PhysicalResidualBridge.commonGraph (ChartScales.Q (reference l)) CorrectionInitialization.ActualPrimary.h (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (reference l))).radial

theorem NavierStokes.ActualSignedPhysicalBinding.primary_angular {B N0 : ℕ} (l : Label B N0) : (primary l).directions.angular = (0, 1)

theorem NavierStokes.ActualSignedPhysicalBinding.primary_axial {B N0 : ℕ} (l : Label B N0) (n : ℕ) : (primary l).directions.axialField (primary l).strip n = (PhysicalResidualBridge.commonGraph (ChartScales.Q (reference l)) CorrectionInitialization.ActualPrimary.h (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (reference l))).axial

theorem NavierStokes.ActualSignedPhysicalBinding.primary_chart {B N0 : ℕ} (l : Label B N0) (n : ℕ) : PhysicalSignedWave.ChartGeometry (primary l).base (primary l).strip (primary l).directions n CorrectionInitialization.ActualPrimary.h (ChartScales.Q (reference l)) (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (reference l))

noncomputable def NavierStokes.ActualSignedPhysicalBinding.nativeStateData {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : (nativeViews l).StateData

The actual current common state supplies the torus-mean request. The primitive hypotheses concern only the real local incoming fields.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualSignedPhysicalBinding.nativeStateData_referenceRequest {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (x : Cylinder) : (nativeStateData l P u H hp).referenceRequest (reference l) x = LocalSignedRequest.fullRequest (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) P (2 * CorrectionInitialization.ActualPrimary.h) (CorrectionInitialization.ActualPrimary.commonContext B) u (reference l) ((toCommonCylinder l) x)

theorem NavierStokes.ActualSignedPhysicalBinding.primary_phase_affine {B N0 : ℕ} (l : Label B N0) (n : ℕ) : CopyAngularInvariance.AffinePhase (0, 1) (↑(PrimaryGeometryAssembly.angularMode CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared l.2 l.1) / (primary l).base.frequency n) ((primary l).base.phase n)

noncomputable def NavierStokes.ActualSignedPhysicalBinding.primaryAngular {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : (primary l).Angular (nativeStateData l P u H hp).referenceRequest (reference l)

Primary angular, bundling mode, phase, coordinate, target and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.

The same individual native copy as the frozen signed stage.

theorem NavierStokes.ActualSignedPhysicalBinding.label_large {B N0 : ℕ} (l : Label B N0) : 4 ≤ (spatialLabel l).1

noncomputable def NavierStokes.ActualSignedPhysicalBinding.layout {B N0 : ℕ} (l : Label B N0) : ActualPeriodizedSignedRealization.Layout

Layout, given by ActualSignedPhysicalData.layout slots outgoing.data.h_pos.le (spatialLabel l) (label_large l) 0.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.layout_geometry {B N0 : ℕ} (l : Label B N0) (n : ℕ) : (layout l).geometry n = geometry l

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.layout_window {B N0 : ℕ} (l : Label B N0) (n : ℕ) : (layout l).window n = CorrectionInitialization.ActualPrimary.clockWindow l.1

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.pulse_length {B N0 : ℕ} (l : Label B N0) (j : Fin 2) (n : ℕ) : (pulse l j).L n = ChartScales.slotLength CorrectionInitialization.ActualPrimary.slots.radius CorrectionInitialization.ActualPrimary.h (reference l)

noncomputable def NavierStokes.ActualSignedPhysicalBinding.nativeCopyPoint {B N0 : ℕ} (l : Label B N0) (k : TorusInverse.Frequency) (x : Cylinder) : ActualSignedGeometry.Native

Native copy point, given by ((x.1.1, x.1.2.1), (geometry l).coordinates k x.1.2.2).

Equations

• NavierStokes.ActualSignedPhysicalBinding.nativeCopyPoint l k x = ((x.1.1, x.1.2.1), (NavierStokes.ActualSignedPhysicalBinding.geometry l).coordinates k x.1.2.2)

theorem NavierStokes.ActualSignedPhysicalBinding.nativePoint_reference {B N0 : ℕ} (l : Label B N0) (k : TorusInverse.Frequency) (x : Cylinder) : ActualSignedStageControls.nativePoint l (reference l) k ((toCommonCylinder l) x) = nativeCopyPoint l k x

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.signed_coefficientScale_reference {B N0 : ℕ} (l : Label B N0) : ActualSignedStageControls.coefficientScale l (reference l) = 1

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.signed_clockScale_reference {B N0 : ℕ} (l : Label B N0) : ActualSignedStageControls.clockScale l (reference l) = 1

@[simp]

theorem NavierStokes.ActualSignedPhysicalBinding.signed_normalScale_reference {B N0 : ℕ} (l : Label B N0) : ActualSignedStageControls.normalScale l (reference l) = 1

theorem NavierStokes.ActualSignedPhysicalBinding.signed_matrix_reference {B N0 : ℕ} (l : Label B N0) (k : TorusInverse.Frequency) (x : Cylinder) : ActualSignedStageControls.matrix l k (reference l) ((toCommonCylinder l) x) = (primary l).matrix (reference l) x

theorem NavierStokes.ActualSignedPhysicalBinding.signed_target_reference {B N0 : ℕ} (l : Label B N0) (k : TorusInverse.Frequency) (x : Cylinder) : ActualSignedStageControls.target l k (reference l) ((toCommonCylinder l) x) = (primary l).target (reference l) x

theorem NavierStokes.ActualSignedPhysicalBinding.signed_mask_reference {B N0 : ℕ} (l : Label B N0) (k : TorusInverse.Frequency) (x : Cylinder) : ActualSignedStageControls.mask l k (reference l) ((toCommonCylinder l) x) = (primary l).mask (reference l) x

theorem NavierStokes.ActualSignedPhysicalBinding.signed_unit_reference {B N0 : ℕ} (l : Label B N0) (k : TorusInverse.Frequency) (x : Cylinder) : ActualSignedStageControls.fundamental l k (reference l) ((toCommonCylinder l) x) = ActualPeriodizedSignedRealization.nativeUnit (primary l) (layout l) (nativeViews l) l.2 k (reference l) x

theorem NavierStokes.ActualSignedPhysicalBinding.signed_cutoff_reference {B N0 : ℕ} (l : Label B N0) (k : TorusInverse.Frequency) (x : Cylinder) : ActualSignedStageControls.cutoff l k (reference l) ((toCommonCylinder l) x) = PartitionedCovariance.cutoff CorrectionInitialization.ActualPrimary.slots.radius ((geometry l).coordinates k x.1.2.2).1 * (layout l).nativeGaussian (reference l) k x.1.2.2

theorem NavierStokes.ActualSignedPhysicalBinding.nativeClock_on_core {B N0 : ℕ} (l : Label B N0) (k : TorusInverse.Frequency) {x : Cylinder} (hx : (geometry l).coordinates k x.1.2.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.1).core) : nativeClock l x.1.2.2 = ((geometry l).coordinates k x.1.2.2).2

theorem NavierStokes.ActualSignedPhysicalBinding.signed_normalMotion_reference {B N0 : ℕ} (l : Label B N0) (k : TorusInverse.Frequency) {x : Cylinder} (hx : (geometry l).coordinates k x.1.2.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.1).core) : ActualSignedStageControls.normalMotion l k (reference l) ((toCommonCylinder l) x) = (primary l).normalMotion (reference l) x

theorem NavierStokes.ActualSignedPhysicalBinding.signed_action_reference {B N0 : ℕ} (l : Label B N0) (k : TorusInverse.Frequency) {x : Cylinder} (hx : (geometry l).coordinates k x.1.2.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.1).core) : ActualSignedStageControls.action l k (reference l) ((toCommonCylinder l) x) = (primary l).action (reference l) x

theorem NavierStokes.ActualSignedPhysicalBinding.carrier_midpoint {B N0 : ℕ} (l : Label B N0) (k : TorusInverse.Frequency) : ActualSignedPhysicalData.center (spatialLabel l) k = (geometry l).center + TorusAverages.latticePoint k + CorrectionInitialization.ActualPrimary.slots.radius • ActualSignedGeometry.temporalVector

The lower endpoint is the integration anchor; the physical carrier retains the individual copy midpoint.

theorem NavierStokes.ActualSignedPhysicalBinding.primary_radial_pull {B N0 : ℕ} (l : Label B N0) (n : ℕ) (x : Cylinder) : (primary l).directions.radialField n x = (toCommonCylinder l).symm ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField (reference l) ((toCommonCylinder l) x))

theorem NavierStokes.ActualSignedPhysicalBinding.primary_axial_pull {B N0 : ℕ} (l : Label B N0) (n : ℕ) (x : Cylinder) : (primary l).directions.axialField (primary l).strip n x = (toCommonCylinder l).symm ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).axialField (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion)) (reference l) ((toCommonCylinder l) x))

theorem NavierStokes.ActualSignedPhysicalBinding.primary_normal_reference {B N0 : ℕ} (l : Label B N0) (n : ℕ) (x : Cylinder) : (primary l).base.normal (primary l).strip (primary l).directions n x = (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).normal (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion)) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)) (reference l) ((toCommonCylinder l) x)

Actual Fréchet derivatives transform with the native frame; no smoothness of the raw phase outside its active domain is postulated.

theorem NavierStokes.ActualSignedPhysicalBinding.nativeView_base {B N0 : ℕ} (l : Label B N0) : (ActualPeriodizedSignedRealization.periodizedPrimary (primary l) (layout l)).viewBase (nativeViews l).background (nativeViews l).frequency (fun (n : ℕ) => ⇑((nativeViews l).map n)) (reference l) = (primary l).base

theorem NavierStokes.ActualSignedPhysicalBinding.nativeViews_clock {B N0 : ℕ} (l : Label B N0) (n : ℕ) : (nativeViews l).clock n = 1

theorem NavierStokes.ActualSignedPhysicalBinding.nativeViews_normal {B N0 : ℕ} (l : Label B N0) (n : ℕ) : (nativeViews l).normal n = 1

theorem NavierStokes.ActualSignedPhysicalBinding.nativeView_target {B N0 : ℕ} (l : Label B N0) : (ActualPeriodizedSignedRealization.periodizedPrimary (primary l) (layout l)).viewTarget (nativeViews l).strip (nativeViews l).velocity (fun (n : ℕ) => ⇑((nativeViews l).map n)) (reference l) = (primary l).target

noncomputable def NavierStokes.ActualSignedPhysicalBinding.nativeCoefficients {B N0 : ℕ} (l : Label B N0) (R : ℕ → Cylinder → SignedWaveUpdate.Vec2) (k : TorusInverse.Frequency) : LinearWaveBounds.WaveCoefficients Cylinder

Native coefficients, constructed using SignedWaveUpdate.coefficients.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.nativeRequest {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) : ℕ → Cylinder → SignedWaveUpdate.Vec2

The scalar and the reference copy family are definable before proving their regularity. No proof or independently chosen request is stored.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.nativeCopies {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) : PeriodizedWaveBounds.CopyData Cylinder TorusInverse.Frequency

Native copies, constructed using ActualSignedPhysicalData.dynamicCopyData.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualSignedPhysicalBinding.nativeStateData_request_eq {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : (nativeStateData l P u H hp).referenceRequest = nativeRequest l P u

theorem NavierStokes.ActualSignedPhysicalBinding.dynamicCoefficients_eq {B N0 : ℕ} (l : Label B N0) (R : ℕ → Cylinder → SignedWaveUpdate.Vec2) (k : TorusInverse.Frequency) : ActualSignedPhysicalData.dynamicCoefficients CorrectionInitialization.ActualPrimary.slots ⋯ (spatialLabel l) ⋯ 0 (primary l) (nativeViews l) R l.2 k = nativeCoefficients l R k

noncomputable def NavierStokes.ActualSignedPhysicalBinding.referenceCopies {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : PeriodizedWaveBounds.CopyData Cylinder TorusInverse.Frequency

Reference copies, constructed using ActualSignedPhysicalData.dynamicCopyData.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.commonCopies {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) : PeriodizedWaveBounds.CopyData Cylinder TorusInverse.Frequency

Common copies as an element of PeriodizedWaveBounds.CopyData Cylinder TorusInverse.Frequency.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualSignedPhysicalBinding.signedVector_reference {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (k : TorusInverse.Frequency) (x : Cylinder) : SignedWaveUpdate.signedVector (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion)) (ActualSignedStageControls.matrix l k) (ActualSignedStageControls.target l k) (LocalSignedRequest.fullRequest (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) P (2 * CorrectionInitialization.ActualPrimary.h) (CorrectionInitialization.ActualPrimary.commonContext B) u) (ActualSignedStageControls.mask l k) (ActualSignedStageControls.fundamental l k) l.2 (reference l) ((toCommonCylinder l) x) = SignedWaveUpdate.signedVector (primary l).strip (primary l).matrix (primary l).target (nativeStateData l P u H hp).referenceRequest (primary l).mask (ActualPeriodizedSignedRealization.nativeUnit (primary l) (layout l) (nativeViews l) l.2 k) l.2 (reference l) x

theorem NavierStokes.ActualSignedPhysicalBinding.raw_amplitude_reference {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (k : TorusInverse.Frequency) (x : Cylinder) : (commonCopies l P u).amplitude (reference l) k ((toCommonCylinder l) x) = (referenceCopies l P u H hp).amplitude (reference l) k x

theorem NavierStokes.ActualSignedPhysicalBinding.raw_pressure_reference {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (k : TorusInverse.Frequency) {x : Cylinder} (hx : (geometry l).coordinates k x.1.2.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.1).core) : (commonCopies l P u).pressure (reference l) k ((toCommonCylinder l) x) = (referenceCopies l P u H hp).pressure (reference l) k x

theorem NavierStokes.ActualSignedPhysicalBinding.cutoff_reference {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (k : TorusInverse.Frequency) (x : Cylinder) : (commonCopies l P u).cutoff (reference l) k ((toCommonCylinder l) x) = (referenceCopies l P u H hp).cutoff (reference l) k x

theorem NavierStokes.ActualSignedPhysicalBinding.reference_cutoff_core {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (k : TorusInverse.Frequency) {x : Cylinder} (hx : (referenceCopies l P u H hp).cutoff (reference l) k x ≠ 0) : (geometry l).coordinates k x.1.2.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.1).core

theorem NavierStokes.ActualSignedPhysicalBinding.localized_amplitude_reference {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (k : TorusInverse.Frequency) (x : Cylinder) : ((commonCopies l P u).localized k).amplitude (reference l) ((toCommonCylinder l) x) = ((referenceCopies l P u H hp).localized k).amplitude (reference l) x

theorem NavierStokes.ActualSignedPhysicalBinding.localized_pressure_reference {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (k : TorusInverse.Frequency) (x : Cylinder) : ((commonCopies l P u).localized k).pressure (reference l) ((toCommonCylinder l) x) = ((referenceCopies l P u H hp).localized k).pressure (reference l) x

theorem NavierStokes.ActualSignedPhysicalBinding.referenceCopies_eq_nativeCopies {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : referenceCopies l P u H hp = nativeCopies l P u

theorem NavierStokes.ActualSignedPhysicalBinding.referenceCopies_localized {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (k : TorusInverse.Frequency) : (referenceCopies l P u H hp).localized k = (ActualPeriodizedSignedRealization.copyData (primary l) (layout l) (nativeViews l) (nativeStateData l P u H hp).referenceRequest l.2).localized k

Exact cutoff repartition into the existing compact periodized family.

theorem NavierStokes.ActualSignedPhysicalBinding.common_amplitude_reference {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (x : Cylinder) : (commonCopies l P u).common.amplitude (reference l) ((toCommonCylinder l) x) = (referenceCopies l P u H hp).common.amplitude (reference l) x

theorem NavierStokes.ActualSignedPhysicalBinding.common_pressure_reference {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (x : Cylinder) : (commonCopies l P u).common.pressure (reference l) ((toCommonCylinder l) x) = (referenceCopies l P u H hp).common.pressure (reference l) x

theorem NavierStokes.ActualSignedPhysicalBinding.reference_background {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : (referenceCopies l P u H hp).background = (primary l).base

theorem NavierStokes.ActualSignedPhysicalBinding.reference_common_normal {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : (referenceCopies l P u H hp).common.normal (primary l).strip (primary l).directions (reference l) = (primary l).base.normal (primary l).strip (primary l).directions (reference l)

theorem NavierStokes.ActualSignedPhysicalBinding.curlCoefficient_reference {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (x : Cylinder) : CurlClassBounds.inverseCarrier ((referenceCopies l P u H hp).common.frequency (reference l)) • CurlClassBounds.coefficient ((referenceCopies l P u H hp).common.radius (reference l)) ((primary l).directions.radialField (reference l)) (fun (x : Cylinder) => (primary l).directions.angular) ((primary l).directions.axialField (primary l).strip (reference l)) ((referenceCopies l P u H hp).common.phase (reference l)) ((referenceCopies l P u H hp).common.amplitude (reference l)) x = CurlClassBounds.inverseCarrier ((commonCopies l P u).common.frequency (reference l)) • CurlClassBounds.coefficient ((commonCopies l P u).common.radius (reference l)) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField (reference l)) (fun (x : Cylinder) => (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).angular) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).axialField (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion)) (reference l)) ((commonCopies l P u).common.phase (reference l)) ((commonCopies l P u).common.amplitude (reference l)) ((toCommonCylinder l) x)

theorem NavierStokes.ActualSignedPhysicalBinding.reference_phase {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (x : Cylinder) : (referenceCopies l P u H hp).common.phase (reference l) x = (commonCopies l P u).common.phase (reference l) ((toCommonCylinder l) x)

theorem NavierStokes.ActualSignedPhysicalBinding.curlPotential_reference {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (x : Cylinder) : (referenceCopies l P u H hp).common.curlPotential (primary l).strip (primary l).directions (reference l) x = (commonCopies l P u).common.curlPotential (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion)) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)) (reference l) ((toCommonCylinder l) x)

The complete oscillatory curl potential, including its carrier, is the same native reference.

theorem NavierStokes.ActualSignedPhysicalBinding.reference_exactCoefficients {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : (referenceCopies l P u H hp).commonCorrected (primary l).strip (primary l).directions = (ActualPeriodizedSignedRealization.views (primary l) (layout l) (nativeViews l)).exactCoefficients (nativeStateData l P u H hp).referenceRequest l.2

Bind to the literal request after the actual particular update.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.afterParticular {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) : CorrectionState.State Point

After particular, given by (ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (commonContext B) x.state.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualSignedPhysicalBinding.cycleStateData {B N0 : ℕ} (l : Label B N0) (x : CorrectionStep.CycleState (Label B N0)) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) (afterParticular x)) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (afterParticular x).pressure) : (nativeViews l).StateData

Cycle state data, given by nativeStateData l ActualInitialization.patch (afterParticular x) H hp.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualSignedPhysicalBinding.afterParticular_pressure {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) (afterParticular x)) : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (afterParticular x).pressure

noncomputable def NavierStokes.ActualSignedPhysicalBinding.cycleStateDataOfPrimitive {B N0 : ℕ} (l : Label B N0) (x : CorrectionStep.CycleState (Label B N0)) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) (afterParticular x)) : (nativeViews l).StateData

Cycle state data of primitive, given by cycleStateData l x H (afterParticular_pressure x H).

Equations

• NavierStokes.ActualSignedPhysicalBinding.cycleStateDataOfPrimitive l x H = NavierStokes.ActualSignedPhysicalBinding.cycleStateData l x H ⋯

theorem NavierStokes.ActualSignedPhysicalBinding.cycleStateData_request {B N0 : ℕ} (l : Label B N0) (x : CorrectionStep.CycleState (Label B N0)) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) (afterParticular x)) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (afterParticular x).pressure) (z : Cylinder) : (cycleStateData l x H hp).referenceRequest (reference l) z = (ActualCycleParameters.fixedParameters B N0).signedRequest x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state (reference l) ((toCommonCylinder l) z)