Геометрия пути Евклида: стрела, кривизна и пересечение прямых¶

← 48. Числа Ферма · Оглавление · 50. Кода →

Lean-источник: Engine/GeometryFront — зелёная часть, вся 🟢 (капстоун geometry_of_euclids_path); §6-кода — ровно две декларации, 🟡. Проза-контекст: 01. EPMI, 33. Причина через первопричину, 23. Чистый граф. Обозначения статуса: 🟢 — доказано при стандартных аксиомах; 🟡 — условно на аксиому step00FirstCause; 🔴 — открытый вход.

Где мы¶

Мы построили конкретный граф спуска Step00 — состояния (центры, дефекты, поглотители), рёбра (clean, boundary, peel, absorb) — и провели через него семь великих задач. Всё это время граф был для нас машиной: он ковал свидетелей, платил рангом, убивал двигатели. Теперь посмотрим на ту же конструкцию иначе — не как на механизм, а как на место. У места есть форма. И если путь назван именем Евклида, то честно задать ему три вопроса, с которых началась вся геометрия.

Первый: течёт ли время — есть ли на этом пути направление, различающее «до» и «после», и необратимо ли оно? Второй: какова форма пространства — плоское оно, сферическое, седловидное; и можно ли эту форму не постулировать, а посчитать? Третий, самый древний: пересекаются ли прямые — верен ли на пути Евклида его собственный пятый постулат, есть ли параллельные, сходятся ли все линии в одной точке?

Ответы, как выяснится, читаются прямо с рёбер графа — и каждый из них оказывается не постулатом, а теоремой. А последний ответ переворачивает самого Евклида.

Стрела времени: направление, которое доказано¶

Начнём с времени, потому что без него у геометрии нет ориентации. На пути Евклида роль собственного времени играет lexRank — лексикографический ранг состояния, его «высота» в вполне-упорядоченном ряду. И это время не выбрано, а вычислено: оно строго падает на каждом ребре.

Теорема 49.1 (timeArrow_step, 🟢). Каждый реальный шаг строго уменьшает lexRank: из RealStep A M0 U V следует lexRank V < lexRank U.

Почему это верно. Это реэкспорт несущей теоремы конкретного графа: любой из четырёх конструкторов шага — clean, boundary, peel, absorb — роняет ранг. Из локального факта об одном ребре разворачивается вся кинематика.

Вдоль любого непустого пути ранг строго убывает (timeArrow_path); ни одно состояние не достижимо из самого себя (no_return — время не закольцовано); бесконечного бега не существует вовсе (no_eternal_run — прямое следствие корневого EPMI, no_infinite_descent). И более того — время не просто идёт вперёд, оно ограничено сверху своим стартом:

Теорема 49.2 (every_journey_halts, 🟢). Любой маршрут останавливается не позже, чем за lexRank стартового состояния: k реальных шагов возможны только при k ≤ lexRank (run 0).

Почему это верно. Это квалифицированный «второй закон», проведённый через Engine.turned_engine_halts: строго убывающая на натуральных числах последовательность не может сделать больше шагов, чем её начальное значение.

Стрела времени здесь — не философский образ и не допущение о термодинамике: это теорема о конечном графе, у которой есть точная численная граница. Всякое путешествие по пути Евклида начинается высоко и кончается на дне, и длина его отмерена заранее.

Кривизна, вычисленная: спектр формы пространства¶

Теперь форма пространства. Обычно кривизну задают метрикой и тензорами; у нас метрики нет — есть только рёбра. Но у ориентированного графа есть своя, комбинаторная кривизна, и она считается:

Определение 49.3 (curvature). Кривизна вершины — это κ(v) = 1 − outdeg(v), целое число, где outdeg — исходящая степень, число геодезических сегментов, выходящих из v вниз.

Скажем сразу и громко, как во всех главах программы: это комбинаторная кривизна графа, дефицит или избыток исходящего потока геодезических, аналог формулы Эйлера. Это не риманова кривизна, не секционная, не Ricci–Ollivier; ни метрики, ни тензоров, ни гладкой структуры здесь нет, и слово «кривизна» законно ровно в смысле дискретной теории графов — и только в нём.

