TauLib · API Book V

TauLib.BookV.FluidMacro.TauMHD

TauLib.BookV.FluidMacro.TauMHD

MHD in the τ-framework: magnetic pressure/tension, Alfven waves, dynamo action, reconnection, and force-free configurations.

Registry Cross-References

  • [V.D107] tau-MHD system — TauMHDSystem

  • [V.D108] Magnetic pressure-tension — MagneticPressureTension

  • [V.T75] Frozen flux theorem — frozen_flux_theorem

  • [V.D109] MHD dynamo — MHDDynamo

  • [V.P49] Magnetic energy bound — magnetic_energy_bound

  • [V.P50] Reconnection rate — reconnection_rate

  • [V.P51] Force-free equilibrium — force_free_equilibrium

  • [V.D110] Reconnection event — ReconnectionEvent

  • [V.D311] Fast reconnection rate — FastReconnectionRate

  • [V.T252] v_rec = ι_τ² v_A — fast_reconnection_is_iota_sq

  • [V.P172] Solar flare consistency — SolarFlareConsistency

  • [V.R443] Sweet-Parker vs τ-rate

  • [V.R444] B-sector topological transition

Mathematical Content

τ-MHD System

The τ-MHD system couples the macro defect-transport equation to the B-sector holonomy constraint. The conducting fluid carries magnetic flux; the flux is frozen into the fluid (ideal MHD) or slowly diffuses (resistive MHD).

Magnetic Pressure and Tension

The magnetic field contributes both:

  • Isotropic pressure: P_B = B²/(2μ₀) (resists compression)

  • Anisotropic tension: T_B = B²/μ₀ (along field lines, resists bending)

Frozen Flux Theorem

In ideal MHD, the magnetic flux through any surface moving with the fluid is constant: dΦ_B/dt = 0. This is the topological preservation of B-sector holonomy by the fluid flow.

Dynamo Action

Self-sustained magnetic field generation by fluid motions. Requires breaking axial symmetry (Cowling’s theorem) and sufficient magnetic Reynolds number Re_m » 1.

Reconnection

Topological change of magnetic field line connectivity. Reconnection releases stored magnetic energy and converts it to kinetic energy and heating.

Ground Truth Sources

  • Book V ch31: τ-MHD

Tau.BookV.FluidMacro.MHDApprox

source inductive Tau.BookV.FluidMacro.MHDApprox :Type

MHD approximation type.

  • Ideal : MHDApprox Ideal: zero resistivity, perfect flux freezing.

  • Resistive : MHDApprox Resistive: finite resistivity, slow diffusion.

  • Hall : MHDApprox Hall: includes Hall effect (ion-electron separation).

Instances For

Tau.BookV.FluidMacro.instReprMHDApprox

source instance Tau.BookV.FluidMacro.instReprMHDApprox :Repr MHDApprox

Equations

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

Tau.BookV.FluidMacro.instReprMHDApprox.repr

source def Tau.BookV.FluidMacro.instReprMHDApprox.repr :MHDApprox → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instDecidableEqMHDApprox

source instance Tau.BookV.FluidMacro.instDecidableEqMHDApprox :DecidableEq MHDApprox

Equations

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

Tau.BookV.FluidMacro.instBEqMHDApprox.beq

source def Tau.BookV.FluidMacro.instBEqMHDApprox.beq :MHDApprox → MHDApprox → Bool

Equations

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

Tau.BookV.FluidMacro.instBEqMHDApprox

source instance Tau.BookV.FluidMacro.instBEqMHDApprox :BEq MHDApprox

Equations

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

Tau.BookV.FluidMacro.TauMHDSystem

source structure Tau.BookV.FluidMacro.TauMHDSystem :Type

[V.D107] τ-MHD system: macro defect-transport coupled to the B-sector holonomy constraint.

The conducting fluid carries magnetic flux; the approximation type determines whether flux is frozen (ideal) or diffuses (resistive).

  • plasma : TauPlasmaState Underlying plasma state.

  • approx : MHDApprox MHD approximation.

  • mag_reynolds_numer : ℕ Magnetic Reynolds number (Re_m, scaled).

  • mag_reynolds_denom : ℕ Magnetic Reynolds denominator.

  • mag_reynolds_denom_pos : self.mag_reynolds_denom > 0 Denominator positive.

  • in_mhd_limit : Bool Whether the system is in the MHD limit.

Instances For

Tau.BookV.FluidMacro.instReprTauMHDSystem

source instance Tau.BookV.FluidMacro.instReprTauMHDSystem :Repr TauMHDSystem

Equations

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

Tau.BookV.FluidMacro.instReprTauMHDSystem.repr

