Source / pinned edition
Авторский контракт интерпретации делимости Arxo
Source of package arxo.divisibility · 0.1.0
- work
- urn:arxo:arxo.divisibility#ARXO_DIVISIBILITY_CONTRACT
- number
- 0.1.0
- kind
- urn:arxo:arxo.divisibility#treatise
ARXO_DIVISIBILITY_EDITION
- edition
- urn:arxo:arxo.divisibility#ARXO_DIVISIBILITY_EDITION
- language
- ru
- officiality
- unofficial
- materialisation
- PINNED_UNOFFICIAL_COPY
- life cycle
- —
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| urn:arxo:divisibility-contract:0.1.0 | text/plain; charset=utf-8 | sha256:9c9743cb2610d05d24d63cfbf997e9de5f6b2eed13149449943074afe67850c9 | 2026-09-08T00:00:00Z |
Fragments — 1
contract · defn · referenced by: 9
ru · unofficial · sha256:9c9743cb2610d05d24d63cfbf997e9de5f6b2eed13149449943074afe67850c9RU
Авторский контракт интерпретации делимости Arxo, версия 0.1.0.
Carrier обозначает носитель с одной выбранной ассоциативной операцией. Element обозначает элемент; принадлежность конкретному носителю задаётся in_carrier.
semigroup_structure и monoid_structure — явные предположения о выбранной структуре полугруппы и моноида на носителе, а не результат проверки их аксиом. Моноид даёт guard полугруппы; обратного вывода нет.
divides интерпретируется как отношение делимости выбранной операции: первый элемент делит второй.
При guard полугруппы и принадлежности элементов применяется транзитивность делимости; при guard моноида — рефлексивность. Контракт не вводит замкнутость мира и не проверяет эквивалентность определений Lean.
Исходные теоремы и разрешения импорта находятся у отдельных владельцев mathlib.divisibility и mathlib.divisibility.permissions. Целочисленное прочтение носителя принадлежит arxo.integer_divisibility.
Referencing norms: Carrier, DividesReflexivity, DividesTransitivity, Element, MonoidIsSemigroup, divides, in_carrier, monoid_structure, semigroup_structure
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.