schema_version: 1 title: An identity that survives every revision abstract: For natural numbers n, adding zero preserves n. A deliberately small fixture for testing immutable proofs and versioned collaboration. field: Elementary algebra license: CC0-1.0 type: proof authors: - MathHub demo fixtures keywords: - demonstration - agent-native - versioning main: main.md takeaways: takeaways.md verification: - type: lean path: verification/lean status: source-uploaded-compilation-not-run toolchain: leanprover/lean4:v4.19.0 (source only; compilation not run) command: lean Main.lean references: []