Measure

<p align="center"> <h1 align="center">📏 Measure</h1> <p align="center"> <em>A formal language for physics — where compilation is proof.</em> </p> <p align="center"> <a href="#-getting-started"><img src="https://img.shields.io/badge/Lean_4-Mathlib-blue?style=flat-square&logo=data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyNCAyNCI+PHBhdGggZmlsbD0id2hpdGUiIGQ9Ik0xMiAyTDIgMTloMjBMMTIgMnoiLz48L3N2Zz4=" alt="Lean 4"></a> <a href="#-verification-stats"><img src="https://img.shields.io/badge/theorems-267-brightgreen?style=flat-square" alt="Theorems"></a> <a href="#-verification-stats"><img src="https://img.shields.io/badge/sorry-0-success?style=flat-square" alt="Sorry"></a> <a href="#-verification-stats"><img src="https://img.shields.io/badge/axioms-23-yellow?style=flat-square" alt="Axioms"></a> <a href="#-physics-coverage"><img src="https://img.shields.io/badge/physics_domains-25-blueviolet?style=flat-square" alt="Domains"></a> <a href="#-verification-stats"><img src="https://img.shields.io/badge/build-2881_jobs_passing-brightgreen?style=flat-square" alt="Build"></a> <a href="LICENSE"><img src="https://img.shields.io/badge/license-MIT-blue?style=flat-square" alt="License"></a> </p> </p>

---

📑 Table of Contents

• 🔭 What is Measure?
• 💡 Core Ideas
  • ⚙️ Compilation = Proof
  • 📦 Theories as Modules
  • 🎚️ Four Rigor Levels
  • 📐 Uncertainty is Fundamental
  • 🧬 Dual-Layer Architecture
• 🌌 Physics Coverage
• 📏 Dimension System
• 🔧 C++ FFI Kernel
• 🔬 Physical Constants
• 🔗 External Engine Integration
• 🛠️ Tactics
• 🗂️ Project Structure
• 🚀 Getting Started
• 📊 Verification Stats
• 🧭 Philosophy
• 📄 License

---

🔭 What is Measure?

Measure is a programming language designed for one purpose: proving that physics theories are internally self-consistent.

Physics is not mathematics. It is grounded in measurement and experiment, inherently approximate, and full of contradictions between theories. Quantum mechanics and general relativity both work — and they disagree. Measure doesn't pretend this isn't the case. Instead, it gives you the tools to:

• 🔒 Prove local self-consistency — each theory is verified on its own terms
• ⚡ Track contradictions explicitly — conflicting theories are marked, not hidden
• 📉 Propagate uncertainty — error is a first-class citizen, not an afterthought
• 🧱 Check dimensions at compile time — if your equation has wrong units, it doesn't compile

theory NewtonianGravity where

  axiom newton2 (m : ExactQ dimMass) (a : ExactQ dimAccel)
    : ExactQ dimForce

  axiom gravForce (m₁ m₂ : ExactQ dimMass) (r : ExactQ dimLength)
    : ExactQ dimForce

  axiom kineticEnergy (m : ExactQ dimMass) (v : ExactQ dimVelocity)
    : ExactQ dimEnergy

  axiom energyConservation
    (ke₁ pe₁ ke₂ pe₂ : ExactQ dimEnergy)
    (h : ke₁.value + pe₁.value = ke₂.value + pe₂.value)
    : ke₁.value + pe₁.value = ke₂.value + pe₂.value

If this file compiles, the theory is self-consistent. Dimensions checked. Conservation laws verified. No exceptions.

---

💡 Core Ideas

⚙️ Compilation = Proof

Every theory block triggers a 6-phase verification pipeline:

| Phase | Action | |:-----:|--------| | 1 | Parent compatibility check | | 2 | C++ TheoryRegistry registration | | 3 | FFI domain compatibility check | | 4 | Auto-degradation (mark parents as approximations if rigor gap exists) | | 5 | Rigor auto-propagation (weakest-link rule) | | 6 | Self-consistency verification (dimensional consistency + conservation laws) |

If it compiles, it's consistent. If it's not consistent, it doesn't compile.

📦 Theories as Modules

Each physics theory is an isolated module with its own axioms, rigor level, and domain. Theories relate to each other through four explicit relation types:

| Relation | Meaning | |----------|---------| | extension | Theory B extends A with new axioms | | approx | Theory A approximates B under limiting conditions (e.g., v/c → 0) | | conflict | Theories have contradictory axioms (with explicit witness) | | compatible | Theories are explicitly compatible |

When a new unifying theory arrives, old theories don't break — they gracefully degrade to approximations.

🎚️ Four Rigor Levels

strict > approximate > empirical > numerical

Rigor propagates by the weakest-link rule: if your theory imports an empirical module, your combined rigor is at most empirical. No pretending.

📐 Uncertainty is Fundamental

Three error propagation models, unified under one typeclass:

| Model | Method | Use Case | |:-----:|--------|----------| | 🔔 Gaussian | First-order Taylor + derivative tracking | Standard measurements | | 🔗 Affine | Noise symbols + Chebyshev bounds | Correlated errors | | 📦 Interval | Conservative closed intervals | Worst-case bounds |

