Literal cycle parameters on the initialized labels

The current cycle uses the same primary choice, moving strip, pressure gauge, index and rank patch as its initialization. The particular solver orders the sign before the spatial label; initialization and the signed solver order it after the spatial label. The equivalence below transports the actual finite coefficient family, rather than choosing new labels.

This module constructs the parameters and proves their data identities. It does not assume or assert the analytic preservation of a correction cycle.

The actual fixed geometry for every correction cycle

The numerical data, strip, gauge, and operators below are the ones used by ActualInitialization. In particular, compatibility with the excluded-alias estimates is proved independently of the particular and signed wave choices.

@[reducible, inline]

abbrev NavierStokes.ActualCycleGeometry.Point : Type

Point: an abbreviation for ActualInitialization.Point.

Equations

• NavierStokes.ActualCycleGeometry.Point = NavierStokes.ActualInitialization.Point

noncomputable def NavierStokes.ActualCycleGeometry.similarityData : ActualCycleExcluded.SimilarityData

Initialization supplies all numerical hypotheses of the similarity estimates, including the actual finite-window common index.

Equations

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

theorem NavierStokes.ActualCycleGeometry.strip_eq : similarityData.strip = ActualInitialization.strip

theorem NavierStokes.ActualCycleGeometry.strip_eq_geometry : similarityData.strip = ActualInitialization.geometry.strip

theorem NavierStokes.ActualCycleGeometry.gauge_eq : similarityData.gauge = CorrectionInitialization.ActualPrimary.commonGauge

The normalization factor is exactly one, so the similarity gauge agrees with the common reconstruction used by initialization.

theorem NavierStokes.ActualCycleGeometry.gauge_eq_geometry : similarityData.gauge = ActualInitialization.geometry.gauge

theorem NavierStokes.ActualCycleGeometry.region_eq : similarityData.region = ActualInitialization.geometry.region

theorem NavierStokes.ActualCycleGeometry.inner_eq : similarityData.inner = ActualInitialization.geometry.patch.a

theorem NavierStokes.ActualCycleGeometry.outer_eq : similarityData.outer = ActualInitialization.geometry.patch.b

theorem NavierStokes.ActualCycleGeometry.index_eq : similarityData.index = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h

theorem NavierStokes.ActualCycleGeometry.index_bounds : CommonBaseContext.IndexBounds similarityData.h similarityData.index similarityData.gap

theorem NavierStokes.ActualCycleGeometry.slow_eq : similarityData.slow = BaseContextAssembly.slowScale

theorem NavierStokes.ActualCycleGeometry.epsilon_eq : similarityData.strip.epsilon = ChartScales.epsilon CorrectionInitialization.ActualPrimary.h

theorem NavierStokes.ActualCycleGeometry.fast_eq (B : ℕ) : (CorrectionInitialization.ActualPrimary.commonContext B).operators.fastCoefficient = fun (n : ℕ) => ChartScales.Tg ^ similarityData.index n * ChartScales.Q n ^ (1 + similarityData.h)

theorem NavierStokes.ActualCycleGeometry.temporal_eq (B : ℕ) : (CorrectionInitialization.ActualPrimary.commonContext B).operators.vT = (0, 0, TorusInverse.vector TorusInverse.Direction.temporal)

theorem NavierStokes.ActualCycleGeometry.compatible {ι : Type} (B : ℕ) (particular : ι → CorrectionStep.ParticularParameters CorrectionStep.CycleSlow) (signed : ι → CorrectionStep.PeriodizedSignedParameters CorrectionStep.CyclePoint TorusInverse.Frequency) : ActualCycleExcluded.Compatible similarityData (CorrectionStep.CycleParameters.ofGeometry ActualInitialization.geometry CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h) ActualInitialization.axial particular signed CorrectionInitialization.ActualPrimary.rankData) (CorrectionInitialization.ActualPrimary.commonContext B)

Changing either wave family leaves the entire similarity certificate unchanged. The rank stage is the actual reserved rank construction.

theorem NavierStokes.ActualCycleGeometry.operators (B : ℕ) : MeanIncrementBounds.OperatorBounds similarityData.strip (CorrectionInitialization.ActualPrimary.commonContext B).operators ChartScales.kappa

