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

r_0

show as:
view Lean formalization →

r_0 fixes the year-zero CO₂ release rate to 1 in RS-native units for the Mars J-cost terraforming schedule. Engineers working on phi-scaled release timelines cite this constant to anchor the geometric progression r(n) = r_0 * phi^n. The definition is a direct assignment with no supporting lemmas or computations.

claim$r_0 = 1$, where $r_0$ is the initial release rate at year 0 in the Mars atmosphere J-cost schedule.

background

The module derives a J-cost optimal schedule for Mars CO₂ release. Release rate follows r(t) = r_0 · φ^(t / 45) with 45-year gaps per φ-rung; total release over n rungs is the geometric sum r_0 · 45 · (φ^n - 1)/(φ - 1). J-cost is the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Local setting: Mars terraforming via CO₂ release follows a J-cost-optimal schedule with the stated rate and sum formulas. Upstream rung definitions assign integer levels to fermions, ore classes, and anchor sectors on the phi-ladder, supplying the scaling basis.

proof idea

Direct constant definition by assignment of the value 1. No lemmas or tactics are applied.

why it matters in Recognition Science

This constant supplies the base value for releaseRate and the MarsAtmosphereJCostScheduleCert structure that certifies positivity, strict monotonicity, and geometric growth. It implements the initial condition for the geometric sum identity in the J2 track of Plan v5. The construction connects to the phi fixed point (T6) and eight-tick octave from the forcing chain.

scope and limits

Lean usage

def exampleRelease (n : ℕ) : ℝ := r_0 * phi ^ n

formal statement (Lean)

  38def r_0 : ℝ := 1

proof body

Definition body.

  39
  40/-- Release rate at φ-rung `n`. -/

used by (13)

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

depends on (5)

Lean names referenced from this declaration's body.