6. Limits and development status🔗

Slean checks here: the versioned case shape, IDs and references, causal journal order, local exact decimal comparison, stated cost cap, promotion rule, AND/OR gate references, and audience projection. It can report a precise error or preserve an undetermined result.

Slean does not check here: that the measurement happened, that artifact bytes are authentic, that an external clock or evaluator is reliable, that an AND/OR gate proves its target, that a human decision is wise, or that the scientific claim is true. The local Lean theorem concerns a conditional property of the mechanism, not those empirical facts. No independent proof checker is configured.

This site is a local pre-publication prototype. Its examples are synthetic. Public licensing, repository visibility, domain deployment, and integrations remain separate decisions. The build runs tests and compiles examples before generating the manual. build-info.json identifies the source commit, tree cleanliness when Git metadata is available, schema, Lean, and selected tag; without Git metadata, source_tree_clean is null because cleanliness is unknown. A build without a tag remains a development preview.