Compile check of three files from github.com/paulklemstine/Lean (Catalog/Novelty/), 2026-10-20.
Toolchain: Lean 4.34.0, Mathlib 5ed2965256430c3649e86755f9576b54eca72435. Files unmodified, built in a clean Novelty/ layout with `lean -o`, in a no-network sandbox, in dependency order. Kernel replay not run.
Commit d3021737 (2026-08-16T18:47:46Z) per the GitHub per-file history; checkout at HEAD 990ac235.
SHA-256 of the compiled files:
5b71b7a74f813d12dbb69380fd50569529bbb827b0c120c26334c0a95debd09b  EmergentGeometryEntropyCone.lean
4d1493bea9d8e9c4391fab69c3029e98081b6ab75d7c8db16ce8f5b49fe8a409  HolographicCyclicInequality.lean
165c43fee9e571fbc9093c3dd957b116337fc0430eb3fc2054d1f1e036d6cbd4  HolographicContractionCalculus.lean

== build (exit codes)
=== EmergentGeometryEntropyCone
exit 0
=== HolographicCyclicInequality
exit 0
=== HolographicContractionCalculus
exit 0

== #print axioms (probe file: opens EmergentGeometry and prints axioms of the names below)
'EmergentGeometry.entropy_monogamy' depends on axioms: [propext, Classical.choice, Quot.sound]
'EmergentGeometry.entropy_subadditive' depends on axioms: [propext, Classical.choice, Quot.sound]
'EmergentGeometry.entropy_strong_subadditive' depends on axioms: [propext, Classical.choice, Quot.sound]
'EmergentGeometry.exists_minimal_surface' depends on axioms: [propext, Classical.choice, Quot.sound]
'EmergentGeometry.cutWeight_comb' depends on axioms: [propext, Classical.choice, Quot.sound]
'EmergentGeometry.entropy_cyclic5' depends on axioms: [propext, Classical.choice, Quot.sound]
'EmergentGeometry.entropy_le_of_contraction' depends on axioms: [propext, Classical.choice, Quot.sound]
'EmergentGeometry.mmi_of_contraction' depends on axioms: [propext, Classical.choice, Quot.sound]
'EmergentGeometry.subadditive_of_contraction' depends on axioms: [propext, Classical.choice, Quot.sound]
'EmergentGeometry.ssa_of_contraction' depends on axioms: [propext, Classical.choice, Quot.sound]
'EmergentGeometry.minorityMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'EmergentGeometry.cyclicMap' depends on axioms: [propext, Classical.choice, Quot.sound]
exit 0
