eta_bar_pos
plain-language theorem explainer
Positivity of the Wolfenstein eta-bar parameter follows from its constant definition in the CKM module. Researchers modeling CP violation in the quark sector cite it to fix the sign of the Jarlskog invariant. The proof is a one-line wrapper that unfolds the definition and normalizes the numerical inequality.
Claim. In the Wolfenstein parametrization of the CKM matrix, the CP-violation parameter satisfies $0 < 0.35$.
background
The StandardModel.CKMMatrix module derives the CKM matrix from phi-quantized mixing angles tied to the 8-tick phase structure. Wolfenstein_eta is defined as the constant 0.35 that encodes the observed CP phase. Upstream results supply foundational structures for collision-free empirical programs and simplicial ledgers that underwrite the overall construction.
proof idea
The term proof unfolds the definition of wolfenstein_eta to the literal value 0.35 and applies norm_num to discharge the strict inequality.
why it matters
This theorem fixes the positive sign of eta-bar, which is required for J_CP = A²λ⁶η-bar > 0 in the Jarlskog invariant. It anchors the CKM derivations from golden-ratio geometry in the Recognition Science framework and aligns with the eight-tick octave. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.