pith. machine review for the scientific record. sign in
structure definition def or abbrev high

Params

show as:
view Lean formalization →

Params assembles the six real inputs required by ILG gravity and downstream spiral models: the fine-structure constant, the lag constant equal to phi to the minus five, the active edge count per tick, the reference radius, the pitch parameter, and the disk aspect ratio. Flight-geometry lemmas on log-spiral step ratios and discrete pitch families cite this record to fix scaling. The declaration is a bare structure with no computational body or proof obligations.

claimThe ILG parameter record is the sextuple of real numbers $ (α, C_{lag}, A, r_0, p, h_z/R_d) $, where $α$ is the fine-structure constant, $C_{lag} = φ^{-5}$, $A$ is the active edge count per fundamental tick, $r_0$ is the base radius, $p$ is the pitch, and $h_z/R_d$ is the vertical aspect ratio.

background

Recognition Science fixes the fine-structure constant α_EM inside the narrow interval (1/137.039, 1/137.030) and sets the lag constant Clag to φ^{-5}. The active edge count A is defined as 1, satisfying the φ-power balance identity at D=3: φ^(A−gap)·φ^gap = φ. The reference radius r0 carries sector-dependent φ-exponent offsets that originate in wallpaper and cube geometry rather than being chosen freely. The Gravity.ILG module collects these quantities together with the pitch p and aspect ratio hz/Rd to supply the concrete inputs needed by spiral-field calculations.

proof idea

The declaration is a direct structure definition containing only field declarations and no proof body, tactics, or reduction steps.

why it matters in Recognition Science

This record supplies the parameter tuple used by the Flight.Geometry lemmas on kappa discreteness, per-turn ratio, and closed-form step ratio, as well as by ParamProps inside the same module. It thereby links the mass-anchor constants and the φ-ladder to the discrete pitch families that realize the eight-tick octave. The structure closes the interface between the foundational constants (T5–T8) and the geometric applications that depend on log-spiral scaling.

scope and limits

formal statement (Lean)

  51structure Params where
  52  alpha      : ℝ
  53  Clag       : ℝ
  54  A          : ℝ
  55  r0         : ℝ
  56  p          : ℝ
  57  hz_over_Rd : ℝ
  58

used by (37)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 7 more

depends on (9)

Lean names referenced from this declaration's body.