Speed of light
provedc = one voxel per tick in RS-native units. The SI numerical value enters only by external calibration.
gap: SI numerical value of c requires external calibration.
recognition
the machine-checked proof layer behind Pith
Recognition Science is a parameter-free formalization of reality. It begins with distinction ∃ x, y ∈ K : x ≠ y and continues, by forced theorems, to every empirically observed constant. The library is public Lean 4 source. Each module is auditable, every theorem citable.
the proof path
A forced sequence. Each step is a Lean theorem; nothing is fitted.
- 1 distinction
- 2 J-cost
- 3 phi
- 4 D = 3
- 5 constants
- 6 universal forcing
ask recognition
Get a derivation grounded in the formal library. Every answer becomes its own permalink page and can back an explainer.
recognition review
Submit a paper. Recognition Review currently uses Grok 4.3 at high reasoning for the active review lane, plus synthesis grounded in the Recognition library.
check a claim
Speed of light, fine-structure constant, gravity, dimension 3, the mass gap, and more — each linked to its proof.
formal source
Browse every Lean module the framework relies on. Module and theorem pages now have tracked explainer pages.
what can recognition prove?
High-signal claims. Each card links to the load-bearing theorem in Lean. Every claim carries an honest status label.
Why the golden ratio
provedSelf-similar closure forces r^2 = r + 1, so r = phi. No other fixed point survives.
Fine-structure constant
provedalpha-inverse sits inside (137.030, 137.039) by an explicit phi-based derivation; CODATA 137.036 lies inside the interval.
gap: Higher-order corrections beyond the gap-45 term are still being audited.
All constants from phi
provedℏ, G, c, and α are functions of phi alone in RS-native units. No free parameters.
Why space is 3D
provedThe 8-tick recognition cycle forces space dimension D = 3 via 2^(D-1) = 4 closure.
Gravity from the ledger
provedG = phi^5 in RS-native units. Equivalence principle and propagation speed equal to c are automatic.
Yang-Mills mass gap
provedOn the phi-lattice, the spectral gap equals J(phi) = (sqrt(5) - 2)/2.
Baryon asymmetry
provedThe matter-antimatter asymmetry sits at phi-rung 44, an explicit Recognition prediction.
Universal forcing
provedLogic forces one canonical arithmetic across all admissible Law-of-Logic settings. Mathematics and physics are downstream of one invariant law.
Reciprocal cost J(x)
provedThe unique reciprocal-symmetric cost is J(x) = (x + x^-1)/2 - 1. No alternative cost survives.
load-bearing theorems
The named results papers actually map onto. The forcing chain reads roughly top to bottom.
theorem
reality_from_one_distinction
From ∃ x y, x ≠ y the structure of reality is forced.
theorem
law_of_existence
Existence is forced by distinction. The first move of the chain.
def
universal_forcing
Logic forces one canonical arithmetic across all admissible settings.
theorem
washburn_uniqueness_aczel
Reciprocal-symmetric cost has one solution: J(x) = ½(x + x⁻¹) − 1.
theorem
bilinear_family_forced
The bilinear cost family is forced by the d'Alembert factorization.
theorem
phi_unique_self_similar
Self-similar closure forces the golden ratio: r² = r + 1.
theorem
eight_tick_forces_D3
The 8-tick cycle forces space dimension D = 3.
theorem
all_constants_from_phi
All named constants are functions of φ alone.
theorem
gravity_from_ledger
Gravity falls out of the ledger. Equivalence principle automatic.
theorem
spacetime_dim_eq_four
Spacetime, light cone, and proper time emerge from the recognition lattice.
theorem
spectral_gap
Yang-Mills mass gap on the φ-lattice: Δ = J(φ) = (√5 − 2)/2.
theorem
etaBExactRungCert
Baryon asymmetry η_B sits at φ-rung 44.
proof browser
The formal library, grouped by branch. Click through to browse all modules and declarations.
Foundation
From one distinction to a forced arithmetic. The core derivation chain: existence, distinction, recognition lattice, φ, dimension, time, universal forcing.
-
Foundation.RealityFromDistinction -
Foundation.AlexanderDuality -
Foundation.ArithmeticFromLogic
browse →
Cost
Reciprocal-symmetric cost. Uniqueness of J(x) = ½(x + x⁻¹) − 1, convexity, the Aczél class, and the d'Alembert factorization.
-
Cost.FunctionalEquation -
Cost -
Cost.JcostCore
browse →
Constants
Named constants in RS-native units. ℏ = φ⁻⁵, the α⁻¹ band, gravitational coupling, ℓ₀, τ₀ — all as functions of φ.
-
Constants -
Constants.RSUnitsHelpers -
Constants.Derivation
browse →
Gravity
Zero-parameter gravity. G = φ⁵/π, the equivalence principle from the ledger, kappa bounds.
-
Gravity.WeakFieldConformalRegge -
Gravity.JCostInflaton -
Gravity.BlackHoleInformationPreservation
browse →
Unification
Cross-domain consequences. Spacetime emergence, Lorentzian signature uniqueness, the Yang-Mills mass gap on the φ-lattice, octave duality.
-
Unification.YangMillsMassGap -
Unification.SpacetimeEmergence -
Unification.QuantumGravityOctaveDuality
browse →
Cosmology
Cosmological identities. The η_B baryon asymmetry as the φ-rung 44 result, prefactor derivations.
-
Cosmology.EtaBExactRungDerivation -
Cosmology.EtaBPrefactorDerivation -
Cosmology.WMassAnomalyStructure
browse →
Patterns
Discrete pattern algebra used throughout the recognition lattice.
-
Patterns -
Patterns.GrayCycle -
Patterns.GrayCycleGeneral
browse →
Root
Top-level imports and lake configuration.
-
IndisputableMonolith -
lakefile
browse →
all other domains
Auto-discovered from the public mirror. Every directory shown below is sorry-free, admit-free, and contains no domain-specific axioms.
Physics
NumberTheory
Mathematics
Relativity
Masses
Chemistry
Information
RRF
Astrophysics
Complexity
CrossDomain
Materials
NavierStokes
Sociology
Economics
Quantum
Thermodynamics
QFT
RecogGeom
StandardModel
Ethics
Experimental
Measurement
Engineering
Papers
Philosophy
Numerics
ClassicalBridge
Climate
Flight
ILG
Linguistics
RecogSpec
Gap45
Nuclear
Decision
URCAdapters
Action
Geology
MusicTheory
Aesthetics
CondensedMatter
Acoustics
Education
GameTheory
Sport
Algebra
Causality
Core
CPM
Ecology
Recognition
RSBridge
Applied
Certificates
Compat
Cryptography
Geometry
Meta
Modal
Support
TruthCore
URCGenerators
Anthropology
Archaeology
Combustion
Governance
NetworkScience
PhiSupport
Robotics
Statistics
Superhuman
YM
ArtHistory
Bridge
Cognition
Crystallography
Econ
Energy
Jurisprudence
LightCone
Meteorology
QuantumComputing
Sports
Streams
VM
Ablation
Agriculture
Agronomy
Analysis
Architecture
Astronomy
Chain
Common
ConeExport
Config
Cosmochemistry
CostUniqueness
CriminalJustice
Criminology
Cybernetics
Data
Derivations
Ethnomusicology
Experiments
Exports
Geophysics
Hydrology
InternationalRelations
LedgerParityAdjacency
LedgerPostingAdjacency
LedgerUniqueness
LedgerUnits
MaxwellDEC
Music
Musicology
Oceanography
Operations
Paleoanthropology
Particles
PDG
Pipelines
Potential
Predictions
ProjectManagement
QuantumChemistry
Safety
Shims
Spectra
Spiral
Stratigraphy
Theology
Transportation
UnitMapping
Urban
VoxelWalks
search by name
Find a theorem or module by exact identifier. For natural-language questions, use Ask Recognition instead.