Source / pinned edition
Авторский контракт интерпретации порядка Arxo
Source of package arxo.order · 0.1.0
- work
- urn:arxo:arxo.order#ARXO_ORDER_CONTRACT
- number
- 0.1.0
- kind
- urn:arxo:arxo.order#treatise
ARXO_ORDER_EDITION
- edition
- urn:arxo:arxo.order#ARXO_ORDER_EDITION
- language
- ru
- officiality
- unofficial
- materialisation
- PINNED_UNOFFICIAL_COPY
- life cycle
- —
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| urn:arxo:order-contract:0.1.0 | text/plain; charset=utf-8 | sha256:b3d6a483d3fde836b357093f6f6eaab406950c1596d1f2769435e9079dd98b5e | 2026-09-08T00:00:00Z |
Fragments — 1
contract · defn · referenced by: 14
ru · unofficial · sha256:b3d6a483d3fde836b357093f6f6eaab406950c1596d1f2769435e9079dd98b5eRU
Авторский контракт интерпретации порядков Arxo, версия 0.1.0.
Order обозначает носитель с одним выбранным предпорядком. Element обозначает элемент; принадлежность конкретному носителю задаётся in_carrier.
preorder_structure — явное предположение о выбранном предпорядке, а не результат проверки всех его аксиом.
Отношения before_or_equal и strictly_before интерпретируются как нестрогое и строгое отношения выбранного порядка.
При наличии guard порядка и принадлежности всех элементов применяются четыре положительных правила: строгая транзитивность; из x≤y и y<z следует x<z; из x<y следует x≤y; нестрогая транзитивность.
partial_order_structure и linear_order_structure — явные предположения о выбранном частичном и линейном порядке на том же носителе. Иерархия структур задаётся двумя положительными правилами: частичный порядок даёт guard предпорядка, линейный порядок даёт guard частичного порядка. Обратного вывода нет.
Правила используют положительную поддержку supported. Контракт не вводит замкнутость мира, не сравнивает произвольные числа и не проверяет эквивалентность определений Lean и Isabelle.
Исходные теоремы и разрешения импорта находятся у отдельных владельцев mathlib.order и isabelle.order. Совместный сертификат принадлежит arxo.order_composition.
Referencing norms: Element, LinearOrderIsPartialOrder, Order, PartialOrderIsPreorder, StrictImpliesWeak, StrictTransitivity, WeakThenStrict, WeakTransitivity, before_or_equal, in_carrier, linear_order_structure, partial_order_structure, preorder_structure, strictly_before
The hash beside the text is the sha256 of its exact bytes. It is the check that the text shown matches the one pinned in the package: a divergence fails the oracle’s static analysis.