# Formal Proof Data

Acceptance of a proof term by the Lean kernel does not automatically prove the full encyclopedia prose, the natural-language semantic bridge, or every equivalent geometric representation. This catalogue publishes both passed checks and open boundaries.



## Publish the Lean sources OCME actually uses.

The public set contains OCME-owned Lean sources, the pinned toolchain, Lake project configuration, and the dependency lock. It excludes .lake, downloaded Mathlib source, packages, and build caches. Lake retrieves the pinned dependencies during replay.

[View SHA-256 manifest](https://ocme.evemisslab.com/data/formal/lean/manifest.json)


- [formal/lean/lean-toolchain](https://ocme.evemisslab.com/data/formal/lean/sources/lean-toolchain)
- [formal/lean/lakefile.toml](https://ocme.evemisslab.com/data/formal/lean/sources/lakefile.toml)
- [formal/lean/lake-manifest.json](https://ocme.evemisslab.com/data/formal/lean/sources/lake-manifest.json)
- [formal/lean/OCMEFormal.lean](https://ocme.evemisslab.com/data/formal/lean/sources/OCMEFormal.lean)
- [formal/lean/OCMEFormal/Foundations.lean](https://ocme.evemisslab.com/data/formal/lean/sources/OCMEFormal/Foundations.lean)
- [formal/lean/OCMEFormal/Pythagorean.lean](https://ocme.evemisslab.com/data/formal/lean/sources/OCMEFormal/Pythagorean.lean)





## Formal evidence catalogue



## mko-tends-to-relation

For every function f : α → β and filters l₁ and l₂, Filter.Tendsto f l₁ l₂ is equivalent to Filter.map f l₁ ≤ l₂.

evidence-sha256-38b848281997cbb1a2c1ea5559c6937dbb67ee03ac0be338756320a99e0f8b1d · passed



## Limitations and excluded scope


- This evidence formalizes Mathlib's filter semantics for convergence. The bare notation x → a must first specify source and target filters before it can be connected to this statement.
- It is not by itself an epsilon-delta definition, and it does not prove the limit of any particular function.
- The evidence depends on Lean 4.30.0 and Mathlib v4.30.0.



[View raw Evidence JSON](https://ocme.evemisslab.com/data/evidence/38b848281997cbb1a2c1ea5559c6937dbb67ee03ac0be338756320a99e0f8b1d.json)



## mko-euclid-pythagorean-theorem

In every real inner product space, if the angle between vectors x and y is π/2, then the squared norm of their sum equals the sum of their squared norms.

evidence-sha256-4d31c152012f8b561749e354f3789344c91e1fea26cead1468e95417b2e84752 · passed



## Limitations and excluded scope


- This evidence proves the vector core theorem. A separate side-length theorem supplies the explicit bindings for a, b, and c.
- The evidence depends on Lean 4.30.0, Mathlib v4.30.0, and the declared imported module.
- A formal proof does not replace review of the encyclopedia wording, symbol roles, or geometric model.



[View raw Evidence JSON](https://ocme.evemisslab.com/data/evidence/4d31c152012f8b561749e354f3789344c91e1fea26cead1468e95417b2e84752.json)



## mko-euclid-pythagorean-theorem

For every real inner product space, vectors x and y, and real numbers a, b, and c, if x and y meet at angle π/2 and a = ‖x‖, b = ‖y‖, c = ‖x + y‖, then a·a + b·b = c·c.

evidence-sha256-701b8066d363dadf2cc1ec21bc0d21f7c680a6eb187a37fd309c0f2e4c86d08e · passed



## Limitations and excluded scope


- This evidence closes the side-length model declared by OCME; it is not automatically identical to every affine-plane, coordinate, or triangle construction.
- The hypotenuse length is defined as the norm of the vector sum. Other vertex orderings require a separate equivalence proof.
- The evidence depends on Lean 4.30.0, Mathlib v4.30.0, and the pythagorean_vector theorem.



[View raw Evidence JSON](https://ocme.evemisslab.com/data/evidence/701b8066d363dadf2cc1ec21bc0d21f7c680a6eb187a37fd309c0f2e4c86d08e.json)



## mko-set-membership

For every type α, element x : α, and set A : Set α, the proposition x ∈ A is equivalent to evaluating the predicate A x.

evidence-sha256-702de77019f352eb431eb67bd7b266491b7c36c922d952e44be2b11ba95bcb5d · passed



## Limitations and excluded scope


- This evidence formalizes Lean's representation of Set as α → Prop; it does not claim to cover every foundation of set theory.
- A membership test in a programming container does not therefore become general mathematical set membership.
- The evidence depends on Lean 4.30.0 and Mathlib v4.30.0.



[View raw Evidence JSON](https://ocme.evemisslab.com/data/evidence/702de77019f352eb431eb67bd7b266491b7c36c922d952e44be2b11ba95bcb5d.json)



## mko-function-mapping

For every pair of types X and Y, function f : X → Y, and input x : X, there exists a unique y : Y such that f x = y.

evidence-sha256-d999133c1ae711b73752af8ee4b1b3ce74ca135ff7c06aabbe9fc8a3186f434b · passed



## Limitations and excluded scope


- This evidence formalizes the existence and uniqueness of output for Lean total functions; it does not cover partial functions, random procedures, or effectful programs.
- The codomain Y and the actual range of f remain different concepts; the theorem does not claim that f is surjective.
- The evidence depends on Lean 4.30.0 and Mathlib v4.30.0.



[View raw Evidence JSON](https://ocme.evemisslab.com/data/evidence/d999133c1ae711b73752af8ee4b1b3ce74ca135ff7c06aabbe9fc8a3186f434b.json)