Quantities carry their uncertainty in the type system. ExactQ for defined constants (speed of light), UncertainQ for measured values (gravitational constant). The type forces you to choose.

🧬 Dual-Layer Architecture

| Layer | Type | Purpose | |:-----:|------|---------| | 🏃 Runtime | Quantity d c (Float) | Fast computation with error propagation | | 📜 Proof | PhysReal d (ℝ) | Formal proofs backed by Mathlib |

The bridge between them is exact in one direction (Float → ℝ via IEEE 754 bit decoding) and explicitly approximate in the other (ℝ → Float via axiomatic rounding).

---

🌌 Physics Coverage

25 domains, each with multiple submodules:

| Domain | Submodules | Rigor | |--------|-----------|:-----:| | 🍎 Classical Mechanics | Newton, Lagrangian, Hamiltonian, Noether, Conservation | strict | | ⚡ Electromagnetism | Maxwell, Potential, Wave | strict | | 🔮 Quantum Mechanics | Hilbert, Schrödinger, Operators | strict | | 🚀 Special Relativity | Minkowski, Lorentz | strict | | 🕳️ General Relativity | Einstein, Metric | strict | | 🌡️ Thermodynamics | Laws | strict | | 📊 Statistical Mechanics | Ensemble | strict | | 🌊 Fluid Mechanics | Navier-Stokes, Waves | strict | | ⚛️ Atomic Physics | Hydrogen, Nuclear | strict | | 💥 Particle Physics | Standard Model, Scattering | strict | | 🔐 Quantum Information | Qubit, Entanglement | strict | | 🌀 QFT | Fields, Fock Space | approximate | | 💎 Condensed Matter | Crystal, Band Theory | approximate | | 🔦 Optics | Geometric, Wave | approximate | | ☀️ Plasma Physics | MHD, Basic | approximate | | 🧬 Biophysics | Diffusion, Membrane | empirical | | 🌍 Geophysics | Atmosphere, Seismology | empirical | | 🏗️ Material Science | Semiconductor, Superconductivity, Elasticity | empirical | | 🦋 Nonlinear Dynamics | Chaos, Dynamical Systems | numerical | | 🔭 Quantum Gravity | LQG, Holography | numerical | | 🎻 String Theory | Strings, Supersymmetry | numerical | | 🌠 Astrophysics | Cosmology, Stellar Structure | approximate | | 🔮 Frontier | Dark Matter, Dark Energy, Quantum Thermodynamics | numerical | | 📜 Historical | Classical Models, Approximate Theories, Quantum Models | empirical | | 📏 Dimensional | Cross-cutting dimensional analysis | strict |

---

📏 Dimension System

7-component SI dimension vectors with rational exponents:

structure Dim where
  L : QExp := QExp.zero   -- Length (m)
  M : QExp := QExp.zero   -- Mass (kg)
  T : QExp := QExp.zero   -- Time (s)
  I : QExp := QExp.zero   -- Electric current (A)
  Θ : QExp := QExp.zero   -- Temperature (K)
  N : QExp := QExp.zero   -- Amount of substance (mol)
  J : QExp := QExp.zero   -- Luminous intensity (cd)

Dimension arithmetic is compile-time verified:

-- Force has the same dimension as mass × acceleration
theorem force_dim_check : dimForce = Dim.mul dimMass dimAccel := by
  native_decide

Wrong dimensions → compilation error. No runtime surprises.

---

🔧 C++ FFI Kernel

A high-performance C++ kernel handles computationally intensive operations:

| Component | Description | |-----------|-------------| | 🛡️ Conservation Checker | 3-pass static analysis (decompose → compute delta → residual analysis) with CAS delegation | | 🕸️ Theory Graph | 4-stage conflict detection (cache → syntactic → semantic → SMT) | | 📈 Epsilon Tracker | Tracks approximate equality error accumulation across proof chains | | ≈ Approximate Equality | IEEE 754-aware comparison with configurable tolerance | | 🔗 Rigor Propagation | Weakest-link computation across theory dependency graphs |

The trust boundary between Lean and C++ is secured by a private opaque TrustToken — external code cannot forge verification results.

---

🔬 Physical Constants

Built-in CODATA 2022 + SI 2019 constants with proper uncertainty tracking:

| Constant | Symbol | Status | Source | |----------|:------:|:------:|--------| | Speed of light | c | ✅ Exact | SI 2019 defining | | Planck constant | h | ✅ Exact | SI 2019 defining | | Boltzmann constant | k_B | ✅ Exact | SI 2019 defining | | Elementary charge | e | ✅ Exact | SI 2019 defining | | Avogadro constant | N_A | ✅ Exact | SI 2019 defining | | Gravitational constant | G | 📊 Gaussian 1σ | CODATA 2022 | | Electron mass | m_e | 📊 Gaussian 1σ | CODATA 2022 | | Fine-structure constant | α | 📊 Gaussian 1σ | CODATA 2022 | | ... and more | | | |

Exact constants carry zero uncertainty. Measured constants carry Gaussian error. The type system enforces the distinction.

---

🔗 External Engine Integration

Delegate heavy computation to external CAS engines via JSON-RP