residualFraction
plain-language theorem explainer
The definition sets the residual contaminant fraction after n cycles equal to the per-cycle reduction factor raised to the power n. Engineers applying the Identity-Tick Bioremediation Pilot would cite it to track exponential decay of PFAS or microplastics under the Recognition Science J-cost model. It is introduced as a direct power definition that inherits all algebraic properties of real exponentiation from the upstream reductionFactor.
Claim. Let $r = 5/2 - phi$. The residual contaminant fraction after $n$ cycles is $r^n$.
background
In the Identity-Tick Bioremediation Pilot module the per-cycle degradation multiplier is supplied by reductionFactor, defined as 5/2 - phi and equal to 1 - J(φ). The upstream doc-comment states: 'The J-cost reduction factor: 1 - J(φ) = 1 - (φ - 3/2) = 5/2 - φ'. This places the construction inside the Recognition Science forcing chain at the J-uniqueness step (T5) and the self-similar fixed point phi (T6), with the eight-tick octave supplying the discrete cycle count n.
proof idea
One-line definition that directly sets residualFraction n to reductionFactor ^ n.
why it matters
The definition supplies the explicit exponential form required by the master certificate IdentityTickBioremediationPilotCert and by the one-statement theorem bioremediation_one_statement. It closes the engineering derivation track J8 by converting the abstract J-cost reduction into a concrete residual that is strictly anti-monotonic and positive for n > 0, directly linking to the module falsifier of degradation inconsistent with (1 - J(φ))^n scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.