identityTickBioremediationPilotCert
plain-language theorem explainer
Engineers modeling PFAS and microplastic degradation under Recognition Science cite this definition for the certified per-cycle reduction factor and residual scaling. It packages the interval 0.87 < r < 0.89 on r together with the power-law properties of the residual fraction f(n) = r^n. The construction is a direct structure instantiation that references eight sibling lemmas establishing positivity, bounds, normalization, and recurrence.
Claim. Let $r$ be the per-cycle reduction factor satisfying $0 < r < 1$ and $0.87 < r < 0.89$. Define the residual contaminant fraction by $f(n) := r^n$ for $n : ℕ$. The certificate asserts $f(0) = 1$, $f(n) > 0$ for every $n$, $f(n) < 1$ whenever $n ≥ 1$, $n < m$ implies $f(m) < f(n)$, and $f(n+1) = f(n) · r$.
background
The module develops an engineering application of the J-cost to phantom-cavity bioremediation (RS_PAT_041). It accelerates degradation of PFAS, microplastics and POPs by lowering the activation barrier from $E_a$ to $E_a · (1 - J(φ))$, yielding a per-cycle factor $r ≈ 0.882$. The structure IdentityTickBioremediationPilotCert collects the minimal mathematical properties needed to certify this scaling: bounds on $r$ and the listed algebraic and ordering facts for the residual $f(n) = r^n$ (defined via reductionFactor ^ n in the sibling residualFraction). Upstream lemmas reductionFactor_pos, reductionFactor_lt_one and reductionFactor_band establish the interval on $r$ from the standard bounds phi_gt_onePointSixOne and phi_lt_onePointSixTwo; the residualFraction_* theorems then lift these to the power properties via pow_pos and pow_lt_one₀.
proof idea
The definition constructs an instance of IdentityTickBioremediationPilotCert by direct field assignment. It supplies reductionFactor_pos for factor_pos, reductionFactor_lt_one for factor_lt_one, reductionFactor_band for factor_band, residualFraction_zero for residual_zero, residualFraction_pos for residual_pos, residualFraction_lt_one_of_pos for residual_lt_one_pos, residualFraction_strict_anti for residual_strict_anti, and residualFraction_succ for residual_succ. No additional tactics or reductions are performed.
why it matters
This definition closes the engineering derivation for Track J8 of Plan v5. It supplies the concrete certificate that the per-cycle degradation factor lies in the stated band and that residuals decay exactly as $r^n$, thereby operationalizing the J-uniqueness (T5) and phi-ladder for remediation modeling. The module doc states the falsifier: pilot-scale data showing degradation inconsistent with $(1 - J(φ))^n$ scaling beyond 5σ. No downstream uses appear yet, but the structure is the required interface for any later application of the Recognition Composition Law to activation-barrier reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.