Но внутри этого смысла всё честно: out-множество каждой вершины предъявлено как Finset и доказано ровно совпадающим с RealStep (несущая лемма mem_outTargets), так что outdeg считает настоящие рёбра, а не абстракцию.

Почему кривизна ориентирована вперёд — тоже не удобство, а теорема:

Теорема 49.4 (inDegree_infinite_at_origin, 🟢). В исток absorber 0 входит бесконечное семейство рёбер: каждый дефект вида defect 0 q minus по всем q втекает в могилу нуля.

Почему это верно. Absorb-ребро в absorber 0 требует лишь 0 ≤ M0, а таких дефектов бесконечно много. Значит, in-степень истока бесконечна, симметричная «полная степень» не существует как Finset, и неориентированная кривизна невычислима в принципе. Ориентированная κ = 1 − outdeg — единственная вычислимая версия; форма пространства обязана смотреть вперёд, по стреле времени.

А посчитанный спектр — при масштабе (A, M0) = (5, 4), каждое значение проверено ядром через decide — сам по себе есть портрет мира.

Поглотители несут положительную кривизну κ = +1 (curvature_absorber): это полюса, где поток гаснет, где геодезические фокусируются, как меридианы сходятся к точке на глобусе. Дефекты с единственным выходом — плоские коридоры κ = 0 (curvature_defect_0_2, curvature_defect_6_5): труба без ветвления. Дефект (4, 5, +), у которого есть и peel, и absorb, — ветвление κ = −1 (curvature_defect_4_5). А чистые центры — всё более гиперболические воронки: центр 2 даёт κ = −3, центр 3 даёт κ = −4, центр 7 даёт κ = −8 (curvature_center_2, curvature_center_3, curvature_center_7).

Закономерность читается голыми руками: чем выше центр, тем больше дорог ведёт от него вниз, тем отрицательнее кривизна. Генеалогия — гиперболична; дно — сферично. И всю эту картину стягивает дискретный аналог Гаусса–Бонне:

Теорема 49.5 (gaussBonnet_cone3, 🟢). На forward-замкнутом световом конусе под центром 3 полная кривизна равна эйлеровой характеристике: χ(cone3) = Σκ = −5.

Почему это верно. Комбинаторное тождество Σκ = |W| − Σ outdeg (gaussBonnet_sum) на forward-замкнутом окне cone3 (замкнутость проверена ядром, cone3_forwardClosed) даёт −5: два полюса и центр 0 с κ = +1 каждый не перекрывают ветвления воронок −3 и −4. Полная кривизна конуса отрицательна — конус в целом гиперболичен, несмотря на сферическое дно.

Нормировка κ = 1 − outdeg — конечно, выбор, и связь с настоящей формулой Гаусса–Бонне — аналогия, а не теорема дифференциальной геометрии; но внутри выбранной нормировки характеристика посчитана точно, ядром, без единого допущения.

Плоский мир — вечный двигатель: кривизна не украшение, а необходимость¶

Здесь геометрия смыкается с главным запретом программы. Спросим: а могло ли пространство пути Евклида быть плоским всюду — κ ≡ 0, ровным коридором без полюсов? Ответ — нет, и причина глубока.

Теорема 49.6 (nonpositive_curvature_forces_engine, 🟢). Если бы кривизна была нигде не положительна (∀ v, κ(v) ≤ 0), из каждой вершины шёл бы шаг, итерация выбора построила бы бесконечный бег — запрещённый вечный двигатель. Такого мира не существует.

Почему это верно. κ(v) ≤ 0 означает outdeg(v) ≥ 1 — у вершины есть продолжение (hasStep_of_curvature_nonpos). Если так всюду, аксиома выбора склеивает из этих продолжений бесконечную геодезическую, а она есть в точности вечный двигатель Евклида, убитый no_eternal_run. Отсюда — вывод, который стоит выделить:

Теорема 49.7 (space_positively_curved_somewhere, 🟢). Пространство пути Евклида где-то положительно искривлено: ∃ v, 0 < κ(v).

Кривизна здесь не декоративна — она вынуждена. Положительно искривлённая точка (полюс, дно, поглотитель) обязана существовать, иначе спуск не имел бы дна и бежал бы вечно. Форма пространства диктуется не выбором координат, а невозможностью двигателя: у мира должно быть где остановиться.

