QuarkNonCircularity
plain-language theorem explainer
Packages the non-circularity certificate for the six-quark forward mass pipeline: yardstick exponents come from cube geometry, integer rungs from generation torsion, and gap inputs Z from electric charge, with no PDG mass entering any formula. Anyone auditing that quark mass ratios are genuine forward predictions (not fits) cites this bundle. It is a structure of three Prop fields; the equalities are discharged by a later instance, not proved here.
Claim. A non-circularity certificate for the quark forward pipeline is a triple of design assertions: (i) sector yardsticks are geometric, $B_{\mathrm{pow}}(\mathrm{up})=-1$, $r_0(\mathrm{up})=35$, $B_{\mathrm{pow}}(\mathrm{down})=23$, $r_0(\mathrm{down})=-5$; (ii) rungs come from generation torsion, $r_{\mathrm{up}}(u,c,t)=(4,15,21)$ and $r_{\mathrm{down}}(d,s,b)=(4,15,21)$; (iii) $Z$ comes from charges, $Z(\mathrm{up},2/3)=276$ and $Z(\mathrm{down},-1/3)=24$. No measured quark mass appears in any of these inputs.
background
The module builds a single Convention-A forward pipeline for all six quark masses. Sector yardstick $A_s=2^{B_{\mathrm{pow}}(s)}E_{\mathrm{coh}}\varphi^{r_0(s)}$, integer rung $r_i=$ baseline $+$ generation torsion, and band correction $\mathrm{gap}(Z_i)=\log_\varphi(1+Z_i/\varphi)$ feed the mass law $m_i(\mu^*)=A_s\varphi^{r_i-8+\mathrm{gap}(Z_i)}$. Outputs are dimensionless ratios $m_q/m_e$ at the anchor scale, so no absolute-mass calibration seam is required.
$B_{\mathrm{pow}}$ is not free: Anchor derives it from cube edge counting ($B_{\mathrm{pow}}(\mathrm{UpQuark})=-A=-1$, $B_{\mathrm{pow}}(\mathrm{DownQuark})=2E_{\mathrm{total}}-1=23$). The same counting layer supplies $V=8,E=12,F=6$ and related integers; $\varphi$ enters from the T5/T6 forcing chain. The design claim is that every arrow in predict_mass $\to$ yardstick / rung / gap terminates on those integers or on charge, never on a PDG quark mass.
proof idea
No proof body: this is a structure whose three fields are propositions. Instantiation is deferred to non_circular, which fills the fields by named equalities (B_pow_UpQuark_eq, r0_UpQuark_eq, B_pow_DownQuark_eq, r0_DownQuark_eq), the bundled rung lemma quark_rungs_from_torsion, and quark_Z_from_charges. The structure itself only records the certificate shape that those lemmas must satisfy.
why it matters
Without an explicit non-circularity certificate, the quark mass ratios could be accused of PDG-targeting. This structure is the type of that certificate; the sole downstream consumer is non_circular, which asserts the certificate is inhabited. It locks the three input channels of the RS mass formula (yardstick $\times\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) to cube geometry, generation torsion, and charge-band $Z$, consistent with the module's "no PDG input" mandate and with $\varphi$ from T5/T6. It does not itself close the absolute-mass seam or the T-minus-1 ledger bridge; it only certifies that the quark forward path, as coded, does not smuggle measured quark masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.