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

Physical

show as:
view Lean formalization →

The Physical structure bundles the three positivity conditions 0 < B.c, 0 < B.hbar and 0 < B.G for any BridgeData record. Analysts cite it to discharge positivity hypotheses when proving identities for the recognition length. The declaration is a pure structure definition with no computational content or additional proof steps.

claimLet $B$ be a BridgeData record with real components $G$, $ħ$, $c$. The proposition Physical($B$) holds precisely when $0 < B.c$, $0 < B.ħ$ and $0 < B.G$.

background

Bridge.DataCore isolates the minimal data structure BridgeData containing the external anchors $G$, $ħ$, $c$ together with display units $τ_0$ and $ℓ_0$. The module keeps the certified import closure small by avoiding IndisputableMonolith.Core. Physical packages the positivity statements that are separately established for the RS-native constants in the Constants module.

proof idea

The declaration is a structure definition that directly encodes the three field hypotheses. No lemmas or tactics are applied; it functions as a reusable Prop wrapper for the positivity assumptions.

why it matters in Recognition Science

Physical supplies the hypothesis interface for lemmas such as lambda_rec_dimensionless_id_physical and lambda_rec_pos that establish the dimensionless identity and positivity of the recognition length. It appears in the derivation chain leading to gauge-invariant results for $α^{-1}$ and curvature corrections. The structure closes the gap between abstract BridgeData and the concrete positivity lemmas proved for the RS constants.

scope and limits

Lean usage

lemma lambda_rec_pos (B : BridgeData) (H : Physical B) : 0 < lambda_rec B := by unfold lambda_rec; apply Real.sqrt_pos.mpr; apply div_pos; exact mul_pos H.hbar_pos H.G_pos

formal statement (Lean)

  28structure Physical (B : BridgeData) : Prop where
  29  c_pos    : 0 < B.c
  30  hbar_pos : 0 < B.hbar
  31  G_pos    : 0 < B.G
  32
  33/-- Recognition length from anchors: λ_rec = √(ħ G / c^3). -/

used by (40)

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

… and 10 more

depends on (19)

Lean names referenced from this declaration's body.