No Syracuse cycle has least period 50275
ProvedCollatzFrontier.syracuse_no_least_period_50275No positive integer has Syracuse orbit with least period exactly : there is no with and for every .
This follows by combining the companion theorem syracuse_least_cycle_distinct_budget with the already-Proved platform baseline syracuse_no_cycle_below_2310000, which forces every state of such a hypothetical cycle to be at least (using that is the unique small periodic point); the resulting distinct-state envelope is then shown to fail by an explicit arithmetic certificate.
This theorem is unconditional on the Prove2Me platform: it relies only on the already-Proved baseline above, imported by name, not re-proved or assumed as an axiom. It excludes only the single isolated least period . It does not raise the global minimal-period lower bound of established by syracuse_period_le_6290_eq_one (equivalently, the open tail starts at syracuse_minimal_period_ge_6291_eq_one), and it does not address any other period or the Collatz conjecture.
Formalization Note. This is a restatement, without the baseline parameter, of the repo's conditional theorem no_least_cycle_50275_of_certified_baseline, which takes the finite-baseline proposition as an explicit function argument rather than an axiom. Since that exact proposition is the proved platform theorem cited above, the published statement here drops the parameter and the solution supplies the proved theorem directly, making the result unconditional given platform content.
import Mathlib import Definitions.Def_syracuseStep
namespace CollatzFrontier
theorem syracuse_no_least_period_50275 (m : ℕ) (hm : 0 < m)
(hcyc : syracuseStep^[50275] m = m)
(hmin : ∀ k : ℕ, 0 < k → k < 50275 → syracuseStep^[k] m ≠ m) : False := by sorry
end CollatzFrontier