Совершенные числа: зелёный Евклид–Эйлер и нечётный свидетель¶
← 46. Гольдбах и Лежандр · Оглавление · 48. Числа Ферма →
Lean-источник:
Engine/PerfectNumberBranch.lean— зелёная ветвь Евклида–Эйлера, вся 🟢 (обе стороны — реэкспорт из mathlib Archive:Theorems100, автор Aaron Anderson, Apache 2.0);Engine/OddPerfectManifestationFront.lean— манифестационный фронт нечётной стороны, аксиомо-свободный, вся 🟢. Проза-контекст: 34. Ветка Мерсенна, 43. Мерсенн через первопричину, 42. Ходж. Обозначения статуса: 🟢 — доказано при стандартных аксиомах; 🟡 — условно на аксиомуstep00FirstCause; 🔴 — открытый вход.
Где мы¶
Глава 34 закончилась теоремой Евклида–Эйлера как обещанием: простые Мерсенна и чётные
совершенные числа — один объект, увиденный с двух сторон, а мост между ними тянется от Евклида к
Эйлеру через всю историю теории чисел. Тогда мы сформулировали это словами прозы; в репозитории же
MersennePrimesInfinite стоял именованным 🔴-входом, а сама совершенность не была ни определена, ни
разрешена машиной.
Глава 43 добавила к нити виток о ставках, но и она оставила совершенные числа ждать: «они ждали Евклида две тысячи лет — подождут и решения».
Эта глава закрывает то, что закрывается, — и не выдаёт за закрытое то, что открыто. Обе стороны теоремы Евклида–Эйлера теперь зелёные в репозитории, машинно, реэкспортом из mathlib. Появилась зелёная эквивалентность, которая связывает старейший открытый вопрос «Начал» ровно с вопросом о простых Мерсенна.
И появился нечётный фронт — тот самый манифестационный двигатель («отклонение обязано проявиться», см. словарь), но с отклонением на другой стороне арифметики, чем у Мерсенна. Ни одна открытая задача при этом не объявлена решённой; новость — про то, что именно стало машинно-проверяемым, и где геометрия проводит границу открытого.
Зелёный Евклид, зелёный Эйлер¶
Начнём с того, что перестало быть только прозой. Обе половины древнейшей теоремы теперь стоят в ветке как доказанные, реэкспортом из архива mathlib — и мы это честно указываем: работа Aaron Anderson по сотне теорем Виджика, лицензия Apache 2.0. Наш вклад здесь — не доказательство, а встраивание в язык программы: связывание с центрами Мерсенна из 34 и с манифестационной архитектурой Римана.
Теорема 47.1 (perfect_of_mersennePrime', 🟢). При 2 ≤ p и простом mersenne p число
2^(p−1) · mersenne p совершенно — направление Евклида, «Начала» IX.36.
Почему это верно. Это ровно та конструкция, что Евклид записал две тысячи триста лет назад:
если 2^p − 1 просто, сумма собственных делителей 2^(p−1)·(2^p−1) в точности равна самому числу.
Мы не переписываем евклидову геометрию сумм — мы берём её проверенную машиной форму из архива и
переводим на p-язык ветки Мерсенна, где 2^p − 1 = 6m_p + 1 — верхняя сторона центра.
Теорема 47.2 (evenPerfect_eq, 🟢). Всякое чётное совершенное число имеет вид 2^k · (2^(k+1) − 1)
с простым множителем Мерсенна — направление Эйлера.
Почему это верно. Эйлер замкнул обратное спустя две тысячи лет: у чётной совершенности нет иной
формы, кроме евклидовой. Отсюда и следует, что простые Мерсенна и чётные совершенные числа — один
объект: каждый простой Мерсенна строит совершенное (Евклид), и всякое чётное совершенное происходит
ровно из простого Мерсенна (Эйлер). Машинно это две стрелки, perfect_of_mersennePrime' и
evenPerfect_eq, и вместе они — вся классическая теорема, зелёная, без единого sorry.
Примечание. Что здесь зелено — и что нет. Зелены обе стороны теоремы Евклида–Эйлера и поточечная разрешимость совершенности:
instance DecidablePred Nat.Perfect, а с ней машинно проверенныеperfect_6,perfect_28. Что чётных совершенных чисел (равно простых Мерсенна) бесконечно много — не утверждается: маркерNoMersenneInfinitudeClaimedстоит документом, что этот вопрос остаётся открытым. Мы закрыли классическую теорему, а не античную задачу о бесконечности.
Эквивалентность, связавшая «Начала» с Мерсенном¶
Теперь — теорема, ради которой ветка и существует как мост. «Начала» задали вопрос, который две тысячи лет остаётся без ответа: продолжаются ли совершенные числа бесконечно? Через Евклида–Эйлера этот вопрос про чётные совершенные оказывается тем же самым, что вопрос о простых Мерсенна, — и теперь это не риторика прозы, а зелёная теорема.
Теорема 47.3 (mersennePrimesInfinite_iff_evenPerfectUnbounded, 🟢). Цель-маркер
MersennePrimesInfinite эквивалентен неограниченности чётных совершенных чисел
(EvenPerfectUnbounded).
Почему это верно. Вперёд — через евклидову конструкцию и оценку роста. Из простого Мерсенна
mersenne p строим совершенное 2^(p−1)·mersenne p (та же Теорема 47.1, perfect_of_mersennePrime'), а
неравенство N < p < 2^p ≤ 2^(p−1)·mersenne p гонит совершенные вверх без потолка: каждый новый
простой Мерсенна даёт совершенное строго больше любого наперёд заданного порога.
Назад — через эйлерову классификацию плюс арифметику Ферма. Неограниченное чётное совершенное
разбирается Теоремой 47.2 (evenPerfect_eq) в форму 2^k·(2^(k+1)−1), а простота числа Мерсенна 2^(k+1) − 1
вынуждает простой показатель — это Nat.prime_of_pow_sub_one_prime (составной показатель дал бы
алгебраический делитель). Оценка 2^k·mersenne(k+1) < 2^(2k+1) показывает, что растущее
совершенное тянет за собой растущий простой показатель.
Вывод. Две открытые проблемы оказались буквально одной, и эта одинаковость — машинно-проверенная.
Стоит остановиться на том, что именно здесь зелено. Не бесконечность — обе стороны ↔ открыты и
останутся открытыми. Зелена сама эквивалентность: доказано, что старейший вопрос «Начал» и
вопрос о простых Мерсенна — не два родственных вопроса, а один и тот же, до последней запятой.
Это в точности честность программы. Мы не сдвинули границу знания ни на шаг — мы показали, что по обе стороны этой границы стоит один и тот же неизвестный.
Нечётный фронт: свидетель-объект и та сторона, где отклонение живёт¶
У чётной стороны, как мы только что видели, есть двигатель в буквальном смысле: perfect_of_mersennePrime'
строит совершенное число из простого Мерсенна. Отклонение — если оно и есть — не может жить здесь:
чётная сторона зелёно-конструктивна и заперта Эйлером в евклидову форму. Значит, если у совершенных
чисел и есть неведомый обитатель, он нечётен. Геометрия знает, какая сторона закрыта.
Нечётный свидетель устроен не как граница Мерсенна (Π-утверждение об отсутствии), а как отклонение Римана — объект-данные: конкретное нечётное совершенное число.
Определение 47.4 (OddPerfectNumber). Тип свидетелей открытой проблемы: подтип
{N // Odd N ∧ Nat.Perfect N} — нечётное число вместе с доказательствами обоих свойств. Гипотеза
«нечётных совершенных нет» (NoOddPerfect) — ровно пустота этого типа
(noOddPerfect_iff_no_witness 🟢).
Сила непредъявимости — того свойства свидетеля, что предъявить его стоило бы вечного двигателя (см. словарь), — здесь сильнейшая из возможных: поточечная разрешимость. Совершенность разрешима, поэтому всякая фальшивка умирает вычислением:
Теорема 47.5 (not_perfect_945, 🟢). 945 — наименьшее нечётное избыточное число — не совершенно
(машинная проверка decide).
Почему это верно. Сумма собственных делителей 945 вычислима, машина её считает и сравнивает —
и 945 не проходит. Любой предъявленный кандидат в нечётные совершенные проверяется тем же
decide; фальшивка не переживёт вычисления. Мы знаем и нижнюю грань домена настоящего свидетеля:
Теорема 47.6 (oddPerfect_ge_101, 🟢). Всякий нечётный совершенный свидетель ≥ 101 — все меньшие
нечётные кандидаты отсеяны машинной проверкой.
Почему это верно. Для каждого нечётного M < 101 разрешимость даёт вердикт ¬ Nat.Perfect M
одним decide; свидетель не может сидеть ниже 101.
Здесь — и вся правда о границах. В литературе известно, что нечётное совершенное, если оно есть,
больше 10^2200; но эта граница не формализована — зелёно у нас только ≥ 101. Мы не
протаскиваем чужой результат под видом своего: предъявить настоящего свидетеля значило бы решить
задачу, открытую с античности, и поточечная проверка малых случаев такого решения не заменяет.
На нечётном фронте закон манифестации устроен чуть иначе, чем у Мерсенна, и это различие
принципиально. У Мерсенна закон приходилось гейтить свидетелем отсутствия — иначе при P = 0 он
взорвался бы. Здесь свидетель — сам объект, и якорь масштаба привязан к самому числу: закон
объект-квантифицирован (∀ W, OddPerfectManifests W), высота отклонения есть само отклонение, и
негейченной взрывной формы просто не существует. Это зеркало Римана, не Мерсенна.
Теорема 47.7 (oddPerfectWitness_carries_engine, 🟢 — читаемая форма). Конкретное нечётное
совершенное число + закон манифестации + сведённые книги на масштабе не ниже самого числа
предъявляют вечный двигатель — как объект, ConcreteEuclideanEngineWitness, до всякого убийства.
Теорема 47.8 (noOddPerfect_of_manifestation_and_boundary, 🟢 — essence). Нет двигателей + принятая
граница + закон манифестации ⟹ нечётных совершенных чисел нет.
Почему это верно. Зеркало римановой и мерсенновской essence-лемм, с тем же стандартом честности.
Гипотетический свидетель W даёт масштаб M0 := W.1. Разрешающая проекция превращает вселенную в
безэнергетически стабильную — это и есть «книги сведены» (см. словарь), — а закон поставляет бесконечную семью потоков — не ex falso (то есть не даровым «из лжи что угодно»), а как
данные. Из коллизии на конечном ключе собирается двигатель-свидетель, и убивает построенный
двигатель именно гипотеза «двигателей нет».
Три гипотезы потребляются по-настоящему, ни одна не декоративна.
Примечание. Контраст раскрыт машинно (
evenSide_constructible🟢): чётная сторона зелёно строится из простых Мерсенна, поэтому отклонение фронта живёт строго на нечётной стороне — там, где за две с половиной тысячи лет не построено ничего. И знак эвристики здесь направлен за отсутствие: квантор закона пробегает ожидаемо пустой тип, закон ожидаемо вакуумно-истинен — точное зеркало RH, а не инвертированный знак Мерсенна.Обратная сторона закона вакуумна, и это вскрыто аудитом. При границе закон ⟺
NoOddPerfect— поле было бы ровно силы старейшей открытой задачи, — и всё же поле не добавлено, намеренно: закон живёт определением (прецедент 43/§16), серийное расширение декрета обесценило бы карантин.Ни одного свободного Prop-поля, свободного гейта или переименованного вывода в модуле нет; аксиом и
sorryнет.
Философское отступление¶
Совершенные числа — старейший объект теории чисел, старше самих простых как предмета изучения. Евклид записал их конструкцию в IX.36 «Начал»; Никомах Герасский окружил их числовой мистикой, расставив по величине как добродетель между избытком и недостатком; и с тех пор человечество ждало Эйлера две тысячи лет, чтобы узнать, что евклидова форма — единственная возможная для чётных. Ни один объект математики не нёс так долго так простую нерешённую загадку.
Загадка эта — про баланс. Совершенное число задаётся условием σ(N) = 2N: сумма всех делителей
ровно вдвое больше самого числа, то есть сумма собственных делителей в точности равна ему. Это
условие сохранения — число в идеальном равновесии со своими же частями, 6 = 1 + 2 + 3,
28 = 1 + 2 + 4 + 7 + 14.
В прочтении заряда из 42 мы читали класс Ходжа как квантованную величину, а
алгебраический цикл — как её оплату. Здесь σ(N) = 2N — это условие сохранения заряда самого
числа: делители должны в сумме оплатить удвоенное число ровно, без излишка и без недостачи.
Избыточное 945 переплачивает; недостаточные числа не добирают; совершенное — в точном балансе.
А отклонение — нечётное совершенное, если оно есть, — было бы неоплаченным зарядом на нечётной стороне, разрывом в вакууме, который манифестационный закон превращает в вечный двигатель. Ровно тот же мотив, что несёт всю причинную линию программы: дисбаланс, которого не может быть там, где книги сведены.
И есть особая уместность в том, что именно эта загадка досталась двигателю, названному в честь Евклида. Чётный угол его старейшей теоремы теперь зелен целиком — конструкция и её единственность. Открытым остаётся один нечётный угол: существует ли нечётное совершенное число.
Это последний незакрытый угол старейшей теоремы Евклида, и геометрия фронта говорит нам о нём больше, чем мы умеем доказать: чётная сторона конструктивна и заперта, отклонение может жить только нечётным, а всякая подделка умирает вычислением. Мы знаем, где искать, знаем, чем это обернулось бы, — и не знаем, есть ли там кто-нибудь. Совершенные числа всё ещё ждут; но теперь видно, у какой именно двери.
Совершенные числа за тем же горизонтом¶
И у этой двери есть эпистемический чертёж. У стены из 39 и
56 — той, о которую разбиваются внутренние решения P/NP и Коллатца, —
обнаружился третий склон, и он падает сюда, в нечётный фронт: Engine/OddPerfectEpistemic.lean,
целиком зелёный модуль, говорит две вещи.
Первая: предъявить нечётного свидетеля — значит предъявить вечный двигатель, и потому свидетель зелёно непредъявим.
Теорема 47.9 (oddPerfectWitness_green_unpresentable, 🟢 — условная). При принятой границе
step00-обязательства и законе манифестации тип нечётных совершенных свидетелей пуст:
\(\text{TheStrictLastStep00Obligation} \to \text{OddPerfectManifestationLaw} \to \neg\,\text{Nonempty}\,\text{OddPerfectNumber}.\)
Условность здесь названа условностью: обе гипотезы
явные — закон манифестации живёт определением (поле не декретировано), граница подаётся снаружи;
предъявленный свидетель при законе и сведённых книгах строил бы двигатель
(Теорема 47.7, oddPerfectWitness_carries_engine), а двигателей зелёно нет (no_someConcreteEuclideanEngine).
Безусловной формы у этого фронта нет и быть не может — она была бы решением самой задачи.
Вторая: самообоснование самоуничтожается. Структура InternalisedOddPerfectGround несёт свидетеля
внутри собственного проверенного горизонта — и машинную развёртку этого самого горизонта,
kernel-факт oddPerfect_horizon_swept 🟢, ровно внутренность доказательства oddPerfect_ge_101.
Из этой пары выводится False — самообоснование в точности ⊥ (no_internalisedOddPerfectGround 🟢):
Теорема 47.10 (oddPerfectCause_unknowable, 🟢). Внутреннее знание причины для нечётных
совершенных чисел невозможно: \(\neg\,\text{InternalKnowledgeOfOddPerfectCause}\) — эквивалентно тому,
что \(\text{InternalisedOddPerfectGround} \to \bot\) (структура, несущая свидетеля внутри собственного
проверенного горизонта, противоречива).
«Узнать нельзя изнутри» — не лозунг, а теорема, зеркало
collatzCause_unknowable и pnpCause_unknowable. Ноги структуры — не логические дополнения друг
друга: противоречие добывается настоящей медиацией, распаковкой свидетеля и переводом нечётности на
язык остатков, и kernel-оплата горизонта входит в само опровержение.
А что остаётся, когда оба внутренних пути заперты? Ровно то, что было: зелёной нижней планкой
остаётся oddPerfect_ge_101 — свидетель, если он есть, не ниже 101, и
no_oddPerfectWitness_below_horizon 🟢 закрывает подвал безусловно.
Сводка
oddPerfect_verification_not_derivation 🟢 добавляет пуант, уникальный для этого фронта: «внешняя
проверка» тут — буквально поточечная разрешимость совершенности, каждый кандидат решается
вычислением, и решение находимо ровно настолько далеко, насколько досчитывает ядро. Итоговый статус
собран в oddPerfect_locked_behind_engine_status 🟢: свидетель ≥ 101 — теорема; внутреннее знание
невозможно — теорема; всё остальное — условно, с гипотезами, оставленными на виду.
Примечание (что мы не утверждаем). Это не решение старейшей открытой задачи математики и не Гёдель: никакой независимости и никакой неподвижной точки — только вычислительный отсев и стена вечного двигателя; вся конструкция — модель-внутренняя эпистемика, и утверждает она невозможность самообоснования, а не (не)существование нечётного совершенного числа.
Третий конъюнкт
oddPerfect_verification_not_derivationклассически тривиален — его машинное содержание в маршруте через разрешающий instance, не в силе утверждения. Модуль не импортирует карантин, не добавляет ни аксиом, ниsorry; таинт репозитория не меняется.
Форма Эйлера: анатомия несуществующего свидетеля¶
До сих пор нечётный свидетель был для нас объектом-загадкой: тип, который может быть пуст, а может и
нет, с зелёной нижней планкой ≥ 101 и стеной вечного двигателя вокруг. Но у этого гипотетического
обитателя есть кое-что, чего не было у мерсенновского свидетеля отсутствия, — проверенная машиной
анатомия. Классическая теорема Эйлера о нечётных совершенных числах теперь зелёная целиком, в
Engine/OddPerfectEulerForm.lean.
Теорема 47.11 (odd_perfect_euler_form, 🟢). Всякое нечётное совершенное n имеет вид n = q^α · m²,
где q простое, q ≡ 1 (mod 4), α ≡ 1 (mod 4) и q ∤ m. В языке свидетеля та же форма —
oddPerfect_euler_form: всякий W : OddPerfectNumber обязан носить именно эту структуру.
Почему это верно. Всё держится на одном наблюдении об арифметике σ(n) = 2n. У нечётного n
двойка входит в правую часть ровно в первой степени, и σ, будучи мультипликативной, раскладывается по
факторизации: σ(n) = ∏_p σ(p^{a_p}). Для нечётного простого p сумма σ(p^a) = 1 + p + … + p^a
состоит из a + 1 нечётных слагаемых — она чётна тогда и только тогда, когда a нечётен. Значит
двойку в σ(n) вносит показатель: он обязан быть нечётным ровно у одного простого делителя.
Лестница из четырёх ступеней разбирает это по косточкам: exists_unique_odd_exponent (ровно один
нечётный показатель — ноль дал бы нечётное σ(n), два дали бы 4 ∣ 2n против нечётности n),
special_prime_one_mod_four (этот особый q сравним с 1 по модулю 4), exponent_one_mod_four
(его показатель α ≡ 1 (mod 4)), и упаковка всех остальных, чётных, показателей в квадрат m².
Остановимся на вычетах, потому что они и есть сердцевина. Почему q ≡ 1 (mod 4)? Будь q ≡ 3
(mod 4), беззнаковое спаривание σ(q^α) = (1 + q)·∑(q²)^j дало бы 4 ∣ σ(q^α) (ведь 4 ∣ 1 + q),
а это гонит 4 ∣ 2n — снова против нечётности. Остаётся q ≡ 1 (mod 4), и тогда σ(q^α) ≡ α + 1
(mod 4) пришпиливает и показатель: α ≡ 1 (mod 4). Mod-4 арифметика фиксирует и простое, и его
степень — двумя короткими счётами.
Вот что здесь ново для арки. Свидетель, которого нельзя предъявлять, обрёл машинно-проверенный
портрет. Всякий будущий охотник за нечётным совершенным числом теперь знает точную форму добычи:
не «какое-то нечётное число», а q^α·m² с q ≡ α ≡ 1 (mod 4).
И к этому портрету примыкают ещё два
зелёных сужения домена (Engine/OddPerfectThreePrimes.lean): никакая степень простого не
совершенна — ни нечётная, ни чётная (not_perfect_prime_pow: σ(p^k) ≡ 1 (mod p), тогда как
2·p^k ≡ 0, откуда p ∣ 1), и всякое нечётное совершенное имеет не меньше трёх различных простых
делителей (odd_perfect_three_le_card_primeFactors, в языке свидетеля oddPerfect_min_three_prime_factors
— через оценку изобилия 2·∏(p−1) ≤ ∏p).
Итог раздела. Три качественных обруча — ≥ 101, ≥ 3 простых, форма
q^α·m² — стягивают домен несуществующего свидетеля с трёх сторон сразу.
Примечание (честность формы). Это не решение задачи и не Гёдель: ни существование, ни несуществование нечётного совершенного числа здесь не утверждается. Все теоремы модуля — безусловная арифметика, оплаченная mathlib-мультипликативностью σ₁ и mod-2/mod-4 счётом; якорей и границ в нём нет. Мы доказали не то, что свидетель есть, а то, какую форму он обязан иметь, если он есть, — классику XVIII века, впервые встроенную в язык программы. Таинт 16 не меняется.
Место в общем ходе¶
Нить, открытая закрывающей репликой 34 и продолженная ставочной честностью 43, получила
машинно-проверенное тело. Обе стороны Евклида–Эйлера зелены реэкспортом; античный вопрос «Начал» о
бесконечности чётных совершенных доказан эквивалентным вопросу о простых Мерсенна
(mersennePrimesInfinite_iff_evenPerfectUnbounded); а нечётная сторона проведена через
манифестационную архитектуру Римана — с отклонением-объектом, поточечной разрешимостью подделок и
раскрытым контрастом: закрыт чётный угол, отклонение живёт на нечётном.
И ровно то, чего эта глава не сделала, — её главная честность. Бесконечность простых Мерсенна (а
значит, и чётных совершенных) не утверждается — обе стороны зелёной эквивалентности открыты.
Существование нечётного совершенного числа не решено — зелено лишь ≥ 101, а литературная граница
> 10^2200 не формализована. Манифестационное поле нечётной стороны, как и мерсенновское, допустимо
по машинному критерию, но не взято — по тому же вердикту против серийности декрета.
twin_prime_conjecture остаётся sorry; таинт карантина не сдвинут; ни одна открытая задача не
объявлена решённой.
Закрыта — машинно и с открытыми глазами — только та классическая теорема, что была теоремой уже у Евклида и Эйлера. Загадка их совершенных чисел ждёт дальше, теперь у одной, ясно указанной, нечётной двери.