Ядро печатало «доказано индукцией» об утверждении, которое рантайм тут же отвергал

Самая серьёзная из найденных ошибок, потому что она била в само основание.

Что было. При дробной границе условия — если н меньше 2.5 при н: нат — верх дна считался как К минус 1, то есть 1.5. В базу при этом попадает и н = 2. Ядро печатало «доказано индукцией», а рантайм тут же отвергал утверждение на н = 2 кодом FLANG_PROPERTY.

Измерено, а не предположено. Найдено при слиянии двух веток ядра, обнаружено прогоном.

Как починено. Отказом, а не подгонкой: граница обязана быть целым числом. Подделка отвергается кодом FLANG_PROOF_INDUCTION_BRANCH, и рантайм независимо опровергает на н = 2.

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

Это оказался класс, а не случай: за те же сутки нашёлся второй такой же — the-core-accepts-falsehood-a-class.

Связано: zero-axioms, silent-merge-conflicts, a-record-field-laundered-a-value