yardstick_pos
plain-language theorem explainer
Every sector yardstick is strictly positive. Forward-mass and residue-form arguments in the quark pipeline cite this to discharge positivity side-conditions. The proof unfolds the product definition and applies positivity of powers of 2 and of φ.
Claim. For every mass sector $s$, the sector yardstick $A_s = 2^{B_{\mathrm{pow}}(s)}\, E_{\mathrm{coh}}\, \varphi^{r_0(s)}$ satisfies $0 < A_s$.
background
The QuarkForwardPipeline module builds a single Convention-A forward map for all six quark masses with no PDG targets. Inputs are counting-layer integers, the golden ratio $\varphi$ (forced at T5/T6), and $\alpha$ from the same layer. Absolute masses are avoided; the testable outputs are dimensionless ratios $m_q/m_e$ at the anchor scale $\mu^*$.
The first pipeline step is the sector yardstick $A_s = 2^{B_{\mathrm{pow}}(s)} \times E_{\mathrm{coh}} \times \varphi^{r_0(s)}$. Here $E_{\mathrm{coh}}$ is the coherence energy fixed by the RS-native $\hbar = \varphi^{-5}$, $B_{\mathrm{pow}}(s)$ is the integer cube-geometry exponent for sector $s$, and $r_0(s)$ is the sector baseline rung. Predicted masses then read $m_i(\mu^*) = A_s , \varphi^{r_i-8+\mathrm{gap}(Z_i)}$.
Positivity of $A_s$ is the elementary gate before any mass or ratio comparison: every later factor is a power of $\varphi$ or a gap correction, so the sign of $m_i$ tracks the sign of the yardstick.
proof idea
Term-mode proof by unfolding. Expand yardstick and E_coh to the three-factor product $2^{B_{\mathrm{pow}}(s)} \cdot \varphi^{-5} \cdot \varphi^{r_0(s)}$. Apply mul_pos twice. Each factor is discharged by zpow_pos: base $2>0$ with integer exponent $B_{\mathrm{pow}}(s)$; base $\varphi>0$ (from phi_pos) with exponents $-5$ and $r_0(s)$. No sector case-split is required.
why it matters
This lemma is the positivity hypothesis consumed by pipeline_equals_residue_form, which equates the Convention-A core prediction to the residue form with electron reference mass via core_eq_residue_of_positive (yardstick_pos s) m_electron_pos. Without $A_s>0$, that identification does not fire.
In the broader RS mass story the yardstick is the sector-dependent prefactor in the $\varphi$-ladder formula $m = A_s , \varphi^{r-8+\mathrm{gap}(Z)}$. Establishing $A_s>0$ for every sector closes the trivial but mandatory sign step of the no-PDG forward pipeline and underwrites the sibling positivity facts for the six quarks and the electron. It does not itself force rung integers or gap values; those sit upstream in torsion and charge-band maps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.