Signed mean gain with fixed physical labels

The physical wave family keeps its original label type. At each band an injection on the active finite set identifies its coefficient data with the relative native labels used by SignedMeanGain.NativeData. Finite-sum reindexing then gives the actual native cross identity. The mean-gain theorem is applied to the original family, with its original uniform constants.

Coefficient and carrier identities at one band

structure NavierStokes.BandReindexedSignedMeanGain.SameCarrierAt {D : Type} (a b : CorrectionState.HarmonicBlock D) (n : ℕ) : Prop

The carrier metadata needed to compare the actual fields at one band. No relationship at another band is required.

• frequency : b.frequency n = a.frequency n
• phase : b.phase n = a.phase n
• angular : b.angularFrequency n = a.angularFrequency n

theorem NavierStokes.BandReindexedSignedMeanGain.sameCarrierAt_of_sameCarrier {D : Type} {a b : CorrectionState.HarmonicBlock D} (h : LabelSumBounds.SameCarrier a b) (n : ℕ) : SameCarrierAt a b n

theorem NavierStokes.BandReindexedSignedMeanGain.oscillation_eq_at_band_of_coefficients {D : Type} (a b : CorrectionState.HarmonicBlock D) (n : ℕ) (hv : a.velocity n = b.velocity n) (hc : SameCarrierAt a b n) : a.oscillation n = b.oscillation n

Equality of the stored coefficients and carrier metadata identifies the actual harmonic field at this band. Pressure data are not used in covariance.

Finite reindexing of actual fields

theorem NavierStokes.BandReindexedSignedMeanGain.fieldSum_reindex_of_coefficients {D ι κ : Type} [DecidableEq κ] (labels : ℕ → Finset ι) (nativeLabels : ℕ → Finset κ) (a : ι → CorrectionState.HarmonicBlock D) (b : κ → CorrectionState.HarmonicBlock D) (e : ℕ → ι → κ) (he : ∀ (n : ℕ), Set.InjOn (e n) ↑(labels n)) (hlabels : ∀ (n : ℕ), Finset.image (e n) (labels n) = nativeLabels n) (hv : ∀ (n : ℕ), ∀ l ∈ labels n, (a l).velocity n = (b (e n l)).velocity n) (hc : ∀ (n : ℕ), ∀ l ∈ labels n, SameCarrierAt (a l) (b (e n l)) n) : (LabelSumBounds.fieldSum labels fun (l : ι) => (a l).oscillation) = LabelSumBounds.fieldSum nativeLabels fun (l : κ) => (b l).oscillation

Reindex a finite sum using only the coefficient and carrier identities on its active labels. Inactive labels need not have distinct images.

The native requested cross for arbitrary physical labels

theorem NavierStokes.BandReindexedSignedMeanGain.native_fields (G : SignedMeanGain.Geometry) (B : SignedMeanGain.NativeData G) (c : CorrectionState.Context SignedMeanGain.Point) (u : CorrectionState.State SignedMeanGain.Point) {ι : Type} {P : ι → ℕ → SignedMeanGain.Point → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily G.strip P α δ β η) (a : SignedMeanGain.Assembly f) (e : ℕ → ι → SignedMeanGain.NativeIndex) (he : ∀ (n : ℕ), Set.InjOn (e n) ↑(a.labels n)) (hlabels : ∀ (n : ℕ), Finset.image (e n) (a.labels n) = B.labels n) (hp : ∀ (n : ℕ), ∀ l ∈ a.labels n, (f.primary l).velocity n = (B.primaryBlocks (e n l)).velocity n) (hcp : ∀ (n : ℕ), ∀ l ∈ a.labels n, SameCarrierAt (f.primary l) (B.primaryBlocks (e n l)) n) (ht : ∀ (n : ℕ), ∀ l ∈ a.labels n, (f.tangent l).velocity n = (B.signedBlocks c u (e n l)).velocity n) (hct : ∀ (n : ℕ), ∀ l ∈ a.labels n, SameCarrierAt (f.tangent l) (B.signedBlocks c u (e n l)) n) : (SignedMeanGain.primaryField f a = LabelSumBounds.fieldSum B.labels fun (l : SignedMeanGain.NativeIndex) => (B.primaryBlocks l).oscillation) ∧ SignedMeanGain.tangentField f a = LabelSumBounds.fieldSum B.labels fun (l : SignedMeanGain.NativeIndex) => (B.signedBlocks c u l).oscillation

