residualFraction_lt_one_of_pos
plain-language theorem explainer
The theorem shows that the residual contaminant fraction after any positive integer number of bioremediation cycles is strictly less than one. Engineers modeling PFAS or microplastic degradation in identity-tick pilots would cite the bound to confirm that repeated cycles produce net reduction. The proof unfolds the power definition and invokes the standard inequality for a positive base strictly below one raised to a positive integer exponent.
Claim. Let $n$ be a natural number satisfying $ngeq 1$. Then the residual contaminant fraction after $n$ cycles is strictly less than 1.
background
The Identity-Tick Bioremediation Pilot treats phantom-cavity remediation as repeated application of a per-cycle reduction factor derived from the J-cost function. The residual fraction after $n$ cycles is defined as this factor raised to the power $n$. Upstream results establish that the reduction factor lies strictly between 0 and 1 by applying bounds on the golden ratio phi.
proof idea
The proof unfolds the definition of residualFraction to obtain the power expression. It then applies pow_lt_one₀, feeding in the positivity of the base from reductionFactor_pos, the strict upper bound from reductionFactor_lt_one, and using omega to verify that the exponent is at least one.
why it matters
The result supplies a required strict inequality to the identityTickBioremediationPilotCert definition. It completes one step in the engineering derivation for track J8, confirming that the exponential decay drives residuals toward zero under the stated conditions. The module falsifier remains a pilot-scale observation of degradation rates inconsistent with the predicted scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.