Geometry of the actual broad primary carrier

The Gaussian source carrier keeps the native slow mask and source rectangle, but does not keep a separate dyadic mask. A single geometric threshold, chosen before the actual primary family, controls this larger carrier.

@[reducible, inline]

abbrev NavierStokes.ActualCarrierGeometry.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.ActualCarrierGeometry.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

abbrev NavierStokes.ActualCarrierGeometry.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.ActualCarrierGeometry.Slow = NavierStokes.PhaseCalculus.Slow

noncomputable def NavierStokes.ActualCarrierGeometry.geometricThreshold : ℕ

This threshold depends only on the fixed nominal profile and its actual positive reference cells. In particular, it is independent of the Borel order, the chosen primary label, and the correction stage.

Equations

• NavierStokes.ActualCarrierGeometry.geometricThreshold = NavierStokes.ActualCarrierGeometry.geometricThreshold._proof_3.choose

noncomputable def NavierStokes.ActualCarrierGeometry.startingThreshold (requested : ℕ) : ℕ

The final construction can enlarge its requested starting band once, before selecting ActualPrimary.choice.

Equations

• NavierStokes.ActualCarrierGeometry.startingThreshold requested = max requested NavierStokes.ActualCarrierGeometry.geometricThreshold

theorem NavierStokes.ActualCarrierGeometry.requested_le_startingThreshold (requested : ℕ) : requested ≤ startingThreshold requested

theorem NavierStokes.ActualCarrierGeometry.geometricThreshold_le_startingThreshold (requested : ℕ) : geometricThreshold ≤ startingThreshold requested

theorem NavierStokes.ActualCarrierGeometry.startingThreshold_le_prepared (B requested : ℕ) : startingThreshold requested ≤ (CorrectionInitialization.ActualPrimary.choice B (startingThreshold requested)).prepared.N

theorem NavierStokes.ActualCarrierGeometry.threshold_le_band {B N0 : ℕ} (hN : geometricThreshold ≤ N0) (L : CorrectionInitialization.ActualPrimary.Label B N0) : geometricThreshold ≤ BaseChartJets.cellBand L

theorem NavierStokes.ActualCarrierGeometry.cell_geometry {B N0 : ℕ} (hN : geometricThreshold ≤ N0) (L : CorrectionInitialization.ActualPrimary.Label B N0) {p : Slow} (hp : p ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) : 0 < p.1 ∧ √(NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) / 2 ≤ p.1 ∧ ‖p‖ ≤ PositiveRepresentatives.cellBound (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal) ∧ 0 < p.2.2 ∧ SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h p ∈ Set.Ioo (1 / 4) 4 ∧ SimilarityHomogeneity.chartX CorrectionInitialization.ActualPrimary.h p ∈ Set.Ioo (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal / 2) (2 * NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)

The original positive-cell theorem applies to the same selected label; no new representative or prepared family is chosen.

theorem NavierStokes.ActualCarrierGeometry.sourceCell_subset_clock {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) : ActualGaussianCoverage.sourceCell CorrectionInitialization.ActualPrimary.slots.radius (ChartScales.slotLength CorrectionInitialization.ActualPrimary.slots.radius CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) 1 ⊆ (CorrectionInitialization.ActualPrimary.clockWindow L).core

theorem NavierStokes.ActualCarrierGeometry.labelCarrier_slow_core {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : Point} (hx : x ∈ ActualInitialExcluded.labelCarrier l n) : ActualPrimaryCovariance.nativePoint n x l.2 ∈ ActualGaussianCoverage.actualSlowCore CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared l.2

