Physical
plain-language theorem explainer
Physical packages the three positivity assumptions 0 < B.c, 0 < B.hbar and 0 < B.G for an arbitrary BridgeData record. Analysts cite the structure to discharge the positivity hypotheses that appear in lemmas about the recognition length without repeating the inequalities. The declaration is a bare structure definition that simply lists the three field assertions.
Claim. Let $B$ be a BridgeData record. The predicate Physical($B$) holds precisely when $0 < B.c$, $0 < B.hbar$ and $0 < B.G$.
background
BridgeData is the structure that carries the external constants G, ħ, c, τ₀ and ℓ₀ as real numbers with no axioms attached. The module isolates these anchors so the certified import closure stays small and excludes the larger Core subsystem. Upstream positivity results c_pos, hbar_pos and G_pos from Constants establish the same three inequalities for the RS-native values; Physical merely repackages them for a generic BridgeData instance.
proof idea
The declaration is a structure definition that directly enumerates the three positivity fields; no lemmas or tactics are invoked.
why it matters
It supplies the packaged positivity hypotheses required by lambda_rec_dimensionless_id_physical and lambda_rec_pos. Those lemmas in turn feed the dimensionless identity for λ_rec and the gauge-invariance result for α⁻¹. The structure therefore sits at the narrow bridge layer that connects RS-native constants (c = 1, ħ = φ⁻⁵, G = φ⁵/π) to analytic statements while keeping the import surface minimal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.