residualFraction_pos
plain-language theorem explainer
The theorem asserts that the residual contaminant fraction after any finite number of bioremediation cycles is strictly positive. Engineers modeling PFAS or microplastic degradation under the identity-tick protocol cite it to guarantee that exact zero is never reached in finite steps. The proof is a one-line wrapper that invokes the standard positivity of powers on the already-proven positive reduction factor.
Claim. For every natural number $n$, if $r$ denotes the per-cycle reduction factor then $0 < r^n$.
background
The module treats phantom-cavity bioremediation as an engineering derivation in which the activation barrier drops by the factor $1 - J(phi)$. The reduction factor is the resulting per-cycle multiplier, shown positive by reductionFactor_pos via the bound phi < 1.62. The residual fraction is defined directly as the n-th power of this multiplier, so its positivity follows once the base is known to be positive. The local setting is the theorem track for RS_PAT_041, whose falsifier is a pilot deployment whose observed degradation deviates from the predicted exponential scaling.
proof idea
The proof is a one-line wrapper that applies pow_pos to the already-established positivity of the reduction factor, with the natural-number exponent supplied implicitly.
why it matters
This result supplies the positivity property of the residual fraction required by the identity-tick bioremediation pilot certificate. It closes one link in the engineering derivation that begins from J-uniqueness and the phi fixed-point steps of the forcing chain. The certificate bundles it with the zero-residual limit and band constraints to certify the overall protocol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.