К основному содержимому
Исследование

Порядок математики

Почему в доказательстве формулы Коши, связывающей значение функции с интегралом по контуру, понадобилась теорема о компактности? В разобранном здесь доказательстве компактность помогает построить окрестность всей замкнутой области, в которой можно стянуть контур. Короткая ссылка на соседний результат скрывает этот математический переход. Чтобы понять его, нужно открыть опору, проверить условия и вернуться к исходной цели.

Авторский Порядок Nareshka собирает 14 выбранных разделов математики и их внешние основания в общую карту. Читатель видит место результата в этой области и может обратиться к тексту его опор. Статья прослеживает, как из формулировок, доказательных отношений и решений о составе корпуса получается такое расположение. Мы разберем конкретные переходы, объясним расчет порядка и выясним, что карта помогает найти, а что остается проверять по математическому тексту.

14 разделов Порядка967 кандидатов композиции1 230 записей полного корпуса
01
Замысел

Математика становится Порядком.

14выбранных разделов

Порядок задает выбранную область чтения. От расположения разделов читатель может перейти к точной формулировке и к записанным опорам.

От результата к его основаниям

Среди записанных опор теоремы Коши об интегральной формуле в Порядке есть теорема Гейне-Бореля о компактности. Два названия еще не объясняют переход. Что именно дает компактность в доказательстве формулы? В сохраненном доказательстве компактность позволяет выбрать конечное подпокрытие: из множества малых окрестностей выбрать конечный набор, который все еще покрывает нужную область. Как этот шаг помогает доказать интегральную формулу, мы разберем в главе о чтении. Уже сейчас виден исходный вопрос: какое основание работает здесь и почему его условия подходят?

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

В авторском Порядке Nareshka, режиме математического графа на странице /knowledge-graph/math, выбранный материал разложен по 14 разделам. Перед ними расположен опорный фундамент с записями из других областей. Общий вид остается ориентиром, пока читатель открывает отдельный результат и разбирает его основания. Статья объясняет эту композицию и работу с ней. Основная демонстрация проходит в Порядке; общая сеть нужна для дополнительных исследовательских проекций.

Каждая точка адресует математическую запись: отдельный текст о теореме, определении, алгоритме или семействе вариантов. Что именно считать математическим объектом, нужно установить по содержанию записи. Папка сообщает его предметную принадлежность. Связь между записями может обозначать опору, использование или обычную ссылку. Линия помогает найти текст; условия и шаг применения объясняют его роль в аргументе.

Что входит в эту композицию

Числа состава в этой статье относятся к индексу msc2020, опубликованному 12 октября 2026 года в 18:13:46 UTC и пересчитанному 13 октября. Живая публикация может измениться; глава методов сохраняет точный вход расчета и правила счета.

Полный математический корпус этого снимка содержит 1230 файловых записей в 53 папках. Четырнадцати выбранным разделам принадлежат 914 записей. Еще 53 записи из 18 внешних папок входят в опорный фундамент. Эти группы не пересекаются: внутренние записи остаются в выбранных разделах, внешние вынесены в пролог. Вместе они дают состав кандидатов Порядка:

914+53=967.914 + 53 = 967.

Единица этого счета - файловая математическая запись. Оставшиеся 263 записи, 1230 - 967 = 263, сохраняются в полном корпусе за пределами этой выборки. Они не вошли в Порядок по действующему правилу отбора; из этого не следует решение об их математической важности или правильности.

Область авторского Порядка

Выбранные разделы и внешний фундамент вместе образуют область Порядка. Остальные записи сохраняются в полном корпусе.
ОбластьЗаписейСмысл
14 выбранных разделов914Авторская основная область
Внешний фундамент53Внешняя часть записанного контекста опор
Вне последовательности263Остальной опубликованный корпус
Всего опубликовано1 230Файловые записи корпуса

Разложение на рисунке показывает, как выбранный материал соотносится с полным корпусом. У двух чисел 53 разные единицы: 53 папки всего корпуса и 53 внешние записи фундамента. Последние приходят из 18 папок, сохраняя свою предметную принадлежность. Фундамент не превращает эти папки в дополнительные основные разделы и не образует пятнадцатую математическую дисциплину.

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

Четырнадцать разделов как авторская область

Состав разделов задан авторским списком. Алгоритм получает выбранную область и располагает материал внутри нее; размеры папок и центральность узлов не определяют, какие дисциплины включить. Предпочтительный исходный порядок тоже принадлежит авторской композиции; алгоритм согласует расположение глав с записанными связями и использует это предпочтение при неоднозначности. Таблица показывает итоговый опубликованный порядок всех 14 разделов и число записей в каждом.

14 разделов в опубликованном порядке

Порядок сохраняет каждый раздел отдельной целой панелью. Слои и полка описывают расположение записей внутри нее; фундамент образует отдельный пролог.
ПозицияРазделЗаписейСлоевЗаписей на полке
1Математическая логика и основания82911
2Вещественные функции84125
3Линейная и полилинейная алгебра67107
4Мера и интегрирование5093
5Функциональный анализ5884
6Теория вероятностей и случайные процессы108826
7Комбинаторика120556
8Выпуклая и дискретная геометрия4664
9Статистика61523
10Теория информации и коммуникации5359
11Компьютерные науки54326
12Вариационное исчисление и оптимальное управление2671
13Исследование операций математическое программирование26413
14Численный анализ79348

В таблице есть два признака внутренней раскладки. Число слоев показывает, сколько уровней имеет лента раздела по направленным файловым связям внутри панели. Связи с другими разделами в этот локальный расчет не входят. На полке размещены записи, не участвующие ни в одном учитываемом внутрипанельном файловом ребре. У них могут быть основания или применения в других разделах; положение на полке само по себе не делает материал факультативным. Визуальный язык объяснит, как читать эти признаки, а композиция - как они вычислены.

Содержательная классификация помогает понять, какие вопросы объединяет эта область. Логика дает язык условий и утверждений. Комбинаторика и компьютерные науки добавляют дискретные конструкции и алгоритмы. Алгебра, анализ и мера позволяют говорить о пространствах, функциях и интегралах. Вероятность, статистика и информация ведут к случайности, оцениванию и ограничениям вывода. Геометрия, оптимизация, управление и численные методы обращаются к выбору решений и вычислению. Так можно объяснить содержание собранных разделов. Их порядок в таблице получен отдельно, по записанным связям.

Собственная методология корпуса связывает область с математическим фундаментом машинного обучения и анализа данных. Протокол требует проверять выбранные разделы целиком. Непосредственная популярность результата в ML не определяет его роль: на промежуточной лемме может строиться важный шаг доказательства, хотя ее название не встречается в описании модели. Причину ее использования нужно искать в самом аргументе.

Выбранные разделы задают материал для чтения, но их достаточность для любой ML- или DS-задачи не установлена. Предметное объяснение разделов также не восстанавливает личную историю их выбора: статья рассматривает состав, который автор задал, и показывает, как с ним работать.

Почему основания выходят за границу разделов

Предметная принадлежность результата не определяет все области, к которым придется обратиться при чтении его доказательства. Результат статистики может использовать факт из анализа; численный метод - результат линейной алгебры. Внутренние опоры остаются в основных разделах. Если же записанная цепочка ведет за пределы выбранных папок, Порядок сохраняет внешнюю часть в отдельном прологе.

Для этого обход начинается сразу со всех записей основных разделов. Он идет к их записанным предпосылкам, затем к предпосылкам этих предпосылок. Обход заканчивается, когда больше не находит новых записей. Фундамент показывает внешние записи, найденные по этим цепочкам. Включение одной записи внешней папки не означает включения всей папки.

У теоремы Коши это различие видно непосредственно. В наблюденном эпизоде выбор точки открыл ее формулировку на фоне Порядка. Запись сохранила принадлежность к функциям комплексной переменной, хотя находится в панели фундамента. Панель сообщает о роли в композиции, папка - о предмете. Открытие карточки подтверждает доступ к тексту; содержательный смысл опоры Гейне-Бореля раскрывается отдельно в сохраненном доказательстве, с которого началась эта глава.

Чтобы использовать вычисленное замыкание для чтения, нужно вернуться к выбранному доказательству. Разные способы могут использовать разные наборы опор, а парный граф не хранит, к какому способу относится каждая связь. Получившийся список способен объединить опоры нескольких доказательств. Поэтому полный записанный контекст не обязан быть минимальным набором для одного способа доказательства или личной программой подготовки читателя. Совместимость условий и конкретный шаг применения остаются математическими вопросами, даже когда обход выполнен без ошибок.

От композиции к следующему чтению

Как связать авторский отбор разделов, смысл отношений и расчет расположения, чтобы от нужного результата можно было вернуться к его основаниям? Этот вопрос мы будем решать на конкретном Порядке. Его общий вид и текст записи нужны вместе: карта показывает, куда обратиться, а доказательство объясняет, зачем нужен найденный результат. Сопоставление с другими системами уточнит возможности этой модели, а синтез соберет выводы о том, что удалось организовать.

У проверки записи, расчета композиции и наблюдения интерфейса разные области. Содержательная приемка относится к более ранней версии корпуса; по имеющимся свидетельствам нельзя перенести ее на каждую запись октябрьской публикации. Вычисления подтверждают состав и композицию заданного входа, а наблюдения - выполненные действия интерфейса. Улучшение понимания читателя потребовало бы отдельного исследования, которого для Порядка здесь нет. Поэтому мы будем оценивать построенную систему по ее устройству и проверенным действиям, не объявляя универсальный охват или превосходство над другими системами.

Вернемся к выбранной точке Коши. Открыв текст, читатель получает формулировку с условиями. Что делает ее точной версией математического результата и чем такая запись отличается от определения или алгоритма? С этого начнется следующая глава.

выбранных разделов
14
записей основных разделов
914
внешние опоры
53
Оговорки
  • Количество файловых записей не равно количеству теорем. Состав последовательности не является подсчетом видимых на экране точек.
  • Размер раздела не устанавливает полноту его содержания; положение на полке не делает запись факультативной.
02
Объекты

У каждой записи есть точный предмет.

7категорий в протоколе корпуса

Точка ведет к записи корпуса. Чтобы понять утверждение, нужно прочитать его контекст, гипотезы и заключение; один адрес этой работы не выполняет.

Что находится за точкой

Выберем в Порядке запись Теорема Коши об интегральной формуле. В наблюденной сцене ее карточка открылась на фоне панелей разделов и показала предметную область Функции комплексной переменной вместе со связями записи. Знакомому читателю название подсказывает интеграл по замкнутому контуру. Но название еще не сообщает, на какой области определена функция, какой контур допустим и для какой точки утверждается равенство. Без этих условий нельзя решить, применима ли формула в следующем рассуждении. Первое действие содержательного чтения - перейти от названия к точной формулировке.

Единица Порядка - отдельная математическая запись корпуса. Запись может вводить понятие, утверждать результат, описывать процедуру или собирать несколько вариантов одного принципа. Файл задает адрес записи и определяет, какой материал читатель откроет целиком. В одном файле могут находиться несколько утверждений и доказательств. Поэтому число файлов характеризует устройство корпуса, но само по себе не сообщает число теорем или законченных доказательств.

Чтобы увидеть, зачем нужны эти границы, дальше проследим один вопрос: когда разрешено интегрировать сумму функций почленно? Он проведет нас от названия результата к условиям, от условий к доказательству, а затем к способу распределить материал между записями. Это учебный пример, отдельный от содержательной приемки карточки Коши и всего опубликованного корпуса.

Точная версия результата

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

Для нашего примера зафиксируем интеграл Римана, конечный отрезок [a,b][a,b] с a<ba<b и конечное положительное целое число mm. Пусть все вещественные функции f1,…,fmf_1,\ldots,f_m интегрируемы на этом отрезке. Тогда их сумма тоже интегрируема, и линейность дает

∫ab(∑j=1mfj(x)) dx=∑j=1m∫abfj(x) dx.\int_a^b\left(\sum_{j=1}^{m}f_j(x)\right)\,dx =\sum_{j=1}^{m}\int_a^b f_j(x)\,dx.

Теперь можно назвать части точного утверждения. Контекст задает интеграл Римана и вещественные функции на конечном отрезке. Гипотезы требуют интегрируемости каждой функции; заключение включает интегрируемость суммы и равенство интегралов. Конечность числа слагаемых тоже существенна: линейность применяется последовательно, без предельного перехода.

Обозначим контекст через Γ\Gamma, гипотезы через HH, заключение через CC. Контекст включает используемые определения и систему оснований, поэтому одинаковые слова при разных соглашениях могут задавать разные задачи. Точную версию утверждения SS опишем схемой

S=(Γ,H,C),Γ,H⊢C.S=(\Gamma,H,C),\qquad \Gamma,H\vdash C.

Знак ⊢\vdash отмечает, что заключение должно быть обосновано из указанных оснований. Составление тройки SS этого не доказывает и не сообщает, какие предпосылки конкретное доказательство действительно использует. Мы ввели язык чтения, а не новые поля индекса или формальную модель доказательств VaultGraph.

Это различие понадобится в следующем шаге. В конечной сумме хватило интегрируемости слагаемых. При переходе к бесконечному ряду появляется новая операция, для которой нужны собственные условия.

Пусть частичные суммы ряда sm=∑j=1mfjs_m=\sum_{j=1}^m f_j сходятся к функции ss. Каждую конечную сумму можно интегрировать по прежнему правилу. Но для почленного интегрирования всего ряда осталось установить, что ss интегрируема и интегралы sms_m сходятся к ее интегралу. Рассмотрим конкретное достаточное условие: все sms_m непрерывны на [a,b][a,b] и сходятся к ss равномерно. Равномерность означает, что ошибка εm=sup⁡x∈[a,b]∣sm(x)−s(x)∣\varepsilon_m=\sup_{x\in[a,b]}|s_m(x)-s(x)| стремится к нулю. Одно и то же ограничение работает для всех точек отрезка.

Равномерный предел непрерывных функций непрерывен. Проверим этот переход в фиксированной точке x0∈[a,b]x_0\in[a,b]. Для требуемой точности ε>0\varepsilon>0 сначала выбираем один номер MM, при котором общая ошибка ∣sM(x)−s(x)∣|s_M(x)-s(x)| меньше ε/3\varepsilon/3 на всем отрезке. Затем непрерывность выбранной функции sMs_M дает δ>0\delta>0: при x∈[a,b]x\in[a,b] и ∣x−x0∣<δ|x-x_0|<\delta изменение ∣sM(x)−sM(x0)∣|s_M(x)-s_M(x_0)| меньше ε/3\varepsilon/3. Номер MM уже зафиксирован и не меняется вместе с xx. Неравенство треугольника складывает три ошибки: от s(x)s(x) к sM(x)s_M(x), от sM(x)s_M(x) к sM(x0)s_M(x_0) и обратно к s(x0)s(x_0). Поэтому ∣s(x)−s(x0)∣<ε|s(x)-s(x_0)|<\varepsilon. Точка x0x_0 была произвольной: предел непрерывен на всем отрезке, а значит, интегрируем по Риману.

Теперь ∣sm(x)−s(x)∣≤εm|s_m(x)-s(x)|\le\varepsilon_m во всех точках. Модуль интеграла разности не превышает длину отрезка, умноженную на эту ошибку:

∣∫absm(x) dx−∫abs(x) dx∣≤(b−a)sup⁡x∈[a,b]∣sm(x)−s(x)∣⟶0.\left|\int_a^b s_m(x)\,dx-\int_a^b s(x)\,dx\right| \le (b-a)\sup_{x\in[a,b]}|s_m(x)-s(x)|\longrightarrow 0.

Оценка завершает переход: конечная линейность дает интеграл каждой sms_m, а равномерный контроль ошибки позволяет перейти к интегралу ss. Например, на отрезке длины 2 общая ошибка частичной суммы не больше εm\varepsilon_m дает ошибку интеграла не больше 2εm2\varepsilon_m. Можно искать другие достаточные условия, но сам перенос предела требует обоснования.

Когда предел функции теряет площадь

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

hn(x)=n2x(1−x)n,x∈[0,1],n=1,2,….h_n(x)=n^2x(1-x)^n,\qquad x\in[0,1],\quad n=1,2,\ldots.

На концах отрезка значение равно нулю. Для фиксированного 0<x<10<x<1 число q=1−xq=1-x лежит между нулем и единицей, и n2qnn^2q^n стремится к нулю: отношение соседних членов равно q(1+1/n)2q(1+1/n)^2 и со временем становится меньше некоторого постоянного числа, меньшего единицы. Значит, hn(x)h_n(x) сходится к нулю в каждой точке.

Что происходит с интегралом? Подстановка u=1−xu=1-x превращает его в n2∫01(1−u)un dun^2\int_0^1(1-u)u^n\,du. Две степени интегрируются непосредственно, поэтому

∫01hn(x) dx=n2(1n+1−1n+2)=n2(n+1)(n+2)⟶1.\int_0^1 h_n(x)\,dx =n^2\left(\frac{1}{n+1}-\frac{1}{n+2}\right) =\frac{n^2}{(n+1)(n+2)}\longrightarrow 1.

Интеграл предельной нулевой функции равен нулю, а предел интегралов равен единице. В точках по отдельности функция исчезает; общая площадь не исчезает, собираясь все ближе к левому концу отрезка. Противоречия нет: точка, в которой велика ошибка, может зависеть от nn. Равномерного контроля, использованного в предыдущей оценке, здесь нет.

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

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

Разные объекты требуют разных свидетельств

В этом примере рядом понадобились разные виды знания. Определение равномерной сходимости объяснило смысл гипотезы. Теорема о непрерывности равномерного предела позволила интегрировать ss. Оценка ошибки оправдала перенос предела. Контрпример показал границу более слабой версии. Все эти части могут выглядеть как одинаковые точки на карте, но проверять их нужно по разным вопросам.

Протокол корпуса различает теорему, характеристику, определение, аксиому, алгоритм, эвристику и семейство результатов. Утверждение о существовании требует доказательства существования; утверждение о единственности добавляет другую обязанность. Характеристика, сформулированная как эквивалентность, требует обеих импликаций. Так, достаточное условие из нашего примера не становится характеристикой всех случаев, когда разрешен перенос предела.

Как проверять разные математические объекты

Чтобы проверить запись, сначала определяют ее математический предмет: условия теоремы, смысл определения и гарантия алгоритма требуют разных свидетельств.
ОбъектСодержаниеНужное свидетельство
ТеоремаУсловия и заключениеПолное доказательство точной версии
ХарактеристикаЭквивалентность свойства и условийОба направления утверждения
ОпределениеЗначение термина и соглашенияИсточник и согласованность контекста
АксиомаПринятое основание системыФормулировка и система оснований
АлгоритмПроцедура вычисленияДоказательство корректности и условия гарантирующей теоремы
ЭвристикаПравило выбора без полной гарантииОбласть применения и ограничения
Семейство результатовНесколько связанных вариантовРазделение версий, гипотез и доказательств

У определения проверяют область, соглашения и связь с уже используемыми понятиями. Определение не должно незаметно переносить свойство на более широкий класс объектов. У аксиомы фиксируют систему, в которой она принимается. Доказательство следствия из аксиомы не является доказательством самой аксиомы в этой системе.

Для алгоритма читатель устанавливает вход, последовательность действий и выход. Затем отдельно рассматривает каждую заявленную гарантию: корректность, сходимость, ограничение ошибки, стоимость вычисления. Примером такого разделения служит сама композиция Порядка: конкретная процедура размещения вершин и математический критерий качества расположения имеют разные роли. В алгоритмической главе мы увидим, где решается точная задача, а где применяется эвристика. Называть всю процедуру оптимальной можно лишь после указания критерия и области гарантии.

Эвристика тоже может быть содержательным объектом корпуса. У нее есть правило действия и область применения, но обещание улучшить результат не становится доказанной гарантией оттого, что правило записано рядом с теоремами. Семейство результатов требует различимых вариантов: общий принцип помогает ориентации, однако несовместимые условия нельзя молча объединить в одно точное утверждение.

В опубликованной технической схеме поле type узла принимает значения resolved, unresolved и tag. resolved обозначает узел существующей файловой записи, unresolved - файловую цель без найденного файла, tag - узел классификационной метки. Они не являются математической разметкой перечисленных типов. Распределение всего замороженного корпуса по теоремам, определениям и алгоритмам не вычислено. Вывести его из технических типов означало бы подменить исследуемое свойство другим.

Имя, адрес и содержание

Мы уже различили математические версии. Как система позволяет найти нужную запись и открыть ее снова? У выбранной записи Коши адрес файла имеет вид 30_Функции_комплексной_переменной/Теорема Коши об интегральной формуле.md. В индексе раздельно хранятся идентификатор, показываемое название, папка и путь. Идентификатор получается из имени файла без расширения. Перемещение файла с прежним именем сохраняет такой идентификатор; переименование меняет его. Совпадение имени в разных папках создало бы неоднозначный идентификатор, поэтому сборщик индекса запрещает такие совпадения без учета регистра. Показываемый заголовок извлекается отдельно из текста. Содержание и заголовок способны измениться при сохранении того же идентификатора.

Адрес позволяет найти файл. Чтобы установить, какое утверждение сейчас находится внутри, нужно прочитать его условия и заключение. Например, одинаковое имя записи о почленном интегрировании не сообщает, сохранилось ли требование равномерной сходимости после редактуры.

