📏 Measure

A formal language for physics — where compilation is proof.

---

📑 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-RPC 2.0:

Engine	Backend	Use Case
🟣 Julia	SymbolicUtils.jl	Symbolic algebra
🐍 Python	SymPy	Symbolic computation
🔴 Mathematica	Wolfram Language	Full CAS

Plus database connectors for NIST CODATA and PDG particle data, with 4-tier caching (memory → disk → network → fallback).

---

🛠️ Tactics

Six physics-aware proof tactics:

Tactic	Purpose
dim_check	📏 Verify dimensional consistency
conserve	🛡️ Verify conservation laws via C++ checker
approximate	📐 Verify approximation error bounds
by_symmetry	🔄 Simplify proofs using symmetry arguments
limit_of	🔭 Verify limiting processes between theories
native_decide	⚡ Lean's built-in decidable verification

---

🗂️ Project Structure

measure/
  src/
    Main.lean                 # 🚪 CLI entry point
    Measure.lean              # 📦 Root barrel file
    Measure/
      Dim/                    # 📏 7-dimensional SI system with rational exponents
      Quantity/               # 🔢 Dimensioned values with certainty tracking
      Error/                  # 📉 Gaussian, Affine, Interval uncertainty models
      Theory/                 # 🧩 Theory modules, relations, rigor levels
      Conservation/           # 🛡️ Noether theorem, conservation law verification
      Syntax/                 # ✏️ Tactics, theory blocks, attributes
      Kernel/                 # 🔧 C++ FFI bridge and wrappers
      External/               # 🔗 CAS engine integration (Julia/Python/Mathematica)
      Math/                   # 📐 Mathlib bridge (real analysis, linear algebra)
      Physics/                # 🌌 25 physics domain formalizations
      Unit/                   # ⚖️ Unit system and conversions
      Constants.lean          # 🔬 CODATA 2022 physical constants
      Examples/               # 📝 Worked examples (Newton, SR, EM, QM, Thermo)
    kernel/                   # ⚡ C++ kernel source
      conservation.{cpp,h}    #   Conservation checker
      theory_graph.{cpp,h}    #   Theory conflict detection
      epsilon_tracker.{cpp,h} #   Error accumulation tracking
      ffi_bridge.cpp          #   Lean ↔ C++ bridge (60+ functions)
  lib/measure/
    lakefile.lean             # 🏗️ Lake build configuration
test/
  TestDim.lean                # Dimension system tests
  TestQuantity.lean           # Quantity arithmetic tests
  TestConstants.lean          # Physical constants tests
  TestBridge.lean             # Float↔Real bridge tests
  TestPhysics.lean            # Physics module tests
  TestProperties.lean         # Property-based tests
  TestIntegration.lean        # Integration tests
  TestStress.lean             # Stress tests

---

🚀 Getting Started

Prerequisites:

• elan — Lean 4 toolchain manager
• C++17 compiler
• CMake >= 3.16

# Clone
git clone https://github.com/SStarrySSky/Measure.git
cd Measure

# Build (fetches Mathlib automatically)
cd measure/lib/measure
lake build

# Run tests
lake build MeasureTest

# CLI
lake exe measure-cli help
lake exe measure-cli check src/Measure/Physics/
lake exe measure-cli constants
lake exe measure-cli theories

---

📊 Verification Stats

Metric	Value
📄 Source files	161 (.lean) + 18 (C++)
📝 Lines of code	~20,000 (Lean) + ~3,000 (C++)
✅ Theorems / Lemmas	267
📌 Axioms	23 (20 physics/math, 2 trust boundary, 1 computational)
🚫 Sorry	0
🏗️ Build jobs	2,881 (all passing)
🧪 Test jobs	2,639 (all passing)
🌌 Physics domains	25

Every axiom is documented and justified. The 20 physics/math axioms represent genuine theorems that require Mathlib infrastructure not yet available (multivariate calculus, ergodic theory, etc.). The 2 trust boundary axioms are guarded by a private token. Zero sorry means zero incomplete proofs.

---

🧭 Philosophy

Physics is not mathematics. It is built on measurement, experiment, and approximation. Theories contradict each other — and that's fine. What matters is that each theory is self-consistent on its own terms, and that the contradictions are tracked, not hidden.

Measure doesn't try to unify all of physics into one consistent framework. That's not possible, and pretending otherwise is dishonest. Instead, it provides the infrastructure to:

1. 📝 Formalize any physics theory as a typed, dimension-checked module
2. ✅ Verify its internal self-consistency at compile time
3. 🔗 Relate it to other theories with explicit compatibility/conflict declarations
4. 🔢 Compute with proper uncertainty propagation
5. 📜 Prove properties using Mathlib-backed real analysis

The goal is not to replace physicists. It's to give them a tool where the compiler catches the mistakes that humans miss — wrong dimensions, violated conservation laws, inconsistent approximations — so they can focus on the physics.

---

📄 License

MIT