И замкнутая геодезическая — легальный непустой цикл — тоже была бы двигателем-свидетелем (closedGeodesic_is_engineWitness), уже убитым ацикличностью lexRank (no_closedGeodesic). Плоскость и замкнутость — два лица одной запрещённой машины.

Ирония постулатов: путь Евклида ломает Евклида¶

Теперь третий, самый древний вопрос — о прямых. Определим прямую так, как её и мыслил Евклид: максимальный путь спуска, продолжаемый, пока есть куда шагнуть. И спросим, верен ли на этом пути пятый постулат.

Теорема 49.8 (every_line_ends, 🟢). Каждая прямая упирается в терминал: из любого состояния за конечное число шагов доходишь до вершины без выхода.

Почему это верно. Сильная индукция по собственному времени lexRank v: если v уже терминально — путь пуст; иначе первый шаг строго роняет ранг (стрела времени!), и по индуктивному предположению хвост конечен. Стрела времени напрямую порождает конечность прямых. А отсюда:

Теорема 49.9 (no_infinite_line, 🟢). Бесконечных прямых нет вовсе: никакую прямую нельзя продолжить неограниченно.

И вот подлинная ирония всей программы. Утверждение «прямую можно продолжить неограниченно» — это второй постулат Евклида, тот, что скромнее и древнее знаменитого пятого. На пути Евклида падает именно он (euclid_postulate_two_fails): путь, названный его именем, нарушает его собственную аксиому — и не пятую, о параллельных, а более глубокую, вторую, о самой продолжимости прямой.

Параллельных при этом тоже нет (no_parallel_lines) — но по вырожденной причине: параллельные суть две бесконечные прямые, а не существует уже и одной.

Здесь необходимо быть скрупулёзно честным, и Lean-источник настаивает на этом громче всего. Это вырожденная, а не эллиптическая геометрия. Наивное «все прямые встречаются» ложно:

Теорема 49.10 (bottom_not_unique и two_disjoint_lines, 🟢). Дно не единственно — absorber 0 и absorber 1 оба легальны и терминальны; и существуют две полностью непересекающиеся конечные прямые (при (5,4): маршрут center 7 → defect 4 5 plus → absorber 4 и маршрут center 3 → defect 0 2 minus → absorber 0), все девять состояний которых попарно различны.

Так что «все линии сходятся в одну точку» в лоб — неправда. Есть две разные точки схода и есть пары прямых, не встречающихся нигде. Кто хочет читать вырождение второго постулата как «эллиптичность», обязан читать его через эту честную границу — иначе получится ложь.

Пересечение через могилу нуля¶

Но есть и честная, квалифицированная форма пересечения — и она красивее наивной. Она проходит через единственную особую точку графа.

Теорема 49.11 (zeroPoint_absorbs_all_divisors, 🟢). Точка 0 поглощает все делители: sideValue minus 0 = 6·0 − 1 = 0 в ℕ, а на ноль делится всё; значит любое q делит сторону нуля.

Раскроем это громко, как требует источник: перед нами одновременно артефакт и маркер.

Артефакт — потому что усечённое вычитание в ℕ даёт 6·0 − 1 = 0, тогда как в ℤ было бы −1; мы не утверждаем, что арифметика «знает» это тождество вне ℕ-модели.

Маркер — потому что 0 есть единственная точка, чьи стороны поглощают все делители сразу, единственная, через которую проходимы все дороги вниз; это ℕ-след того самого события 0 → 1 из первопричины, начала стрелы времени. Могила нуля живёт на ℕ-усечении — и она же есть отметка происхождения.

Теорема 49.12 (line_to_origin, 🟢). Из любого чистого центра m ≥ 1 (при 2 ≤ A) есть путь длины 2 в могилу нуля: boundary-шаг в дефект (0, 2, −) — легальный, ибо 2 ∣ 0, — затем absorb в absorber 0.

Две чистые прямые, пришедшие из сколь угодно далёкого верха, встречаются в две ступени в общем дне. И чистые истоки есть над каждым горизонтом:

Теорема 49.13 (web_above_every_horizon, 🟢). Для 2 ≤ A и любого N существует чистый центр m > N, чей путь ведёт в могилу нуля.

