MarsAtmosphereJCostScheduleCert
plain-language theorem explainer
The Mars atmosphere J-cost schedule certificate structure collects the positivity, phi-multiplicative recurrence, and strict monotonicity of the CO2 release rate along with the zero, recurrence, nonnegativity, and monotonicity properties of the cumulative release sum. Engineers working on J-cost optimal Mars terraforming timelines cite this as the complete verified schedule. It is introduced as a structure definition whose fields are populated by the individual release rate and cumulative sum lemmas.
Claim. A certificate structure for the Mars CO₂ release schedule asserting that the rate function $r(n) := r_0 φ^n$ (with $r_0 = 1$) satisfies $r(0) = r_0$, $r(n) > 0$, $r(n+1) = r(n) φ$, and is strictly increasing, while the cumulative function $C(n) := ∑_{k=0}^{n-1} r(k)$ satisfies $C(0) = 0$, $C(n+1) = C(n) + r(n)$, $C(n) ≥ 0$, and is strictly increasing.
background
The module models Mars terraforming as a J-cost optimal CO₂ release schedule with release rate $r(t) = r_0 φ^{t/45}$, where the 45-year gap corresponds to one phi-rung. Release rate is defined as $r(n) = r_0 φ^n$ and cumulative release as the finite sum $C(n) = ∑_{k=0}^{n-1} r(k)$. These functions are shown to obey the geometric progression and summation identities required by the Recognition Composition Law.
proof idea
The declaration is a plain structure definition with eight fields. Each field directly encodes one required property of the releaseRate or cumulativeRelease functions. The downstream instantiation marsAtmosphereJCostScheduleCert populates the structure by referencing the separate lemmas that establish rate_zero, rate_pos, rate_succ, rate_strict_mono, cumulative_zero, cumulative_succ, cumulative_nonneg, and cumulative_strict_mono.
why it matters
This structure supplies the master certificate for the Mars atmosphere J-cost schedule in the engineering derivation track. It is used by the downstream marsAtmosphereJCostScheduleCert definition to assemble the full set of invariants. The certificate verifies the geometric release schedule against the phi-ladder and J-uniqueness from the forcing chain, closing the J2 track of Plan v5. It leaves open the alignment of the 45-year rung spacing with actual Martian climate response times.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.