The actual primary and tangent sums agree with the native sums after bandwise finite reindexing. This theorem does not reindex SignedFamily, so none of its uniform coefficient bounds acquire a label-dependent constant.

theorem NavierStokes.BandReindexedSignedMeanGain.native_family_cross (G : SignedMeanGain.Geometry) (B : SignedMeanGain.NativeData G) (c : CorrectionState.Context SignedMeanGain.Point) (u : CorrectionState.State SignedMeanGain.Point) {ι : Type} {P : ι → ℕ → SignedMeanGain.Point → ℝ} {α δ β η : ℝ} (f : LabelSumBounds.SignedFamily G.strip P α δ β η) (a : SignedMeanGain.Assembly f) (e : ℕ → ι → SignedMeanGain.NativeIndex) (he : ∀ (n : ℕ), Set.InjOn (e n) ↑(a.labels n)) (hlabels : ∀ (n : ℕ), Finset.image (e n) (a.labels n) = B.labels n) (hp : ∀ (n : ℕ), ∀ l ∈ a.labels n, (f.primary l).velocity n = (B.primaryBlocks (e n l)).velocity n) (hcp : ∀ (n : ℕ), ∀ l ∈ a.labels n, SameCarrierAt (f.primary l) (B.primaryBlocks (e n l)) n) (ht : ∀ (n : ℕ), ∀ l ∈ a.labels n, (f.tangent l).velocity n = (B.signedBlocks c u (e n l)).velocity n) (hct : ∀ (n : ℕ), ∀ l ∈ a.labels n, SameCarrierAt (f.tangent l) (B.signedBlocks c u (e n l)) n) : MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a 0 1)) (SignedMeanGain.physicalSigma G 2 (u.thetaResidual c)) ∧ MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a 0 2)) (SignedMeanGain.physicalSigma G 1 (u.axialResidual c))

The same primary matrix, masks, fundamental, and signed inverse supply the requested physical stress. Both cross identities are conclusions.

The gain for the original family and literal reconstructed state

theorem NavierStokes.BandReindexedSignedMeanGain.native_signed_mean_gain (G : SignedMeanGain.Geometry) (B : SignedMeanGain.NativeData G) (c : CorrectionState.Context SignedMeanGain.Point) (u : CorrectionState.State SignedMeanGain.Point) {ι : Type} {P : ι → ℕ → SignedMeanGain.Point → ℝ} {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : 0 ≤ κ) (hκsmall : κ ≤ 1 / 100000) (f : LabelSumBounds.SignedFamily G.strip P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ)) (a : SignedMeanGain.Assembly f) (e : ℕ → ι → SignedMeanGain.NativeIndex) (he : ∀ (n : ℕ), Set.InjOn (e n) ↑(a.labels n)) (hlabels : ∀ (n : ℕ), Finset.image (e n) (a.labels n) = B.labels n) (hp : ∀ (n : ℕ), ∀ l ∈ a.labels n, (f.primary l).velocity n = (B.primaryBlocks (e n l)).velocity n) (hcp : ∀ (n : ℕ), ∀ l ∈ a.labels n, SameCarrierAt (f.primary l) (B.primaryBlocks (e n l)) n) (ht : ∀ (n : ℕ), ∀ l ∈ a.labels n, (f.tangent l).velocity n = (B.signedBlocks c u (e n l)).velocity n) (hct : ∀ (n : ℕ), ∀ l ∈ a.labels n, SameCarrierAt (f.tangent l) (B.signedBlocks c u (e n l)) n) (q : CorrectionState.OscillatoryScalar SignedMeanGain.Point) (gaussian : CorrectionState.Oscillation SignedMeanGain.Point) (hold : u.oscillation = SignedMeanGain.oldField f a) (H : SignedMeanGain.LocalData G c u (SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q gaussian) (ho : MeanIncrementBounds.OperatorBounds G.strip G.operators κ) (hX : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.incrementTensor f a i j)) (hS : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.crossTensor f a i j)) (hθ : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.thetaResidual c)) (hz : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.axialResidual c)) (hd : CorrectionState.DefectBounds G.slowStrip (σ - κ) c u) : have v := SignedMeanGain.waveStage G.gauge c u (SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q gaussian; WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.thetaResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.axialResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100) (StateMomentBalances.meanBar (v.thetaResidual c)) ∧ WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100) (StateMomentBalances.meanBar (v.axialResidual c))

Signed-wave mean gain for fixed physical labels and a band-dependent native reindexing. The input uniform bounds remain those of f on the original label type. The output is the actual moving-gauge reconstructed state, including the supplied Gaussian error and all covariance terms.