The Natural Framework Lean Proof

The Natural Framework is 2,800+ lines of Lean 4 that formalize the six-role information processing pipeline. Zero sorry. No Mathlib.

Each page below explains one file in plain English. The code is shown for reference.

Foundations

• Support.lean — which outputs a computation can produce
• Kleisli.lean — stochastic functions compose
• Axioms.lean — five empirical assumptions
• Pipeline.lean — six stages, one cycle

Contracts and composition

• Contracts.lean — postconditions on morphism outputs
• Handshake.lean — stage N's guarantee = stage N+1's assumption
• Boundary.lean — why each stage is forced
• Uniqueness.lean — the ordering is unique
• Removal.lean — remove any postcondition, system dies

Stochasticity and termination

• Pigeonhole.lean — no injection from n+1 to n
• Stochasticity.lean — determinism → confusion → error
• DeathConditions.lean — three ways to die
• Induction.lean — life persists iff all six fire
• Fractal.lean — recursive consolidation with budget termination

Hoare logic layer

• Hoare/Core.lean — triples, COMP, AND, OR, consequence
• Hoare/WP.lean — weakest precondition
• Hoare/Bridge.lean — contracts = Hoare triples
• Hoare/Comp.lean — full pipeline composition
• Hoare/Graded.lean — grades from a preordered monoid
• Hoare/Effects.lean — Boolean effect embedding
• Hoare/Static.lean — iteration stability
• Hoare/Divergence.lean — NonExpanding as threshold triples

Variational and morphisms

• Variational.lean — contracts from optimization
• Corollary.lean — competitive core, control/data split
• SupportMonadMorphism.lean — support as monad morphism