residualFraction_strict_anti
plain-language theorem explainer
The theorem shows that the residual contaminant fraction after m cycles is strictly smaller than after n cycles for any natural numbers n < m. Environmental engineers modeling PFAS degradation under the Identity-Tick Bioremediation Pilot would cite this to establish exponential decay. The proof is a direct one-line wrapper that unfolds the power definition and invokes the standard inequality for bases in (0,1).
Claim. Let $r$ denote the per-cycle reduction factor satisfying $0 < r < 1$. For natural numbers $n < m$, the residual fraction after $m$ cycles is strictly less than after $n$ cycles: $r^m < r^n$.
background
In the Identity-Tick Bioremediation Pilot the residualFraction is defined by residualFraction n := reductionFactor ^ n, where reductionFactor equals the per-cycle degradation factor 1 - J(φ) and lies in (0.87, 0.89). The upstream theorems reductionFactor_pos and reductionFactor_lt_one establish that this base is positive and strictly less than one. The module derives engineering consequences from Recognition Science, with per-cycle reduction (1 - J(φ)) ≈ 0.882 and residual fraction scaling as (1 - J(φ))^n.
proof idea
The proof is a one-line wrapper. It unfolds the definition of residualFraction to obtain reductionFactor^m and reductionFactor^n, then applies the lemma pow_lt_pow_right_of_lt_one₀ using reductionFactor_pos, reductionFactor_lt_one, and the hypothesis n < m.
why it matters
This result supplies the strict anti-monotonicity clause inside bioremediation_one_statement, which consolidates the pilot's key properties into a single assertion. It confirms the exponential decay of residuals predicted by the RS framework under J-uniqueness and the phi-ladder. The declaration closes part of engineering track J8 by linking the J-cost reduction to measurable degradation rates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.