pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Astrophysics.SolarWindFromPhiLadder

show as:
view Lean formalization →

The module defines types and functions for solar wind speeds at adjacent rungs of the phi-ladder. Astrophysicists modeling solar phenomena in Recognition Science would cite these to relate observed speeds to the ladder structure. It consists entirely of type declarations, speed assignments, and a certification predicate with no proof content.

claimLet SolarWindType be the inductive type classifying solar wind at phi-ladder rungs. Define solarWindSpeed : SolarWindType → ℝ to assign speeds at each rung, solarWindSpeedRatio to compute the ratio between adjacent rungs, and SolarWindCert as the predicate certifying valid assignments.

background

Recognition Science places physical quantities on the phi-ladder whose rungs differ by integer powers of φ, the self-similar fixed point forced at T6. The upstream Constants module supplies the base time quantum τ₀ = 1 tick. This module extends the ladder to solar wind by introducing SolarWindType to label adjacent speed classes, together with the speed map and a certification predicate that enforces consistency with the ladder spacing.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the solar-wind interface for the Astrophysics domain, linking observed flow speeds to the phi-ladder mass formula and the eight-tick octave. It prepares definitions that later results in the framework can use to connect solar wind ratios to the J-uniqueness relation at T5 and the three spatial dimensions fixed at T8.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)