The actual operator bounds on precisely the strip in the certificate.

theorem NavierStokes.ActualCycleGeometry.base_bounds (B : ℕ) : MeanIncrementBounds.BaseBounds similarityData.strip (CorrectionInitialization.ActualPrimary.commonContext B).base

These bounds concern the actual same-profile base in the common context.

theorem NavierStokes.ActualCycleGeometry.radius_pos (B : ℕ) (x : Point) (hx : x ∈ similarityData.strip.domain) : 0 < (CorrectionInitialization.ActualPrimary.commonContext B).operators.radius x

theorem NavierStokes.ActualCycleGeometry.strip_time (x : Point) (hx : x ∈ similarityData.strip.domain) : 0 < x.2.1.1

Exact transport of the stored coefficient family

noncomputable def NavierStokes.ActualCycleParameters.reindexCoefficients {ι κ : Type} (e : κ ≃ ι) (v : CorrectionStep.CycleCoefficients ι) : CorrectionStep.CycleCoefficients κ

Reindex coefficients, bundling labels, blocks, gaussian, aliasCoefficients and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualCycleParameters.reindexState {ι κ : Type} (e : κ ≃ ι) (x : CorrectionStep.CycleState ι) : CorrectionStep.CycleState κ

Reindex state, bundling state, coefficients, axisymmetricAlias.

Equations

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

noncomputable def NavierStokes.ActualCycleParameters.reindexParameters {ι κ : Type} (e : κ ≃ ι) (p : CorrectionStep.CycleParameters ι) : CorrectionStep.CycleParameters κ

Reindex parameters, bundling gauge, strip, patch, coordinate and the required compatibility proofs.

Equations

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

@[simp]

theorem NavierStokes.ActualCycleParameters.reindexCoefficients_mem {ι κ : Type} (e : κ ≃ ι) (v : CorrectionStep.CycleCoefficients ι) (n : ℕ) (l : κ) : l ∈ (reindexCoefficients e v).labels n ↔ e l ∈ v.labels n

@[simp]

theorem NavierStokes.ActualCycleParameters.reindexState_state {ι κ : Type} (e : κ ≃ ι) (x : CorrectionStep.CycleState ι) : (reindexState e x).state = x.state

@[simp]

theorem NavierStokes.ActualCycleParameters.reindexState_axis {ι κ : Type} (e : κ ≃ ι) (x : CorrectionStep.CycleState ι) : (reindexState e x).axisymmetricAlias = x.axisymmetricAlias

@[simp]

theorem NavierStokes.ActualCycleParameters.reindexState_band {ι κ : Type} (e : κ ≃ ι) (x : CorrectionStep.CycleState ι) : (reindexState e x).coefficients.residualBand = x.coefficients.residualBand

theorem NavierStokes.ActualCycleParameters.reindexCoefficients_symm {ι κ : Type} (e : κ ≃ ι) (v : CorrectionStep.CycleCoefficients ι) : reindexCoefficients e.symm (reindexCoefficients e v) = v

theorem NavierStokes.ActualCycleParameters.reindexState_symm {ι κ : Type} (e : κ ≃ ι) (x : CorrectionStep.CycleState ι) : reindexState e.symm (reindexState e x) = x

theorem NavierStokes.ActualCycleParameters.reindexCoefficients_sum {ι κ : Type} (e : κ ≃ ι) (v : CorrectionStep.CycleCoefficients ι) {E : Type u_1} [AddCommMonoid E] (n : ℕ) (f : ι → E) : ∑ l ∈ (reindexCoefficients e v).labels n, f (e l) = ∑ l ∈ v.labels n, f l

theorem NavierStokes.ActualCycleParameters.reindexState_representation {ι κ : Type} (e : κ ≃ ι) (x : CorrectionStep.CycleState ι) (H : CorrectionStep.CycleRepresentation x.coefficients x.state x.axisymmetricAlias) : CorrectionStep.CycleRepresentation (reindexState e x).coefficients (reindexState e x).state (reindexState e x).axisymmetricAlias

theorem NavierStokes.ActualCycleParameters.reindexState_bands {ι κ : Type} (e : κ ≃ ι) (x : CorrectionStep.CycleState ι) (H : CorrectionStep.CoefficientBands x.coefficients) : CorrectionStep.CoefficientBands (reindexState e x).coefficients

