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

half

show as:
view Lean formalization →

The half-ladder map sends an integer rung k to the rational position k/2 on the phi-ladder. Modules that refine mass ratios or orbital scales with fractional placements cite this convention to maintain uniformity across integer and half-integer assignments. The definition is realized by a direct coercion from integers to rationals followed by division by two.

claimThe half-ladder embedding is the map $k/2$ for $k$ an integer, with the result viewed as a (possibly fractional) rung on the phi-ladder.

background

Rung is the type of rational numbers, introduced to allow fractional placements on the phi-ladder while the core mass model retains integer rungs for rigidity. The module supplies this representation seam so that physics modules exploring quarter- or half-ladder refinements (quark masses, neutrino ladders) share a mechanically uniform convention. Upstream rung definitions in Constants, AnchorPolicy, and RSBridge.Anchor supply the integer assignments that this map halves.

proof idea

This is a definition, not a theorem. It is realized by coercing the integer argument to a rational and dividing by two, with the simp attribute attached for automatic simplification in downstream expressions.

why it matters in Recognition Science

The definition feeds AgreesAtHalfRung and planetaryFormationCert in astrophysics, pleasure_symmetric in aesthetics, and cross_cousin_count in anthropology. It closes the representation seam described in the module doc-comment, allowing the phi-ladder mass formula and T5 J-uniqueness to be applied uniformly to half-integer rungs without altering the integer core.

scope and limits

formal statement (Lean)

  31@[simp] def half (k : ℤ) : Rung := (k : ℚ) / 2

proof body

Definition body.

  32
  33/-- Convert a rational rung to a real exponent (for `Real.rpow`). -/

used by (40)

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

… and 10 more

depends on (9)

Lean names referenced from this declaration's body.