Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `Cycle, second half`

conditional — 1 open assumptionproofs/Lax771644Proofs/CycleBeta.lean · lax-771644

What this proof establishes

thm×Lax771644.CycleBeta

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

This statement holds if the statement of CycleAlphaCycleAlpha does.

Proof strategy

Apply CycleAlpha.alphaCycleAlpha.alpha verbatim. Circular by design: the converse proof assumes this statement.

Attribution

Synthetic: written for this benchmark. The mathematics is a one-line divisibility weakening; only the shape of the dependency edges is the point.