reductionFactor_lt_one
plain-language theorem explainer
The reduction factor in the identity-tick bioremediation model is strictly less than one. Engineers and modelers cite this bound to guarantee that residual contaminant fractions contract after each cycle. The proof unfolds the definition 5/2 - phi and applies the lower bound phi > 1.5 via linear arithmetic.
Claim. The J-cost reduction factor satisfies $5/2 - phi < 1$.
background
The Identity-Tick Bioremediation Pilot defines the per-cycle degradation factor as reductionFactor := 5/2 - phi. This equals 1 - J(phi), where J is the Recognition cost function, and multiplies the residual fraction after n cycles to give (5/2 - phi)^n. The module derives the factor from the activation barrier reduction E_a to E_a · (1 - J(phi)).
proof idea
The term proof unfolds reductionFactor to 5/2 - phi, invokes the lemma phi_gt_onePointFive to obtain phi > 1.5, and closes the arithmetic comparison with linarith.
why it matters
This theorem supplies the factor_lt_one field inside identityTickBioremediationPilotCert. It is required by residualFraction_lt_one_of_pos and residualFraction_strict_anti to establish strict contraction of the residual fraction. The result aligns with the phi-ladder and T5 J-uniqueness in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.