Formal companion
Lean 4 Blueprint
A machine-readable view of the proof-development layer behind the papers.
Lean 4 and mathlib provide a checkable substrate for the programme's definitions, claims, and dependency structure. The generated document below keeps that formal layer close to the public research narrative.
This is a proof-development companion, not a publication manuscript. The current generated view contains four formal chapters; claim mappings remain owned by the Lean blueprint.