Почему это верно. Плотность не нужна — примориальный носитель Residuals.carrier_nonempty_above предъявляет чистый центр выше любой границы, а мост clean_of_cleanZ переводит его чистоту с ℤ на ℕ. Отсюда — единственный законный смысл «прямые пересекаются»:

Теорема 49.14 (lines_meet_at_origin, 🟢). Любые два чистых старта (при 2 ≤ A) имеют общий терминал — могилу нуля absorber 0.

Не «единственную точку схода» и не «пересечение любых путей» — а: у любой пары чистых линий есть общее дно, к которому обе приходят. Все дороги вниз проходят через нуль, и потому все чистые линии там и встречаются.

Пятый постулат опровергнут в честной, а не в наивной форме: прямые пересекаются — на могиле нуля.

Той же аксиомой: пересечение есть, но узнать его изнутри нельзя¶

Остаётся эпистемический итог — и здесь единственные во всей главе жёлтые строки. Всё выше зелено; кода несёт ровно две заражённые декларации, и таинт идёт не через новую аксиому, а через уже принятую причинную границу близнецов (twinLowersInfinite_from_step00CausalClosure), переведённую на язык вершин графа.

Теорема 49.15 (twin_vertices_beyond_every_horizon, 🟡). Над каждым горизонтом есть twin-вершина: для любого N существует twin-центр m > N, обе стороны которого 6m ± 1 просты.

Почему это верно. Мост twinCenter_of_twinLower (сам 🟢, axiom-free) показывает разбором вычета по модулю 6, что младший член любой пары близнецов p > 3 есть 6m − 1 для twin-центра m; а бесконечность близнец-младших — ровно принятая граница. Никакого нового содержания декрета: та же самая аксиома первопричины, что держит бесконечность близнецов, здесь лишь надета на вершины.

Теорема 49.16 (lines_meet_but_unknowable_from_inside, 🟡). Полный итог четырьмя фактами: (1) факт пересечения зелён; (2) twin-вершины есть над каждым горизонтом (эта строка несёт таинт); (3) внутреннего основания факта пересечения нет; (4) будь оно — это был бы запрещённый двигатель Евклида.

Почему это верно. Факт пересечения IntersectionFact доказан зелено (intersectionFact_green — общий терминал есть могила нуля). Но попытка вывести этот факт как внутреннюю первопричину Step00-мира — InternalisedIntersectionGround — по архитектуре есть в точности boundary-crossing self-proof, запрещённый двигатель. Его нет (no_internalisedIntersectionGround, 🟢), и знать бы его изнутри значило построить движок (knowing_meeting_costs_engine).

Более того, само это внутреннее основание тавтологично: оно эквивалентно P ∧ ¬P (internalisedIntersectionGround_iff — раскрыто честно), несущего содержания в нём нет, всё содержание — в зелёном факте.

Итог укладывается в одну фразу: прямые пересекаются, но узнать это изнутри нельзя. Геометрический факт зелен; его внутреннее обоснование стоит вечного двигателя.

У пары близнецов, которую называет эта кода, есть ещё одна зелёная симметрия: флип ±, переставляющий её два члена, ортогонален собственному времени (lexRank_side_invariant, 44) — инволюция при фиксированном времени, не обращение времени. Зафиксировав один близнец, мы ставим его напарника в тот же миг.

Примечание (честные границы, все шесть). Соберём то, что нельзя раздувать.

κ здесь комбинаторная, не риманова, и «кривизна» законна лишь в смысле теории графов.

Гаусс–Бонне — аналогия при выбранной нормировке κ = 1 − outdeg, а не теорема дифференциальной геометрии.

Могила нуля живёт на ℕ-усечении: 6·0 − 1 = 0 в ℕ, но −1 в ℤ.

Наивная эллиптичность ложна: дно не единственно, есть непересекающиеся прямые; верна лишь квалифицированная форма Теоремы 49.14 (lines_meet_at_origin).

Несущая теорема отсутствия параллельных — это падение второго постулата (Теорема 49.9, no_infinite_line), а не пятого; геометрия вырожденная, не эллиптическая.

Кода — ровно две 🟡-декларации, таинт через существующую границу близнецов, без новой аксиомы.

