pith. sign in
module module high

IndisputableMonolith.Astrophysics.CoronalLyapunovTime

show as:
view Lean formalization →

The CoronalLyapunovTime module fixes the reference Alfvén-crossing timescale at the RS-native unit of one tick and introduces the coronalTime function together with its basic monotonicity and ratio properties. Solar physicists working inside the Recognition Science framework cite these objects when modeling Lyapunov times for coronal loops or flux tubes. The module is entirely definitional, consisting of a reference constant, a recursive time function, positivity and increase lemmas, and a certification structure.

claim$τ_{ref} = 1$ (Alfvén-crossing time in RS-native ticks). Define $t_{cor}(n)$ recursively on $ℕ$ with $t_{cor}(0) = τ_{ref}$ and successor ratios fixed by framework constants; the module also supplies $CoronalLyapunovCert$ as a structure witnessing the Lyapunov time.

background

The module imports the fundamental RS time quantum $τ_0 = 1$ tick from IndisputableMonolith.Constants. It sets referenceTime to the Alfvén-crossing timescale at this unit value. The remaining declarations introduce coronalTime as a function on natural numbers, together with lemmas establishing positivity, strict monotonicity, and adjacent ratios, plus the CoronalLyapunovCert structure.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the timescale primitives required by coronal Lyapunov calculations in the Recognition Science astrophysics layer. It extends the time quantum declared in Constants and provides the base objects referenced by later certification steps for solar corona dynamics.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)