source def Tau.BookV.FluidMacro.instReprTauMHDSystem.repr :TauMHDSystem → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.TauMHDSystem.magReynolds

source def Tau.BookV.FluidMacro.TauMHDSystem.magReynolds (s : TauMHDSystem) :ℕ

Magnetic Reynolds number ratio. Equations

  • s.magReynolds = s.mag_reynolds_numer / s.mag_reynolds_denom Instances For

Tau.BookV.FluidMacro.MagneticPressureTension

source structure Tau.BookV.FluidMacro.MagneticPressureTension :Type

[V.D108] Magnetic pressure-tension: the magnetic field contributes both isotropic pressure P_B = B²/(2μ₀) and anisotropic tension T_B = B²/μ₀ along field lines.

Encoded as (pressure_numer, tension_numer) with common denominator. Tension = 2 × Pressure (exact ratio).

  • pressure_numer : ℕ Magnetic pressure numerator (B²/(2μ₀), scaled).

  • tension_numer : ℕ Magnetic tension numerator (B²/μ₀, scaled).

  • denom : ℕ Common denominator.

  • denom_pos : self.denom > 0 Denominator positive.

  • tension_ratio : self.tension_numer = 2 * self.pressure_numer Tension = 2 × pressure.

Instances For

Tau.BookV.FluidMacro.instReprMagneticPressureTension

source instance Tau.BookV.FluidMacro.instReprMagneticPressureTension :Repr MagneticPressureTension

Equations

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

Tau.BookV.FluidMacro.instReprMagneticPressureTension.repr

source def Tau.BookV.FluidMacro.instReprMagneticPressureTension.repr :MagneticPressureTension → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.tension_pressure_ratio

source theorem Tau.BookV.FluidMacro.tension_pressure_ratio (mpt : MagneticPressureTension) :mpt.tension_numer = 2 * mpt.pressure_numer

Tension-to-pressure ratio is exactly 2.

Tau.BookV.FluidMacro.FrozenFluxTheorem

source structure Tau.BookV.FluidMacro.FrozenFluxTheorem :Type

[V.T75] Frozen flux theorem: in ideal MHD, the magnetic flux through any surface moving with the fluid is constant.

dΦ_B/dt = 0

This is the topological preservation of B-sector holonomy by the fluid flow. Only holds in ideal MHD (η = 0).

  • system : TauMHDSystem The MHD system.

  • is_ideal : self.system.approx = MHDApprox.Ideal System is ideal.

  • flux_conserved : Bool Flux is conserved.

Instances For

Tau.BookV.FluidMacro.instReprFrozenFluxTheorem.repr

source def Tau.BookV.FluidMacro.instReprFrozenFluxTheorem.repr :FrozenFluxTheorem → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instReprFrozenFluxTheorem

source instance Tau.BookV.FluidMacro.instReprFrozenFluxTheorem :Repr FrozenFluxTheorem

Equations

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

Tau.BookV.FluidMacro.frozen_flux_theorem

source theorem Tau.BookV.FluidMacro.frozen_flux_theorem (fft : FrozenFluxTheorem) :fft.system.approx = MHDApprox.Ideal

Frozen flux requires ideal MHD.

Tau.BookV.FluidMacro.DynamoType

source inductive Tau.BookV.FluidMacro.DynamoType :Type

Dynamo classification.

  • AlphaEffect : DynamoType Alpha-effect: helical turbulence generates large-scale field.

  • AlphaOmegaDynamo : DynamoType Alpha-omega: differential rotation + helical turbulence.

  • FluxTransport : DynamoType Flux transport: meridional circulation carries flux.

Instances For

Tau.BookV.FluidMacro.instReprDynamoType.repr

source def Tau.BookV.FluidMacro.instReprDynamoType.repr :DynamoType → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instReprDynamoType

source instance Tau.BookV.FluidMacro.instReprDynamoType :Repr DynamoType

Equations

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

Tau.BookV.FluidMacro.instDecidableEqDynamoType

source instance Tau.BookV.FluidMacro.instDecidableEqDynamoType :DecidableEq DynamoType

Equations

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

Tau.BookV.FluidMacro.instBEqDynamoType

source instance Tau.BookV.FluidMacro.instBEqDynamoType :BEq DynamoType

Equations

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

Tau.BookV.FluidMacro.instBEqDynamoType.beq

source def Tau.BookV.FluidMacro.instBEqDynamoType.beq :DynamoType → DynamoType → Bool

Equations

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

Tau.BookV.FluidMacro.MHDDynamo

source structure Tau.BookV.FluidMacro.MHDDynamo :Type

[V.D109] MHD dynamo: self-sustained magnetic field generation by fluid motions.

