pi0_error_bound
plain-language theorem explainer
Recognition Science calculations for the neutral pion lifetime error are bounded by showing that 1/71 lies below 15/1000. Modelers of 8-tick phase mismatches cite this to keep the predicted discrepancy under 1.5 percent. A single norm_num call verifies the inequality by arithmetic normalization.
Claim. $ 1/71 < 15/1000 $
background
In the QFT anomalies module, quantum effects such as the chiral anomaly for neutral pion decay arise from mismatches between continuous phases and the discrete 8-tick structure of Recognition Science. The local setting treats anomalies as consequences of phase quantization at the eight-tick octave, with the doc-comment noting the error reaches approximately 1.41 percent where 1/71 approximates 0.0141.
proof idea
The proof is a term-mode application of the norm_num tactic, which normalizes the rational numbers and discharges the inequality by direct computation.
why it matters
This result anchors the error estimate for the pi0 lifetime prediction in the anomalies section. It feeds into sibling theorems on relative error and the two-percent bound, confirming consistency with the eight-tick period and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.