residualFraction_succ
plain-language theorem explainer
Engineers modeling PFAS degradation in the identity-tick bioremediation pilot rely on this relation to iterate residual fractions cycle by cycle. It shows that the fraction after n+1 cycles equals the prior fraction multiplied by the fixed reduction factor 5/2 - phi. The short proof unfolds the power definition and invokes the successor rule for exponents.
Claim. For every natural number $n$, the residual fraction after $n+1$ cycles satisfies $r_{n+1} = r_n · ρ$, where $r_n = ρ^n$ and $ρ = 5/2 - φ$ is the J-cost reduction factor.
background
In the Identity-Tick Bioremediation Pilot the reduction factor is defined as 5/2 - phi, which equals 1 - J(φ) and supplies the per-cycle multiplier ≈0.882. The residual fraction after n cycles is then defined as the nth power of this factor, producing the exponential decay (1 - J(φ))^n that appears in the module doc-comment for track J8 of Plan v5.
proof idea
The proof first unfolds the definition of residualFraction, exposing the power expression. It then rewrites using the pow_succ lemma from Mathlib, which states that a^{n+1} equals a^n times a.
why it matters
This supplies the recursive step that feeds the identityTickBioremediationPilotCert collecting the engineering properties. It fills the scaling relation in the J8 derivation where the per-cycle factor (1 - J(φ)) produces residual (1 - J(φ))^n. The result rests on T5 J-uniqueness and T6 phi fixed-point forcing from the upstream chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.