The two label orders describe the same primary choice

@[reducible, inline]

abbrev NavierStokes.ActualCycleParameters.Index (B N0 : ℕ) : Type

Index: an abbreviation for ActualInitialization.Index B N0.

Equations

• NavierStokes.ActualCycleParameters.Index B N0 = NavierStokes.ActualInitialization.Index B N0

@[reducible, inline]

abbrev NavierStokes.ActualCycleParameters.ParticularIndex (B N0 : ℕ) : Type

Particular index: an abbreviation for ActualParticularStageControls.Label B N0.

Equations

• NavierStokes.ActualCycleParameters.ParticularIndex B N0 = NavierStokes.ActualParticularStageControls.Label B N0

noncomputable def NavierStokes.ActualCycleParameters.swap (B N0 : ℕ) : Index B N0 ≃ ParticularIndex B N0

Swap, given by Equiv.prodComm _ _.

Equations

• NavierStokes.ActualCycleParameters.swap B N0 = Equiv.prodComm (NavierStokes.CorrectionInitialization.ActualPrimary.Label B N0) (Fin 2)

@[simp]

theorem NavierStokes.ActualCycleParameters.swap_apply {B N0 : ℕ} (l : Index B N0) : (swap B N0) l = (l.2, l.1)

@[simp]

theorem NavierStokes.ActualCycleParameters.swap_symm_apply {B N0 : ℕ} (l : ParticularIndex B N0) : (swap B N0).symm l = (l.2, l.1)