Содержание, запись и адрес

Содержание утверждения, выбранная запись и ее адрес отвечают на разные вопросы: что утверждается, какую версию читать и как найти текст.
Уровень описанияЧто фиксируетсяЧего это не устанавливает
Математический объектКонтекст, гипотезы, заключениеНазвание само по себе не устанавливает эквивалентность
Запись корпусаВыбранная версия и ее текстОдин файл может адресовать семейство вариантов
Технический адресИдентификатор, путь, альтернативные имена, версия публикацииРазрешенная ссылка не доказывает математическую правильность

Название помогает человеку найти материал. Синонимы и альтернативные названия помогают поиску, но не устанавливают тождество результатов. Два имени могут обозначать эквивалентные формулировки; одно имя может объединять разные версии. Чтобы установить математическое соответствие, нужно сопоставить условия и заключения, а при эквивалентности - показать допустимые переходы между формулировками.

Похожие различения встречаются в других математических системах. Stacks Project присваивает адресуемым частям текста теги и отделяет постоянный адрес от истории изменений текста. В Порядке действует собственное правило идентификаторов из имен файлов; сходная задача адресации не означает одинаковый механизм стабильности. Stacks Project, Tags.

OntoMathPRO отдельно рассматривает предметный и лингвистический уровни: математические объекты и их отношения нужно отличать от терминов, которыми эти объекты называются. Это помогает различить обозначение объекта, его математическое содержание и запись, в которой оно изложено. Такое сопоставление не приписывает VaultGraph реализованную онтологию OntoMathPRO. Основание сравнения - принятое чтение статьи 2022 года, с. 30-32, включая рис. 3. Елизаров и соавт., OntoMathPRO.

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

Утверждение и его доказательства

Вернемся к переносу предела: точная формулировка уже известна, но нужно различить ее и способ обоснования. Разобранный выше способ использует непрерывность равномерного предела, чтобы установить интегрируемость ss, и оценку интеграла через общую ошибку, чтобы получить сходимость интегралов. Эти опоры выполняют разные работы. Из того, что оба названия стоят в окружении цели, еще нельзя восстановить места применения; они выясняются из самого аргумента.

Если для той же точной версии найдено и проверено другое доказательство, оно может использовать иные опоры. Поэтому утверждение и его доказательства следует различать, а ссылку относить к использующему ее способу. Совместное использование не обязательно означает один непосредственный шаг: результаты могут работать в разных частях одного доказательства. Альтернатива не отменяет опор первого способа и не делает их обязательными для любого доказательства цели. Запись выводимости с перечисленными предпосылками сама по себе не показывает, какие из них аргумент действительно вызвал.

В NaturalProofs текст утверждения отделен от объектов доказательств, а ссылки принадлежат конкретным доказательствам. Так сохраняется принадлежность ссылок конкретному аргументу. В VaultGraph техническое ребро связывает записи; отдельная модель доказательств в индексе не реализована. Основание сопоставления - принятая конференционная версия NaturalProofs 2021 года, основной текст §3 и табл. 2, дополнительные материалы A.1/D. Welleck et al., NaturalProofs.

Список всех предков записи может объединить опоры разных маршрутов. Полученное множество полезно для обзора контекста, но без дополнительного разбора его нельзя считать совместно обязательным набором опор одного доказательства. В следующей главе это различие станет основой интерпретации стрелок.

Нарезка корпуса влияет на счет

Предположим, что вся подготовка к переносу предела собрана в одной записи AA, а сам результат занимает запись TT. Можно сохранить ту же математику и разделить подготовку на две записи: в A1A_1 установить непрерывность предела, в A2A_2 вывести нужную оценку интеграла для него. В условной модели это даст две разные нарезки:

A⟶T,A1⟶A2⟶T.A\longrightarrow T, \qquad A_1\longrightarrow A_2\longrightarrow T.

В показанных моделях у TT один предок и два предка соответственно; длина пути тоже меняется. Мы считаем только нарисованные записи и связи, без дополнительных внешних оснований. Новая математическая идея при разбиении не появилась: изменилось распределение уже разобранного материала между записями. Поэтому число предков зависит от гранулярности записей. Оно полезно для описания именно этого корпуса, но не задает единицу объема знания, независимую от нарезки.

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

Оговорка. Принятый протокол описывает обязанности содержательной проверки; наличие протокола не доказывает выполнение каждого пункта для каждой записи октябрьского снимка. В этой главе таблица типов является матрицей чтения и проверки, а условные примеры - объясняющими схемами. Ни таблица, ни схемы не расширяют область принятого аудита.

Открывая точку в Порядке, читатель получает запись. Чтобы понять представленный объект, он устанавливает контекст и условия; чтобы понять опоры, обращается к конкретному доказательству. Следующая глава рассматривает линию между двумя такими записями: какое отношение она обозначает и какой математический переход позволяет утверждать?

фиксируют точную версию утверждения
Условия
контекст, гипотезы, заключение
Утверждение
узел имеющегося файла
resolved

Источники главы

Ссылки и границы использованного чтения
ИсточникМесто и область подтверждения
OntoMathPROОфициальный PDF 2022; с.30-32, рис.3; принято чтение 7 страниц
Stacks Project: TagsПрочитанные страницы Tags, тег 00CR и Statistics; адреса текста, не число теорем
NaturalProofsNeurIPS Datasets and Benchmarks 2021; §3, таблица 2, дополнение A.1/D
Оговорки
  • Типы resolved/unresolved/tag различают узел имеющегося файла, неразрешенную файловую цель и тег. Распределение записей по математическим типам не рассчитано.
  • Таблица различает содержание, версию записи и адрес. Гипотезы и заключение не выделены в отдельные структурированные поля индекса; их читают в тексте записи.
03
Связи

Опора получает смысл в доказательстве.

4типа связей в индексе

Направление связи сообщает записанную роль опоры. Конкретный шаг аргумента и совместимость условий проверяются по тексту.

Что должно стоять за стрелкой

Две записи могут относиться к одной теме и находиться рядом на экране. Доказательная связь требует большего: нужно показать, какой результат используется в аргументе, что он позволяет получить и почему выполнены его условия. В Порядке стрелка B→AB\to A направлена от опоры BB к использующей записи AA. Чтобы понять такую стрелку, разберем один переход целиком, а затем посмотрим, что от него остается в индексе.

Как доказать теорему Лагранжа через теорему Ролля

Теорема Лагранжа о среднем значении связывает изменение функции на всем отрезке с ее производной в одной внутренней точке. Для вещественной функции ff, непрерывной на [a,b][a,b] и дифференцируемой на (a,b)(a,b), при a<ba<b требуется найти c∈(a,b)c\in(a,b), такое что

f′(c)=f(b)−f(a)b−a.f'(c)=\frac{f(b)-f(a)}{b-a}.

Правая часть - наклон секущей через концы графика. Обозначим этот наклон через mm; деление допустимо, поскольку b−a>0b-a>0. Требуется найти внутри отрезка точку, где касательная имеет такой же наклон. Теорема Ролля гарантирует нулевую производную, если значения функции на концах равны. У ff эти значения могут различаться, поэтому условие Ролля еще не выполнено.

Чтобы уравнять концы, вычтем из ff функцию секущей. Обозначим эту линейную функцию через ℓ\ell, а разность через gg:

ℓ(x)=f(a)+m(x−a),g(x)=f(x)−ℓ(x).\ell(x)=f(a)+m(x-a),\qquad g(x)=f(x)-\ell(x).

Разность gg непрерывна на закрытом отрезке и дифференцируема внутри него: эти свойства есть и у ff, и у линейной функции ℓ\ell. Значения на концах вычисляются непосредственно:

g(a)=0,g(b)=f(b)−f(a)−m(b−a)=0.g(a)=0,\qquad g(b)=f(b)-f(a)-m(b-a)=0.

Все условия Ролля выполнены для gg, поэтому существует c∈(a,b)c\in(a,b) с g′(c)=0g'(c)=0. Однако наша цель касается производной ff. Связь между двумя производными дает ℓ′(x)=m\ell'(x)=m:

g′(c)=f′(c)−m=0,f′(c)=m.g'(c)=f'(c)-m=0, \qquad f'(c)=m.

Это и есть требуемое равенство Лагранжа. Производные на концах отрезка и непрерывность f′f' для данного аргумента не требуются. Нужны непрерывность ff на всем закрытом отрезке и существование производной в каждой внутренней точке.

Маршрут приведен в MIT 18.100A, лекция 19, теоремы 5 и 7, страницы 3-4. В лекции вспомогательная функция нормирована через правый конец: f(x)−f(b)+m(b−x)f(x)-f(b)+m(b-x). Она совпадает с нашей gg, поскольку m(b−a)=f(b)−f(a)m(b-a)=f(b)-f(a). Здесь пример служит самостоятельным разбором доказательного отношения; он не означает новую приемку конкретного ребра замороженного корпуса.

Теперь можно объяснить стрелку Ролль -> Лагранж: в этом способе доказательства Ролль применяется к построенной функции gg, условия применения проверены, а равенство g′(c)=0g'(c)=0 дает f′(c)=mf'(c)=m, то есть нужный наклон касательной. Указание на имя теоремы этого объяснения не заменяет: оно не сообщает ни версию утверждения, ни место применения, ни переход обратно к цели.

У той же пары результатов возможно обратное рассуждение: из уже доказанного Лагранжа получается Ролль как частный случай при f(a)=f(b)f(a)=f(b). Оба перехода корректны по отдельности, но доказать обе теоремы только друг через друга нельзя. В первом маршруте Ролль должен быть установлен независимо до применения к Лагранжу; во втором уже имеется доказательство Лагранжа. Взаимные линии без указания маршрутов не сохраняют этой разницы. Использование BB в одном доказательстве AA также не делает BB необходимым для всех доказательств AA.

Что именно объявлено в заметке

Когда использование результата разобрано, его можно объявить в заметке. Но далеко не всякая ссылка объявляет доказательную опору. В корпусе также нужны переходы к применениям, обычные ссылки между текстами и теги для классификации. Тематическая близость и совет освоить одну тему раньше другой тоже помогают ориентироваться, но сами по себе не показывают использования результата в доказательстве.

Как объявления превращаются в связи

Направление читают по объявленной роли связи. Если A опирается на B, ребро B -> A ведет от используемого основания к использующей записи.
ДекларацияРебро индексаПредел вывода
A: Опирается на Bprerequisite B -> AТребуется проверка места применения и гипотез
A: Используется в Bapplication A -> BКонкретная математическая роль остается в тексте
A: ссылка вне точных секцийreference A -> BНавигационная ссылка не удостоверяет использование в доказательстве
A: распознанный тег qtag A -> tag:qОбщая классификация не создает доказательной опоры

Язык заметок Nareshka различает эти случаи по месту объявления. Если запись AA содержит ссылку на BB в точной секции Опирается на, парсер извлекает prerequisite, а сборщик направляет связь B→AB\to A. В секции Используется в ссылка объявляет application от текущей записи к названной: A→BA\to B. Остальные распознанные wikilinks дают reference; распознанные теги связывают запись с узлами категорий. Секция сообщает, как автор объявил связь. Формулировка и аргумент объясняют, оправдано ли это объявление.

Читая применение, нужно выяснить роль результата. Теорема может давать гарантию сходимости алгоритма, ограничивать ошибку, обосновывать действие процедуры или пояснять мотивирующий пример. Для гарантии сходимости нужно проверить гипотезы теоремы у рассматриваемого алгоритма; упоминания ее имени во введении недостаточно. Тип application эти роли не различает, поэтому за объяснением приходится возвращаться к тексту.

Определение задает смысл объекта или термина и может понадобиться уже для понимания формулировки. Его использование следует отличать от применения теоремы. Отдельного типа ребра definition в текущем перечислении нет: определение на одном конце связи не определяет автоматически ни ее тип, ни роль. Поэтому при чтении важно сопоставить два уровня: что объявлено в секции и что действительно сделано в математическом тексте.

Почему одной цепочки недостаточно

Знания формулировки Ролля еще недостаточно, чтобы восстановить разобранное доказательство. Нужно построить подходящую функцию, проверить условия, вычислить g′=f′−mg'=f'-m и перенести вывод на ff. Если последний переход непонятен, одна линия Ролль -> Лагранж его не восполнит. Выбранный способ требует всех своих опор, в том числе тех, которые работают на других шагах. Какие из этих шагов становятся отдельными записями и ребрами, зависит от гранулярности корпуса; пример не задает минимального списка зависимостей Лагранжа.

Пусть теперь у условной цели TT есть опоры PP и QQ. В первой модели один рассматриваемый способ использует обе совместно. Во второй существуют два способа: один использует PP, другой QQ. Будем считать сами способы корректными, а условия применения опор выполненными. Если читателю доступна только PP, способ из первой модели пока не обеспечен всеми опорами. Во второй модели можно выбрать способ через PP.

Граф, который соединяет каждую упомянутую опору с целью и забывает принадлежность способу, в обоих случаях даст одинаковые ребра:

E={P→T,  Q→T}.E=\{P\to T,\;Q\to T\}.

Чтобы сохранить различие, каждому способу нужно сопоставить свой набор опор. Внутренние скобки объединят опоры одного способа, внешние соберут все рассматриваемые способы. Обозначим семейство для совместного использования через Sjoint(T)\mathcal S_{\mathrm{joint}}(T), а семейство для альтернатив через Salternative(T)\mathcal S_{\mathrm{alternative}}(T):

Sjoint(T)={{P,Q}},Salternative(T)={{P},{Q}}.\mathcal S_{\mathrm{joint}}(T)=\{\{P,Q\}\}, \qquad \mathcal S_{\mathrm{alternative}}(T)=\{\{P\},\{Q\}\}.

Совместные опоры и альтернативные маршруты

В верхней модели единственный способ требует P и Q совместно; в нижней каждый из двух способов использует одну опору. Обе модели дают парные связи P -> T и Q -> T. Промежуточный узел обозначает совместный набор опор.
Модель способовНаборы опорОдинаковая парная проекция
Совместная модельОдин способ: {P,Q}P -> T; Q -> T
Альтернативная модельСпособ 1: {P}; способ 2: {Q}P -> T; Q -> T

У первой модели один способ с двумя совместными опорами. У второй два способа с одной опорой каждый. Это различие обычно называют AND/OR: получить все входы выбранного способа и выбрать один из подходящих способов. Формальное различение AND и OR дано в Martelli и Montanari, Additive AND/OR Graphs, раздел 2, страницы 2-3. Gallo и соавторы, Directed Hypergraphs and Applications, авторская рукопись 1990 с пересмотром октября 1992, страницы 4-6 и 15-19 рассматривают направленные переходы с совместными входами. Эти модели помогают объяснить потерю группировки при парном представлении; Nareshka не объявляется их реализацией.

Выбор способа не отменяет проверки условий. Если опора дана только для конечномерного пространства, наличие ее формулировки не разрешает применять результат в бесконечномерном случае. В примере Лагранжа мы проверили непрерывность и дифференцируемость gg, равенство ее концов и a<ba<b. Поэтому возможность пройти выбранный способ требует и всего набора опор, и выполненных условий.

Запишем это условие для семейства рассматриваемых проверенных способов R\mathcal R. Через KK обозначим конкретные версии результатов, доступные читателю для использования в рассуждении. Совместный набор опор способа rr обозначим через SrS_r, а утверждение о выполнении его условий - через HrH_r. Для разобранного способа Лагранжа в SrS_r входит используемая версия Ролля, а HrH_r включает a<ba<b, непрерывность и дифференцируемость gg на соответствующих областях и равенство ее концов. Наличие результата среди доступных опор и применимость к построенному объекту проверяются отдельно. Тогда возможность следовать хотя бы одному из рассматриваемых способов выражается так:

∃r∈R:Sr⊆K∧Hr.\exists r\in\mathcal R:\quad S_r\subseteq K\quad\land\quad H_r.

Первая часть условия проверяет, собраны ли все опоры способа, вторая - можно ли их применить. Здесь rr обозначает разобранный аргумент, а не произвольный путь в графе. Его корректность уже предполагается установленной; включение множеств ее не доказывает. Для сохранения этой информации нужно различать результат, его доказательства и ссылки каждого доказательства. Такое разделение имеется, например, в NaturalProofs, supplement A.1. Оно не превращает любую извлеченную ссылку в минимальную логическую предпосылку.

Как математический рассказ сжимается в индекс

Пояснение шага, источник и способ доказательства могут оставаться в тексте заметки. Текущий индекс VaultGraph не хранит идентификатор доказательства, номер шага и группы совместных опор как отдельные поля ребра. Он помогает найти связанные тексты, но не позволяет автоматически восстановить структуру аргумента. Полнота таких пояснений во всех заметках замороженной публикации этой работой не установлена; область содержательной приемки будет разобрана в следующей главе.

При сборке индекса объявления одной пары записей, включая противоположные направления, сводятся к одной canonical-связи. Типы выбираются по приоритету: prerequisite, затем application, затем reference. Тип с более высоким приоритетом сохраняет свое направление; при конфликте объявлений одинакового типа остается направление первого обработанного объявления. В итоге одно опубликованное ребро представляет пару записей, но не перечисляет все ее объявления. Такое правило сборки само по себе не разрешает математического противоречия между ними.

Флаг confirmed относится к этой обработке. Он означает не менее двух объявлений пары после удаления повторов одной цели и одного типа внутри каждого файла. Например, ссылка на BB в секции Опирается на записи AA и обычная ссылка на BB в другой секции этой же записи дают два объявления разных типов. Этого уже достаточно для счетчика, хотя обе ссылки пришли из одного файла. Следовательно, confirmed не измеряет независимость источников или согласие проверяющих. Он описывает обработку разметки; обоснование отношения остается в математическом тексте.

Какой контекст можно получить из связей

Обход входящих prerequisite-ребер собирает всех уникальных предков выбранной цели в предоставленном графе. Конус предков показывает основания оснований, которые не помещаются в одной цепочке. Но если ссылки разных способов уже объединены в проекции, конус соберет их опоры вместе. Читатель получит контекст для разбора, а не автоматически выбранное доказательство.

Обход может перечислить всех предков в переданном графе, но он не проверяет полноту математических гипотез, минимальность набора опор или совместимость включенных записей. Две линии P→TP\to T и Q→TQ\to T без принадлежности способам не сообщают, понадобятся ли обе опоры для выбранного аргумента. Одна цепочка к TT, напротив, может пропустить боковую посылку конкретного шага.

Поэтому после перехода по линии нужно вернуться к аргументу: к какому объекту применяется опора и как ее заключение помогает цели? В примере Лагранжа опора применялась к gg, а к производной ff нас вернуло равенство g′(c)=f′(c)−mg'(c)=f'(c)-m. Следующая глава объясняет, как формулировки, способы доказательства и отношения проверяются до того, как из них рассчитывается композиция корпуса.

обосновывает математическую роль связи
Шаг аргумента
направление от опоры к использующей записи
B -> A
повторная декларация
confirmed

Источники главы

Ссылки и границы использованного чтения
ИсточникМесто и область подтверждения
NaturalProofsNeurIPS Datasets and Benchmarks 2021; §3, таблица 2, дополнение A.1/D
Gallo et al.: Directed Hypergraphs and ApplicationsАвторская рукопись, пересмотренная в октябре 1992; с.4-6 и 15-19; побайтовое совпадение с опубликованной журнальной версией не установлено
Martelli and Montanari: Additive AND/OR GraphsОфициальный PDF IJCAI 1973; §2, с.2-3; отдельно принято более широкое чтение текста и фигур
MIT OCW 18.100A: Lecture 19Теоремы 5 (Ролль) и 7 (MVT), доказательства с.3-4; новое адресное чтение вне состава принятого DIG
Оговорки
  • Объединение деклараций в каноническую пару сохраняет повторяемость объявления. Флаг confirmed обозначает повторную декларацию, а не независимую математическую проверку.
  • Схема показывает условные способы доказательства. Промежуточный узел совместного набора служит объяснению; таких узлов доказательств VaultGraph не хранит.
04
Корпус

Корпус собирается и проверяется.

6этапов протокола

Проверка записи связывает точную формулировку, полный аргумент и роль каждой опоры. После исправлений итоговую версию читает независимый проверяющий.

Работа, которая предшествует картинке

Представим, что запись обещает найти точку, в которой производная равна наклону секущей. Название теоремы знакомо, ссылка на учебник есть, рядом проведена стрелка от Ролля. Чего еще не хватает? Если в формулировке потеряна непрерывность на концах отрезка, запись обещает больше, чем доказывает источник. Индекс может без ошибок извлечь имя и связь, а Порядок - расположить запись среди других. Пропущенное условие от этого не восстановится.

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

Проследим эту работу на условном редакционном примере с теоремой Лагранжа, затем разберем общие правила. Мы не сообщаем о найденной ошибке Nareshka: пример показывает, какое решение должна изменить проверка. Описанный протокол задает требования к корпусу. Какие из них выполнены, устанавливают по конкретной принятой версии и области; в конце главы названы границы уже выполненной работы.

От источника до принятой записи

