Recognition Science: A Machine‑Verified, Parameter‑Free Framework Deriving Physics from a Single Axiom

Abstract

We present a certificates‑first, machine‑verified software artifact in Lean 4. From a single axiom ("nothing cannot recognize itself"), we derive a discrete recognition calculus, expose only dimensionless observables via a units‑quotiented bridge, and package the result as machine‑checked propositions with one‑line #eval reports on a pinned toolchain. What is proven includes: RSRealityMaster(φ) (reality bundle and spec closure), PrimeClosure (framework uniqueness up to units and MPMinimal), Exclusivity+ (unique φ pinning selection+closure and bi‑interpretability), Coherence + category‑theory equivalence at the pinned φ, UltimateClosure (exists! φ with exclusivity+, units‑class coherence, categorical equivalence), and algebraic φ selection (unique positive root of x^2 = x + 1). Representative consequences include exact 8‑tick minimality (3D), a discrete light‑cone bound with slope c, Planck normalization (c^3 λ_rec^2)/(ℏG) = 1/π under mild positivity, and φ‑power mass‑ratio ladders. Reports are pure terms; failures deterministically flip or refuse to elaborate. The artifact is a reusable, open‑source digital instrument: rerun the manifest to reproduce every OK.