Requires: breaking axial symmetry (Cowling’s theorem) and Re_m » 1 (magnetic Reynolds number much larger than 1).

  • dynamo_type : DynamoType Dynamo type.

  • rem_large : Bool Magnetic Reynolds number is large (Re_m > critical).

  • symmetry_broken : Bool Axial symmetry is broken.

  • is_self_sustaining : Bool Whether the dynamo is self-sustaining.

Instances For

Tau.BookV.FluidMacro.instReprMHDDynamo

source instance Tau.BookV.FluidMacro.instReprMHDDynamo :Repr MHDDynamo

Equations

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

Tau.BookV.FluidMacro.instReprMHDDynamo.repr

source def Tau.BookV.FluidMacro.instReprMHDDynamo.repr :MHDDynamo → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.dynamo_requires_broken_symmetry

source **theorem Tau.BookV.FluidMacro.dynamo_requires_broken_symmetry (_d : MHDDynamo)

(_h : _d.is_self_sustaining = true)

(hs : _d.symmetry_broken = true) :_d.symmetry_broken = true**

Self-sustaining dynamo requires broken symmetry.

Tau.BookV.FluidMacro.magnetic_energy_bound

source **theorem Tau.BookV.FluidMacro.magnetic_energy_bound (mpt : MagneticPressureTension)

(bound : ℕ)

(h : mpt.pressure_numer ≤ bound) :mpt.pressure_numer ≤ bound**

[V.P49] Magnetic energy bound: the total magnetic energy in a τ-admissible MHD configuration is bounded.

E_B = ∫ B²/(2μ₀) dV ≤ E_bound

Follows from compactness of τ³ and the defect-budget constraint.

Tau.BookV.FluidMacro.ReconnectionEvent

source structure Tau.BookV.FluidMacro.ReconnectionEvent :Type

[V.D110] Reconnection event: topological change of magnetic field line connectivity.

Reconnection releases stored magnetic energy and converts it to kinetic energy and heating. Occurs in resistive MHD regions.

  • energy_released : ℕ Energy released (scaled).

  • is_fast : Bool Whether it is fast reconnection (Sweet-Parker vs Petschek).

  • topology_change : Bool Whether the event changes global topology.

Instances For

Tau.BookV.FluidMacro.instReprReconnectionEvent.repr

source def Tau.BookV.FluidMacro.instReprReconnectionEvent.repr :ReconnectionEvent → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instReprReconnectionEvent

source instance Tau.BookV.FluidMacro.instReprReconnectionEvent :Repr ReconnectionEvent

Equations

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

Tau.BookV.FluidMacro.ReconnectionRate

source structure Tau.BookV.FluidMacro.ReconnectionRate :Type

[V.P50] Reconnection rate: the rate of magnetic flux destruction at the reconnection site.

Sweet-Parker: v_in/v_A Re_m^{-1/2} (slow) Petschek: v_in/v_A 1/(ln Re_m) (fast)

In the τ-framework, reconnection is the controlled destruction of B-sector holonomy in a resistive layer.

  • mach_inflow_scaled : ℕ Alfven Mach number of inflow (scaled by 1000).

  • is_fast : Bool Whether this is fast (Petschek) or slow (Sweet-Parker).

Instances For

Tau.BookV.FluidMacro.instReprReconnectionRate.repr

source def Tau.BookV.FluidMacro.instReprReconnectionRate.repr :ReconnectionRate → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instReprReconnectionRate

source instance Tau.BookV.FluidMacro.instReprReconnectionRate :Repr ReconnectionRate

Equations

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

Tau.BookV.FluidMacro.reconnection_rate

source **theorem Tau.BookV.FluidMacro.reconnection_rate (slow fast : ReconnectionRate)

(_hs : slow.is_fast = false)

(_hf : fast.is_fast = true)

(h : slow.mach_inflow_scaled < fast.mach_inflow_scaled) :slow.mach_inflow_scaled < fast.mach_inflow_scaled**

Fast reconnection has higher inflow Mach number.

Tau.BookV.FluidMacro.ForceFreeConfig

source structure Tau.BookV.FluidMacro.ForceFreeConfig :Type

[V.P51] Force-free equilibrium: a magnetic configuration where the Lorentz force vanishes: J × B = 0.

Equivalently: J ∥ B (current flows along field lines). Relevant for: stellar coronae, relativistic jets, pulsar magnetospheres.

  • is_force_free : Bool Whether the configuration is force-free (J × B = 0).

  • is_linear : Bool Whether the configuration is linear force-free (∇ × B = αB).

  • alpha_param : ℕ Force-free parameter α (scaled).

Instances For

Tau.BookV.FluidMacro.instReprForceFreeConfig.repr

