pith. machine review for the scientific record. sign in
def definition def or abbrev high

lambda_rec

show as:
view Lean formalization →

This definition supplies the recognition length as the square root of ħ times G divided by pi times c to the third power, using values from the bridge data structure. Researchers in Recognition Science cite it when connecting the fundamental length to gravitational and Planck constants. The code is a direct one-line square root computation on the supplied anchors.

claimFor a structure $B$ supplying real anchors $G$, $ħ$, and $c$, define the recognition length by $λ_{rec}(B) := √(ħ · G / (π · c³))$.

background

BridgeData is a structure holding external anchors G (Newton's gravitational constant), ħ (reduced Planck constant), c (speed of light), plus display values τ₀ and ℓ₀. The module isolates these core anchors and the recognition length expression to keep the certified import closure small, avoiding larger subsystems. Upstream results include the Constants definition of G as λ_rec² c³ / (π ħ), which inverts the present relation, and the native recognition length set to ℓ₀ in the eight-tick cycle.

proof idea

This declaration is a one-line definition that applies the real square root directly to the product of the hbar and G fields divided by pi times the cube of the c field.

why it matters in Recognition Science

The definition underpins the lemma lambda_rec_dimensionless_id establishing the identity (c³ λ_rec²) / (ħ G) = 1/π under positivity assumptions. It also supports the derivation of G in Constants and anchors the recognition length in the eight-tick octave (T7) of the forcing chain. This closes a key relation for the fundamental length scale in the Recognition Science framework.

scope and limits

formal statement (Lean)

  34noncomputable def lambda_rec (B : BridgeData) : ℝ :=

proof body

Definition body.

  35  Real.sqrt (B.hbar * B.G / (Real.pi * (B.c ^ 3)))
  36
  37/-- Dimensionless identity for λ_rec (under mild physical positivity assumptions):
  38    (c^3 · λ_rec^2) / (ħ G) = 1/π. -/

used by (21)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.