TauLib · API Book V

TauLib.BookV.FluidMacro.TauAlfven

TauLib.BookV.FluidMacro.TauAlfven

Alfven wave modes: dispersion, damping, magnetoacoustic synthesis, shear vs compressional modes.

Registry Cross-References

  • [V.D111] Alfven wave mode — AlfvenWaveMode

  • [V.P52] Alfven dispersion — alfven_dispersion

  • [V.D112] Magnetoacoustic mode — MagnetoacousticMode

  • [V.R156] Alfven wave damping — alfven_damping

  • [V.P53] Magnetoacoustic synthesis — magnetoacoustic_synthesis

  • [V.D312] Alfvén damping rate — AlfvenDampingRate

  • [V.D313] Coronal heating flux — CoronalHeatingFlux

  • [V.T253] τ-Alfvén damping = ι_τ² ω — tau_alfven_damping_rate

  • [V.P173] Coronal flux consistency — CoronalFluxConsistency

  • [V.R445] Parker Solar Probe testability

Mathematical Content

Alfven Waves

Alfven waves are transverse oscillations of the magnetic field and plasma, propagating along the magnetic field lines at the Alfven speed:

v_A = B / √(μ₀ ρ)

They are incompressible (no density change) and carry energy along B.

Shear vs Compressional

In a general MHD medium, three MHD wave modes exist:

  • Shear Alfven wave (incompressible, v = v_A cos θ)

  • Fast magnetoacoustic wave (compressional, v > v_A)

  • Slow magnetoacoustic wave (compressional, v < v_A)

The fast and slow modes involve both magnetic pressure and gas pressure; the shear mode involves only magnetic tension.

Alfven Wave Damping

Alfven waves damp via:

  • Ion-neutral friction (partially ionized plasmas)

  • Viscous dissipation

  • Resistive dissipation (finite conductivity)

  • Phase mixing (inhomogeneous medium)

All damping mechanisms are bounded in the τ-framework by the defect-budget constraint.

Ground Truth Sources

  • Book V ch32: τ-Alfven waves

Tau.BookV.FluidMacro.MHDPolarization

source inductive Tau.BookV.FluidMacro.MHDPolarization :Type

MHD wave polarization.

  • Shear : MHDPolarization Shear (transverse, incompressible).

  • Fast : MHDPolarization Fast magnetoacoustic (compressional, v > v_A).

  • Slow : MHDPolarization Slow magnetoacoustic (compressional, v < v_A).

Instances For

Tau.BookV.FluidMacro.instReprMHDPolarization.repr

source def Tau.BookV.FluidMacro.instReprMHDPolarization.repr :MHDPolarization → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instReprMHDPolarization

source instance Tau.BookV.FluidMacro.instReprMHDPolarization :Repr MHDPolarization

Equations

  • Tau.BookV.FluidMacro.instReprMHDPolarization = { reprPrec := Tau.BookV.FluidMacro.instReprMHDPolarization.repr }

Tau.BookV.FluidMacro.instDecidableEqMHDPolarization

source instance Tau.BookV.FluidMacro.instDecidableEqMHDPolarization :DecidableEq MHDPolarization

Equations

  • Tau.BookV.FluidMacro.instDecidableEqMHDPolarization x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Tau.BookV.FluidMacro.instBEqMHDPolarization

source instance Tau.BookV.FluidMacro.instBEqMHDPolarization :BEq MHDPolarization

Equations

  • Tau.BookV.FluidMacro.instBEqMHDPolarization = { beq := Tau.BookV.FluidMacro.instBEqMHDPolarization.beq }

Tau.BookV.FluidMacro.instBEqMHDPolarization.beq

source def Tau.BookV.FluidMacro.instBEqMHDPolarization.beq :MHDPolarization → MHDPolarization → Bool

Equations

  • Tau.BookV.FluidMacro.instBEqMHDPolarization.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx) Instances For

Tau.BookV.FluidMacro.AlfvenWaveMode

source structure Tau.BookV.FluidMacro.AlfvenWaveMode :Type

[V.D111] Alfven wave mode: transverse oscillation of the magnetic field and plasma, propagating along B at the Alfven speed v_A.

v_A = B / √(μ₀ ρ)

