r_0
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.