Капстоун geometry_of_euclids_path собирает всю зелёную половину одной теоремой без пользовательских аксиом (ожидаемая тройка: propext, Classical.choice, Quot.sound).

Обобщение: полная кривизна — эйлерова характеристика, и плоского места нет нигде¶

Зелёную половину замкнём обобщением двух её опор — дискретного Гаусса–Бонне (Теорема 49.5) и вынужденной положительности (Теоремы 49.6–49.7) — с одного конкретного конуса и со всего графа на любую forward-замкнутую область.

Теорема 49.17 (gaussBonnet_eq_euler, 🟢). На любом forward-замкнутом окне W полная кривизна равна эйлеровой характеристике: Σκ = |V| − |E| = χ(W), где |E| — число рёбер порождённого подграфа (inducedEdges).

Почему это верно. Комбинаторное тождество Σκ = |W| − Σ outdeg (gaussBonnet_sum) выполнено всегда; forward-замкнутость добавляет ровно то, что превращает правую часть в характеристику: все рёбра из W ведут внутрь W, поэтому Σ outdeg считает в точности внутренние рёбра (forwardClosed_inducedEdges_eq). А раз граф ацикличен (no_closedGeodesic), антипараллельных рёбер нет, направленный счёт совпадает с ненаправленным — и |V| − |E| есть добросовестная эйлерова характеристика 1-комплекса. Это по-прежнему аналогия при нормировке κ = 1 − outdeg (честная граница 1), а не теорема дифференциальной геометрии; но внутри неё χ посчитана точно. Конкретный конус 49.5 — частный случай: eulerChar 5 4 cone3 = −5 (eulerChar_cone3).

Теорема 49.18 (forwardClosed_has_pole, 🟢). В каждой непустой forward-замкнутой области есть полюс: вершина-терминал с κ = +1.

Почему это верно. Из любой вершины окна прямая доходит до терминала за конечное число шагов (every_line_ends), а forward-замкнутость держит весь путь внутри W (pathN_stays_in_forwardClosed), так что и терминал лежит в W; у терминала выходов нет, значит outdeg = 0 и κ = +1 (curvature_one_of_terminal). Это локальная форма Теоремы 49.7: положительная кривизна вынуждена не «где-то во всём графе», а в каждой ограниченной области.

Теорема 49.19 (forwardClosed_not_flat, 🟢). Ни одна непустая forward-замкнутая область не плоская: κ ≤ 0 всюду в ней невозможно.

Почему это верно. Полюс κ = +1 из Теоремы 49.18 противоречит κ ≤ 0. Это локальная форма Теоремы 49.6: плоским не может быть не только весь мир, но и никакой его замкнутый вниз по течению времени кусок — у каждого есть дно.

Так давление на плоское пространство доведено до предела: у существования дно не только глобально, но и в каждой области, замкнутой по ходу стрелы. Кривизна вынуждена не как украшение и не как один-единственный полюс на весь мир, а локально, всюду.

Философское отступление¶

Есть особая горечь и особая красота в том, что путь, названный именем Евклида, нарушает постулат самого Евклида. Двадцать три века геометры бились над пятым постулатом — о параллельных, — и из этой борьбы родились Лобачевский, Риман, вся неевклидова революция. А путь Евклида ломает не пятый, а второй — тот, что казался настолько очевидным, что его почти не замечали: «ограниченную прямую можно непрерывно продолжать».

На вполне-упорядоченном ряду со стрелой времени этот скромный постулат ложен: продолжать вечно нельзя, потому что вечное продолжение и есть запрещённый вечный двигатель. Самая незаметная из аксиом «Начал» оказалась самой хрупкой — и падает она не от смены метрики, а от термодинамики.

В этом, пожалуй, глубочайшая ирония всей программы: мы вернулись к древнейшему доказательному объекту математики, к бесконечному спуску, восходящему к тем же «Началам», — и обнаружили, что он отменяет один из постулатов, с которых «Начала» начинались.

Форма получившегося пространства — не случайна, а узнаваема. Оно закручено внутрь: гиперболическая генеалогия наверху, где каждый центр расщепляется на всё больше нисходящих дорог, и фокусирующее, сферическое дно внизу, где всё стягивается к полюсам-поглотителям.