Shear Alfven waves are incompressible and carry energy along B.

  • polarization : MHDPolarization Polarization type.

  • speed_numer : ℕ Alfven speed numerator (scaled).

  • speed_denom : ℕ Alfven speed denominator.

  • speed_denom_pos : self.speed_denom > 0 Denominator positive.

  • angle_deg_scaled : ℕ Propagation angle θ relative to B (in degrees, scaled by 10).

  • is_incompressible : Bool Whether the wave is incompressible.

Instances For

Tau.BookV.FluidMacro.instReprAlfvenWaveMode

source instance Tau.BookV.FluidMacro.instReprAlfvenWaveMode :Repr AlfvenWaveMode

Equations

  • Tau.BookV.FluidMacro.instReprAlfvenWaveMode = { reprPrec := Tau.BookV.FluidMacro.instReprAlfvenWaveMode.repr }

Tau.BookV.FluidMacro.instReprAlfvenWaveMode.repr

source def Tau.BookV.FluidMacro.instReprAlfvenWaveMode.repr :AlfvenWaveMode → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.AlfvenWaveMode.speedFloat

source def Tau.BookV.FluidMacro.AlfvenWaveMode.speedFloat (a : AlfvenWaveMode) :Float

Alfven speed as Float. Equations

  • a.speedFloat = Float.ofNat a.speed_numer / Float.ofNat a.speed_denom Instances For

Tau.BookV.FluidMacro.shear_is_incompressible

source **theorem Tau.BookV.FluidMacro.shear_is_incompressible (a : AlfvenWaveMode)

(_h : a.polarization = MHDPolarization.Shear)

(hi : a.is_incompressible = true) :a.is_incompressible = true**

Shear Alfven waves are incompressible.

Tau.BookV.FluidMacro.AlfvenDispersion

source structure Tau.BookV.FluidMacro.AlfvenDispersion :Type

Alfven dispersion relation. Shear: ω = v_A · k · cos θ Fast: ω² = k²(v_A² + c_s²)/2 + k²√((v_A² + c_s²)²/4 - v_A²c_s²cos²θ) Slow: same with minus sign.

  • mode : AlfvenWaveMode Wave mode.

  • freq_numer : ℕ Frequency numerator (scaled).

  • wavenumber_numer : ℕ Wavenumber numerator (scaled).

  • denom : ℕ Common denominator.

  • denom_pos : self.denom > 0 Denominator positive.

Instances For

Tau.BookV.FluidMacro.instReprAlfvenDispersion

source instance Tau.BookV.FluidMacro.instReprAlfvenDispersion :Repr AlfvenDispersion

Equations

  • Tau.BookV.FluidMacro.instReprAlfvenDispersion = { reprPrec := Tau.BookV.FluidMacro.instReprAlfvenDispersion.repr }

Tau.BookV.FluidMacro.instReprAlfvenDispersion.repr

source def Tau.BookV.FluidMacro.instReprAlfvenDispersion.repr :AlfvenDispersion → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.alfven_dispersion

source theorem Tau.BookV.FluidMacro.alfven_dispersion :”Shear: omega = v_A k cos(theta), Fast: v_phi > v_A, Slow: v_phi < v_A” = “Shear: omega = v_A k cos(theta), Fast: v_phi > v_A, Slow: v_phi < v_A”

[V.P52] Alfven dispersion: the phase velocity depends on polarization and angle.

Shear: v_φ = v_A cos θ (angle-dependent) Fast: v_φ > v_A (faster than Alfven speed) Slow: v_φ < v_A (slower than Alfven speed)

Structural recording.

Tau.BookV.FluidMacro.MagnetoacousticMode

source structure Tau.BookV.FluidMacro.MagnetoacousticMode :Type

[V.D112] Magnetoacoustic mode: compressional MHD wave involving both magnetic pressure and gas pressure.

Fast mode: compressions of B and ρ are in phase Slow mode: compressions of B and ρ are out of phase

  • is_fast : Bool Whether fast or slow.

  • sound_speed_numer : ℕ Sound speed numerator (scaled).

  • sound_speed_denom : ℕ Sound speed denominator.

  • sound_denom_pos : self.sound_speed_denom > 0 Denominator positive.

  • alfven_speed_numer : ℕ Alfven speed numerator (scaled).

  • alfven_speed_denom : ℕ Alfven speed denominator.

  • alfven_denom_pos : self.alfven_speed_denom > 0 Denominator positive.

  • compressions_in_phase : Bool In-phase (fast) or out-of-phase (slow).

  • phase_correct : self.compressions_in_phase = self.is_fast Phase matches fast/slow classification.