noncomputable def NavierStokes.ActualCycleParameters.particularState {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : CorrectionStep.CycleState (ParticularIndex B N0)

Particular state, given by reindexState (swap B N0).symm x.

Equations

• NavierStokes.ActualCycleParameters.particularState x = NavierStokes.ActualCycleParameters.reindexState (NavierStokes.ActualCycleParameters.swap B N0).symm x

@[simp]

theorem NavierStokes.ActualCycleParameters.particularState_state {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : (particularState x).state = x.state

theorem NavierStokes.ActualCycleParameters.particularState_blocks {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : (particularState x).coefficients.blocks ((swap B N0) l) = x.coefficients.blocks l

theorem NavierStokes.ActualCycleParameters.particularState_gaussian {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : (particularState x).coefficients.gaussian ((swap B N0) l) = x.coefficients.gaussian l

theorem NavierStokes.ActualCycleParameters.particularState_alias {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : (particularState x).coefficients.aliasCoefficients ((swap B N0) l) = x.coefficients.aliasCoefficients l

theorem NavierStokes.ActualCycleParameters.particularState_mem {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (n : ℕ) (l : Index B N0) : (swap B N0) l ∈ (particularState x).coefficients.labels n ↔ l ∈ x.coefficients.labels n

theorem NavierStokes.ActualCycleParameters.particularState_roundtrip {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : reindexState (swap B N0) (particularState x) = x

The actual four-stage parameter constructor

noncomputable def NavierStokes.ActualCycleParameters.parameters {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : CorrectionStep.CycleParameters (Index B N0)

Parameters, constructed using CycleParameters.ofGeometry.

Equations

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

noncomputable def NavierStokes.ActualCycleParameters.parametersInParticularOrder {B N0 : ℕ} (x : CorrectionStep.CycleState (ParticularIndex B N0)) : CorrectionStep.CycleParameters (ParticularIndex B N0)

The same literal builder expressed in the particular solver's label order. This has no additional geometric or analytic choices.

Equations

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

theorem NavierStokes.ActualCycleParameters.parameters_swap {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : reindexParameters (swap B N0).symm (parameters x) = parametersInParticularOrder (particularState x)

@[simp]

theorem NavierStokes.ActualCycleParameters.parameters_gauge {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : (parameters x).gauge = CorrectionInitialization.ActualPrimary.commonGauge

@[simp]

theorem NavierStokes.ActualCycleParameters.parameters_strip {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : (parameters x).strip = ActualInitialization.strip

@[simp]

theorem NavierStokes.ActualCycleParameters.parameters_patch {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : (parameters x).patch = ActualInitialization.patch

@[simp]

theorem NavierStokes.ActualCycleParameters.parameters_coordinate {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : (parameters x).coordinate = 2 * CorrectionInitialization.ActualPrimary.h

@[simp]

theorem NavierStokes.ActualCycleParameters.parameters_timeExponent {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : (parameters x).timeExponent = CorrectionInitialization.ActualPrimary.h

@[simp]

theorem NavierStokes.ActualCycleParameters.parameters_commonIndex {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : (parameters x).commonIndex = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h

@[simp]

theorem NavierStokes.ActualCycleParameters.parameters_axial {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : (parameters x).axial = ActualInitialization.axial

@[simp]

theorem NavierStokes.ActualCycleParameters.parameters_rank {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : (parameters x).rank = CorrectionInitialization.ActualPrimary.rankData

@[simp]

theorem NavierStokes.ActualCycleParameters.parameters_particular {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : (parameters x).particular l = ActualParticularStageControls.parameters (particularState x) ((swap B N0) l)

@[simp]

theorem NavierStokes.ActualCycleParameters.parameters_signed {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : (parameters x).signed l = ActualSignedStageControls.parameters l

theorem NavierStokes.ActualCycleParameters.parameters_indexBounds {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : CommonBaseContext.IndexBounds CorrectionInitialization.ActualPrimary.h (parameters x).commonIndex (CorrectionInitialization.CommonWindow.gap CorrectionInitialization.ActualPrimary.h)

theorem NavierStokes.ActualCycleParameters.parameters_geometry_operators {B N0 : ℕ} (_x : CorrectionStep.CycleState (Index B N0)) : ActualInitialization.geometry.operators = (CorrectionInitialization.ActualPrimary.commonContext B).operators

theorem NavierStokes.ActualCycleParameters.parameters_compatible {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : ActualCycleExcluded.Compatible ActualCycleGeometry.similarityData (parameters x) (CorrectionInitialization.ActualPrimary.commonContext B)

noncomputable def NavierStokes.ActualCycleParameters.bandFloor (B N0 : ℕ) : ℕ

The physical band floor belongs to the already selected primary choice and does not change with the current correction state.

Equations

• NavierStokes.ActualCycleParameters.bandFloor B N0 = (NavierStokes.CorrectionInitialization.ActualPrimary.choice B N0).prepared.N

noncomputable def NavierStokes.ActualCycleParameters.sourceBand {B N0 : ℕ} (l : Index B N0) : ℕ

Source band, given by BaseChartJets.cellBand l.1.

Equations

• NavierStokes.ActualCycleParameters.sourceBand l = NavierStokes.BaseChartJets.cellBand l.1

theorem NavierStokes.ActualCycleParameters.bandFloor_ge (B N0 : ℕ) : N0 ≤ bandFloor B N0

theorem NavierStokes.ActualCycleParameters.sourceBand_ge_floor {B N0 : ℕ} (l : Index B N0) : bandFloor B N0 ≤ sourceBand l

theorem NavierStokes.ActualCycleParameters.particular_reference_band {B N0 : ℕ} (l : Index B N0) : (ActualParticularStageControls.reference ((swap B N0) l)).band = sourceBand l

theorem NavierStokes.ActualCycleParameters.particular_gap {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ActualParticularStageControls.gap ((swap B N0) l) n = ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (sourceBand l) - CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n

theorem NavierStokes.ActualCycleParameters.activeLabel_band {B N0 : ℕ} (n : ℕ) (l : Index B N0) (hl : l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : sourceBand l ∈ CorrectionInitialization.CommonWindow.levels n

theorem NavierStokes.ActualCycleParameters.activeLabel_index {B N0 : ℕ} (n : ℕ) (l : Index B N0) (hl : l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (sourceBand l)

theorem NavierStokes.ActualCycleParameters.activeLabel_particular {B N0 : ℕ} (n : ℕ) (hn : 1 ≤ n) (l : Index B N0) (hl : l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : 1 ≤ n ∧ BaseChartJets.cellBand ((swap B N0) l).2 ∈ CorrectionInitialization.CommonWindow.levels n

The particular source really is the current stored residual.

theorem NavierStokes.ActualCycleParameters.particular_assembly_context {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : (ActualParticularStageControls.assembly (particularState x) ((swap B N0) l)).context = StateReindex.context CorrectionStep.cycleAssoc.symm (CorrectionInitialization.ActualPrimary.commonContext B)

theorem NavierStokes.ActualCycleParameters.particular_assembly_state {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : (ActualParticularStageControls.assembly (particularState x) ((swap B N0) l)).state = StateReindex.state CorrectionStep.cycleAssoc.symm x.state

theorem NavierStokes.ActualCycleParameters.particular_assembly_carrier {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : (ActualParticularStageControls.assembly (particularState x) ((swap B N0) l)).carrierBlock = StateReindex.block CorrectionStep.cycleAssoc.symm (x.coefficients.blocks l)

theorem NavierStokes.ActualCycleParameters.particular_assembly_gaussian {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : (ActualParticularStageControls.assembly (particularState x) ((swap B N0) l)).gaussianInput = StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm (x.coefficients.gaussian l)

theorem NavierStokes.ActualCycleParameters.particular_assembly_alias {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : (ActualParticularStageControls.assembly (particularState x) ((swap B N0) l)).aliasInput = StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm (x.coefficients.aliasCoefficients l)

theorem NavierStokes.ActualCycleParameters.particular_source {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) (j : ℤ) : (((parameters x).particular l).copyData (StateReindex.context CorrectionStep.cycleAssoc.symm (CorrectionInitialization.ActualPrimary.commonContext B)) (StateReindex.state CorrectionStep.cycleAssoc.symm x.state) (StateReindex.block CorrectionStep.cycleAssoc.symm (x.coefficients.blocks l)) (StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm (x.coefficients.gaussian l)) (StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm (x.coefficients.aliasCoefficients l)) j).source = ParticularWaveAssembly.sourceFamily (StateReindex.context CorrectionStep.cycleAssoc.symm (CorrectionInitialization.ActualPrimary.commonContext B)) (StateReindex.state CorrectionStep.cycleAssoc.symm x.state) (StateReindex.block CorrectionStep.cycleAssoc.symm (x.coefficients.blocks l)) (StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm (x.coefficients.gaussian l)) (StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm (x.coefficients.aliasCoefficients l)) j

theorem NavierStokes.ActualCycleParameters.signed_request {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : (parameters x).signedRequest x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state = LocalSignedRequest.fullRequest ActualInitialization.strip ActualInitialization.patch (2 * CorrectionInitialization.ActualPrimary.h) (CorrectionInitialization.ActualPrimary.commonContext B) ((parameters x).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state)

The signed update uses the initialized primary carrier

theorem NavierStokes.ActualCycleParameters.signed_frequency (p : CorrectionStep.PeriodizedSignedParameters CorrectionStep.CyclePoint TorusInverse.Frequency) (s : WeightedClasses.StripData CorrectionStep.CyclePoint) (request : ℕ → CorrectionStep.CyclePoint × ℝ → SignedWaveUpdate.Vec2) : (p.exactBlock s request).frequency = p.base.frequency

theorem NavierStokes.ActualCycleParameters.signed_phase (p : CorrectionStep.PeriodizedSignedParameters CorrectionStep.CyclePoint TorusInverse.Frequency) (s : WeightedClasses.StripData CorrectionStep.CyclePoint) (request : ℕ → CorrectionStep.CyclePoint × ℝ → SignedWaveUpdate.Vec2) : (p.exactBlock s request).phase = fun (n : ℕ) (z : CorrectionStep.CyclePoint) => p.base.phase n (z, 0)

theorem NavierStokes.ActualCycleParameters.signed_angular (p : CorrectionStep.PeriodizedSignedParameters CorrectionStep.CyclePoint TorusInverse.Frequency) (s : WeightedClasses.StripData CorrectionStep.CyclePoint) (request : ℕ → CorrectionStep.CyclePoint × ℝ → SignedWaveUpdate.Vec2) : (p.exactBlock s request).angularFrequency = p.angularFrequency

theorem NavierStokes.ActualCycleParameters.primaryPiece_frequency (p : CorrectionInitialization.PrimaryPiece (CorrectionStep.CyclePoint × ℝ)) (phase : ℕ → CorrectionStep.CyclePoint → ℝ) (angular : ℕ → ℤ) : (p.harmonicBlock phase angular).frequency = p.coefficients.frequency

theorem NavierStokes.ActualCycleParameters.primaryPiece_phase (p : CorrectionInitialization.PrimaryPiece (CorrectionStep.CyclePoint × ℝ)) (phase : ℕ → CorrectionStep.CyclePoint → ℝ) (angular : ℕ → ℤ) : (p.harmonicBlock phase angular).phase = phase

theorem NavierStokes.ActualCycleParameters.primaryPiece_angular (p : CorrectionInitialization.PrimaryPiece (CorrectionStep.CyclePoint × ℝ)) (phase : ℕ → CorrectionStep.CyclePoint → ℝ) (angular : ℕ → ℤ) : (p.harmonicBlock phase angular).angularFrequency = angular

theorem NavierStokes.ActualCycleParameters.signed_primary_carrier {B N0 : ℕ} (l : Index B N0) (s : WeightedClasses.StripData CorrectionStep.CyclePoint) (request : ℕ → CorrectionStep.CyclePoint × ℝ → SignedWaveUpdate.Vec2) : CorrectionStep.SameCarrier (ActualInitialization.primaryBlock l) ((ActualSignedStageControls.parameters l).exactBlock s request)

theorem NavierStokes.ActualCycleParameters.signed_tangent_carrier {B N0 : ℕ} (l : Index B N0) (s : WeightedClasses.StripData CorrectionStep.CyclePoint) (request : ℕ → CorrectionStep.CyclePoint × ℝ → SignedWaveUpdate.Vec2) : CorrectionStep.SameCarrier (ActualInitialization.tangentBlock l) ((ActualSignedStageControls.parameters l).exactBlock s request)

theorem NavierStokes.ActualCycleParameters.parameters_signed_carrier {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (c : CorrectionState.Context CorrectionStep.CyclePoint) (l : Index B N0) (H : CorrectionStep.SameCarrier (x.coefficients.blocks l) (ActualInitialization.tangentBlock l)) : CorrectionStep.SameCarrier (x.coefficients.blocks l) ((parameters x).signedBlock x.coefficients c x.state l)

theorem NavierStokes.ActualCycleParameters.parameters_particular_carrier {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (c : CorrectionState.Context CorrectionStep.CyclePoint) (l : Index B N0) : CorrectionStep.SameCarrier (x.coefficients.blocks l) ((parameters x).particularBlock x.coefficients c x.state l)

theorem NavierStokes.ActualCycleParameters.parameters_gaussian_carrier {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (c : CorrectionState.Context CorrectionStep.CyclePoint) (l : Index B N0) : CorrectionStep.SameCarrier (x.coefficients.blocks l) ((parameters x).particularGaussianBlock x.coefficients c x.state l)

theorem NavierStokes.ActualCycleParameters.invariant_signed_carrier {B N0 : ℕ} {x : CorrectionStep.CycleState (Index B N0)} {P : Index B N0 → ℕ → CorrectionStep.CyclePoint → ℝ} {labelCarrier : Index B N0 → ℕ → Set CorrectionStep.CyclePoint} {sigma : ℝ} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P labelCarrier sigma x) (l : Index B N0) : CorrectionStep.SameCarrier (x.coefficients.blocks l) ((parameters x).signedBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l)

theorem NavierStokes.ActualCycleParameters.initial_signed_carrier (B N0 : ℕ) (l : Index B N0) : have x := ActualInitialization.initialCycleState B N0; CorrectionStep.SameCarrier (x.coefficients.blocks l) ((parameters x).signedBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l)

The same fixed primitives at every valid state

noncomputable def NavierStokes.ActualCycleParameters.fixedParameters (B N0 : ℕ) : CorrectionStep.CycleParameters (Index B N0)

Fixed parameters, constructed using CycleParameters.ofGeometry.

Equations

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

@[simp]

theorem NavierStokes.ActualCycleParameters.fixedParameters_particular (B N0 : ℕ) (l : Index B N0) : (fixedParameters B N0).particular l = ActualParticularStageControls.canonicalParameters (l.2, l.1)

@[simp]

theorem NavierStokes.ActualCycleParameters.fixedParameters_signed (B N0 : ℕ) (l : Index B N0) : (fixedParameters B N0).signed l = ActualSignedStageControls.parameters l

@[simp]

theorem NavierStokes.ActualCycleParameters.fixedParameters_strip (B N0 : ℕ) : (fixedParameters B N0).strip = ActualInitialization.geometry.strip

@[simp]

theorem NavierStokes.ActualCycleParameters.fixedParameters_gauge (B N0 : ℕ) : (fixedParameters B N0).gauge = ActualInitialization.geometry.gauge

@[simp]

theorem NavierStokes.ActualCycleParameters.fixedParameters_patch (B N0 : ℕ) : (fixedParameters B N0).patch = ActualInitialization.geometry.patch

@[simp]

theorem NavierStokes.ActualCycleParameters.fixedParameters_coordinate (B N0 : ℕ) : (fixedParameters B N0).coordinate = ActualInitialization.geometry.coord

@[simp]

theorem NavierStokes.ActualCycleParameters.fixedParameters_timeExponent (B N0 : ℕ) : (fixedParameters B N0).timeExponent = CorrectionInitialization.ActualPrimary.h

@[simp]

theorem NavierStokes.ActualCycleParameters.fixedParameters_commonIndex (B N0 : ℕ) : (fixedParameters B N0).commonIndex = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h

@[simp]

theorem NavierStokes.ActualCycleParameters.fixedParameters_axial (B N0 : ℕ) : (fixedParameters B N0).axial = ActualInitialization.axial

@[simp]

theorem NavierStokes.ActualCycleParameters.fixedParameters_rank (B N0 : ℕ) : (fixedParameters B N0).rank = CorrectionInitialization.ActualPrimary.rankData

theorem NavierStokes.ActualCycleParameters.fixedParameters_compatible (B N0 : ℕ) : ActualCycleExcluded.Compatible ActualCycleGeometry.similarityData (fixedParameters B N0) (CorrectionInitialization.ActualPrimary.commonContext B)

theorem NavierStokes.ActualCycleParameters.current_frequency {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) (H : CorrectionStep.SameCarrier (x.coefficients.blocks l) (ActualInitialization.tangentBlock l)) (n : ℕ) : (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.ActualCycleParameters.parameters_particular_eq_fixed {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) (H : CorrectionStep.SameCarrier (x.coefficients.blocks l) (ActualInitialization.tangentBlock l)) : (parameters x).particular l = (fixedParameters B N0).particular l

theorem NavierStokes.ActualCycleParameters.parameters_eq_fixed {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (H : ∀ (l : Index B N0), CorrectionStep.SameCarrier (x.coefficients.blocks l) (ActualInitialization.tangentBlock l)) : parameters x = fixedParameters B N0

theorem NavierStokes.ActualCycleParameters.invariant_parameters_eq_fixed {B N0 : ℕ} {x : CorrectionStep.CycleState (Index B N0)} {P : Index B N0 → ℕ → CorrectionStep.CyclePoint → ℝ} {labelCarrier : Index B N0 → ℕ → Set CorrectionStep.CyclePoint} {sigma : ℝ} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P labelCarrier sigma x) : parameters x = fixedParameters B N0

theorem NavierStokes.ActualCycleParameters.initial_parameters_eq_fixed (B N0 : ℕ) : parameters (ActualInitialization.initialCycleState B N0) = fixedParameters B N0

theorem NavierStokes.ActualCycleParameters.fixedParameters_signed_carrier {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (c : CorrectionState.Context CorrectionStep.CyclePoint) (l : Index B N0) (H : CorrectionStep.SameCarrier (x.coefficients.blocks l) (ActualInitialization.tangentBlock l)) : CorrectionStep.SameCarrier (x.coefficients.blocks l) ((fixedParameters B N0).signedBlock x.coefficients c x.state l)

theorem NavierStokes.ActualCycleParameters.invariant_fixedParameters_signed_carrier {B N0 : ℕ} {x : CorrectionStep.CycleState (Index B N0)} {P : Index B N0 → ℕ → CorrectionStep.CyclePoint → ℝ} {labelCarrier : Index B N0 → ℕ → Set CorrectionStep.CyclePoint} {sigma : ℝ} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P labelCarrier sigma x) (l : Index B N0) : CorrectionStep.SameCarrier (x.coefficients.blocks l) ((fixedParameters B N0).signedBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l)