When meters become feet, what stays true?
- What it is
- A paper gives a mathematical language for physical units that can convert between them while proving limited rescaling laws.
- Who did it
- Eric Allen.
- What it could mean
- If its theorems hold, mathematicians and language designers gain a sharper boundary for which changes of units leave a calculation unchanged.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
A Calculus for Units of Measure with Conversion ↗See the proposed checks
Map named theorems to Lean declarations; inspect no-unit-constant, positive-factor, nonzero, first-order and decline assumptions; check exact factor extraction.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
Different units, the same quantity
The rulers illustrate a quantity staying fixed while its numerical description changes units. The paper gives formal conditions for conversions to preserve meaning. This is not a numerical conversion table or a tested engineering system.
Read the source · Theorems 5.2–5.3 · dimension-coherent conversion ↗- What it claims
- The typed calculus characterizes surviving rescaling invariance with conversions, checks finite unit declarations, and gives a first-order drift procedure that can certify, name a factor, or decline. This is overdue source recovery, not a deployed-software claim.
- Why this could matter
- When meters become feet, what stays true? A calculation can appear dimensionally sound yet change its answer when conversion factors change. This paper claims exact rules for when unit-aware programs keep their meaning, and a checker that can flag dependence or decline.
- If it holds up
- It would extend dimensional-analysis theory to a calculus with conversions and give a Lean-mechanized route for checking its stated invariance and factor-declaration results.
- If it does not
- A counterexample would show where conversion, declaration consistency, or a claimed invariance condition needs a narrower rule.
- Impact horizon
- Methods · Dimensional analysis · Programming-language semantics · Formalized mathematics
- Version
- submitted 2026-09-29 03:16:30 UTC
- Why we tracked it
- unexamined mathematical theorem intake, not a proof verdict or homepage feature.
- Highest-risk dependency
- Conversion invariance is conditional on coherent rescaling; consistent declarations may still be insufficient to determine a factor. No external workflow guarantee follows.
- Available artifacts
- Lean 4 mechanization reported at https://github.com/ericeallen/lambda-s; repository and evaluator not downloaded or run.
- Current boundary
- Intake record only; examination not started.