This page publishes materials such as Lean source code that cannot be withdrawn once in a public repository; some papers are under review and must not be de-anonymised — thank you for your understanding.
The grades
Grade
Rule
T0
T0 rule retained: any version under anonymous review has its title, venue and identifier absent from this site; if a version enters anonymous review, this site immediately withdraws the relevant searchable information.
T1
A placeholder: title and status shown, no file. Awaiting the author's own manual verification.
T2
A link out, to a location that already exists elsewhere.
T3
A full deposit, with a downloadable file. Requires explicit human verification before it can appear.
Current items
Paper · T3The Boundary Potential V (κ): A Computable, Machine-Checked Answer to the Autonomy-Boundary QuestionSubmitted to Third Workshop on Agents in the Wild, NeurIPS 2026. Not accepted (decision date: 2026-09-30). The archived PDF is the exact version submitted for review, unchanged.This is a preprint. A revised version is in preparation for arXiv. License: CC BY 4.0.File: files/V-A-2026-08-31-reviewed.pdf (17 pages, 355,111 B) · SHA-256 214ba9dddf5b22122ddecbf6db8ef03ecf3a45105819d127f215433203b02613Full text · T3Download PDF
Lean source · T1CausModel: a machine-checked categorical layer for the boundary programmeThe de-identified public build of the categorical layer: internal organisation markers and absolute paths removed, then re-verified by compiling — removing names must not be allowed to break proofs. Licensed Apache-2.0, with a CITATION.cff carrying the ORCID. A downloadable archive is not yet posted: it awaits manual verification. A downloadable copy is not posted yet; to request the reviewed version, contact the author via the identity listed in the ORCID record.Placeholder — pending verification
Not shownOne item is graded T0Under the first iron rule it appears nowhere on this site: not its title, not its venue, not its identifier — because any of those is searchable and would connect the author to the submission. The site says only that such an item exists, so that a reader is not misled into thinking this is the whole record.Withheld
How There Is: A Machine-Checked Programme for Boundary, Level and Identification
Preprint in preparation · formal spine complete
B slice 53 / 417 / 77
boundary = closure fixed point, criterion = threshold level set of the kernel; seam Fix(c_{Lθ})=S_θ (L(θ)=ln((2−θ)/θ)); no-go: level-invariant information alone cannot pick the level
C
Boundary Form and Boundary Position
v3 writing plan · in preparation
no new Lean
model-first reconstruction of Kant's Grenze/Schranke: one boundary structure described two ways, not two boundaries
Source & archive
Source snapshot: limisys.github.io/boundary-axiom/ (available after push). Unified repository: 56/467/90. The de-identified public build of CausModel remains at grade T1 — the placeholder rule is unchanged.
Licences
Asset
Licence
What it permits
Written works (papers)
CC BY 4.0
Free to read, cite and redistribute, with attribution.
Source code (Lean etc.)
Apache-2.0
Free to use, modify and distribute, retaining the notice.
Text of this site
CC BY 4.0
Free to read, cite and redistribute, with attribution.
A boundary that must be stated. Mathematical theorems and formulae are themselves not protected by copyright. What is licensed here is expression, and the machine-checkable proof scripts — not the mathematical facts. No monopoly over those is claimed or possible.
AI use disclosure
Large language models served as a drafting tool that produced candidate code for the Lean 4 formal proofs and the three Python verification scripts. Every machine-checked conclusion rests on re-running the compiler and the independent scripts — never on the identity of the generator. A conclusion is machine-checked because the check passes, not because of who or what wrote it.
What is not posted, and why
Item
Reason
Any version under anonymous review
Publishing would break anonymity. Withheld
The boundary-programme development body (the larger Lean corpus)
Not yet de-identified; it still contains machine-specific absolute paths. De-identification must be followed by a fresh compile before it can be posted.
The submitted manuscripts that were reviewed
Posted at grade T3 (archived unchanged).
Why grades rather than judgement calls. Every rule on this page is enforced by a script at build time: the status gate, the anonymity scan, the licence check, the hash re-computation, and a red line that fails the build if a withheld item's title or venue appears anywhere in the output. A rule that lives in someone's memory is not a rule.