Проверка идет от точной версии через доказательство и роль опор к исправленной записи. Итоговую версию принимает независимый проверяющий; таблица описывает обязанности протокола.
ШагПредмет проверкиСвидетельство
ИдентичностьТочная формулировка и версияКонтекст, гипотезы, заключение
ДоказательствоПолный аргумент, основания и применения записиКонкретный шаг применения каждой опоры
Внешняя проверкаВерсия источника и независимостьОдин сильный источник; два для новых и трудных стыков
КлассификацияMSC, альтернативные имена и разбор разметкиПравильная предметная область и разрешение адресов
Проверка после исправленийПримененные правки, объявления отношений на затронутых концах и конечный индексПроверка изменений исходных заметок и индекса, отсутствие регрессий
Независимая приемкаИтоговая версия после измененийДругой проверяющий читает итоговый аргумент и проверяет связи и полноту

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

От найденного названия к точному утверждению

Предположим, программа курса или книжный указатель привели нас к теореме Лагранжа о среднем значении. Прежде чем добавлять запись, нужно выяснить, нет ли этого результата в корпусе под другим именем. Поэтому сначала ищут русские и английские варианты названия. Незнакомое имя может адресовать уже имеющуюся запись, а одно привычное имя - несколько утверждений с разными условиями.

Теперь можно открыть источник и установить полное утверждение. В рассматриваемой версии a<ba<b, вещественная функция ff непрерывна на [a,b][a,b] и дифференцируема на (a,b)(a,b). Заключение - существование c∈(a,b)c\in(a,b), для которого

f′(c)=f(b)−f(a)b−a.f'(c)=\frac{f(b)-f(a)}{b-a}.

И условия, и доказательство этой версии приведены в MIT 18.100A, лекция 19, теоремы 5 и 7, с. 3-4. Тот же источник поддерживал математический пример предыдущей главы; здесь он позволяет решить, что должна содержать запись.

Теперь видно, что именно потеряла бы сокращенная запись без непрерывности на концах. Возьмем отрезок [0,1][0,1] и функцию