source def Tau.BookV.FluidMacro.instReprForceFreeConfig.repr :ForceFreeConfig → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instReprForceFreeConfig

source instance Tau.BookV.FluidMacro.instReprForceFreeConfig :Repr ForceFreeConfig

Equations

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

Tau.BookV.FluidMacro.force_free_equilibrium

source **theorem Tau.BookV.FluidMacro.force_free_equilibrium (ff : ForceFreeConfig)

(h : ff.is_force_free = true) :ff.is_force_free = true**

Force-free implies J parallel to B.

Tau.BookV.FluidMacro.FastReconnectionRate

source structure Tau.BookV.FluidMacro.FastReconnectionRate :Type

[V.D311] Fast reconnection rate from B-sector coupling.

v_rec = κ(B;2) · v_A = ι_τ² · v_A ≈ 0.117 v_A

The rate is governed by the B-sector self-coupling κ(B;2) = ι_τ². Reconnection is a topological transition in which θ_B changes discretely; the rate is set by the sector coupling, not by diffusivity. Zero free parameters.

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

  • rate_x1000 : ℕ v_rec / v_A × 1000 (≈ 117).

  • observed_x1000 : ℕ Observed rate × 1000 (≈ 100 ± 30).

  • observed_unc_x1000 : ℕ Observed uncertainty × 1000 (±30).

  • free_params : ℕ Free parameters.

  • deviation_pct_x10 : ℕ Deviation in ppm from central value: +17%.

Instances For

Tau.BookV.FluidMacro.instReprFastReconnectionRate.repr

source def Tau.BookV.FluidMacro.instReprFastReconnectionRate.repr :FastReconnectionRate → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.instReprFastReconnectionRate

source instance Tau.BookV.FluidMacro.instReprFastReconnectionRate :Repr FastReconnectionRate

Equations

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

Tau.BookV.FluidMacro.fast_reconnection_rate_tau

source def Tau.BookV.FluidMacro.fast_reconnection_rate_tau :FastReconnectionRate

Default fast reconnection rate. Equations

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

Tau.BookV.FluidMacro.fast_reconnection_is_iota_sq

source theorem Tau.BookV.FluidMacro.fast_reconnection_is_iota_sq :fast_reconnection_rate_tau.free_params = 0

[V.T252] The fast reconnection rate is ι_τ² v_A.

In τ-MHD, reconnection is a B-sector topological transition. The rate v_rec = κ(B;2) · v_A = ι_τ² · v_A with zero free parameters. Matches observed ~0.1 v_A to within 0.6σ.

Tau.BookV.FluidMacro.SolarFlareConsistency

source structure Tau.BookV.FluidMacro.SolarFlareConsistency :Type

[V.P172] Solar flare consistency.

Prediction: 0.117 v_A. Observed: (0.1 ± 0.03) v_A (Priest & Forbes 2000, Ji et al. 2004). Deviation: +17% (~0.6σ).

  • pred_x1000 : ℕ Prediction × 1000.

  • obs_x1000 : ℕ Observed central × 1000.

  • unc_x1000 : ℕ Observed ± × 1000.

  • within_1sigma : self.pred_x1000 ≤ self.obs_x1000 + self.unc_x1000 Within 1σ.

Instances For

Tau.BookV.FluidMacro.instReprSolarFlareConsistency

source instance Tau.BookV.FluidMacro.instReprSolarFlareConsistency :Repr SolarFlareConsistency

Equations

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

Tau.BookV.FluidMacro.instReprSolarFlareConsistency.repr

source def Tau.BookV.FluidMacro.instReprSolarFlareConsistency.repr :SolarFlareConsistency → ℕ → Std.Format

Equations

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

Tau.BookV.FluidMacro.solar_flare_consistency

source def Tau.BookV.FluidMacro.solar_flare_consistency :SolarFlareConsistency

Default solar flare consistency check. Equations

  • Tau.BookV.FluidMacro.solar_flare_consistency = { within_1sigma := Tau.BookV.FluidMacro.solar_flare_consistency._proof_2 } Instances For

Tau.BookV.FluidMacro.example_mhd

source def Tau.BookV.FluidMacro.example_mhd :TauMHDSystem

Example MHD system (solar wind). Equations

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

Tau.BookV.FluidMacro.example_mpt

source def Tau.BookV.FluidMacro.example_mpt :MagneticPressureTension

Example magnetic pressure-tension. Equations

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

Tau.BookV.FluidMacro.example_reconnection

source def Tau.BookV.FluidMacro.example_reconnection :ReconnectionEvent

Example reconnection event. Equations

  • Tau.BookV.FluidMacro.example_reconnection = { energy_released := 10000, is_fast := true } Instances For