theorem NavierStokes.ActualCarrierGeometry.labelCarrier_in_cell {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (hx : x ∈ ActualInitialExcluded.labelCarrier l n) : ActualPrimaryCovariance.nativePoint n x l.2 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier l.2

theorem NavierStokes.ActualCarrierGeometry.labelCarrier_q {B N0 : ℕ} (hN : geometricThreshold ≤ N0) (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (hx : x ∈ ActualInitialExcluded.labelCarrier l n) : SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h (ActualPrimaryCovariance.nativePoint n x l.2) ∈ Set.Ioo (1 / 4) 4

theorem NavierStokes.ActualCarrierGeometry.logCoordinate_in_broad_band {q : ℝ} (hq : 0 < q) {n : ℕ} (hlo : ChartScales.Q n / 4 < q) (hhi : q < 4 * ChartScales.Q n) : SquaredPartition.logCoordinate q ∈ Set.Ioo (↑n - 2) (↑n + 2)

theorem NavierStokes.ActualCarrierGeometry.labelCarrier_log_band {B N0 : ℕ} (hN : geometricThreshold ≤ N0) (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (hx : x ∈ ActualInitialExcluded.labelCarrier l n) : SquaredPartition.logCoordinate (CorrectionInitialization.ActualPrimary.physicalScale n x) ∈ Set.Ioo (↑(BaseChartJets.cellBand l.2) - 2) (↑(BaseChartJets.cellBand l.2) + 2)

theorem NavierStokes.ActualCarrierGeometry.strip_log_band (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) : SquaredPartition.logCoordinate (CorrectionInitialization.ActualPrimary.physicalScale n x) ∈ Set.Icc (↑n - 1) (↑n + 1)

theorem NavierStokes.ActualCarrierGeometry.labelCarrier_band_distance {B N0 : ℕ} (hN : geometricThreshold ≤ N0) (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (hc : x ∈ ActualInitialExcluded.labelCarrier l n) : n ≤ BaseChartJets.cellBand l.2 + 2 ∧ BaseChartJets.cellBand l.2 ≤ n + 2

The strict broad-cell range saves one integer level: the true band distance is at most two, despite the absence of the dyadic mask.

theorem NavierStokes.ActualCarrierGeometry.labelCarrier_near {B N0 : ℕ} (hN : geometricThreshold ≤ N0) (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (hc : x ∈ ActualInitialExcluded.labelCarrier l n) : ActualPrimaryBounds.near l n

theorem NavierStokes.ActualCarrierGeometry.labelCarrier_phaseCell {B N0 : ℕ} (hN : geometricThreshold ≤ N0) (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ ActualPrimaryBounds.fullStrip.domain) (hc : x.1 ∈ ActualInitialExcluded.labelCarrier l n) : ∃ (k : TorusInverse.Frequency), ActualPrimaryBounds.near l n ∧ (ActualPrimaryBounds.fullCopy l n k x).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier l.2 ∧ (ActualPrimaryBounds.fullCopy l n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core

theorem NavierStokes.ActualCarrierGeometry.position_component {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (p : Slow) (j : Fin 3) : CorrectionInitialization.ActualPrimary.position L p j = ChartScales.Q (BaseChartJets.cellBand L) ^ SlotColoring.axisExponent (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) j * PrimaryRepresentatives.position p j

theorem NavierStokes.ActualCarrierGeometry.width_eq (D : ℝ) (j : Fin 3) (n : ℕ) : SlotColoring.width D j n = ChartScales.Q n ^ SlotColoring.axisExponent D j * SquaredPartition.nativeSpacing n

theorem NavierStokes.ActualCarrierGeometry.nativeSlowCore_physicalBox {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) {p : Slow} (hp : p ∈ ActualGaussianCoverage.actualSlowCore CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared l.2) : CorrectionInitialization.ActualPrimary.position l.2 p ∈ SlotColoring.physicalBox (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (ActualPrimaryCovariance.signedLabelOf (l.2, l.1))

theorem NavierStokes.ActualCarrierGeometry.labelCarrier_window {B N0 : ℕ} (hN : geometricThreshold ≤ N0) (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (hc : x ∈ ActualInitialExcluded.labelCarrier l n) : ActualPrimaryCovariance.physicalWindow n x ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (ActualPrimaryCovariance.signedLabelOf (l.2, l.1))

The broad source carrier fits the existing closed two-level, two-mesh window. Its missing dyadic factor is not restored or assumed.

theorem NavierStokes.ActualCarrierGeometry.signedLabel_injective {B N0 : ℕ} : Function.Injective fun (l : ActualPrimaryBounds.SignedLabel B N0) => ActualPrimaryCovariance.signedLabelOf (l.2, l.1)

theorem NavierStokes.ActualCarrierGeometry.labelCarrier_window_card {B N0 : ℕ} (hN : geometricThreshold ≤ N0) (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (s : Finset (ActualPrimaryBounds.SignedLabel B N0)) (hs : ∀ l ∈ s, x ∈ ActualInitialExcluded.labelCarrier l n) : s.card ≤ 2250

theorem NavierStokes.ActualCarrierGeometry.geometry_liftedSupport (g : CommonCoverSolve.Geometry) {C S : Set TorusInverse.Plane} (hCS : (fun (z : TorusInverse.Plane) => g.center + g.basis z) '' C ⊆ S) (k : TorusInverse.Frequency) {Y : TorusInverse.Plane} (hY : g.coordinates k Y ∈ C) : Y ∈ SlotGeometry.liftedSupport g.gap S

theorem NavierStokes.ActualCarrierGeometry.clock_core_in_slot {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) : (fun (z : TorusInverse.Plane) => (CorrectionInitialization.ActualPrimary.geometry l.1 l.2).center + (CorrectionInitialization.ActualPrimary.geometry l.1 l.2).basis z) '' (CorrectionInitialization.ActualPrimary.clockWindow l.2).core ⊆ PartitionedCovariance.slotSet CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius CorrectionInitialization.ActualPrimary.radialVector CorrectionInitialization.ActualPrimary.temporalVector (ActualPrimaryCovariance.signedLabelOf (l.2, l.1))

theorem NavierStokes.ActualCarrierGeometry.labelCarrier_liftedSupport {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : Point} (hx : x ∈ ActualInitialExcluded.labelCarrier l n) : ActualPrimaryCovariance.absoluteAuxiliary n x ∈ SlotGeometry.liftedSupport (SlotColoring.nativeIndex CorrectionInitialization.ActualPrimary.h (ActualPrimaryCovariance.signedLabelOf (l.2, l.1)).1) (PartitionedCovariance.slotSet CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius CorrectionInitialization.ActualPrimary.radialVector CorrectionInitialization.ActualPrimary.temporalVector (ActualPrimaryCovariance.signedLabelOf (l.2, l.1)))

The source rectangle lies in the actual selected absolute slot. This part is purely geometric and needs neither the threshold nor strip membership.

theorem NavierStokes.ActualCarrierGeometry.labelCarrier_disjoint {B N0 : ℕ} (hN : geometricThreshold ≤ N0) (n : ℕ) {l m : ActualPrimaryBounds.SignedLabel B N0} (hne : l ≠ m) : Disjoint ((BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain ∩ ActualInitialExcluded.labelCarrier l n) ((BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain ∩ ActualInitialExcluded.labelCarrier m n)

Distinct broad carriers are disjoint on the actual strip. Separation comes from the original rational slot system and the proved window bound.