Physical
plain-language theorem explainer
The positivity predicate on bridge data asserts that c, ħ and G are positive. Analysts deriving properties of the recognition length λ_rec cite this predicate to bundle the required inequalities for analytical lemmas. The predicate is introduced directly as a structure with three field assertions.
Claim. For bridge data $B$, the predicate holds precisely when $0 < B.c$, $0 < B.ħ$ and $0 < B.G$.
background
BridgeData supplies the external anchors G, ħ, c together with display parameters tau0 and ell0; its doc-comment states these are provided as data with no axioms. Physical packages the minimal positivity requirements on the three anchors. Upstream lemmas c_pos, hbar_pos and G_pos from Constants establish the same inequalities for the RS-native constants, which Physical reuses when the bridge data is instantiated with those constants. The module isolates the recognition length identity λ_rec = √(ħ G / c³) inside a deliberately small import closure.
proof idea
The declaration is a structure definition that directly asserts the three positivity fields; no tactics or lemmas are applied.
why it matters
Physical serves as the hypothesis carrier for lambda_rec_dimensionless_id_physical and lambda_rec_pos. It is invoked inside alphaInv_gauge_invariant and dimensions_status. It supports the bridge from external anchors to the RS-native constants c = 1, ħ = φ^{-5}, G = φ^5 / π that appear in the recognition length and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.