Это в точности дискретное лицо того перевёрнутого, стягивающегося самоподобия, которое кода назовёт главной формой пути Евклида: классический фрактал разбегается наружу, к бесконечности, а этот — сматывается к началу. Наш посчитанный спектр кривизны — числовой портрет той же спирали: отрицательная кривизна разветвления вверху, положительная кривизна схода внизу, и полная характеристика конуса χ = −5, тянущая к седловине, к воронке, а не к сфере. Геометрия не убегает — она возвращается.

И сшивают эту форму два самых фундаментальных запрета вместе. Стрела времени — необратимость lexRank — задаёт ориентацию: у пространства есть верх и низ, «до» и «после», и назад хода нет. Невозможность двигателя — запрет бесконечного спуска — задаёт завершённость: у формы есть дно, и кривизна обязана где-то стать положительной, чтобы это дно существовало.

Ни одно из этих свойств не постулировано; оба доказаны, и из них двоих вылеплена геометрия. Пространство здесь — не сцена, на которой разыгрывается запрет двигателя, а его тень: направленность, кривизна, конечность прямых, единая точка схода — всё это грани одной невозможности, прочитанной геометрически.

Это ставит путь Евклида рядом с самой смелой программой современной физики — теорией причинных множеств, где пространство-время моделируется как локально конечное частично упорядоченное множество: порядок и есть причинность-время, дискретность и есть пространство. Наш вполне-упорядоченный ряд со строгой стрелой — ровно такой объект.

И самое поразительное здесь — эпистемический предел. Факт, что все чистые прямые встречаются на могиле нуля, зелен и доказуем. Но обосновать этот факт изнутри мира, сделать пересечение внутренней первопричиной самого себя — невозможно, ибо это самозамкнутое обоснование тавтологически есть P ∧ ¬P и стоило бы вечного двигателя.

Знание о форме собственного пространства имеет цену, и цена — запрещена. Наблюдатель внутри пути Евклида может доказать, что прямые сходятся, но не может обосновать это, стоя внутри; обоснование приходит только извне, единственной принятой первопричиной. Геометрия познаваема; её самообоснование — нет. И в этом «нельзя узнать изнутри» живёт та же бесконечность близнецов, что держит всю программу: единственное, что нельзя удостоверить из глубины стягивающегося порядка.

Отсюда — последняя ирония, тоньше постуляционной. Путь Евклида конечен: его второй постулат пал, и всякая прямая обрывается на могиле нуля — ведь бесконечное продолжение и есть запрещённый вечный двигатель. И тот же путь бесконечен — ибо конца ему изнутри не увидеть: удостоверить, что близнецы иссякнут, значило бы завести тот же двигатель, и для идущего внутри дорога всегда тянется дальше. Конечный по термодинамике и бесконечный по незнанию; замкнутый для взгляда извне и разомкнутый для того, кто идёт. Обе истины строги — и живут в одной и той же прямой.

Место в общем ходе¶

Три вопроса Евклиду получили ответы, и все три — теоремы, а не постулаты. Время течёт и необратимо (timeArrow_step, every_journey_halts). Пространство искривлено, и его кривизна посчитана ядром, с положительным дном и гиперболической генеалогией, стянутой формулой Гаусса–Бонне. Прямые конечны — падает второй постулат Евклида, — и все чистые линии встречаются на могиле нуля, хотя узнать это изнутри нельзя.

Зелёную половину бунтует одной теоремой капстоун geometry_of_euclids_path; жёлтую кода несёт ровно двумя декларациями, той же принятой аксиомой близнецов, без нового декрета.

Теперь у нас есть не только семь масок одного запрета, но и форма того места, где все они живут. Стрела, кривизна, точка схода — это уже не свойства отдельной задачи, а свойства самого пространства-времени пути Евклида. Всё готово к последнему шагу: кода (глава 50) соберёт стрелу времени, вынужденную кривизну, стягивающийся фрактал и невозможность самообоснования в единый синтез — прочтение пути Евклида как возможной структуры пространства-времени, где древнейший доказательный объект математики оказывается скелетом самого молодого вопроса физики.

← 48. Числа Ферма · Оглавление · 50. Кода →