Support Rung Fractions

The quarter-ladder seam

In Recognition Science, particle masses are thought to sit on a ladder of steps, each step a power of the golden ratio φ ≈ 1.618. The core mass model uses only whole-number steps, which keeps the formal reasoning rigid. But some physics modules, especially those exploring quark masses and neutrino refinements, want to test placements between the whole steps, such as a quarter of the way up. Support rung fractions is the convention file that makes those fractional placements explicit and uniform.

Think of a ruler marked in whole inches. The core model measures only at the inch marks. The fractional-rung file adds tick marks at quarter and half inches, so a module can say a particle sits at the 1.25 mark rather than rounding to 1 or 2. The file defines a rung (a step on the ladder) as a rational number, embeds whole-number rungs into that system, and provides two standard embeddings: the quarter-ladder, mapping integer k to k/4, and the half-ladder, mapping k to k/2. It also converts a rational rung to a real exponent for use in power calculations.

The file is deliberately modest about what it proves. Its two theorems, quarter_eq and half_eq, merely state that the quarter and half embeddings equal their defining fractions. That is a convention made explicit, not a discovery. The docstring is unambiguous: this is not yet a proof that fractional rungs are canonical. It is a representation seam, a way to keep different modules speaking the same language while exploring ratios that whole steps cannot express.

In Recognition Science, the framework's library of formal theorems keeps the integer-rung core rigid while this seam lets exploratory physics modules test finer placements. The practical payoff is modularity: a quark-mass model can experiment with quarter-ladder positions without rewriting the core mass ladder or weakening its formal guarantees. The cost is honesty about status, the fractional placements remain an exploration tool, not a derived result.

/-- A (possibly fractional) rung on the φ‑ladder. -/
abbrev Rung := ℚ

/-- Embed an integer rung into a rational rung. -/
@[simp] def ofInt (z : ℤ) : Rung := (z : ℚ)

/-- The quarter‑ladder embedding: `k ↦ k/4`. -/
@[simp] def quarter (k : ℤ) : Rung := (k : ℚ) / 4

/-- The half‑ladder embedding: `k ↦ k/2`. -/
@[simp] def half (k : ℤ) : Rung := (k : ℚ) / 2

theorem quarter_eq (k : ℤ) : quarter k = (k : ℚ) / 4 := rfl

theorem half_eq (k : ℤ) : half k = (k : ℚ) / 2 := rfl

What this page does not claim

Fractional rungs are a proven feature of the mass ladder. The quarter-ladder is the unique or preferred fractional embedding. This file derives any particle mass value.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Support/RungFractions.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: