residualFraction_zero
plain-language theorem explainer
The residual contaminant fraction after zero cycles equals one by the power definition. Bioremediation engineers cite this base case to anchor the exponential decay model in the identity-tick pilot protocol. The proof is a one-line wrapper that unfolds the definition and simplifies the zero-exponent identity.
Claim. Let $r(n) = ρ^n$ denote the residual contaminant fraction after $n$ cycles, where $ρ$ is the per-cycle reduction factor. Then $r(0) = 1$.
background
In the Identity-Tick Bioremediation Pilot the residual fraction after $n$ cycles is defined by unfolding to the $n$-th power of the reduction factor, which the module identifies with $(1 - J(φ)) ≈ 0.882$. This supplies the exponential decay law for PFAS and microplastic degradation under repeated phantom-cavity treatments that lower the activation barrier from $E_a$ to $E_a · (1 - J(φ))$. The upstream definition is exactly residualFraction n := reductionFactor ^ n.
proof idea
The proof is a one-line wrapper that unfolds residualFraction and applies simp to reduce the zero-exponent case to the identity 1 = 1.
why it matters
This base case is invoked by the bioremediation_one_statement theorem, which packages the reduction band, the zero-residual identity, and strict anti-monotonicity into a single engineering claim. It also supplies the residual_zero field of the IdentityTickBioremediationPilotCert structure. The declaration closes the n = 0 anchor for track J8 of the Recognition Science engineering derivation, where the reduction factor itself traces to J-uniqueness and the phi fixed point; the module falsifier remains empirical inconsistency with the $(1 - J(φ))^n$ scaling beyond 5σ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.