f(x)={x,0≤x<1,2,x=1.f(x)= \begin{cases} x,&0\le x<1,\\ 2,&x=1. \end{cases}

Внутри отрезка производная равна 1, а наклон секущей равен (f(1)−f(0))/(1−0)=2(f(1)-f(0))/(1-0)=2. Точки с требуемой производной нет. Разрыв в правом конце нарушает условие теоремы, хотя дифференцируемость внутри сохранилась. Этот самостоятельный контрпример показывает, почему условие необходимо вернуть в нашу объясняющую запись. Он не сообщает о дефекте опубликованной карточки.

Проверка формулировки всегда связывает условия с заключением. Запишем эту связь как H⇒CH\Rightarrow C, где HH - существенные условия, CC - заключение. В нашем примере непрерывность входит в HH; ее удаление расширяет допустимые функции и разрушает вывод. Поэтому сходства имени и заключения недостаточно для переноса доказательства на другие условия. После сравнения версий решают, уточнить ли существующую запись, разделить ли несовместимые варианты или добавить новый объект. Две записи одного результата можно объединить; изменение только предметного места требует переноса. При каждом решении сохраняют судьбу исходных идентификаторов и отношений.

Прочитать доказательство и установить место опоры

В этом маршруте Лагранжа опорой служит Ролль. Положим m=(f(b)−f(a))/(b−a)m=(f(b)-f(a))/(b-a) и вычтем из функции секущую:

g(x)=f(x)−f(a)−m(x−a).g(x)=f(x)-f(a)-m(x-a).

У gg равны значения на концах: g(a)=g(b)=0g(a)=g(b)=0. Непрерывность ff на закрытом отрезке дает непрерывность gg, а дифференцируемость внутри дает производную g′=f′−mg'=f'-m. Именно теперь применим Ролль: для некоторого c∈(a,b)c\in(a,b) производная g′(c)=0g'(c)=0, следовательно, f′(c)=mf'(c)=m. У стрелки Ролль -> Лагранж появился проверяемый смысл: названы точные условия опоры, функция, к которой она применяется, шаг вызова и перенос вывода на цель.

Теперь понятно, что делать с пропущенным условием. Нужно уточнить формулировку и проверить связанные применения: не использовал ли следующий результат ложную, более сильную версию? Работа не заканчивается заменой строки. Если изменились допустимые условия опоры, решения о ее последующих применениях нужно проверить снова.

Такое чтение требуется хотя бы для одного полного доступного доказательства каждой теоремы записанной версии, со всеми существенными шагами и условиями. Большой аргумент можно разбирать по частям, но непрочитанная часть остается явно незавершенной. Список опор, название книги без места и ссылка на стандартное доказательство не объясняют переходы. В итоговой заметке нужны краткая проверенная схема, раздел или номер теоремы и страница источника, а у связи - пояснение применения. Иначе читатель получит имя опоры, но не сможет проверить ее роль. Служебный журнал эту часть заметки не заменяет.

Из разобранных способов выбирают основной: он должен соответствовать формулировке, быть полным и ясным. Меньшее число стрелок само по себе не делает доказательство лучше. Проверенные альтернативы сохраняют свои наборы опор. Если один способ использует BB и DD совместно, а другой - EE, три входящие линии объединяют несколько маршрутов. По ним нельзя восстановить минимальный обязательный набор для одного доказательства. Способ без BB также не опровергает установленное использование BB в первом способе.

После проверки результата нужно прочитать все объявленные входящие и исходящие отношения, включая связи с записями за пределами главы. Само каноническое отношение проверяют один раз, а его объявления на обоих концах сверяют отдельно. Прямой вызов, цепочку использования и техническую вспомогательную зависимость объясняют раздельно. Затем проверяют маршрут целиком: согласованы ли пространства и гипотезы, есть ли нужные определения и совместные опоры, не возвращается ли аргумент к еще не доказанному результату? Несколько правильных отдельных ребер не гарантируют согласованности цепочки. Тематическую близость, историческую мотивацию и рекомендацию читать раньше сохраняют как другие отношения.

Почему объект определяет способ проверки

Вопросы проверки зависят от того, что содержит запись. У характеристики объекта проверяют утверждаемое свойство; эквивалентность требует обеих сторон. В семействе результатов нужно различить варианты: доказанный частный случай не подтверждает более общий. Поэтому запись рассматривают целиком - ее тип, имя и альтернативные названия, условия, заключение, доказательство, классификацию, возможные дубли и происхождение.

Определение требует установить область, соглашения и употребление по авторитетным источникам. Особенно важно сохранить определение, без которого непонятны условия следующей теоремы. Для аксиомы указывают систему, в которой она принимается; доказательство следствия из аксиомы не является доказательством самой аксиомы независимо от системы. Новое или существенно измененное определение либо аксиома требуют двух независимых источников. Проверяют формулировку и контекст, не приписывая им выдуманного доказательства.

У алгоритма сначала разбирают вход, процедуру и выход, затем каждую заявленную гарантию с ее условиями и доказательством. Выполнить шаги алгоритма еще не значит установить сходимость, ограничение ошибки или оценку сложности. У эвристики проверяют правило и область применения; обещание улучшения требует отдельного обоснования, прежде чем его можно назвать гарантией. Так методы могут находиться рядом с теоремами, сохраняя понятный ответ на вопрос, что именно подтверждено.

Что считается сильным свидетельством

Ссылка на источник тоже требует вопроса: что в нем действительно прочитано? Программа курса показывает тему, указатель помогает найти название, полный текст позволяет разобрать утверждение и доказательство. В реестре различают найденный источник, просмотренный указатель, прочитанную формулировку, разобранное доказательство и выполненную формальную проверку. Сохраняют авторов и издание либо фиксированную ревизию библиотеки, точное место, маршрут поиска, доступность текста, прочитанные страницы и ограничения. Скачанный PDF становится свидетельством после чтения нужного аргумента, а не после извлечения текста.

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

Как понять, независимы ли найденные свидетельства? Нужно проследить происхождение аргумента. Зеркало книги, переиздание с тем же доказательством и его пересказ не дают трех подтверждений. Несколько сервисов поиска по одному доказательству mathlib расширяют способы его найти, но не число источников. Другой проверяющий может заметить ошибку в чтении первого; при этом одна книга не становится двумя независимыми математическими свидетельствами.

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

Разные свидетельства отвечают на разные вопросы

У каждого свидетельства свой вопрос: доказательство подтверждает утверждение, хеш фиксирует версию, расчет дает число, наблюдение показывает действие.
СвидетельствоЧто подтверждаетЧего не подтверждает
Математический источникУтверждение и аргумент конкретной версииКорректность всех записей корпуса
Объявление связи в заметкеЗаписанную связьВыполненность гипотез используемого результата
Июльская приемкаРезультаты в пределах принятой проверкиПоэлементную привязку ко всему октябрьскому корпусу
Зафиксированный снимокСостав и технические поля записейПедагогическую достаточность
ПересчетЧисла заданной проекцииНовый математический аудит
Наблюдение интерфейсаНаблюденное действие и действующие настройкиЛюбой размер окна или универсальное удобство

Каждая строка таблицы отвечает на свой вопрос. Полный аргумент подтверждает математическое решение; независимый проверяющий оценивает его в названной области; контрольная сумма фиксирует байты; пересчет проверяет вычисление; наблюдение интерфейса показывает конкретное действие. Поэтому рядом с результатом важно сохранить предмет проверки: одна надпись OK не объясняет, проверили ли формулу, файл или кнопку.

Независимая проверка, отказ и исправление

Желаемый порядок способен незаметно повлиять на оценку отношения: удобную стрелку хочется сохранить. Поэтому первичное решение фиксируют до знакомства со старым вердиктом и предпочтительной композицией. Затем скептик полностью проверяет изменения, конфликты, критические, межглавные, фундаментальные и существенные отрицательные решения. Обычные неизмененные объекты получают дополнительный выборочный контроль: минимум 10% каждого представленного типа узла и обычных ребер каждой главы.

Пусть NN - неотрицательное целое число объектов в одной такой группе. Минимальное число проверяемых объектов nn равно

n=⌈N10⌉.n=\left\lceil\frac{N}{10}\right\rceil.

Обе величины считают объекты одной группы; знак ⌈⋅⌉\lceil\cdot\rceil округляет вверх. Если группа пуста, проверять нечего; в любой непустой группе округление дает хотя бы один объект и не менее 10% ее состава. Для условной группы из 23 неизмененных определений нужно проверить не менее 3. Это пример правила, а не выполненная выборка текущего корпуса. Чтобы отбор можно было повторить, сохраняют размер группы и начальное значение генератора выбора, seed. Выборочный контроль дополняет полный первичный проход. Он не заменяет этот проход и не позволяет вычислить вероятность правильности всей группы. Если обнаружена системная ошибка, перепроверяют весь затронутый класс.

Что делать, если подтверждение не найдено? Сначала отделить ложное утверждение от неподтвержденной связи. Для удаления разбирают исходный аргумент, точную версию и независимое возражение; причину исключения сохраняют. Спорный отказ от результата стандартного математического канона требует второго независимого поиска. Недоступное доказательство, отсутствие формального соответствия или неудачный запрос означают пробел в проверке. Математическую невозможность результата они не доказывают.

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

После принятого решения изменяют внешнюю заметку и сверяют оба конца отношений, альтернативные имена и результат парсинга. При разделении записи старое применение может остаться у неверной версии; при объединении - потеряться подтвержденная связь; переименование способно оборвать адрес. Поэтому исходную версию сохраняют неизменной, а различие файлов показывает судьбу каждого затронутого идентификатора и ссылки. Зависимые решения проверяют снова. Односторонняя декларация сама по себе не требует обратной ссылки ради симметрии.

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

Даже правильные имеющиеся записи оставляют вопрос: не пропущен ли результат, необходимый для выбранной области? Его ищут по стандартному канону, университетской базе, углубленным и прикладным источникам, вариантам и межглавным границам. Заканчивать этот поиск нужно отдельно для узлов и для отношений. Критерий насыщения означает, что дальнейшие проверочные проходы перестали давать допустимые новые находки. Для этого должны быть разобраны семейства источников или объяснены пробелы, указаны прочитанные разделы, приняты решения по всем найденным вариантам и кандидатам, проверены библиографические продолжения. Два последовательных независимых прохода на завершающем этапе не должны дать новых принятых результатов или существенных связей. Новый контрольный источник, не использованный в прежних решениях, также должен не обнаружить допустимого пропуска. Каждая новая принятая находка возвращает затронутые темы в цикл. Даже выполненный критерий характеризует конечный поиск, а не доказывает полноту математической области.

Как принятое содержание доходит до читателя

Как убедиться, что читатель получает именно принятую редакцию? Исправленная заметка остается во внешнем каталоге подготовки с адресным источником. Отдельно запускаемый сборщик извлекает адреса и отношения и рассчитывает индекс. Публикационный manifest связывает точные пути и контрольные суммы документов с неизменяемой коллекцией Content. API проверяет индекс и отдает тексты заметок; Порядок использует эту опубликованную проекцию. Изменяемая авторская заметка и опубликованная версия таким образом различаются.

Технический формат сохраняет лишь часть аргумента. ID получается из имени файла без расширения; точные разделы Опирается на и Используется в задают типизированные связи, остальные wikilinks дают reference. Индекс хранит концы и тип отношения, но не отдельный объект доказательства, номер шага или группы совместных опор. Поэтому объяснение использования Ролля должно оставаться в заметке. Поле confirmed сообщает повторную декларацию пары после удаления повторов парсером. Оно не свидетельствует о независимой математической проверке.

Читатель теперь может пройти обратно от карты к записи и выяснить, почему опора применима. Версия и происхождение связывают этот ответ с тем материалом, который принимали проверяющие. Изменение заметки требует проверки последствий; ее новая публикация должна согласовать текст и индекс. Расположение рассчитывается по записанным отношениям, а математический смысл этих отношений остается в тексте.

Какая область проверки принята

Какая из описанной работы уже принята? Аудит от 22 июля 2026 года относится к версии со статусом release candidate. Его заявленная область - 879 теоремных карточек, 849 в главах и 30 в фундаменте, а также 896 внутренних доказательных ребер. Эти числа закреплены в audit_run принятого manifest. Коллекция содержит 1165 документов-заметок и индекс: число документов уже тогда отличалось от числа проверенных карточек. Статья использует эту принятую проверку в ее области и не сообщает о новом поэлементном проходе. Связь свидетельств и версии.

Числа состава и композиции статьи получены на более поздней публикации от 12 октября 2026 года, зафиксированной для аналитики 13 октября. Она содержит 1230 файлов-заметок. baseline.json и SHA-256 опубликованного индекса фиксируют, какие данные использовал расчет. На этом входе воспроизведены 16 семейств анализа и 101 численная проверка, записанные в analysis-manifest.json. Они проверяют вычисления по одному входу, а не 101 теорему, и не повторяют карточный аудит. Методы и контрольные суммы.

В паспорте октябрьской публикации указан промежуточный рабочий снимок, опубликованный по поручению владельца. Общая математическая полнота, итоговая приемка четырнадцати глав и приемка ML-фундамента и порядка остаются открытыми. Чтобы установить, какие октябрьские записи наследуют июльскую приемку, нужно связать точные версии карточек с решениями об изменениях и затронутыми отношениями. Такого поэлементного соответствия для всех файлов нет. Даже прежний текст одного файла сам по себе не подтверждает его новое окружение.

Оговорка. Протокол объясняет, что следует проверить; manifest аудита указывает, какая версия и область приняты; аналитический журнал подтверждает расчетную приемку. Наблюдение API 13 октября установило совпадение с зафиксированным индексом на момент чтения. Поэтому структурные числа относятся к октябрьскому снимку, а принятая содержательная проверка - к июльской области. Переносить одну приемку на другую автоматически нельзя.

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

этапов объясняющей схемы протокола
6
карточек в области принятой июльской проверки
879
записей октябрьской публикации
1230

Источники главы

Ссылки и границы использованного чтения
ИсточникМесто и область подтверждения
MIT OCW 18.100A: Lecture 19Теоремы 5 (Ролль) и 7 (MVT), доказательства с.3-4; новое адресное чтение вне состава принятого DIG
Оговорки
  • Наличие протокола не подтверждает его выполнение для всех 1230 записей. Статья использует результаты принятого аудита в его прежних границах.
  • 101 численная проверка не является 101 независимым наблюдением или 101 теоремой.
05
Классификация

Разделы задают область. Фундамент связывает её.

53внешние записи фундамента

Предметная рубрика описывает содержание записи, авторский список выбирает основные разделы, а граф опор определяет внешний фундамент.

Где проходит граница Порядка

Теорема Коши об интегральной формуле находится в Опорном фундаменте Порядка, хотя ее предметная область - функции комплексной переменной. Комплексный анализ не входит в выбранные четырнадцать разделов. Ее место в прологе помогает различить два вопроса: к какой области относится результат и зачем он вошел в контекст выбранной математики. Папка отвечает на первый вопрос, записанные отношения опоры - на второй. Место в виртуальной панели не меняет предмет результата.

У этой записи сохраняются папка 30_Функции_комплексной_переменной и теги math/комплексный_анализ, msc/30E20. В индексе она отмечена как внешняя опора выбранных разделов (coreTail). Эти сведения взяты из зафиксированного снимка. Код MSC приведен как поле снимка. Пример показывает сохранение предметной принадлежности, а не результат новой проверки рубрики. На этом примере удобно разобрать границу Порядка: классификация помогает найти и описать запись, авторский отбор задает основную область, а обход отношений обнаруживает ее внешние опоры.

Четырнадцать разделов заданы явно. Протокол работы с корпусом связывает эту область с математическими основаниями ML и требует проверять выбранные разделы целиком, включая базовые и промежуточные результаты. Поэтому немедленная прикладная полезность теоремы для конкретной модели машинного обучения не служит единственным условием ее присутствия. Расчет располагает уже выбранный материал; он не восстанавливает за автора причины выбора каждой дисциплины.

Что именно классифицируется

Папка задает основное предметное место записи в корпусе. MSC-тег указывает предметную рубрику. Дополнительные математические и ML-теги описывают другие темы и применения записи. MSC2020 служит предметной классификацией математической литературы и поддерживается Mathematical Reviews и zbMATH. Названия и рубрики доступны в официальной базе MSC2020; назначение классификации описывает справка MathSciNet. Доказательная связь описывает записанное использование одного результата в аргументе другого. Два результата могут относиться к одной теме, не используя друг друга в доказательстве. И наоборот, доказательная опора может находиться в другой папке. Поэтому общую рубрику и использование результата устанавливают раздельно.

Классификация, отбор и фундамент

Папка и MSC описывают предмет записи. Авторский список выбирает основную область; направленные связи с опорами добавляют внешний фундамент.
МеханизмЕдиницаНазначение
ПапкаФайловая записьОсновное предметное место в корпусе
Основная MSC-рубрикаМетаданные записиПредметная классификация; согласование с папкой требует проверки
Дополнительные меткиЗапись и узел тегаПересекающиеся предметные характеристики
Класс тега (TagClass)Узел тегаКлассификация словаря тегов
Авторский список (CORE_FOLDERS)Явный список папокАвторский выбор 14 разделов
Обход к опорам (Prerequisite-BFS)Записанный граф опорВнешнее замыкание для выбранной области

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

В зафиксированной публикации каждая из 1230 разрешенных файловых записей имеет хотя бы один тег с префиксом msc/, включая все 967 кандидатов Порядка. Эта проверка отвечает только на вопрос о наличии метки. Чтобы оценить правильность классификации, нужен разбор назначенных рубрик; чтобы оценить полноту математического охвата, нужен перечень ожидаемых результатов. Заполненное поле не заменяет ни одну из этих проверок.

Поле tagClass хранит дополнительную группировку тегов. Префиксы msc/ и math/ распознаются непосредственно, а ml/ проходит словарную эвристику. Она сверяет название метки без префикса и его отдельные части со словарем и назначает первый подходящий класс: область, применение, метод или понятие. При отсутствии совпадения метка остается без класса. В обоих случаях правило описывает метку. Математический тип записи, правильность ее доказательства и включение в основные главы этим правилом не устанавливаются. Например, класс application у ML-тега обозначает словарную категорию применения. Одноименное ребро application связывает записи по объявленному использованию результата. Совпадение названий не создает такого ребра.

Различие предметных рубрик и математических понятий полезно и при сравнении с другими информационными системами. OntoMathPRO организует математические понятия и их отношения. LibMeta использует предметные рубрики вместе с терминологическим и библиотечным описанием. Эти работы помогают сформулировать различие между рубрикой, понятием и связью. Они не удостоверяют разметку Nareshka и не являются ее реализованной онтологией. OntoMathPRO, 2022, с. 30-31, LibMeta, 2024, с. 4-5 и 11.

Четырнадцать разделов как область чтения

Читатель уже встретил состав и опубликованный порядок четырнадцати разделов в первой главе. Теперь важна граница отбора: список папок задает исходные записи для поиска оснований. Сам классификатор охватывает и другие области. Папка функций комплексной переменной существует в корпусе, хотя не входит в этот список. Запись из нее включается как внешняя опора, если к выбранным результатам ведет prerequisite-путь; собственная рубрика записи при этом сохраняется.

Четырнадцать папок выбраны автором и перечислены явно. Алгоритм не выбирает их по числу записей, центральности или порогу размера. В частности, параметр coreMinNodes=20 не определяет состав этих разделов в MSC-Порядке. Сначала применяется перечень папок, затем зависимости влияют на расположение глав и записей. Поэтому большое число записей в комбинаторике не доказывает ее большую важность, а небольшой раздел вариационного исчисления не доказывает достаточность его охвата.

Рабочая область связана с математическими основаниями ML, но из ее состава нельзя вывести достаточную программу подготовки для любой ML/DS-задачи. Причины выбора каждой папки имеющиеся свидетельства не устанавливают; здесь рассматриваются заданный состав и способ его чтения.

Зачем нужен внешний фундамент

Доказательства не обязаны укладываться в границы выбранных каталогов. Если результат из основной главы использует внешнюю опору, читателю нужна возможность увидеть этот вход и открыть его текст. В Порядке такие записи собраны в отдельный пролог, называемый Опорным фундаментом. Исходные папки записей при этом сохраняются.

Основная область и внешний фундамент

Внешний фундамент F состоит из предков выбранной области C, лежащих за ее пределами. Обход идет от выбранных записей к опорам, навстречу направлению prerequisite-ребер.
ОбластьЗаписиПапкиПравило
Основная область C91414Явный авторский список
Фундамент F5318Путь от внешней опоры к C по связям prerequisite; F = A(C) вне C
Остальной корпус263Вне отбораНе включен в последовательность

Чтобы понять состав пролога, отделим внешние основания от опор внутри основных глав. Для этого рассмотрим граф Gp=(V,Ep)G_p=(V,E_p) зафиксированного снимка. Множество VV состоит из разрешенных файловых записей; EpE_p содержит только prerequisite-ребра, направленные от опоры к использующей записи. Узлы тегов и отношения application/reference в этот граф не входят. В данном снимке неразрешенных файловых целей нет.

Пусть C⊆VC\subseteq V - все записи четырнадцати выбранных папок. Обозначим через A(C)A(C) множество записей v∈Vv\in V, от которых существует направленный prerequisite-путь длиной хотя бы одно ребро к некоторой записи c∈Cc\in C. Так в A(C)A(C) попадают и внутренние, и внешние основания выбранных записей. Чтобы оставить только внешние, вычтем CC:

F=A(C)∖C.F = A(C) \setminus C.

Здесь FF обозначает внешний фундамент, а знак ∖\setminus удаляет из A(C)A(C) участников основной области. Путь содержит хотя бы одно ребро: одного членства в CC недостаточно, чтобы считать запись собственной опорой. При цикле некоторые записи из CC могут попасть и в A(C)A(C) по пути, содержащему ребра; разность множеств все равно исключит их из FF. Поэтому определение не требует заранее предположить ацикличность.

Проверим правило на маленьком условном графе. Пусть основная область состоит из двух записей, C={P,T}C=\{P,T\}, а все ребра заданы как P→TP\to T, Y→TY\to T и X→YX\to Y. Тогда A(C)={P,X,Y}A(C)=\{P,X,Y\}: запись PP дает внутреннюю опору, YY - прямую внешнюю, XX - внешнюю через YY. Вычитание CC оставляет F={X,Y}F=\{X,Y\}. Опора PP остается в своей основной главе. Это условный пример операции над множествами. Он показывает, почему внешний фундамент не перечисляет все основания Порядка: внутренняя опора PP в нем отсутствует.

Для расчета обход начинают сразу со всех записей CC и идут против направления prerequisite-ребер: от использующей записи к опоре. Затем ищут опоры найденных записей. Обход заканчивается, когда больше не находит новых участников; каждую запись учитывают один раз. Учитываются и связи с транзитивным флагом. Тематические теги, reference-ссылки, показатели центральности и цвет узла этого состава не определяют.

В зафиксированном снимке CC содержит 914 записей, FF - 53 записи из 18 внешних папок. Их объединение дает 967 кандидатов Порядка. Полный корпус содержит 1230 файловых записей, поэтому 263 остаются за границей этой выборки. Все численные характеристики этой главы относятся к публикации от 12 октября 2026 года и зафиксированному расчету 13 октября; привязка к версии и процедура проверки приведены в методах. Числа описывают состав выборки. Сколько точек одновременно различимо на экране, зависит от масштаба и настроек вида.

Среди восемнадцати внешних папок есть функции комплексной переменной, общая топология, теория чисел, теория полей и дифференциальные уравнения. Обход включает найденную опору; остальные записи ее папки автоматически не добавляются. Так объясняется место Коши, с которого началась глава: запись сохраняет классификацию комплексного анализа, а в композиции показывает внешний вход в выбранную область.

Пролог не становится пятнадцатой математической дисциплиной. Это место для внешней части контекста выбранной области. Для одной конкретной теоремы нужен другой набор: замыкание отдельной цели может включать и записи основных глав, и внешние опоры, тогда как FF объединяет внешние основания всей области CC.

Что гарантирует замыкание и чего еще требует доказательство

Обход отвечает на вопрос, из каких внешних записей можно дойти до основной области по записанным prerequisite-связям. Если существует prerequisite-путь от внешней разрешенной записи к записи основной области, эта внешняя запись попадает в FF. Но вычисление пути не проверяет математическую применимость его шагов. Нужно дополнительно установить, что версии результатов совместимы, пространства согласованы, гипотезы выполнены и шаг использования действительно относится к выбранному доказательству.

Это ограничение относится и к выбору доказательства. Глава об отношениях показала, как парная проекция объединяет опоры разных способов. Поэтому внешний контекст может оказаться шире оснований одного выбранного аргумента. Присутствие Коши в прологе означает, что от нее есть записанный путь к основной области; чтобы выяснить, где работает ее формула, нужно открыть конкретное использующее доказательство, сопоставить области голоморфности, допустимые контуры и положение точки. Из членства в FF эти условия не восстановить.

Здесь Опорный фундамент означает внешний prerequisite-контекст выбранных разделов в зафиксированной публикации. Это название не обозначает аксиоматический базис, минимальную обязательную программу ML или завершенную приемку всех совместимых доказательных маршрутов. Повторный обход может подтвердить тот же состав. Применимость доказательных шагов проверяют по их содержанию и условиям.

Как оценивать охват

Для разговора о полноте нужен перечень ожидаемого содержания. Протокол корпуса предусматривает несколько направлений поиска: канонические математические источники, университетскую базу и профильные прикладные или продвинутые источники. Канонические тексты помогают найти признанные результаты и их версии. Базовый учебный материал выявляет переходы, которые легко пропустить среди сложных теорем. Профильные источники показывают условия методов и промежуточные результаты, важные для заявленной области применения.

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

Проверка корректности уже существующей карточки не закрывает этот поиск. Две записи могут быть верными, а необходимая для перехода промежуточная опора - отсутствовать. При этом появление дополнительного MSC-тега само по себе не указывает на новую теорему: рубрика и математический результат остаются разными объектами.

Для октябрьского корпуса достаточность ML-фундамента и завершенный охват всех четырнадцати разделов по этим направлениям не установлены. Содержательная приемка принята для июльской версии. Октябрьский расчет проверяет более поздний снимок и не подтверждает сам по себе, что каждая его запись прошла ту же математическую проверку.

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

внешние записи фундамента
53
внешних папок фундамента
18
явный выбор области
CORE_FOLDERS

Источники главы

Ссылки и границы использованного чтения
ИсточникМесто и область подтверждения
OntoMathPROОфициальный PDF 2022; с.30-32, рис.3; принято чтение 7 страниц
LibMetaPDF издателя 2024; с.4-11, таблицы 1-4; §3, с.13-15, рис.7-8; принято чтение 21 страницы
AMS: MSC2020 database and search helpБаза MSC2020 и справка Search MSC; адресное чтение для предметной классификации, вне состава принятого DIG
Оговорки
  • MSC описывает предметную рубрику, а не использование результата в доказательстве. Параметр coreMinNodes не выбирает 14 папок основной области.
  • Обход к опорам не проверяет совместимость математических версий. Фундамент не является 15-й дисциплиной; его общей достаточности для ML не установлено.
06
Язык вида

Композиция делает отношения видимыми.

10визуальных различений

Цвет, слой, номер, размер и линия имеют отдельные значения. Их нельзя читать как единую шкалу сложности.

Что видно в одной точке Порядка

Выберем в Порядке на математической карте Теорему Коши об интегральной формуле. Она расположена в Опорном фундаменте, но относится к папке Функции комплексной переменной. В зафиксированном индексе у нее слой 2, дорожка 1, номер 22 и глобальная глубина 9. Панель показывает, что Коши входит во внешний контекст выбранных разделов; папка указывает математическую область; слой, дорожка и номер задают место в ленте. Глубина рассчитана по полному корпусу. Прочитаем эти признаки по очереди, чтобы по размеру точки не угадывать значение написанного на ней числа.

Перед нами панели 14 авторских разделов и отдельный фундамент. Основные разделы раскрыты, поэтому видна и их последовательность, и внутренняя лента каждого. При изменении размера окна панели могут перейти в другие ряды. Их порядок и нумерация сохраняются: меняется упаковка на экране, а не вычисленная композиция.

Цвет и рамка отвечают на разные вопросы

Цвет точки связан с реальной папкой записи. В основных разделах папка обычно совпадает с панелью, и цвет помогает узнать математическую область. У Коши цвет указывает на комплексные функции, а рамка помещает запись в фундамент. Пролог собирает внешние опоры выбранных разделов; включение в него сохраняет настоящую папку каждой записи.

По тем же настоящим папкам интерфейс различает линии. Если концы ребра относятся к разным папкам, связь считается межпапочной, даже когда обе точки стоят внутри рамки фундамента. Рамка объединяет записи по роли в композиции; цвет помогает узнать их предметную область. Оценку доказательства и значение результата для выбранной задачи нужно устанавливать по математическому тексту.

Как читать визуальные свойства

Цвет указывает на реальную папку; панель задает место в композиции. Слой, дорожка, номер, размер и линия передают отдельные свойства записи.
СвойствоЧто означаетЧего не означает
Принадлежность панелиМесто в композиции: основная область или виртуальный фундаментНе всегда реальная папка записи
Цвет папкиРеальная предметная принадлежностьМатематический тип или сложность
Слой (layer)Локальный слой после объединения сильно связных компонентГлобальную глубину
Дорожка (lane)Эвристическое расположение внутри слояЛогический порядок доказательства
Номер (rank)Локальный порядковый номерЦентральность
ПолкаНет внутриглавных файловых связейФакультативность или глобальную изоляцию
Базовый размер при sizing=depthГлобальная глубина файлового графа после сжатия циклов; фокус и статус дополнительно масштабируют точкуНе любой видимый размер, часы обучения или трудность
Линии при обычном фокусеНепосредственные соседи без учета направленияНе все предки цели и не доказательный маршрут
Межпапочная связь (cross-folder)Разные реальные папки на концах ребраНе синоним transitive
Транзитивная отметка (transitive)Отдельный флаг ребра; trans=1 допускает егоНе политика скрытия межпапочных ребер

Слой, дорожка и номер организуют ленту

Чтобы получить слои, алгоритм берет файловые связи между записями одной панели. Сначала он объединяет в группы записи, между которыми можно пройти по направлению связей туда и обратно. Такая группа называется сильно связной компонентой. В графе этих групп циклов уже нет, и слой можно определить по длине наиболее длинной цепочки от корней. Слои нумеруются с нуля. Поэтому слой 2 у Коши - третий слой внутри фундамента; связи с другими панелями в этот локальный расчет не входят.

В одном слое может оказаться много записей. Дорожка задает место каждой из них среди остальных; ее индекс тоже начинается с нуля. Дорожка 1 у Коши означает вторую позицию в слое. Если слой широк, записи переносятся в несколько видимых подколонок с сохранением порядка дорожек. Их взаимное расположение помогает разложить линии, но само соседство не добавляет математической связи, которой нет в данных.

Число на точке - локальный номер, поле seq.rank. Нумерация идет по слоям и дорожкам, а затем продолжается на полке. У каждой панели своя последовательность: номер 22 у Коши относится к фундаменту, а номер 22 в линейной алгебре - к другой ленте. Этот номер помогает найти место записи; показатели центральности и число оснований вычисляются отдельно.

На полку Вне цепочки попадают записи без учитываемых файловых ребер внутри собственной панели. В зафиксированном снимке Неравенство Коши-Шварца находится на полке линейной и полилинейной алгебры и имеет локальный номер 61. В поле слоя у него стоит -1, обозначающее полку за пределами основной ленты. Это значение не участвует в расчете глобальной глубины. Связи с другими разделами у записи могут сохраняться. Чтобы решить, нужна ли она для выбранного доказательства, придется прочитать ее роль в аргументе; положение на полке такого решения не принимает.

Почему глубина меняет размер точки

Слой ограничен одной панелью. Глобальная глубина отвечает на более широкий вопрос: сколько переходов содержит наиболее длинная цепочка до записи в полном файловом графе? Этот граф включает отношения разных типов и записи за пределами Порядка. Сильно связные компоненты здесь тоже объединены; все записи одной компоненты получают общую глубину. Корневой компоненте назначается ноль. Для остальных берется наибольшая глубина непосредственного предшественника и добавляется один переход. Если Pred⁡(C)\operatorname{Pred}(C) обозначает непосредственных предшественников компоненты CC, правило записывается так:

d(C)={0,Pred⁡(C)=∅,1+max⁡P∈Pred⁡(C)d(P),Pred⁡(C)≠∅.d(C)=\begin{cases} 0,&\operatorname{Pred}(C)=\varnothing,\\ 1+\max_{P\in\operatorname{Pred}(C)}d(P),&\operatorname{Pred}(C)\ne\varnothing. \end{cases}

Глубина считает переходы между компонентами в этой полной проекции. Кроме prerequisite в ней участвуют application и reference, поэтому результат нельзя читать как длину цепочки одних доказательных опор. Глубина 9 у Коши получена по полному корпусу, а слой 2 - по связям внутри фундамента. Различаются области расчета. Число переходов также не переводится в часы занятий: граф не измеряет трудность отдельного шага.

При выбранном размере Глубина программа использует это значение для радиуса точки. Сначала глубину делят на общий максимум по корпусу, затем берут квадратный корень и переводят результат в радиус. Обозначим через VresolvedV_{\mathrm{resolved}} все файловые записи загруженного корпуса с признаком resolved. Правило имеет вид:

D=max⁡(1,max⁡u∈Vresolvedd(u)),q(v)=min⁡(1,max⁡(0,d(v)D)),r(v)=4.2+13.8q(v).D=\max\left(1,\max_{u\in V_{\mathrm{resolved}}}d(u)\right),\qquad q(v)=\min\left(1,\max\left(0,\frac{d(v)}{D}\right)\right),\qquad r(v)=4.2+13.8\sqrt{q(v)}.

Здесь d(v)d(v) - глобальная глубина записи, DD - общий максимум с нижней границей 1, q(v)q(v) - нормированное значение, ограниченное диапазоном от 0 до 1. Нижняя граница DD исключает деление на ноль, если все глубины нулевые. При корректных глубинах 0≤d(v)≤D0\le d(v)\le D ограничение не меняет результат. Квадратный корень делает небольшие глубины заметнее: равное приращение глубины сильнее меняет радиус внизу шкалы и слабее - наверху. Базовый радиус лежит между 4.2 и 18 в координатах сцены; нормировка общая для корпуса, поэтому максимум отдельной панели не обязан давать радиус 18.

Для Коши этот расчет можно проверить численно. Принятый расчет зафиксированного корпуса дает максимальную глубину 17; при ее глубине 9 получаем

q=917,r=4.2+13.8917≈14.24.q=\frac{9}{17},\qquad r=4.2+13.8\sqrt{\frac{9}{17}}\approx14.24.

Число 14.24 относится к координатам сцены. Чтобы получить экранный радиус, его дополнительно умножают на масштаб камеры и коэффициент состояния точки. Поэтому этот расчет сам по себе не измеряет пиксели на снимке. В Порядке выбор задает коэффициент 1.4: при единичном масштабе камеры после завершения анимации расчетный радиус выбранной Коши будет около 14.24×1.4≈19.9414.24\times1.4\approx19.94 экранных пикселей. Наведение на невыбранную точку задает коэффициент 1.15, статус Можно браться без выбора и наведения - 1.06. При уменьшении масштаба камеры все эти точки снова выглядят меньше. Таким образом, увеличение при выборе не сообщает о внезапно выросшей глубине: данные записи остались прежними, изменилось визуальное состояние.

Вернемся к исходной точке: глубина 9 определяет ее базовый размер, а внутри остается локальный номер 22. Дорожка 1 задает позицию в слое; цвет указывает на комплексные функции, рамка - на фундамент. Признаки помогают одновременно узнать область записи и найти ее место в композиции. Трудность интегральной формулы из их сочетания не вычисляется. Числа примера взяты из зафиксированного индекса и принятого structure.json, а правило размера - из текущей реализации отображения. Их области и версии разделены в методах статьи.

Выбор точки раскрывает ее окружение

При включенном показе связей Порядок в спокойном состоянии оставляет разрешенные фильтрами внутрипапочные линии и скрывает межпапочные. Наведение или выбор выделяют непосредственное окружение точки из состава Порядка. Разрешенные фильтрами линии, касающиеся этой точки, могут появиться и между папками. Если курсор наведен на другую точку, именно она становится центром подсветки, получая приоритет над выбранной записью.

Подсветка находит соседей без учета направления ребра. Поэтому яркая соседняя точка может быть опорой выбранного результата, записью, которая его использует, или концом обычной reference-ссылки. Чтобы различить их, нужно прочитать направление связи и соответствующую часть карточки. Наконечник стрелки у файловой линии рисуется при активной подсветке или достаточном увеличении; в обзоре он может не различаться. Направление самого отношения сохраняется, даже когда наконечник не виден.

Видимость линии проверяется отдельно от подсветки соседа. На нее влияют включенный показ связей, выбранные типы отношений и требование confirmed. Поэтому соседняя точка иногда выделена, а соединяющая линия скрыта фильтром. В демонстрационной ссылке trans=1 допускает ребра с отметкой transitive, а trunk=0 отключает отдельный фильтр магистрали. Межпапочные линии при этом по-прежнему скрываются в покое и могут проявиться при фокусе. Пустое пространство между панелями само по себе не устанавливает отсутствие отношений. Демонстрационный вид задает основные параметры явно.

Что задает ссылка и что нужно уточнить на месте

Подпись Тихие в меню соответствует внутреннему значению focus: название точки появляется при наведении и выборе. Именно этот режим задает labels=focus в демонстрационной ссылке. Параметры, не указанные в ссылке, могут восстановиться из сохраненного состояния браузера. chainDir=inbound определяет направление соответствующего расширения, но сам не включает его. core=0 отключает дополнительный фильтр Ядро, но правило самого Порядка сохраняется: в свиток входят только записи resolved с опубликованным seq. Поэтому такая ссылка не раскрывает все остальные папки корпуса и не добавляет узлы тегов.

Наконец, яркость точек и полоса изученного в шапке панели могут отражать персональные отметки. Изученные записи приглушаются, записи Можно браться выделяются. Счетчик включает автоматически зачтенные основания и не является результатом независимой проверки понимания. Для проверки способности воспроизвести доказательство потребуется отдельная работа с его аргументом.

В принятом наблюдении 13 октября 2026 года при окне 2305 × 1165 CSS-пикселей были включены связи, выбран размер Глубина, выключены узлы тегов и отмечен режим Тихие. Выбор Коши и открытие ее формулировки наблюдались отдельно от численного расчета. Обзорный кадр был обрезан справа, поэтому не служит переписью всех точек. Объясняющая фигура этой главы передает смысл признаков и не выдает условную раскладку за снимок экрана. Текущий API со временем может вернуть другую публикацию; приведенные значения принадлежат зафиксированному индексу от 12 октября.

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

может отличаться от реальной папки
Панель
локальный номер
Номер (rank)
глобальная глубина
Глубина (depth)
Оговорки
  • Адрес страницы не фиксирует настройки, которые в нем не указаны и сохранены браузером. Межпапочные линии в обычном состоянии скрывает отдельное правило отображения.
07
Чтение

От утверждения к его опорам.

93уникальных предка регулятора LQR

Чтение доказательства Коши показывает, как вернуться от опоры к конкретному шагу аргумента. Отдельный пример регулятора LQR позволяет сравнить прямые опоры со всеми записанными предками.

Открыть результат и поставить вопрос

Почему значение функции внутри области можно получить интегрированием по ее границе? С этим вопросом откроем в Порядке Теорему Коши об интегральной формуле. Карта позволяет выбрать результат, прочитать условия и перейти к записанной опоре. После перехода предстоит главное: выяснить, что опора разрешает сделать в доказательстве, и вернуться с этим ответом к цели.

Именно эту запись выбрали в демонстрации. Карточка показала формулировку и тему Функции комплексной переменной, а вокруг точки проявились связи между панелями. Запись включена в Опорный фундамент, но остается в своей реальной папке комплексных функций. Рамка фундамента сообщает о роли записи в авторской композиции; папка сохраняет ее предметную принадлежность. Теперь от места на карте перейдем к самому утверждению.

Сначала условия, затем формула

В сохраненной формулировке кривая γ:[0,1]→C\gamma:[0,1]\to\mathbb C простая, замкнутая и кусочно C1C^1: концы совпадают, а на [0,1)[0,1) параметризация инъективна. Кривая ограничивает внутреннюю область Ω\Omega. Функция ff голоморфна на открытом множестве UU, содержащем все замыкание Ω‾\overline\Omega, а точка aa лежит внутри Ω\Omega. При положительной ориентации утверждается

f(a)=12πi∫γf(z)z−a dz.f(a)=\frac{1}{2\pi i}\int_\gamma\frac{f(z)}{z-a}\,dz.

Прочтем условия по их работе в аргументе. Простота контура выделяет одну внутреннюю область. Кусочная гладкость позволяет определить контурный интеграл по конечному числу гладких участков. Голоморфность на окрестности всего замыкания дает доступ к функции внутри области, на границе и в небольшом запасе вокруг нее. Внутренняя точка aa не лежит на контуре, поэтому знаменатель на контуре не обращается в нуль. Одного названия теоремы для проверки этих условий недостаточно.

Ориентацию запись задает индексом обхода:

Ind⁡(γ,a)=12πi∫γdzz−a=1.\operatorname{Ind}(\gamma,a)=\frac{1}{2\pi i}\int_\gamma\frac{dz}{z-a}=1.

Это соглашение фиксирует нужное направление. Обращение параметризации меняет знаки обоих контурных интегралов. Ниже получится равенство с индексом, которое учитывает этот знак; для исходной формулы без индекса существенно значение 1.

Чтение выбранного результата

После открытия опоры читатель устанавливает ее работу в аргументе и возвращается к цели. Следующий текст выбирают по оставшемуся математическому вопросу.
ШагВопрос читателяДействие
Выбрать цельЧто я хочу понять?Выделить запись в Порядке
Открыть формулировкуКакая именно версия утверждается?Прочитать гипотезы и заключение
Прочитать опоруГде она работает в аргументе?Сопоставить текст и условия
Вернуться к целиКак опора помогает выводу?Восстановить конкретный шаг
Расширить контекстКакое основание еще неизвестно?Выбрать следующий адресный текст

Какую часть интеграла нужно обнулить

В демонстрации из списка опор открыли Теорему Гейне-Бореля о компактности, затем вернулись к Коши. Чтобы понять назначение этой опоры, разберем сохраненный аргумент. Компактность понадобится для перехода от множества маленьких окрестностей к одному положительному запасу вокруг всей области. Сначала выясним, зачем такому запасу вообще появляться в доказательстве интегральной формулы.

Вычтем из функции ее значение в выбранной точке. На UU определим разностный частный

q(z)={f(z)−f(a)z−a,z≠a,f′(a),z=a.q(z)=\begin{cases} \dfrac{f(z)-f(a)}{z-a},&z\ne a,\\ f'(a),&z=a. \end{cases}

Вне aa это частное голоморфно. В самой точке предел частного равен f′(a)f'(a) по определению производной, поэтому дополненная функция qq непрерывна. Если удастся доказать, что ее интеграл по γ\gamma равен нулю, в исходном интеграле останется только часть с постоянным f(a)f(a). Так у вспомогательной функции появляется ясная задача.

Сохраненный маршрут решает ее через локальные первообразные. Первообразная для qq - функция FF, производная которой равна qq. В области с такой функцией интеграл вдоль кусочно гладкого пути определяется значениями FF на концах. Для замкнутого пути концы совпадают, и интеграл равен нулю. Сначала построим FF в маленьких окрестностях, затем свяжем эти окрестности вдоль всего контура.

Почему исключительная точка не мешает локальному шагу

Рассмотрим координатные прямоугольники вместе с окрестностью внутри UU. Если прямоугольник не содержит aa, частное голоморфно на его окрестности. Теорема Коши об интеграле дает нулевой интеграл по границе. Для прямоугольника, содержащего aa, нужно отдельно обойти точку, в которой пока установлена лишь непрерывность qq.

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

Непрерывность qq около aa дает постоянную верхнюю границу MM для ∣q∣|q|. Периметр оставленного участка стремится к нулю, когда квадрат уменьшается. Модуль интеграла по этому периметру не превышает MM, умноженного на его длину, и тоже стремится к нулю. Значит, интеграл по внешней границе равен нулю и в случае, когда прямоугольник содержит aa.

Теперь в достаточно малом открытом прямоугольнике выберем исходную точку и определим F(z)F(z) интегрированием qq по горизонтально-вертикальной ломаной от нее к zz. Нулевые интегралы по границам прямоугольников позволяют переставить порядок двух отрезков. Поэтому при комплексном приращении hh, достаточно малом для сохранения ломаной в этом прямоугольнике, разность F(z+h)−F(z)F(z+h)-F(z) можно вычислить по короткой такой же ломаной от zz к z+hz+h.

Остается проверить производную. Заменим на короткой ломаной q(w)q(w) постоянным значением q(z)q(z). Интеграл этой постоянной равен q(z)hq(z)h. Ошибка ограничена длиной ломаной, умноженной на наибольшее изменение qq вдоль нее. Длина не превышает 2∣h∣\sqrt{2}|h|, а изменение стремится к нулю по непрерывности qq. После деления ошибки на ∣h∣|h| она стремится к нулю; запись o(∣h∣)o(|h|) обозначает именно это свойство остатка. Получаем

F(z+h)−F(z)=q(z)h+o(∣h∣),F′(z)=q(z).F(z+h)-F(z)=q(z)h+o(|h|),\qquad F'(z)=q(z).

Таким способом первообразная построена и около исключительной точки. Для дальнейшего рассуждения можно выбрать маленькие диски внутри этих прямоугольников и ограничить на них FF. Ни один шаг не требует добавлять непрерывность производной f′f' к условиям исходной теоремы.

Где Гейне-Борель дает общий запас

Локальные первообразные еще не объясняют, как пройти по всему контуру и остаться в области определения функции. В сохраненном доказательстве теорема Жордана-Шёнфлиса дает гомеоморфизм плоскости HH, переводящий Ω‾\overline\Omega в замкнутый единичный диск KK. Гомеоморфизм переносит точки непрерывно в обе стороны. Здесь он нужен для построения стягивания контура; заменять через него переменную в комплексном интеграле мы не будем.

Множество H(U)H(U) открыто и содержит весь KK. Хотелось бы немного увеличить диск, не выйдя из H(U)H(U): тогда после обратного переноса получится открытая дисковая окрестность всего замыкания. У каждой точки KK есть свой маленький запас, но бесконечный набор положительных радиусов может стремиться к нулю. Получить один положительный радиус для всех точек позволяет компактность.

По Гейне-Борелю замкнутый ограниченный диск KK компактен. Для каждой его точки ww выберем шар B(w,r)B(w,r) так, чтобы удвоенный шар B(w,2r)B(w,2r) оставался в H(U)H(U). Это возможно благодаря открытости H(U)H(U). Выбранные шары покрывают KK; компактность позволяет оставить конечное подпокрытие B(wj,rj)B(w_j,r_j), где 1≤j≤m1\le j\le m. Теперь число

δ=min⁡1≤j≤mrj\delta=\min_{1\le j\le m}r_j

положительно: это минимум конечного набора положительных радиусов.

Проверим, как работает запас. Пусть x∈Kx\in K и ∣y−x∣<δ|y-x|<\delta. Выберем шар подпокрытия, содержащий xx. Тогда

∣y−wj∣≤∣y−x∣+∣x−wj∣<δ+rj≤2rj.|y-w_j|\le |y-x|+|x-w_j|<\delta+r_j\le 2r_j.

Точка yy лежит в удвоенном шаре и остается в H(U)H(U). Именно для этого мы выбирали шары с запасом на удвоение. При 0<η<δ0<\eta<\delta любая точка открытого диска B(0,1+η)B(0,1+\eta) находится от KK на расстоянии меньше η\eta, поэтому весь увеличенный диск лежит в H(U)H(U).

Перенесем этот диск обратно:

V=H−1(B(0,1+η)).V=H^{-1}(B(0,1+\eta)).

Полученное множество открыто, содержит Ω‾\overline\Omega, лежит в UU и гомеоморфно диску, а значит односвязно. Вот точная работа опоры: конечное подпокрытие дает положительный минимум, минимум обеспечивает единый запас, а запас позволяет построить дисковую окрестность всего замыкания. Теперь можно вернуться к задаче о нулевом интеграле.

Как связать локальные первообразные вдоль контура

В увеличенном диске образ γ\gamma можно стянуть к образу его начальной точки по прямым отрезкам. Начальная точка остается неподвижной. Обратное отображение H−1H^{-1} переносит это непрерывное стягивание в VV. Но гомеоморфизм не обязан быть гладким: промежуточные кривые могут не допускать контурного интегрирования. Просто объявить интеграл неизменным вдоль всех этих кривых было бы пропуском в доказательстве.

Вместо интегрирования по промежуточным кривым сохраненный аргумент использует конечную сетку. Представим стягивание как непрерывное отображение квадрата параметров: по нижнему краю идет исходный контур, верхний край и оба боковых края отображаются в его начальную точку. Квадрат компактен, поэтому его образ тоже компактен.

Покроем этот образ маленькими дисками с первообразными. Внутри каждого такого диска выбираются меньшие шары с запасом на удвоение. Конечное подпокрытие и минимум радиусов дают общий размер окрестности. Если диаметр участка меньше этого минимума, выбираем шар подпокрытия по одной точке участка; остальные его точки лежат в соответствующем удвоенном шаре и остаются в одном диске с первообразной. Это тот же прием, который только что превратил локальные радиусы в общий запас вокруг KK.

Непрерывное отображение компактного квадрата равномерно непрерывно. Поэтому сетку можно сделать настолько мелкой, чтобы образ каждой клетки целиком лежал в одном из выбранных дисков. Соединим образы соседних вершин сетки прямыми хордами. Диск выпуклый, так что хорды тоже лежат в нем. Теперь для каждой клетки есть кусочно гладкий замкнутый обход, интеграл по которому равен нулю благодаря первообразной.

Сложим эти равенства по всем клеткам. Каждое внутреннее ребро сетки встречается дважды, и одна и та же хорда проходится в противоположных направлениях. Внутренние интегралы сокращаются. Верхний и оба боковых края дают постоянные хорды и нулевые интегралы. Остается нижняя ломаная, соединяющая точки исходного контура.

На каждом участке нижнего края и исходная дуга контура, и заменяющая ее хорда лежат в одном диске с первообразной. У них одинаковые концы, поэтому их интегралы совпадают. Так нулевой интеграл по нижней ломаной переносится на исходный кусочно гладкий контур:

∫γq(z) dz=0.\int_\gamma q(z)\,dz=0.

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

Вернуться к исходной формуле

На контуре точка aa отсутствует, поэтому там можно разложить подынтегральное выражение:

f(z)z−a=q(z)+f(a)z−a.\frac{f(z)}{z-a}=q(z)+\frac{f(a)}{z-a}.

Первое слагаемое дает нулевой интеграл. Во втором f(a)f(a) - постоянная, которую можно вынести за знак интеграла. Получаем

12πi∫γf(z)z−a dz=f(a)Ind⁡(γ,a).\frac{1}{2\pi i}\int_\gamma\frac{f(z)}{z-a}\,dz =f(a)\operatorname{Ind}(\gamma,a).

При принятой ориентации индекс равен 1, и исходная формула доказана в выбранном маршруте. Если изменить ориентацию, равенство с индексом учтет смену знака. Теперь понятна вся роль вспомогательных шагов: локальные первообразные обнуляют маленькие обходы, стягивание позволяет собрать их вдоль контура, а компактность делает локальный контроль общим.

Глобальное равенство с индексом приведено также у Knapp, Basic Real Analysis, Digital Second Edition, 2016, Corollary B.41, с.688 для голоморфной функции в односвязной области и кусочно C1C^1-цикла. Там доказательство использует устранимую особенность разностного частного. В разобранном маршруте сохраненной записи непрерывный частный обрабатывается через прямоугольники, локальные первообразные и сетку стягивания. Одинаковое заключение не стирает различие маршрутов. Разбор этой записи не расширяет приемку на весь октябрьский корпус.

Предпросмотр карты показывает раздел Формулировка. Чтобы выяснить роль опоры, нужно открыть доказательство в тексте записи или адресном источнике. Более короткий пример такого чтения уже дан в главе о связях: Лагранж через Ролля; MIT 18.100A, лекция 19, теоремы 5 и 7, с.3-4 подтверждает тот отдельный учебный маршрут.

От выбора цели к плану и следующему тексту

Гейне-Борель дает общий положительный запас вокруг области; возврат к Коши показывает, зачем этот запас нужен в аргументе. Таблица различает действия в карте и проверку текста.
ОперацияДоступный результатУсловие
Порядок seq=1Композиция 14 разделов и фундаментаОсновной вид
Выбрать КошиНепосредственное окружение и карточкаОбычный фокус не включает цепочку
Открыть текстФормулировка и ее условияНаблюдение чтения отдельно от расчета
Запросить планПредки по записанным связям prerequisite и сама цельЦель плана отличается от текущего выбора
Выбрать следующий текстАдресное продолжение чтенияОтметка изученного не удостоверяет освоение

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

Прямые основания, путь и все записанные предки

Ближайшее окружение помогает сделать первый переход. Один путь показывает цепочку переходов. Полный набор предков добавляет основания оснований и боковые ветви. Эти три области нельзя заменять друг другом.

Для точного различения возьмем направленный граф G=(V,E)G=(\mathcal V,E), где V\mathcal V - записи корпуса, а EE содержит только prerequisite-ребра. Ребро u→vu\to v означает, что uu записан как основание для vv. Прямые основания цели tt - записи, из которых ребро приходит непосредственно в цель:

Direct⁡(t)={v∈V∖{t}:(v,t)∈E}.\operatorname{Direct}(t)=\{v\in\mathcal V\setminus\{t\}:(v,t)\in E\}.

Если повторять переход к основаниям, получится множество всех предков:

Anc⁡(t)={v∈V∖{t}:v⇝Et}.\operatorname{Anc}(t)=\{v\in\mathcal V\setminus\{t\}:v\leadsto_E t\}.

Здесь v⇝Etv\leadsto_E t означает, что от vv к tt существует направленный prerequisite-путь. Саму цель исключаем из обоих наборов; даже путь, вернувшийся в цель из-за цикла, не превращает ее в дополнительную тему. Каждая запись учитывается один раз, сколько бы путей ни вело от нее к цели. Поэтому объем записанного контекста определяется как cost⁡(t)=∣Anc⁡(t)∣\operatorname{cost}(t)=|\operatorname{Anc}(t)|. Различение пути и достижимости соответствует обычному языку ориентированных графов: Lehman, Leighton, Meyer, Mathematics for Computer Science, редакция 2018, §§10.2-10.3.

Проверим определения на условной схеме A -> B, B -> T, C -> B. Путь A -> B -> T пропускает C, хотя C записан как опора промежуточной записи B. Здесь Direct⁡(T)={B}\operatorname{Direct}(T)=\{B\}, а Anc⁡(T)={A,B,C}\operatorname{Anc}(T)=\{A,B,C\}: одна прямая опора и три уникальных предка. Это объясняющая схема, а не дополнительное измерение корпуса.

Путь и боковая опора

Путь A -> B -> T сохраняет одну цепочку. Множество предков T включает также боковую опору C -> B. Пунктир выделяет эту ветвь в условной схеме, а не флаг связи в Порядке.
Ребро условной схемыВ одном пути A -> B -> TВ полном контексте T
A -> BДаДа
B -> TДаДа
C -> BНетДа

Полный набор предков тоже не выбирает доказательство. Как показано в главе о связях, парная проекция теряет принадлежность опор способам доказательства. Ее замыкание может объединить материалы нескольких способов и расширить контекст цели за пределы выбранного аргумента. Группировку совместных входов явно описывают направленные гиперграфы; обычный путь и достижимость с такими входами различаются: Gallo, Longo, Nguyen, Pallottino, авторская рукопись, редакция октября 1992, с.4-6 и 15-19. Здесь эта работа объясняет границу парной проекции; такой решатель не объявляется частью VaultGraph.

Что означает большой контекст: пример регулятора LQR

В зафиксированном prerequisite-графе у Теоремы об оптимальном линейно-квадратичном регуляторе 7 прямых оснований и 93 уникальных предка из 17 реальных папок. Цель исключена из числа 93. Числа рассчитаны по публикации 2026-10-12T18:13:46Z и воспроизведены 2026-10-13. Это отдельный пример расчета; в браузерном эпизоде выбирали Коши.

Три разных масштаба контекста

Anc(t) содержит уникальных предков цели t по записанным prerequisite-связям. Число cost(t) = |Anc(t)| учитывает каждый файл один раз и исключает саму цель.
КонтекстСоставПредел
Прямые опорыНепосредственные входящие опорыНе все предки цели
Направленный путьОдна цепочка записанных отношенийПропускает боковые опоры
Множество предковВсе уникальные предки по связям prerequisite, кроме целиНе обязательные предпосылки всех возможных доказательств
Регулятор LQR, зафиксированная версия7 прямых; 93 уникальных предка; 17 папокОтдельный пример; не браузерный эпизод Коши

Прямые основания составляют 7/93≈7.53%7/93\approx 7.53\% числа предков этой цели. Остальные лежат дальше по входящим связям. Общая опора разных ветвей учитывается один раз. Дробь сравнивает две области записанного контекста, а не известную читателю долю математики или полноту доказательства.

Число 17 здесь считает реальные папки предков. Оно не обозначает учебные разделы Порядка: prerequisite-контекст может выходить за авторские 14 панелей. Для той же записи глобальная глубина тоже равна 17, но вычислена иначе - на полном файловом графе после сжатия сильно связных компонент. Глубина относится к наиболее длинным цепочкам той проекции, количество папок - к классификации prerequisite-предков. Совпадение значений не делает показатели взаимозаменяемыми.

Наличие 93 предков не обязывает сначала прочитать 93 незнакомые темы. Часть записей может быть уже знакома читателю; замыкание может объединять опоры разных маршрутов, а нарезка материала может отличаться от привычного учебника. Сопоставлять список нужно с конкретным пробелом в выбранном аргументе. cost(t) измеряет объем записанного контекста, а не трудность теоремы или время обучения.

Как выбрать действие в Порядке

Найти ближайшую опору

Если вопрос относится к одному шагу, начните с карточки. Обычный фокус подсвечивает непосредственных соседей без требования к направлению. Он не разворачивает автоматически весь Anc(t). Параметр chainDir=inbound задает направление для отдельно включаемой цепочки; само его наличие в URL такую цепочку не включает.

Список Опирается на отбирает входящие prerequisite-связи с заданным показателем посредничества ребра, упорядочивает их по этому показателю и показывает до трех строк. Это начало исследования, а не обещание полного списка прямых родителей. Три строки в карточке и семь прямых оснований результата могут описывать разные области отбора.

Раскрыть основания оснований

Если непонятное место уводит дальше ближайшей опоры, действие Что нужно знать для этого открывает план по входящему prerequisite-замыканию. В план добавляется и сама цель, поэтому число его записей равно ∣Anc⁡(t)∣+1|\operatorname{Anc}(t)|+1. Для LQR на зафиксированном графе ожидаются 94 записи вместе с целью. Это следствие определения и числа 93; выполнение такого браузерного действия здесь не заявляется.

Когда читатель выбирает строку основания, текущая запись меняется, а цель плана сохраняется. Можно разбирать Гейне-Бореля ради вопроса о Коши, не теряя исходную задачу. Персональная отметка изученного - третье состояние; ни цель плана, ни текущий выбор не являются такой отметкой.

Области действия операций

Фокус, план, тур и отметка изученного работают с разными наборами записей. Перед действием нужно понять, какую область оно сохраняет.
ОперацияОбластьОграничение
Фокус в ПорядкеНепосредственные соседи без учета направленияchainDir=inbound сам не включает цепочку
Карточка Опирается наДо трех опор, отобранных для карточки исследованияНе полный список прямых опор
План основанийПредки по записанным связям prerequisite и сама цельЦель плана и выбранный узел могут отличаться
Тур главыРеальная папка; записи Порядка вне полки с номером не ниже выбранногоНе виртуальная панель целиком
Тур планаПорядок планаНе гарантирует порядок последовательности
Отметка изученного (solved)Личные отметки и связи prerequisite между записями Порядка: оба конца имеют seqАвтоматические отметки оснований и готовность используют эту область, а не всю сеть; отметка не измеряет освоение

Продолжить последовательный просмотр

Тур плана проходит записи его групп. Группы задаются реальными папками и упорядочиваются по минимальной глубине записей и идентификатору папки, строки внутри - по глубине и названию записи. Цель поставлена последней в своей группе, однако группа цели может не быть последней во всем списке. Этот тур не обязан повторять Порядок панелей или глобальную топологическую сортировку. Он последовательно открывает выбранный контекст; проверять аргумент все равно нужно по тексту.

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

Связать две записи или вынести список

Поиск пути помогает связать уже знакомую запись с новой. По умолчанию он допускает prerequisite, application и reference и ищет в обоих направлениях. Найденный маршрут удобен для навигации; чтобы прочитать его как доказательную цепочку, нужно отдельно проверить направления, типы ребер и роль каждой опоры.

При копировании также стоит назвать нужный список. Экспорт плана дает сгруппированный Markdown-список с пустыми отметками. Копирование контекста обходит недиректированное окружение на выбранную глубину по всем типам связей. Теги не попадают в список названий, но участвуют в обходе: через tag-узлы на следующем шаге могут добавиться тематические соседи. Поэтому этот экспорт шире исключительно доказательного контекста. Ни один из списков автоматически не включает объяснение шага или оценку знаний пользователя.

Учитывать прочитанное, сохраняя смысл отметки

Персональный прогресс работает на prerequisite-подграфе, в котором оба конца каждого ребра имеют место в Порядке (seq). Отметка цели может автоматически зачесть еще не отмеченных предков этого подграфа. Состояние Можно браться означает, что сама запись еще не отмечена, а все ее прямые родители в той же области отмечены. Предпосылки без такого места в правиле готовности не участвуют.

Эту область учета нужно отличать от полного prerequisite-замыкания плана. Состояние solved отражает отметки и правила зачета, а не измеренное понимание или способность воспроизвести доказательство. Для показанного чтения хватило переходов между формулировкой, опорой и планом; менять прогресс ради демонстрации не потребовалось.

Что именно наблюдалось

В первом эпизоде проверки 2026-10-13 открыли Гейне-Бореля из списка опор и вернулись к Коши. В плане цель сохранялась при смене выбранной строки. Интерфейс показал 16 prerequisite-предков из 6 папок и 17 записей вместе с целью. Тур плана начался с Аксиомы выбора на шаге 1 из 17, затем его явно завершили. Контрольная сумма индекса этого эпизода не зафиксирована, поэтому числа относятся к наблюденному состоянию без отдельной привязки к замороженной версии.

Отдельная проверка производственной публикации получила ETag, совпадающий с замороженным индексом статьи. На этом графе действие Пролететь главой отсюда было доступно: тур начался с Коши на шаге 1 из 9, затем его завершили штатной кнопкой. Девять записей соответствуют отбору по ее реальной папке, месту в Порядке, отсутствию на полке и локальному номеру не ниже 22.

Проверены переход к опоре и возврат, состояние плана, начало и завершение обоих туров. Все 17 записей плана и все 9 записей тура главы последовательно не проходились; отметки прогресса не менялись. Доказательство Коши не читалось в самом браузерном сценарии. Математическая роль Гейне-Бореля разобрана отдельно выше по сохраненному аргументу, а числа LQR принадлежат отдельному расчету зафиксированного индекса.

Теперь выбор следующего текста опирается на вопрос к доказательству. Порядок удерживает общую композицию, пока читатель выясняет условия и роль конкретного основания. В следующей главе разберем, почему эта композиция имеет именно такую последовательность: по какому критерию расположены разделы и как вычислены слои внутри них.

уникальных предка регулятора LQR
93
прямых опор LQR
7
папок в контексте предков
17

Источники главы

Ссылки и границы использованного чтения
ИсточникМесто и область подтверждения
Gallo et al.: Directed Hypergraphs and ApplicationsАвторская рукопись, пересмотренная в октябре 1992; с.4-6 и 15-19; побайтовое совпадение с опубликованной журнальной версией не установлено
Lehman, Leighton, Meyer: Mathematics for Computer ScienceMIT редакция 2018-06-06 13:43; §§10.2-10.3 и 10.5
MIT OCW 18.100A: Lecture 19Теоремы 5 (Ролль) и 7 (MVT), доказательства с.3-4; новое адресное чтение вне состава принятого DIG
Anthony W. Knapp: Basic Real Analysis, Digital Second Edition (2016)Приложение B, следствие B.41, печатная с.688 (страница PDF 718): формулировка и доказательство на этой странице; адресное чтение вне состава принятого DIG
Оговорки
  • Браузерная проверка подтвердила открытие опоры и возврат к Коши; ее математическую роль при этой проверке не разбирали. В главе отдельно рассмотрен шаг с конечным подпокрытием из сохраненного доказательства Коши. У примера Ролля и Лагранжа есть отдельный подтверждающий источник.
  • Условная схема не измеряет пробел в знаниях и не устанавливает, какие опоры требуются совместно для одного способа доказательства.
  • Стоимость cost считает записи, а не личный пробел в знаниях. Путь без учета направления или по обычным ссылкам не является направленной цепочкой доказательных опор.
  • Первый браузерный эпизод показал 16 предков Коши из 6 папок, план из 17 записей с целью и начало тура плана; контрольная сумма индекса этого эпизода не зафиксирована.
  • В отдельной проверке публичного графа ETag совпал с контрольной суммой зафиксированного индекса. Подтверждены старт тура главы с шага 1 из 9 и штатная остановка. Полное прохождение 17 записей плана или 9 записей тура главы не наблюдалось; отметки прогресса не менялись.
  • Проверка интерфейса подтверждает наблюденный сценарий с действовавшими настройками, а не любые их сочетания.
08
Алгоритмы

Порядок рассчитывается под явную цель.

1 154межраздельные связи вперед

Порядок согласует расположение разделов с записанными связями. Внутри каждого раздела слои, дорожки и полка организуют записи; затем панели размещаются на экране.

Как из связей получается композиция

У результатов одного раздела могут быть основания в другом, а у результатов другого - основания в первом. Какой раздел поставить раньше? Отдельные записи можно чередовать, следуя их зависимостям. Порядок, однако, сохраняет каждый математический раздел целой панелью. Это ограничение заставляет выбирать между направлениями связей, даже когда граф отдельных предпосылок не имеет циклов.

Рассмотрим условный пример из шести записей; он объясняет ограничение композиции и не является дополнительным расчетом корпуса. В разделе A находятся записи a₁, a₂, a₃, в разделе B - b₁, b₂, b₃. Записаны три опоры из A в B: a₁ -> b₁, a₂ -> b₂, a₃ -> b₃. Еще одна опора направлена обратно: b₁ -> a₂. Граф записей ацикличен: его цепочка a₁ -> b₁ -> a₂ -> b₂ и отдельная связь a₃ -> b₃ нигде не возвращаются к началу. Однако целые разделы образуют два встречных потока. Если поставить A перед B, три связи пойдут вперед, одна назад. При порядке B, A вперед пойдет одна, назад три. Нельзя удовлетворить все четыре направления, сохранив разделы целыми; можно выбрать порядок с меньшим числом обратных переходов.

Межглавная задача Порядка состоит в таком согласовании. Сначала автор выбирает область из 14 разделов и задает предпочтительную последовательность. Затем алгоритм согласует расположение этих разделов с записанными связями. После выбора последовательности решаются еще две задачи: расположить записи внутри каждой главы и упаковать панели рядами под экран. Перестановка глав меняет последовательность разделов, а перенос ряда меняет геометрию той же последовательности. Ни один из этих расчетов не выбирает математическую область за автора и не проверяет доказательства.

Чего добивается порядок глав

Обозначим множество выбранных разделов через CC. Для разных разделов aa и bb величина W[a,b]W[a,b] равна числу учитываемых связей из aa в bb; если их нет, вес равен нулю. В условном примере W[A,B] = 3, W[B,A] = 1. Каждое ребро дает одну единицу счета. Трудность предпосылки, объем текста и время чтения этот вес не меняют. Критерий оценивает согласованность расположения со связями между файлами; число доказательств или обязательных учебных шагов из него получить нельзя.

Пусть k=∣C∣k=|C|, а pos\mathrm{pos} назначает каждому разделу свое место от 1 до kk. Для выбранной перестановки сложим веса пар, в которых источник расположен раньше цели:

J(pos)=∑a,b∈Cpos(a)<pos(b)W[a,b].J(\mathrm{pos}) = \sum_{\substack{a,b\in C\\\mathrm{pos}(a)<\mathrm{pos}(b)}} W[a,b].

Требуется найти перестановку с наибольшим JJ. При фиксированном наборе межраздельных связей общий вес постоянен, поэтому увеличение веса направлений вперед на столько же уменьшает вес направлений назад. В условном примере порядок A, B получает счет 3, а B, A - счет 1. Критерий выбирает первый порядок, сохраняя один обратный переход. Он не меняет состав CC и не исправляет ошибочные ребра: отбор разделов и проверка смысла связей предшествуют расчету.

Остается определить, какие ребра попадают в WW. Реализация собирает ребра между разрешенными файловыми записями выбранных папок, исключая связи с тегами. Она не требует только типа prerequisite и не удаляет связи с отметкой transitive. В зафиксированной версии все 1183 учитываемые межраздельные связи оказались prerequisite; 690 из них имеют отметку transitive. Ребра с такой отметкой также входят в вес. Отметка transitive описывает структуру опубликованного графа и не устанавливает ненужность опоры в доказательстве. Правило отбора принадлежит computeSequencing.ts; числа взяты из зафиксированного снимка и его расчета paths.json. Методы статьи сохраняют версии и точные локаторы.

Межраздельные связи и порядок

Связь идет вперед, когда раздел опоры стоит раньше раздела, который ее использует. В опубликованном порядке вперед идут 1154 из 1183 учитываемых ребер: 97.55%.

В опубликованном порядке вперед направлены 1154 из 1183 связей, то есть около 97.55%; 29 идут назад. Точный расчет подтверждает, что 1154 - наибольший достижимый счет; этот максимум имеют 60 перестановок. Ни фундамент, ни связи с ним не входят в этот знаменатель: виртуальный пролог добавляется первым отдельно. Поэтому доля 97.55% характеризует только расположение 14 выбранных разделов относительно учитываемых связей между ними. Математическую правильность утверждений и освоение материала эта доля не измеряет.

Условный пример в начале главы показывает причину возможных обратных направлений: расположение целых папок ограничивает допустимые перестановки отдельных записей. В реальном снимке 29 линий остаются обратными даже после точной оптимизации. Поэтому весь свиток нельзя называть строгой топологической сортировкой. Для конкретной темы читателю по-прежнему нужны переходы к ее опорам, разобранные в предыдущей главе.

Почему точный поиск здесь возможен

Полный перебор всех перестановок быстро становится дорогим: для k глав имеется k! порядков. Вклад пары разделов, однако, определяется только их относительным положением. Поэтому можно хранить лучший счет для каждого подмножества глав и использовать его при построении более длинного порядка. Такой расчет называется динамическим программированием.

Для подмножества S⊆CS\subseteq C обозначим через D(S)D(S) наибольший вес направлений вперед среди порядков, содержащих ровно разделы SS. Пустой набор дает счет 0. Теперь выберем последний раздел vv: все разделы S∖{v}S\setminus\{v\} стоят раньше него. Их лучший внутренний счет равен D(S∖{v})D(S\setminus\{v\}), а добавление vv приносит веса W[u,v]W[u,v] от каждого уже расположенного uu. Чтобы выбрать лучшую последнюю главу, сравним эти суммы для всех v∈Sv\in S:

D(S)=max⁡v∈S[D(S∖{v})+∑u∈S∖{v}W[u,v]],D(∅)=0.D(S) = \max_{v\in S}\left[D(S\setminus\{v\}) + \sum_{u\in S\setminus\{v\}} W[u,v]\right],\qquad D(\varnothing)=0.

В условном примере D({A}) = D({B}) = 0: внутри единственной главы нет межглавной пары. Для двух глав сравниваются два завершения: D({A}) + W[A,B] = 3 и D({B}) + W[B,A] = 1. Максимум равен 3, последней ставится B.

Рекурсия учитывает каждую пару один раз: при добавлении последнего раздела пары внутри остатка не меняют свой вклад, а все новые пары связывают этот остаток с последним разделом. У любого порядка SS есть последний раздел vv, а счет предшествующей части не превосходит D(S∖{v})D(S\setminus\{v\}): значит, правая часть рекурсии ограничивает сверху счет любого порядка. Эта граница достижима, потому что к лучшему порядку S∖{v}S\setminus\{v\} можно добавить vv; выбрав лучший из таких вариантов, получаем точный максимум. Для этого рассуждения не требуется ацикличность. Существенны фиксированная матрица W, попарная аддитивность и отсутствие дополнительных жестких ограничений на перестановки. В реализации используется эквивалентная форма динамического программирования по оставшимся продолжениям; формула выше объясняет математический принцип, а не копирует код построчно.

В реализации точный режим применяется при числе глав от 1 до 16, поэтому выбранные 14 разделов входят в его область. Фактический код затрачивает O(k² × 2^k) времени на динамическое программирование и O(2^k + k²) памяти: для каждого состояния перебираются кандидаты, а функция gainOf вновь суммирует входы по k главам. Подготовительный поиск вставками и заключительная стабилизация имеют свою дополнительную стоимость. При числе глав больше 16 остается эвристический поиск, поэтому точная гарантия для этой области не заявляется. Источник: computeSequencing.ts, строки 99-238.

Одинаковый максимум оставляет вопрос о выборе конкретной последовательности. Здесь участвует авторский исходный порядок, который в коде называется prior. Реализация начинает с него, улучшает счет перестановками-вставками, сверяет результат с точным максимумом и затем разрешает соседние перестановки в сторону prior без ухудшения графовой цели. Если поиск вставками уже достиг точного максимума, на стадии сверки с DP его порядок не заменяется реконструированным DP-порядком; последующая стабилизация еще может выполнить равноценные соседние перестановки. Процедура тем самым использует авторское предпочтение, но не гарантирует, что итог окажется глобально ближайшим к prior по произвольной метрике расстояния между перестановками. Не обещается и глобальный лексикографический минимум среди 60 решений. Устойчивость конкретной презентации и точность ее счета - отдельные свойства.

Шестьдесят оптимальных порядков показывают оставшуюся свободу композиции. По этой целевой функции они равноценны, но это ничего не сообщает о равенстве их учебного эффекта. Можно одинаково хорошо согласовать направления линий и по-разному познакомить читателя с идеями. Проверка такого различия потребовала бы отдельного исследования людей и заданий; численный расчет графа ее не заменяет.

Слой, дорожка и полка внутри раздела

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

Для построения внутренней ленты берутся файловые отношения prerequisite, application и reference, включая ребра с отметкой transitive. Связи с тегами исключены. Полученный слой относится к этой файловой проекции; для исключительно prerequisite-цепочки потребовалось бы другое правило отбора. Оставшиеся записи разбиваются на сильно связные компоненты. Внутри такой компоненты из каждой записи можно дойти по направлению связей до любой другой. Если компонента содержит цикл, поставить источник каждого ее ребра строго раньше его цели невозможно. Для одиночной компоненты без петли такого препятствия нет. Алгоритм сжимает компоненту в один объект. Полученный граф компонент ацикличен, и на нем уже можно вычислить слои. Этот механизм реализован в layoutChapter файла computeSequencing.ts и указан в методах.

Обозначим компоненту через vv, ее слой через L(v)L(v), а множество непосредственных предшественников через Pred⁡(v)\operatorname{Pred}(v). Слой равен длине самого длинного входящего пути в графе компонент. Корень без предшественников получает слой 0; для остальных компонент правило имеет вид:

L(v)=1+max⁡u∈Pred⁡(v)L(u),Pred⁡(v)≠∅.L(v) = 1 + \max_{u\in\operatorname{Pred}(v)} L(u),\qquad \operatorname{Pred}(v)\ne\varnothing.

Так источник учитываемого ребра оказывается в более раннем слое, чем его цель, если они принадлежат разным компонентам. Для prerequisite-ребра это соответствует направлению от опоры к использующей записи. Однако слой локален: L(v) считается по связям внутри данной главы, а не по всему математическому корпусу. Компонента первого слоя может иметь предпосылки в другой главе или в фундаменте. Номер слоя не измеряет математическую трудность и не показывает количество знаний, необходимых конкретному человеку.

В зафиксированном Порядке нет нетривиальных сильно связных групп ни в одной из 14 глав, ни в прологе. Поэтому сжатие циклов здесь описывает предусмотренный алгоритмом механизм, а не обнаруженный внутри опубликованной панели цикл. Этот локальный результат не удостоверяет ацикличность всей сети: межраздельные связи имеют другую область проверки. Источник наблюдаемого результата - paths.json, таблица sequencing.chapters, и поля scc_groups готовых таблиц фигур.

Слои, дорожки и полка

Две опоры A и C ведут к B, затем к T; S вынесен на отдельную полку. Схема условная. Таблица показывает координаты четырех реальных записей зафиксированной версии корпуса.
ЗаписьПанельРеальная папкаСлойДорожкаНомерГлобальная глубинаПолка
Аксиома выбораМатематическая логика и основанияМатематическая логика и основания0230Нет
Неравенство Коши-ШварцаЛинейная и полилинейная алгебраЛинейная и полилинейная алгебра-10610Да
Теорема Коши об интегралеОпорный фундаментФункции комплексной переменной0238Нет
Теорема Коши об интегральной формулеОпорный фундаментФункции комплексной переменной21229Нет

Слой задает этап внутриглавной ленты, но еще не определяет места записей внутри него. Для этого служат дорожки. Первичный порядок детерминирован через глубину, PageRank и название; затем выполняются шесть пар проходов с барицентрической перестановкой. При проходе по входам позиция компоненты ориентируется на среднее текущих позиций ее предшественников, при проходе по выходам - последователей. Компоненты сортируются по этим средним; равенства разрешаются текущей позицией. Длинные связи учитываются непосредственно, без добавления фиктивных промежуточных вершин.

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

Полка сортируется отдельно: сначала по возрастанию глобальной глубины, затем по убыванию PageRank и по названию. Эти величины помогают получить повторяемый порядок размещения; они не превращают PageRank в оценку важности для конкретного читателя. Например, в разделе вещественных функций 84 записи образуют 12 слоев и полку из 5 записей. В численном анализе 79 записей распределены между 3 слоями и полкой из 48 записей. Здесь сравниваются число слоев и число записей без внутриглавных связей. Плотность графа из этих величин не следует: для нее нужны число ребер и явно заданный знаменатель. Такое сравнение также не доказывает, что численный анализ проще вещественных функций. Числа взяты из order-pilot/figure-data.json, таблицы chapter_rows.

После раскладки seq.rank нумерует записи каждой главы отдельно: по слоям, внутри слоя по дорожкам, затем по полке. Это локальная последовательность чтения. Она не является PageRank, вероятностью освоения или общей нумерацией всего корпуса. Поэтому два одинаковых номера в разных главах не означают одинакового положения в единой цепочке предпосылок.

Что меняет ширина окна

Данные композиции рассчитываются заранее и публикуются вместе с индексом. Браузер читает порядок глав, слои, дорожки и полку, затем преобразует их в координаты. В Порядке физическая симуляция останавливается, а вычисленные позиции закрепляются.

Широкий слой разбивается на подколонки, в каждой из которых помещается не больше 12 дорожек. Чтение сверху вниз и затем слева направо сохраняет исходный порядок дорожек. Сами главы упаковываются рядами в уже установленной последовательности. Чтобы выбрать переносы рядов, геометрический алгоритм перебирает предельную ширину ряда с шагом 200 координатных единиц сцены. Для каждого кандидата главы последовательно упаковываются слева направо; полученный свиток имеет определенные ширину и высоту. Браузерная раскладка задает целевое отношение ширины к высоте по окну, ограничивая его интервалом от 1.2 до 2.4. Поэтому на очень узком или очень широком экране цель отличается от исходных пропорций окна. Затем отношение ширины свитка к его высоте делится на целевое отношение, и берется модуль логарифма этого частного. Нулевая оценка означает совпадение пропорций; меньшая оценка предпочтительна.

Выбирается лучшая из перебранных упаковок; оптимальность по всем возможным разрывам рядов не гарантируется. При изменении размеров окна глава может перейти в другой ряд, сохраняя место в последовательности, номера слоев и локальный порядок записей. Первичный источник: sequencingLayout.ts, функции computeSeqGeometry и seqNodeTarget; остановка симуляции описана в владельце runtime initializeVaultGraphSession.ts.

В результате читатель получает два уровня организации материала. Оглавление сохраняет целостность выбранных математических разделов, а внутренняя лента показывает ход записанных отношений внутри каждого из них. Обратная межраздельная связь, запись на полке и предпосылка из фундамента остаются содержательными поводами открыть конкретный контекст. Композиция помогает сохранять маршрут и возвращаться к опорам. Ее вычислительные гарантии относятся к счету связей и заданным правилам раскладки; правильность доказательства и понимание читателя требуют других свидетельств. С этим различием можно содержательно сравнить Порядок с другими системами представления математики.

межраздельные связи вперед
1154
учитываемых межраздельных ребра
1183
ребер назад
29
Оговорки
  • Все 1183 учитываемых ребра имеют тип prerequisite; 690 отмечены как transitive. Связи с фундаментом не входят в критерий порядка разделов. Наличие 60 равных оптимумов не оценивает качество обучения.
  • Условный ациклический граф не является снимком Порядка или найденным фрагментом корпуса. В зафиксированных панелях нет сильно связных групп из нескольких записей. Четыре реальные записи выбраны для различения координат, а не как типичные представители.
  • Объединение сильно связных компонент и расчет слоев по длиннейшим путям предшествуют барицентрическим проходам и присвоению локальных номеров. Глобальная глубина рассчитана отдельно по полному файловому графу.
10
Синтез

Собственная система имеет ясные границы.

967кандидатов авторской последовательности

Порядок помогает увидеть выбранный контекст и перейти к нужному тексту. Математическую корректность записей, достаточность отбора и эффект для обучения приходится проверять отдельно.

От выбранной области к самостоятельному чтению

Порядок соединяет оглавление выбранной математической области с доступом к записанным основаниям результатов. Читатель может удерживать перед собой 14 разделов, выбрать результат и вернуться от его места в композиции к точной формулировке. Последовательность на карте направляет чтение, а доказательство объясняет, почему результат верен.

Эту возможность создают несколько связанных решений. Автор задает область и предпочтительную последовательность разделов. Методология устанавливает, что требуется проверить у записи и отношения. Индекс превращает записанные связи в данные для расчета. Алгоритм располагает главы и строит внутри них ленты записей. Интерфейс возвращает читателю математический текст и несколько способов исследовать его окружение.

Для зафиксированной октябрьской публикации область состоит из 914 записей основных разделов и 53 внешних опор. Композиция согласует направление 1154 из 1183 учитываемых межраздельных связей с порядком глав. Числа описывают состав области и достигнутый счет композиции на зафиксированном входе. Полноту выбранной математики и понимание читателя придется оценивать по другим основаниям. Авторское предпочтение также сохраняет роль: графовая цель допускает 60 равнооптимальных порядков, а фундамент вынесен вперед отдельным решением. Порядок показывает одну конкретную композицию, сохраняя возможность вернуться к опоре в предыдущей панели. Версия, знаменатели и проверка расчета.

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

Что именно удалось организовать

Вернемся к эпизоду Коши. В Порядке запись находится в Опорном фундаменте, но сохраняет предметную принадлежность к функциям комплексной переменной. Выбор записи открывает формулировку; переход к Гейне-Борелю из списка опор и возврат к цели были наблюдены в интерфейсе. Так проверена навигационная часть эпизода. Назначение опоры выясняется при чтении доказательства: предпросмотр показывает формулировку, поэтому за полным аргументом нужно обратиться к исходной записи или источнику.

В главе о чтении мы разобрали роль компактности в сохраненном доказательстве Коши. После топологического перехода через Жордана-Шёнфлиса замкнутая область представлена замкнутым единичным диском KK внутри открытого множества WW - образа области голоморфности. Чтобы продолжить аргумент, нужен немного больший диск, все еще лежащий в WW. Для каждой точки w∈Kw\in K выбирается положительный радиус rr, при котором B(w,2r)⊂WB(w,2r)\subset W. Шары B(w,r)B(w,r) покрывают KK, а Гейне-Борель позволяет выбрать из них конечное подпокрытие B(wj,rj)B(w_j,r_j), j=1,…,mj=1,\ldots,m. Поэтому можно взять общий положительный запас

δ=min⁡1≤j≤mrj>0.\delta=\min_{1\le j\le m}r_j>0.

Конечность покрытия обеспечивает положительность минимума. В полном разборе неравенство треугольника показывает, что все точки на расстоянии меньше δ\delta от KK остаются в WW; отсюда получается нужный больший диск и затем односвязная окрестность исходной замкнутой области. Так открытая опора отвечает на конкретный вопрос доказательства: локальные окрестности дают один запас для всей области. У бесконечного набора положительных радиусов такого запаса могло бы не быть. Проверен этот локальный шаг выбранного аргумента; условия глобального топологического перехода и остальные шаги интегральной формулы разобраны отдельно. Полный маршрут со всеми оценками приведен в главе о чтении; другие доказательства Коши могут использовать иные опоры.

Этот эпизод показывает, как работают решения Порядка вместе. Классификация удерживает предмет записи, виртуальный фундамент показывает ее роль за границей основных разделов, навигация приводит к опоре, а доказательный текст устанавливает математический переход. По карте можно найти запись и увидеть ее окружение; по фрагменту доказательства - восстановить положительный запас. Порядок дает доступ к обоим масштабам: месту результата в корпусе и тексту его оснований.

Что читатель может делать с этой конструкцией

Следующий шаг чтения определяется тем, что осталось непонятным в аргументе. Для примера Коши таким вопросом стало получение одной окрестности для всей замкнутой области. Этот вопрос указывает, какие условия и какой шаг искать в основаниях. Открытая формулировка сообщает допустимые объекты; доказательство показывает место, где понадобилось нужное свойство.

Чтобы искать опору, можно начать с непосредственного окружения цели и затем расширить контекст. Карточный список Опирается на показывает до трех оснований и служит начальным указателем. В Порядке обычный фокус показывает соседей без требования к направлению, а план оснований следует входящим prerequisite-связям и включает саму цель. Выбранная строка плана открывает основание, сохраняя целевой вопрос. Так читатель может обратиться к Гейне-Борелю ради Коши и затем вернуться к аргументу. Полные правила операций разобраны в главе о чтении.

Для линейно-квадратичного регулятора разница особенно заметна: за 7 прямыми основаниями расчет находит 93 уникальных предка из 17 реальных папок. Это объем записанного контекста, а не приказ изучить 93 темы до открытия доказательства. Замыкание может объединять основания альтернативных маршрутов; часть текстов может быть уже знакома, а нарезка материала может отличаться от принятой в учебнике читателя. Решение о следующем чтении принимается после сопоставления контекста с конкретным разрывом в аргументе. Множества Direct и Anc и область чисел LQR.

После чтения опоры нужно вернуться к цели. В примере компактности возврат позволяет проверить, появился ли нужный общий запас и разрешает ли он следующий шаг. Можно дополнительно спросить, где именно использована конечность покрытия и что останется без нее. Такой вопрос проверяет роль гипотезы, а не память на название теоремы. Предлагаемая практика состоит в этом цикле: уточнить цель, найти опору, разобрать условия и шаг, вернуться к аргументу, затем решить, нужен ли более широкий контекст.

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

Почему возможность чтения еще не доказывает эффект обучения

Что известно о понимании при таком чтении? Во внешних исследованиях получены разные результаты, и каждый относится к своему заданию и способу предъявления материала. В прочитанной v2 Explorable Theorems 16 студентов бакалавриата по компьютерным наукам из одного университета работали в обоих сравниваемых условиях на разных заданиях; порядок инструментов уравновешивался. Помимо отдельного задания на резюме, участники отвечали на вопросы о доказательствах. Авторы сообщили среднюю оценку правильности этих ответов сразу после чтения: 2,58 в интерактивном условии против 1,58 в контрольном по шкале 0-3. Оценщик не знал, к какому условию относится ответ. Шкала оценивает ответы в этом сравнении; переводить ее в процент освоенной математики нельзя. Explorable Theorems, arXiv:2604.02598v2, §§4.2-4.4 и 5.1, приложение B.

Контроль включал тот же письменный математический текст, Gemini, готовые запросы и возможность свободных вопросов. Интерактивное условие объединяло примеры, проверку входов, конкретные шаги, зависимости и сравнение доказательств. Поэтому положительный результат относится ко всему набору функций. Отдельный причинный вклад графа в этом опыте не выделен. В другой задаче той же работы значимого различия в непосредственном восстановлении порядка шагов не обнаружено. Этот результат не доказывает эквивалентность условий. Он показывает, почему выигрыш по правильности ответов нельзя переносить на все виды понимания. Участники были подготовлены к чтению коротких доказательств; выборка была мала. Отложенное сохранение знаний и самостоятельный перенос на новые задачи не оценивались. Уравновешивание порядка не устраняет все возможные различия заданий и перенос между условиями. Та же v2, §§5.2 и 6.1.

Другую картину дает исследование e-Proofs. Во втором опыте с 34 участниками не установлено преимущества пошагового мультимедийного объяснения над текстом по заданиям понимания сразу после чтения. Все сначала читали текстовые доказательства, затем e-Proofs. Такой порядок мог влиять на сравнение; он не был уравновешен. Отсутствие значимых различий также не устанавливает эквивалентность форматов. Roy, Inglis и Alcock, 2017, §5, с.257-262.

В первом опыте участвовали 49 человек. При отложенной проверке время теста сократилось с 30 до 20 минут, а предъявляемое доказательство - с 9 до 8 строк. На каждом тесте обе группы работали в одинаковых условиях, что сохраняет возможность сравнить изменение баллов между группами. Однако абсолютное падение баллов нельзя считать чистой скоростью забывания: вместе со временем изменились условия проверки. e-Proofs объединял несколько средств объяснения; отдельный граф не испытывался. Это исследование предостерегает от общего обещания, что пошаговое предъявление улучшает понимание и сохраняет знания при любых заданиях. Roy, Inglis и Alcock, 2017, §§4-5 и supplement, с.1-2.

Для практики чтения важны различия между вопросами: объяснить общий замысел, оправдать шаг, восстановить порядок и применить идею к измененному случаю - разные задания. Прочитанный авторский текст Mejia-Ramos и соавторов дает модель таких вопросов о понимании доказательства, а не экспериментальное подтверждение интерфейса Порядка. Модель оценки понимания доказательства, 2012, §§3-5.

Мы предлагаем проверять собственное чтение по поставленному вопросу: например, объяснить, почему конечное покрытие дало положительный запас. Это предложение согласовано с различием заданий; внешние исследования не устанавливают его оптимальность. У Nareshka здесь нет собственного эксперимента с читателями. Наблюдение открытия карточки подтверждает доступ к тексту; воспроизведение расчета подтверждает композицию по данному входу. Чтобы установить изменение понимания, потребовались бы ответы читателей, процедура оценивания и основание сравнения. Подменять это оценкой 2,58 из другой системы было бы неверно.

Где проходят границы результата

Границы Порядка определяются тем, какие сведения записаны и как они представлены. Парная проекция не хранит все совместные и альтернативные наборы опор, а нарезка записей влияет на число предков и длину пути. Контекст дает тексты для дальнейшего чтения. Чтобы выбрать опоры одного доказательства, нужно разобрать их совместность и роль в этом аргументе. Размеры 14 разделов описывают выбранную область; достаточность для любой ML/DS-задачи и завершенный охват математики из этих размеров не следуют.

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

Авторский Порядок дает выбранной области обозримую композицию и путь от математической цели к ее записанным основаниям. Проверенный шаг компактности показывает, как этот путь может закончиться содержательным ответом: локальные окрестности превращаются в общий запас благодаря конечному подпокрытию. Следующий шаг выбирается уже по роли опоры и выполненным условиям. Последняя глава дает версии, источники и процедуры, позволяющие проверить отдельно состав, вычисление, навигацию и математическое свидетельство.

кандидатов авторской последовательности
967
разделов авторской области
14
учебный эффект Порядка
не измерен

Источники главы

Ссылки и границы использованного чтения
ИсточникМесто и область подтверждения
Explorable TheoremsТочная версия v2; §§4.2-4.4/5.1-5.2/6.1, приложение B; принято чтение полного основного текста, приложений A-B и фигур 2-6; комплексное сравнение при N=16
Mejia-Ramos et al.: An assessment model for proof comprehension in undergraduate mathematics31-страничная рукопись, §§3-5; DOI 10.1007/s10649-011-9349-7; не эксперимент по воздействию на обучение
Roy, Inglis and Alcock: Multimedia resources designed to support learning from written proofs: an eye-movement studyОпубликованная журнальная версия Springer, 18 страниц + ESM1; §§4-5, ESM1 с.1-2; в исследовании 1 повторно использованы данные, исследование 2 имеет отдельную выборку n=34
Оговорки
  • Собственного эксперимента о влиянии Порядка на обучение нет. Внешние исследования комплексных интерфейсов не измеряют его эффект. Полнота покрытия математики, достаточность для ML и совместимость всех условий не установлены.
11
Методы

Выводы доступны для проверки.

6этапов воспроизводимости

Конкретное утверждение проверяется по своему источнику: тексту, декларации, публикации, пересчету или наблюдению интерфейса.

Как проверить одно число и стоящий за ним вывод

У линейно-квадратичного регулятора в статье указаны 93 предка. Проверить это число значит восстановить конкретный счет: найти целевую запись в том же индексе, выделить prerequisite-отношения, пройти к опорам и посчитать каждую достигнутую запись один раз. Совпадение результата еще нужно истолковать. Девяносто три - объем записанного контекста; количество путей и личный пробел читателя были бы другими величинами. Проследим этот пример от версии источника до расчета, а затем проверим тем же способом остальные используемые числа.

Численный счет, математический аргумент и действие интерфейса проверяются по разным основаниям. Обход графа может подтвердить множество предков, но не применимость каждой теоремы из этого множества. Для применимости придется открыть условия и доказательство. Успешное открытие карточки подтверждает доступ к записи в наблюденной сессии. Различая эти проверки, можно установить, что именно поддерживает вывод, и не переносить успешный результат на другой вопрос.

Основной объект численного исследования - опубликованный набор msc2020 от 12 октября 2026 года, 18:13:46 UTC. Его копия зафиксирована 13 октября для расчетного запуска paper-20261013. Эта версия содержит 1230 файловых записей в 53 папках и 990 теговых узлов. Из 7406 связей 2763 соединяют файловые записи, а 4643 связывают записи с тегами. В файловом слое находятся 2740 отношений prerequisite, 15 application и 8 reference. Отсутствуют неразрешенные ссылки. Нулевая величина последнего счетчика говорит о разрешении адресов, а не о математической истинности содержимого.

Из этой версии Порядок берет 914 записей четырнадцати авторских разделов и 53 внешние опоры из 18 папок: всего 967 кандидатов композиции. Для доли вперед направленных межглавных связей используется другой знаменатель - 1183 ребра между основными разделами, без фундамента. Поэтому проверка любого числа начинается с единицы счета: запись, ребро или пара записей. Затем устанавливают множество, на котором оно получено.

Сначала установить, какую публикацию мы проверяем

Живой адрес может со временем вернуть новую публикацию. Чтобы восстановить расчет статьи, нужен сохраненный индекс с определенной контрольной суммой. SHA-256 его байтов равен:

9e7b523e8aecee7d62d091c1eb628744d3e9bec78c30cf2db0e92cf3a50ca88e

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

b16d202fc74d89aa5bf655e44beef06c7f742a1a417f10fa4ba83460b1e8a8e4

Ревизия производителя индекса в паспорте расчета - 44aadcfe722317294a7adefcc59f2d6b100f7358. Дополнительно сохранены хеши его исходников: номер Git-ревизии сам по себе не описывает возможные изменения рабочей копии. Расчетное окружение зафиксировано как Python 3.13.11, NetworkX 3.7, NumPy 2.5.4 и SciPy 1.18.1. Эти сведения относятся к выполненному расчету, а не к требованиям для чтения статьи в браузере.

Публичный индекс Graphs API - адрес текущей публикации. 13 октября 2026 года в 11:18:12 и 11:18:42 UTC адресные проверки получили HTTP 200 и ETag, совпавший с приведенным хешем. Содержимое ответа также сравнили с зафиксированным индексом. Это наблюдение состояния API в указанное время; для поздней проверки расчета по-прежнему нужны сохраненный вход и его контрольная сумма.

Штатная пересборка индекса на зафиксированных исходниках дала тот же SHA-256, а опубликованный и пересобранный JSON совпали по содержимому. Схемная проверка приняла оба индекса, включая ссылки между 2220 узлами и 7406 ребрами. Побайтовое совпадение проверяет идентичность файла. Сравнение JSON проверяет равенство его содержимого, а схема - допустимую структуру и ссылки. Ни одна из этих проверок не читает математический аргумент заметки. Их результат нужен, чтобы вычислитель и читатель проверяли одну публикацию.

От заметок корпуса к читателю

Каждый этап сохраняет связь с выбранной версией заметок. Текст, опубликованный индекс, рассчитанные координаты и действие интерфейса проверяют отдельно.
ЭтапЧасть системыЧто проверяется
Исходные заметкиМатематический корпусТекст и исходные декларации
Сборщик индексаИнструменты сборки графаРазбор разметки, объединение деклараций, поля Порядка
Неизменяемая коллекция ContentПубликация ContentТочные байты и контрольная сумма
Проверенный Graphs APIСервер графаСхема и состав опубликованного индекса
ПорядокИнтерфейс графаПроекция, действующие настройки и геометрия
Зафиксированный расчет и статьяВоспроизводимый пересчетПривязка входного хеша к числам и фигурам

От авторской заметки до опубликованной композиции

Корпус начинается с Markdown-заметок во внешнем каталоге. Производитель индекса запускается явно: он извлекает адреса и отношения, вычисляет производные поля и записывает результат. Публикационный manifest перечисляет точные пути документов, вид каждого ресурса, MIME-тип и SHA-256. Импортер переносит эти байты в неизменяемую коллекцию Content. Graphs API проверяет хранение, целостность и схему, после чего клиент читает индекс и показывает Порядок. На этой цепочке математический текст превращается в удобную проекцию, но доказательство из стрелок заново не возникает.

Данные и главы статьи также публикуются одной согласованной Content-коллекцией. У нее свои контрольные суммы текстов и bundle. Таким образом, отдельно фиксируются исследуемый корпус и рассказ о нем: редактура главы не меняет математические заметки, а обновление живого корпуса не пересчитывает числа принятой статьи. Число публикационных файлов статьи тоже не становится дополнительным наблюдением графа.

Для проверки 93 предков нужно найти ту же цель по файловому ID. Парсер получает ID из имени файла без расширения, а заголовок H1 и путь хранит отдельно. Два имени, совпадающих без учета регистра, запрещены: такой адрес неоднозначен. В wikilink удаляются подпись, указание на заголовок и префикс папки, поэтому ссылка адресует запись целиком. Перенос файла с прежним именем сохраняет ID; переименование меняет его. Текст при том же ID может обновиться, поэтому одного адреса недостаточно без версии заметки.

Типизированные связи извлекаются из точных разделов Опирается на и Используется в; другие wikilinks становятся reference. Если A опирается на B, направление prerequisite в индексе - B -> A. Повторы и обратные декларации нормализуются до канонической пары; при конкуренции типов приоритет имеет prerequisite, затем application, затем reference. Приоритет выбирает не только тип, но и направление декларации с более высоким приоритетом. Если две противоположные декларации имеют одинаковый тип, сохраняется первое встретившееся направление; такой конфликт требует содержательного решения. Еще до этого парсер удаляет повтор одной цели ссылки в пределах одного типа и одного файла. Поэтому техническое поле confirmed означает не менее двух оставшихся деклараций пары, а не любые два появления ссылки в тексте. Сам производитель индекса не читает доказательный шаг и не превращает этот флаг в математическую приемку.

Проверим правила извлечения на условном примере. Если файл A содержит B и в разделе Опирается на, и в разделе Используется в, после удаления повторов остаются две разнотипные декларации. Первая задает B -> A, вторая A -> B. Канонизация сохраняет prerequisite B -> A и выставляет confirmed. Таким образом, один файл способен дать подтвержденную в техническом смысле пару. Пример не является найденным конфликтом корпуса; он показывает, почему эту метку нельзя читать как два независимых математических свидетельства. Подпись, заданная через alias в wikilink, меняет показанный текст ссылки; математическое тождество результатов по ней не устанавливается.

Извлечение дает парную проекцию заметок. В ней нет отдельного объекта каждого доказательства, локатора применения или группировки совместных посылок. Эти сведения нужно искать в тексте: в точной формулировке, аргументе и источнике шага. Поэтому восстановленный набор 93 предков можно проверить по индексу, а роль каждого основания в выбранном доказательстве придется проверять по заметкам.

Протокол проверки и реально принятая область

Содержательная проверка, подробно разобранная в главе о корпусе, устанавливает тип объекта, точную формулировку, условия, заключение, классификацию, альтернативные названия и происхождение. У теоремы проверяется полное доказательство выбранной версии; у алгоритма процедура и заявленные гарантии проверяются раздельно; у определения и аксиомы устанавливаются контекст и соглашения. Для отношения B -> A нужен конкретный шаг доказательства A, использующий совместимую версию B. Тематическая близость такого свидетельства не дает.

Для обычного существующего объекта или отношения протокол требует один прочитанный сильный источник. Новое, существенно измененное, критическое или неоднозначное решение, межглавный стык и фундамент требуют двух независимых свидетельств. Зеркало, переиздание того же доказательства и разные поисковые интерфейсы к одной библиотеке не создают независимость. Отдельная проверка другим оценщиком также не делает два экземпляра одного текста двумя математическими источниками.

При поиске пропусков неудачный запрос не доказывает ложность результата. При исправлении отношения сверяют оба конца; разделение, объединение, переименование и перенос записи сохраняют явную судьбу ее адресов и ссылок. Пустые опоры не заполняют ради связности картинки. Исполнение этих требований устанавливается для конкретной принятой версии; само наличие протокола его не подтверждает.

Принятый аудит от 22 июля 2026 года имеет ID audrun_vault_msc2020_canon_v2_rc_20260722. Его объявленный охват - 879 математических карточек, из них 849 в главах и 30 в фундаменте, а также 896 внутренних доказательных ребер. Коллекция этого release candidate содержала 1165 документов-заметок. Число документов коллекции и число карточек принятой области различаются уже в этом паспорте.

Октябрьский расчет использует более поздние 1230 заметок. Поэлементного соответствия всей этой версии решениям июльского аудита не установлено. Июльская приемка сохраняет свою область, а октябрьские числа - свой вход. Пересчет предков или порядка глав не расширяет математическую приемку на измененные и добавленные записи.

Разные свидетельства отвечают на разные вопросы

У каждого свидетельства свой вопрос: доказательство подтверждает утверждение, хеш фиксирует версию, расчет дает число, наблюдение показывает действие.
СвидетельствоЧто подтверждаетЧего не подтверждает
Математический источникУтверждение и аргумент конкретной версииКорректность всех записей корпуса
Объявление связи в заметкеЗаписанную связьВыполненность гипотез используемого результата
Июльская приемкаРезультаты в пределах принятой проверкиПоэлементную привязку ко всему октябрьскому корпусу
Зафиксированный снимокСостав и технические поля записейПедагогическую достаточность
ПересчетЧисла заданной проекцииНовый математический аудит
Наблюдение интерфейсаНаблюденное действие и действующие настройкиЛюбой размер окна или универсальное удобство

Вернуться к примеру: получить именно множество предков

Теперь вход определен, но один индекс допускает несколько графов для расчета. Удаление некоторых типов ребер может сохранить слабую связность и изменить направленную достижимость, расстояния или рейтинги. Поэтому для числа 93 нужно явно выбрать отношения и направление обхода, сохранив также правило обработки флагов.

Зададим конечный ориентированный граф G=(V,E)G=(V,E). Множество VV состоит из разрешенных файловых записей зафиксированного корпуса, а EE содержит его prerequisite-ребра: u→vu\to v означает, что запись uu объявлена основанием vv. Теги и отношения application/reference исключены; prerequisite-ребра с флагами soft или transitive остаются. Цель tt - запись Теорема об оптимальном линейно-квадратичном регуляторе.

Нас интересуют все записи, из которых существует направленный путь к цели, без самой цели:

Anc⁡(t)={v∈V∖{t}:v⇝Et},cost⁡(t)=∣Anc⁡(t)∣.\operatorname{Anc}(t)=\{v\in V\setminus\{t\}:v\leadsto_E t\}, \qquad \operatorname{cost}(t)=|\operatorname{Anc}(t)|.

Здесь v⇝Etv\leadsto_E t означает существование направленного prerequisite-пути от vv к tt, а вертикальные черты считают элементы множества. Если одна опора приходит к цели через двух разных родителей, она все равно входит в множество один раз. Практически обход начинается с цели и идет по входящим prerequisite-связям; множество посещенных записей предотвращает повторный счет, в том числе при цикле. После обхода цель удаляется из результата.

На зафиксированном входе получены 93 уникальных предка, 7 непосредственных опор и 17 папок предков. Проверка сопоставляет идентификаторы со строкой сохраненного результата, затем размер множества и его распределение по папкам. Два разных набора могут содержать по 93 записи, поэтому одного совпадения числа было бы недостаточно. После проверки состава можно назвать вывод точно: измерен записанный контекст цели. Он не сообщает, какие записи уже известны читателю или обязательны во всех возможных доказательствах.

Для внешнего фундамента меняется цель обхода. Пусть C⊆VC\subseteq V - 914 записей четырнадцати основных папок, а A(C)A(C) - записи из VV, от которых существует prerequisite-путь положительной длины хотя бы к одному участнику CC. Теперь нужно оставить только основания вне основной области:

F=A(C)∖C.F=A(C)\setminus C.

Буква FF обозначает внешний фундамент; разность множеств удаляет участников CC, даже если они тоже служат опорами. Получены 53 внешние записи из 18 папок. У этого числа и у 93 предков LQR разные области: внешний контекст всех основных глав и полный контекст одной цели. В обоих случаях обход считает записанную достижимость; совместимость математических версий устанавливается по доказательствам.

Проверить композицию: какая цель действительно решена

Для проверки порядка глав нужны уже межглавные ребра, а не множество предков. Матрица W[a,b]W[a,b] считает связи между разрешенными файловыми записями разных выбранных основных папок. Теги исключены, но типы application/reference и флаги transitive/soft сами по себе этим отбором не исключаются. В данном снимке все 1183 учитываемые связи имеют тип prerequisite; 690 помечены transitive. Фундамент и его связи исключены из цели и добавляются первым прологом отдельно.

Обозначим множество выбранных глав через KK, их число через kk, а позицию главы aa в перестановке через pos(a)\mathrm{pos}(a). Фиксированное неотрицательное целое W[a,b]W[a,b] задает число учитываемых ребер из aa в bb. Чтобы проверить согласованность порядка с направлениями, сложим веса тех пар, для которых aa расположена раньше bb:

J(pos)=∑a,b∈Kpos(a)<pos(b)W[a,b].J(\mathrm{pos})=\sum_{\substack{a,b\in K\\\mathrm{pos}(a)<\mathrm{pos}(b)}}W[a,b].

Условная матрица из двух глав с W[a,b] = 3 и W[b,a] = 1 дает счет 3 для порядка a,b и счет 1 для b,a. Ребрам приписан одинаковый единичный вклад. Так формула определяет согласованность размещения с направлениями, сохраняя обратные ребра допустимыми. Она не вводит жесткого требования предшествования и не взвешивает математическую трудность.

Точный максимум находится динамическим программированием. Пусть S⊆KS\subseteq K, а D(S)D(S) - лучший счет среди перестановок глав из SS. Выберем последнюю главу v∈Sv\in S. Лучший внутренний счет остальных равен D(S∖{v})D(S\setminus\{v\}); добавление vv приносит сумму W[u,v]W[u,v] по оставшимся главам uu. Поэтому:

D(∅)=0,D(S)=max⁡v∈S[D(S∖{v})+∑u∈S∖{v}W[u,v]].D(\varnothing)=0,\qquad D(S)=\max_{v\in S}\left[D(S\setminus\{v\})+\sum_{u\in S\setminus\{v\}}W[u,v]\right].

Формула верна для конечной фиксированной матрицы с попарной аддитивной целью: добавление последней главы не меняет относительные позиции остальных, а каждая новая пара учитывается один раз. Ацикличность агрегированного графа не требуется. Производитель решает эквивалентную задачу по суффиксам; независимый расчет использовал рекурсию через последнюю главу. Для 14 глав обе процедуры подтвердили максимум 1154; независимый расчет дополнительно установил 60 равнооптимальных порядков. Остались 29 направлений назад из 1183; знаменатель исключает фундамент.

Точный режим реализации применяется при 1 ≤ k ≤ 16. Функция gainOf вновь суммирует входы по kk главам, поэтому время самого DP составляет O(k² × 2^k), память с матрицей - O(2^k + k²). Поиск вставками и заключительная стабилизация добавляют собственную стоимость. При k > 16 используется эвристический вариант. Авторский prior участвует в выборе стабильного представления среди неоднозначностей; глобальная ближайшая к prior перестановка или лексикографический минимум не гарантированы. Объяснение полного алгоритма дано в главе о композиции; здесь разделены точная цель и область ее воспроизводимой приемки.

Развести локальные координаты и глобальные показатели

Проверка слоя требует вернуться к меньшему графу: файловым отношениям внутри одной панели. Сильно связные компоненты объединяются, и между полученными компонентами уже нет направленных циклов. Для компоненты vv слой L(v)L(v) равен нулю, если у нее нет предшественников; иначе он равен единице плюс наибольший слой непосредственного предшественника uu. Например, у условной цепочки из трех компонент получаются слои 0, 1 и 2. При нескольких входах выбирается максимум, чтобы конец каждого межкомпонентного ребра стоял позже его начала.

Глобальная глубина использует то же правило на конденсации полного файлового графа с разными типами отношений. Поэтому локальный слой и глобальная глубина относятся к разным входам. В опубликованных четырнадцати панелях и фундаменте нет сильно связных групп размера больше одного; этот результат не удостоверяет ацикличность всей сети за их пределами. Свойства конденсации и топологического порядка разобраны в Bang-Jensen и Gutin, исправленное первое издание, §§1.4-1.5 и Lehman, Leighton и Meyer, редакция 2018 года, §§10.2-10.3 и 10.5.

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

Что подтверждено приемкой и что осталось в резерве

Воспроизведенный аналитический набор покрывает 16 семейств: состав; роли и распределения; связность; метрики; ядра и ранги; устойчивость; связи метрик; корни; предки и пути; порядок; потоки; пары и циклы папок; магистрали; развилки; кандидаты; контринтуитивные случаи. Выполнена 101 численная проверка. Это число проверок редукций и таблиц одного входа, а не 101 независимое наблюдение и не 101 проверенная математическая теорема.

Объем независимой проверки задается отдельно для каждой процедуры. Полные значения посредничества сверены с производителем, а альтернативный расчет по долям кратчайших путей проверен на выбранных вершинах и ребрах. Сообщества воспроизведены штатной пересборкой; другой независимый алгоритм их выделения не применялся. Точный порядок глав сопоставлен через две рекурсии: по суффиксам и через последнюю главу. Таким образом, успешная пересборка, полная сверка таблицы и альтернативный расчет имеют свои области подтверждения.

Разберем одно сохраненное расхождение округления. Для него взят простой невзвешенный неориентированный граф всех файловых канонических ребер: prerequisite, application и reference, включая связи с флагами soft и transitive. Направление снято, а длина пути считается числом ребер. Это меняет вопрос: посредничество ребра измеряет накопленный вклад в кратчайшие маршруты данной проекции, независимо от направления доказательной опоры.

Для различных записей s,ts,t, между которыми есть путь, обозначим число кратчайших путей через σst\sigma_{st}, а число проходящих через ребро ee - через σst(e)\sigma_{st}(e). Вклад пары равен σst(e)/σst\sigma_{st}(e)/\sigma_{st}. Если из двух кратчайших путей один проходит через ee, пара добавляет 1/21/2. Ненормированное посредничество b(e)b(e) складывает эти доли по неупорядоченным парам:

b(e)=∑{s,t}⊆Vfiles≠t, σst>0σst(e)σst.b(e)=\sum_{\substack{\{s,t\}\subseteq V_{\mathrm{file}}\\s\ne t,\ \sigma_{st}>0}}\frac{\sigma_{st}(e)}{\sigma_{st}}.

Здесь VfileV_{\mathrm{file}} - файловые записи выбранной полной проекции. Недостижимая пара не добавляет вклада: условие σst>0\sigma_{st}>0 также исключает деление на нуль. Поскольку доли складываются по многим парам, итог может быть значительно больше единицы. Производитель проходит все начальные вершины и в конце делит накопленную сумму на 2, устраняя двойной счет пары (s,t)(s,t) и (t,s)(t,s). Это приведение к неупорядоченным парам; дополнительного деления на число всех возможных пар для нормировки в диапазон от 0 до 1 здесь нет.

Для ребра между Теоремой Макса-потока мин-разреза и Теоремой Дилворта рациональная проверка дала 40351/40=1008.77540351/40=1008.775. Округление точного положительного значения half-up до двух знаков дает сохраненные 1008.78. Альтернативное накопление в арифметике с плавающей точкой (float) дало 1008.7749999999997, немного ниже точной границы округления. Так объяснено расхождение отображаемого числа: оно не потребовало исправлять отношение или математический текст. Проверка этого случая не снимает ограничений остальных вычислительных методов.

PageRank нужен в раскладке для разрешения неоднозначного порядка записей. Чтобы воспроизвести его, берут обратный полный файловый граф, задают всем вершинам одинаковую начальную массу и выполняют ровно 30 синхронных итераций. На каждой итерации доля 0.85 передается по исходящим ребрам обратного графа, равномерно между соседями; оставшаяся доля распределяется по всем вершинам равномерно. В доле 0.85 масса вершин без выходов тоже распределяется по всем вершинам равномерно. Новые значения вычисляются из предыдущего состояния сразу для всех вершин, поэтому порядок обхода вершин внутри итерации не задает результат.

Это контракт фиксированного расчета с коэффициентом 0.85, а не заявление о достижении стационарного распределения за 30 шагов. Направление, старт, перенос из вершин без выходов и число итераций нужны для проверки результата. Полученное значение вместе с глубиной участвует в сортировке ленты и полки. Ни один из этих показателей не измеряет трудность доказательства.

Вместе с результатами расчета сохранены полные рейтинги, направленное и неориентированное посредничество, closeness, сообщества, кандидатные пары и матрицы всех 53 папок. На страницу вынесены величины, объясняющие выбранную область и ее чтение. Этот отбор сохраняет остальные результаты для адресной проверки, оставляя центром рассказа Порядок его четырнадцати разделов.

Источники, версии и границы чтения

Проверка внешнего тезиса требует такого же внимания к входу. Документация устанавливает описанный контракт системы, чтение кода - механизм в указанной ревизии, исследование людей - результат на объявленной выборке и шкале. Поэтому таблица 18 используемых внешних источников сохраняет версии, фрагменты и пределы чтения. Результат чужого интерфейса не переносится на Nareshka.

Для каждого источника важны устойчивый ID, точная прочитанная версия, использованный фрагмент, поддерживаемый тезис и ограничение. Наличие журнальной публикации не означает, что прочитан именно ее финальный PDF. Например, у исследования модели понимания доказательства PC01 принят авторский вариант рукописи; его побайтовая идентичность версии издателя не устанавливалась. У Explorable Theorems, ET01 использована v2 с основным текстом, приложениями A-B и просмотренными фигурами 2-6. V1 и v2 относятся к одной работе и одному семейству исследования. У Roy, Inglis и Alcock, PC10 прочитаны опубликованный текст и ESM1; повторно использованные данные первого исследования не суммируются с родственными публикациями как новые участники.

Принятые OntoMathPRO и LibMeta сохраняют отдельную роль предметного контраста. Для OntoMathPRO использован официальный PDF 2022 года, для LibMeta - PDF издателя 2024 года с таблицами и фигурами. Эти онтологии не встроены в VaultGraph. Статья использует ранее принятое чтение указанных публикаций, не приписывая редактуре новый широкий поиск литературы.

Источники, использованные в статье

От тезиса можно вернуться к конкретной работе, ее версии и прочитанному фрагменту. Собственные данные корпуса подтверждает отдельная цепочка происхождения.
IDИсточникТочный локатор / область
BG01OntoMathPROОфициальный PDF 2022; с.30-32, рис.3; принято чтение 7 страниц
BG02LibMetaPDF издателя 2024; с.4-11, таблицы 1-4; §3, с.13-15, рис.7-8; принято чтение 21 страницы
GM02Stacks Project: TagsПрочитанные страницы Tags, тег 00CR и Statistics; адреса текста, не число теорем
TG04NaturalProofsNeurIPS Datasets and Benchmarks 2021; §3, таблица 2, дополнение A.1/D
MF04Gallo et al.: Directed Hypergraphs and ApplicationsАвторская рукопись, пересмотренная в октябре 1992; с.4-6 и 15-19; побайтовое совпадение с опубликованной журнальной версией не установлено
MF06Martelli and Montanari: Additive AND/OR GraphsОфициальный PDF IJCAI 1973; §2, с.2-3; отдельно принято более широкое чтение текста и фигур
MF02Lehman, Leighton, Meyer: Mathematics for Computer ScienceMIT редакция 2018-06-06 13:43; §§10.2-10.3 и 10.5
MF03Bang-Jensen and Gutin: DigraphsИсправленное первое издание, дата на титуле PDF 2007-08-15; §§1.4-1.5, с.17; не второе издание 2008
GM03LeanBlueprint / plastexdepgraphLeanBlueprint, коммит 56e066d30fb7b608a63f4241fee80982d7eae3ef; plastexdepgraph, коммит e06ff826ebf0ce9d1e137b25b3ce7e3d5fbcc8f4; действующее представление PFR рассматривается отдельно; to_dot, строки 115-146 в принятой закрепленной версии кода
GM01Proofscape: Expansion ModesПрочитанная версия 0.30.3; закрепленный серверный коммит 223d98d944b9dbdc732bc02d333493b95ec74335; содержимое по адресу документации может меняться
GM08Kieffer: Argument Mapping for Mathematics in Proofscape7-страничный авторский PDF, §§3-4, рис.1-2; публикационная запись Diagrams 2014 рассматривается отдельно
GM04pi-Base: Formula / ProverFormula.ts и Prover.ts, коммит 3420abcbd03c85a975459011f8d077518d291ce7; действующая страница теоремы T000001; полный аудит доказательств базы не выполнен; Logic/index.ts, строки 19-83 того же принятого коммита
ET01Explorable TheoremsТочная версия v2; §§4.2-4.4/5.1-5.2/6.1, приложение B; принято чтение полного основного текста, приложений A-B и фигур 2-6; комплексное сравнение при N=16
PC01Mejia-Ramos et al.: An assessment model for proof comprehension in undergraduate mathematics31-страничная рукопись, §§3-5; DOI 10.1007/s10649-011-9349-7; не эксперимент по воздействию на обучение
PC10Roy, Inglis and Alcock: Multimedia resources designed to support learning from written proofs: an eye-movement studyОпубликованная журнальная версия Springer, 18 страниц + ESM1; §§4-5, ESM1 с.1-2; в исследовании 1 повторно использованы данные, исследование 2 имеет отдельную выборку n=34
MIT-MVT-2020MIT OCW 18.100A: Lecture 19Теоремы 5 (Ролль) и 7 (MVT), доказательства с.3-4; новое адресное чтение вне состава принятого DIG
AMS-MSC2020AMS: MSC2020 database and search helpБаза MSC2020 и справка Search MSC; адресное чтение для предметной классификации, вне состава принятого DIG
KNAPP-B41-2016Anthony W. Knapp: Basic Real Analysis, Digital Second Edition (2016)Приложение B, следствие B.41, печатная с.688 (страница PDF 718): формулировка и доказательство на этой странице; адресное чтение вне состава принятого DIG

По таблице можно перейти от тезиса к использованному фрагменту первоисточника. Недоступный текст не получает статус прочитанного, а кандидат поиска не становится принятой опорой. В частности, знакомое название алгоритма не доказывает исторической атрибуции: для нее нужен соответствующий фрагмент оригинала. Сильно связные компоненты, слои и барицентрические проходы здесь объяснены по собственной реализации и проверенным математическим свойствам.

Права на текст статьи, программный код и корпус учитываются раздельно. Лицензия реализации чужой системы не распространяется автоматически на математические заметки, данные или изображения. В фигурах статьи собственные таблицы и условные схемы показывают объявленные объекты; условная схема не подписывается как снимок экрана. При наблюдении интерфейса фиксируют фактические настройки и размер окна: адрес страницы не описывает все значения, унаследованные из localStorage.

Для проверки исходных 93 предков теперь известны необходимые действия: установить вход по контрольной сумме, найти LQR по файловому ID, выделить prerequisite-граф, восстановить уникальное множество предков и сопоставить его с сохраненным набором. Чтобы проверить доказательство регулятора, понадобится следующий, содержательный проход по условиям и шагам использования опор. Численный расчет заканчивается там, где начинается этот другой вопрос.

Так же проверяются остальные выводы статьи: у числа устанавливаются единица, вход и процедура; у математического перехода - точная версия и аргумент; у действия - наблюденное состояние интерфейса. При изменении входа прежний результат не переносится автоматически. Эти правила позволяют вернуться от общей композиции к конкретному проверяемому утверждению, сохраняя авторскую область Порядка и границы выполненной работы.

составляют неизменяемую публикацию
Точные байты
контрольная сумма фиксированной версии
SHA-256
требует новой привязки результатов
Новый вход

Источники главы

Ссылки и границы использованного чтения
ИсточникМесто и область подтверждения
OntoMathPROОфициальный PDF 2022; с.30-32, рис.3; принято чтение 7 страниц
LibMetaPDF издателя 2024; с.4-11, таблицы 1-4; §3, с.13-15, рис.7-8; принято чтение 21 страницы
Lehman, Leighton, Meyer: Mathematics for Computer ScienceMIT редакция 2018-06-06 13:43; §§10.2-10.3 и 10.5
Bang-Jensen and Gutin: DigraphsИсправленное первое издание, дата на титуле PDF 2007-08-15; §§1.4-1.5, с.17; не второе издание 2008
Explorable TheoremsТочная версия v2; §§4.2-4.4/5.1-5.2/6.1, приложение B; принято чтение полного основного текста, приложений A-B и фигур 2-6; комплексное сравнение при N=16
Mejia-Ramos et al.: An assessment model for proof comprehension in undergraduate mathematics31-страничная рукопись, §§3-5; DOI 10.1007/s10649-011-9349-7; не эксперимент по воздействию на обучение
Roy, Inglis and Alcock: Multimedia resources designed to support learning from written proofs: an eye-movement studyОпубликованная журнальная версия Springer, 18 страниц + ESM1; §§4-5, ESM1 с.1-2; в исследовании 1 повторно использованы данные, исследование 2 имеет отдельную выборку n=34
Оговорки
  • Численный пересчет не является повторной математической приемкой карточек. Наблюдение интерфейса подтверждает только свою проверенную область.
  • 101 численная проверка не является 101 независимым наблюдением или 101 теоремой.
  • Таблица содержит использованные источники, а не весь резерв принятого DIG. MIT-MVT-2020, AMS-MSC2020 и KNAPP-B41-2016 не увеличивают его состав; частичное чтение не объявлено полным.