Instances For

Tau.BookV.FluidMacro.instReprMagnetoacousticMode.repr

source def Tau.BookV.FluidMacro.instReprMagnetoacousticMode.repr :MagnetoacousticMode → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instReprMagnetoacousticMode

source instance Tau.BookV.FluidMacro.instReprMagnetoacousticMode :Repr MagnetoacousticMode

Equations

  • Tau.BookV.FluidMacro.instReprMagnetoacousticMode = { reprPrec := Tau.BookV.FluidMacro.instReprMagnetoacousticMode.repr }

Tau.BookV.FluidMacro.fast_slow_opposite_phase

source **theorem Tau.BookV.FluidMacro.fast_slow_opposite_phase (fast slow : MagnetoacousticMode)

(hf : fast.is_fast = true)

(hs : slow.is_fast = false) :fast.compressions_in_phase ≠ slow.compressions_in_phase**

Fast and slow modes have opposite phase relations.

Tau.BookV.FluidMacro.AlfvenDampingMechanism

source inductive Tau.BookV.FluidMacro.AlfvenDampingMechanism :Type

Damping mechanism for Alfven waves.

  • IonNeutralFriction : AlfvenDampingMechanism Ion-neutral friction (partially ionized plasmas).

  • Viscous : AlfvenDampingMechanism Viscous dissipation.

  • Resistive : AlfvenDampingMechanism Resistive dissipation (finite conductivity).

  • PhaseMixing : AlfvenDampingMechanism Phase mixing in inhomogeneous medium.

Instances For

Tau.BookV.FluidMacro.instReprAlfvenDampingMechanism

source instance Tau.BookV.FluidMacro.instReprAlfvenDampingMechanism :Repr AlfvenDampingMechanism

Equations

  • Tau.BookV.FluidMacro.instReprAlfvenDampingMechanism = { reprPrec := Tau.BookV.FluidMacro.instReprAlfvenDampingMechanism.repr }

Tau.BookV.FluidMacro.instReprAlfvenDampingMechanism.repr

source def Tau.BookV.FluidMacro.instReprAlfvenDampingMechanism.repr :AlfvenDampingMechanism → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instDecidableEqAlfvenDampingMechanism

source instance Tau.BookV.FluidMacro.instDecidableEqAlfvenDampingMechanism :DecidableEq AlfvenDampingMechanism

Equations

  • Tau.BookV.FluidMacro.instDecidableEqAlfvenDampingMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Tau.BookV.FluidMacro.instBEqAlfvenDampingMechanism

source instance Tau.BookV.FluidMacro.instBEqAlfvenDampingMechanism :BEq AlfvenDampingMechanism

Equations

  • Tau.BookV.FluidMacro.instBEqAlfvenDampingMechanism = { beq := Tau.BookV.FluidMacro.instBEqAlfvenDampingMechanism.beq }

Tau.BookV.FluidMacro.instBEqAlfvenDampingMechanism.beq

source def Tau.BookV.FluidMacro.instBEqAlfvenDampingMechanism.beq :AlfvenDampingMechanism → AlfvenDampingMechanism → Bool

Equations

  • Tau.BookV.FluidMacro.instBEqAlfvenDampingMechanism.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx) Instances For

Tau.BookV.FluidMacro.AlfvenDamping

source structure Tau.BookV.FluidMacro.AlfvenDamping :Type

[V.R156] Alfven wave damping: all damping mechanisms are bounded in the τ-framework by the defect-budget constraint.

The damping rate γ ≤ γ_max for each mechanism, where γ_max is determined by the defect-budget at the relevant primorial level.

  • mechanism : AlfvenDampingMechanism Damping mechanism.

  • rate : ℕ Damping rate (scaled).

  • max_rate : ℕ Maximum damping rate (from defect budget).

  • rate_bounded : self.rate ≤ self.max_rate Rate is bounded.

Instances For

Tau.BookV.FluidMacro.instReprAlfvenDamping.repr

source def Tau.BookV.FluidMacro.instReprAlfvenDamping.repr :AlfvenDamping → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instReprAlfvenDamping

source instance Tau.BookV.FluidMacro.instReprAlfvenDamping :Repr AlfvenDamping

