This website is machine-verified
This site is built with the Lean 4 theorem prover. Its page structure, the presence of both languages for every editorial field, and the uniqueness of output paths are guaranteed by types and theorems. Internal-link targets, assets and CSP are checked under an audit profile (--audit), and when a check fails the output directory is not updated and the failed build is quarantined. 25 of the 25 type and theorem guarantees identify the Lean type, definition or theorem that enforces them; renaming or deleting such a name fails the build.
Profile "full-audit": every requested check ran.
Headline guarantees (with the supporting Lean declaration)
- i18n completeness —
NoGoals.Bridge.i18nComplete - No file collisions in build plan —
NoGoals.Bridge.plan_unique_paths - Canonical, hreflang and sitemap from one route set —
NoGoals.Meta.hreflang_symmetric - XML injection impossible (sitemap/feeds) —
NoGoals.Meta.xmlEscape_no_specials - Chrome structure well-formed (slots trusted) —
NoGoals.Render.Tree.render_wf_mod - Structural invariants proven for this build —
NoGoals.refine - No duplicate page paths —
NoGoals.Bridge.uniquePages
Build command and source identity
- consumer.commit: 7d08bbc814627b7f70003a97434c656f24336700
- consumer.dirty: false
- nogoals.commit: 05d4a231e03e74f7062f4fd3f8f8d60081166344
- nogoals.dirty: false
The summary and the full report are reserved routes derived by the same path function as every other page, but their content is the post-gate evidence, so they are outside the proofs about the site's page set. The build keeps their paths from colliding with any other file and, under an audit profile, runs the same gates over them in a finalization pass.
Generated: 2026-10-08 05:22:24