Lemma: Agent20_CollatzRound2_01a13459_E20_V2.reverse_family_certificate
If a positive base r grows by step ell and its affine coefficient is at least 2^ell, then every lifted image has a positive smaller ell-step predecessor. Explicit base/coefficient hypotheses.
Exact formal statement
∀ (r ell a : Nat),
LT.lt.{0} 0 r →
LT.lt.{0} r (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter r ell) →
LE.le.{0} (HPow.hPow.{0, 0, 0} 2 ell) (Agent20_CollatzRound2_01a13459_E20_V2.Core.coeff r ell) →
And
(Eq.{1}
(Agent20_CollatzRound2_01a13459_E20_V2.Core.iter
(HAdd.hAdd.{0, 0, 0} r (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 ell) a)) ell)
(HAdd.hAdd.{0, 0, 0} (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter r ell)
(HMul.hMul.{0, 0, 0} (Agent20_CollatzRound2_01a13459_E20_V2.Core.coeff r ell) a)))
(And (LT.lt.{0} 0 (HAdd.hAdd.{0, 0, 0} r (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 ell) a)))
(LT.lt.{0} (HAdd.hAdd.{0, 0, 0} r (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 ell) a))
(HAdd.hAdd.{0, 0, 0} (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter r ell)
(HMul.hMul.{0, 0, 0} (Agent20_CollatzRound2_01a13459_E20_V2.Core.coeff r ell) a))))This is a published formal lemma. Its scope is the exact statement above.
Environment availability: available.