Equations

  • Tau.BookV.FluidMacro.instReprAlfvenDamping = { reprPrec := Tau.BookV.FluidMacro.instReprAlfvenDamping.repr }

Tau.BookV.FluidMacro.alfven_damping

source theorem Tau.BookV.FluidMacro.alfven_damping (d : AlfvenDamping) :d.rate ≤ d.max_rate

Damping is always bounded.

Tau.BookV.FluidMacro.MagnetoacousticSynthesis

source structure Tau.BookV.FluidMacro.MagnetoacousticSynthesis :Type

[V.P53] Magnetoacoustic synthesis: the three MHD wave modes (shear, fast, slow) form a complete basis for small-amplitude perturbations of a uniform magnetized plasma.

Any MHD perturbation decomposes uniquely into these three modes. This is the MHD analogue of the Fourier decomposition.

  • shear_amplitude : ℕ Shear mode amplitude.

  • fast_amplitude : ℕ Fast mode amplitude.

  • slow_amplitude : ℕ Slow mode amplitude.

  • is_complete : Bool Decomposition is complete (all modes present).

Instances For

Tau.BookV.FluidMacro.instReprMagnetoacousticSynthesis.repr

source def Tau.BookV.FluidMacro.instReprMagnetoacousticSynthesis.repr :MagnetoacousticSynthesis → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instReprMagnetoacousticSynthesis

source instance Tau.BookV.FluidMacro.instReprMagnetoacousticSynthesis :Repr MagnetoacousticSynthesis

Equations

  • Tau.BookV.FluidMacro.instReprMagnetoacousticSynthesis = { reprPrec := Tau.BookV.FluidMacro.instReprMagnetoacousticSynthesis.repr }

Tau.BookV.FluidMacro.MagnetoacousticSynthesis.totalEnergy

source def Tau.BookV.FluidMacro.MagnetoacousticSynthesis.totalEnergy (ms : MagnetoacousticSynthesis) :ℕ

Total perturbation energy = sum of modal energies. Equations

  • ms.totalEnergy = ms.shear_amplitude + ms.fast_amplitude + ms.slow_amplitude Instances For

Tau.BookV.FluidMacro.magnetoacoustic_synthesis

source **theorem Tau.BookV.FluidMacro.magnetoacoustic_synthesis (ms : MagnetoacousticSynthesis)

(h : ms.shear_amplitude > 0 ∨ ms.fast_amplitude > 0 ∨ ms.slow_amplitude > 0) :ms.totalEnergy > 0**

Completeness: total energy is nonzero for nontrivial perturbation.

Tau.BookV.FluidMacro.AlfvenDampingRate

source structure Tau.BookV.FluidMacro.AlfvenDampingRate :Type

[V.D312] Alfvén damping rate from B-sector coupling.

γ_A = κ(B;2) · ω_A = ι_τ² · v_A k

The B-sector coupling governs Alfvén wave dissipation. Damping length: L_d = v_A / γ_A = 1/(ι_τ² k).

  • iota_sq_x100000 : ℕ ι_τ² × 100000 (≈ 11649).

  • sector : ℕ Coupling sector (B = 2).

  • free_params : ℕ Free parameters.

Instances For

Tau.BookV.FluidMacro.instReprAlfvenDampingRate.repr

source def Tau.BookV.FluidMacro.instReprAlfvenDampingRate.repr :AlfvenDampingRate → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instReprAlfvenDampingRate

source instance Tau.BookV.FluidMacro.instReprAlfvenDampingRate :Repr AlfvenDampingRate

Equations

  • Tau.BookV.FluidMacro.instReprAlfvenDampingRate = { reprPrec := Tau.BookV.FluidMacro.instReprAlfvenDampingRate.repr }

Tau.BookV.FluidMacro.alfven_damping_rate_tau

source def Tau.BookV.FluidMacro.alfven_damping_rate_tau :AlfvenDampingRate

Default damping rate. Equations

  • Tau.BookV.FluidMacro.alfven_damping_rate_tau = { } Instances For

Tau.BookV.FluidMacro.CoronalHeatingFlux

source structure Tau.BookV.FluidMacro.CoronalHeatingFlux :Type

[V.D313] Coronal heating flux from τ-Alfvén damping.

F_τ = ρ · v_A · v_conv² · (1 - exp(-ι_τ² · L/λ_A))

