sqrt_two_add_sqrt_three_pos
plain-language theorem explainer
Strict positivity of √2 + √3 as a real number. Gravity analysts cite it when checking that the Freudenthal stencil moment tensor A₀ has positive off-diagonal entries. The proof is a three-line positivity split: √3 > 0, √2 ≥ 0, then linear arithmetic.
Claim. One has $0 < \sqrt{2} + \sqrt{3}$ in $\mathbb{R}$.
background
This module is Stage 1 of Test G in the QG full-theory campaign: the action-level continuum limit of the frozen quadratic energy on the canonical periodic Freudenthal triangulation at every side length $N > 2$. The quadratic form of the canonical Regge Hessian is identified with a seven-class nearest-displacement stencil whose weights are $c_d = \sqrt{\ell_d^2}$ for edge-length squares $\ell^2 \in {1,1,1,2,2,2,3}$ (axis, face-diagonal, body-diagonal classes).
The stencil moment tensor is the exact $3\times 3$ matrix $A_0 = \sum_d c_d, d d^\top$, evaluated as $A_0 = (1+\sqrt{2})I + (\sqrt{2}+\sqrt{3})J$ with $J$ the all-ones matrix. Off-diagonal entries are therefore exactly $\sqrt{2}+\sqrt{3}$; this lemma is the elementary positivity fact needed before anisotropy statements.
The sole recorded upstream dependency is a PRC-native positivity predicate on ratio orbits; the body itself uses only Mathlib square-root positivity and nonnegativity.
proof idea
Term/tactic hybrid. First obtain $0 < \sqrt{3}$ from Real.sqrt_pos applied to the norm_num fact $0 < 3$. Separately record $0 \le \sqrt{2}$ via Real.sqrt_nonneg. Feed both inequalities to linarith, which closes $0 < \sqrt{2} + \sqrt{3}$. No Recognition-specific lemmas are invoked in the body.
why it matters
Feeds stencilMomentTensor_offDiag_pos, which rewrites the off-diagonal case of stencilMomentTensor_eq and concludes $0 < A_0_{ij}$ for $i \neq j$ by simpa on this fact. That positivity is the kernel-checked finding that $A_0$ is anisotropic (not a scalar multiple of the identity), the tensor-first signature required for the continuum limit of the Freudenthal stencil energy under panel-locked Test G.
In the broader Recognition gravity stack this is preflight arithmetic for the exact general-$N$ stencil identity and moment tensor, not a forcing-chain landmark (T0–T8). It closes a tiny positivity obligation so the anisotropic continuum analysis can proceed without numeric certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.