The 0.5 line focuses on reportable assurance, structured proof diagnostics, and clearer proof-producing simplification boundaries.
Assurance reports
Kernel differential reports now include reference replay of the Prelude environment, theorem-module-installed environment replay, generated artifact replay, indexed artifact replay, coverage summaries, structured explanations, and timing metadata.
mix theoria.kernel.check
mix theoria.kernel.check --verbose
mix theoria.kernel.check --coverage
mix theoria.kernel.check --explain
mix theoria.kernel.check --json --coverage --explain
Reports use structs and Jason encoders for theorem-module summaries, artifact replay skips, kernel explanations, and timing metadata.
Proof diagnostics
Rewrite and simp steps carry a structured proof result:
step.proof_result.status
step.proof_result.capability
step.proof_result.proofConvenience helpers are available on Theoria.Rewrite.Proof.Result, Theoria.Simp.Step, and Theoria.Simp.Result.
mix theoria.simp --capabilities prints the current proof capability matrix. mix theoria.simp --explain prints step-level capability and status information while running examples.
Equality chains
Simp artifacts now expose proof strategy metadata:
:refl:single:transitive:fallback_defeq
The strategy is available directly on %Theoria.Simp.Result{} and on the realized artifact.
Boundaries
Application and selected equality-side paths can produce checked lifted proofs. Binder and EqRec paths remain explicit kernel-checked boundaries: defeq-safe cases may still be checked via final reflexivity, but there is no extra axiom or unsound extensionality shortcut.
Reference coverage
Reference checks include generated typed dependent fragments and direct EqRec-over-refl normalization tests. Lean remains a contributor-only external oracle, not a trusted runtime dependency.