For L/λ_A ~ 10: damping fraction ≈ 0.688. Predicted F_τ ≈ 2.1 × 10⁵ erg cm⁻² s⁻¹. Required: F_req ≈ 3 × 10⁵ erg cm⁻² s⁻¹ (active regions).

  • flux_x1e5 : ℕ Predicted flux × 10⁻⁵ (erg cm⁻² s⁻¹).

  • required_x1e5 : ℕ Required flux × 10⁻⁵.

  • damping_frac_x1000 : ℕ Damping fraction × 1000 for L/λ = 10.

  • free_params : ℕ Free parameters.

Instances For

Tau.BookV.FluidMacro.instReprCoronalHeatingFlux.repr

source def Tau.BookV.FluidMacro.instReprCoronalHeatingFlux.repr :CoronalHeatingFlux → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instReprCoronalHeatingFlux

source instance Tau.BookV.FluidMacro.instReprCoronalHeatingFlux :Repr CoronalHeatingFlux

Equations

  • Tau.BookV.FluidMacro.instReprCoronalHeatingFlux = { reprPrec := Tau.BookV.FluidMacro.instReprCoronalHeatingFlux.repr }

Tau.BookV.FluidMacro.coronal_heating_flux

source def Tau.BookV.FluidMacro.coronal_heating_flux :CoronalHeatingFlux

Default coronal heating flux. Equations

  • Tau.BookV.FluidMacro.coronal_heating_flux = { } Instances For

Tau.BookV.FluidMacro.tau_alfven_damping_rate

source theorem Tau.BookV.FluidMacro.tau_alfven_damping_rate :alfven_damping_rate_tau.free_params = 0 ∧ alfven_damping_rate_tau.sector = 2

[V.T253] τ-Alfvén damping rate is ι_τ² · ω_A.

The Alfvén damping rate is controlled by the B-sector coupling κ(B;2) = ι_τ². As waves propagate along the base τ¹, the T² fiber introduces dissipation proportional to ι_τ². Zero free parameters.

Tau.BookV.FluidMacro.CoronalFluxConsistency

source structure Tau.BookV.FluidMacro.CoronalFluxConsistency :Type

[V.P173] Coronal flux consistency.

Prediction: F_τ ≈ 2.1 × 10⁵ erg cm⁻² s⁻¹. Required: ≈ 3 × 10⁵ (active regions). Ratio: F_τ/F_req ≈ 0.7 (within factor 1.5). Consistent given order-of-magnitude uncertainties in photospheric parameters (ρ, v_A, v_conv).

  • ratio_x100 : ℕ Predicted / required ratio × 100.

  • within_factor_2 : self.ratio_x100 ≥ 50 Within factor 2.

Instances For

Tau.BookV.FluidMacro.instReprCoronalFluxConsistency

source instance Tau.BookV.FluidMacro.instReprCoronalFluxConsistency :Repr CoronalFluxConsistency

Equations

  • Tau.BookV.FluidMacro.instReprCoronalFluxConsistency = { reprPrec := Tau.BookV.FluidMacro.instReprCoronalFluxConsistency.repr }

Tau.BookV.FluidMacro.instReprCoronalFluxConsistency.repr

source def Tau.BookV.FluidMacro.instReprCoronalFluxConsistency.repr :CoronalFluxConsistency → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.coronal_flux_consistency

source def Tau.BookV.FluidMacro.coronal_flux_consistency :CoronalFluxConsistency

Default consistency check. Equations

  • Tau.BookV.FluidMacro.coronal_flux_consistency = { within_factor_2 := Tau.BookV.FluidMacro.coronal_flux_consistency._proof_2 } Instances For

Tau.BookV.FluidMacro.example_shear_alfven

source def Tau.BookV.FluidMacro.example_shear_alfven :AlfvenWaveMode

Example shear Alfven wave. Equations

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

Tau.BookV.FluidMacro.example_fast_mode

source def Tau.BookV.FluidMacro.example_fast_mode :MagnetoacousticMode

Example fast magnetoacoustic mode. Equations

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

Tau.BookV.FluidMacro.example_synthesis

source def Tau.BookV.FluidMacro.example_synthesis :MagnetoacousticSynthesis

Example synthesis. Equations

  • Tau.BookV.FluidMacro.example_synthesis = { shear_amplitude := 50, fast_amplitude := 30, slow_amplitude := 20 } Instances For