leptonLogAsym_pos
plain-language theorem explainer
The lepton generation-step log-asymmetry is strictly positive: log(11/6) > 0. Anyone building the Item 8 refined mass-ratio family for leptons cites this to guarantee a nonzero log step. The proof is two lines: 11/6 > 1 by numerical normalization, then the standard positivity of real log on (1, ∞).
Claim. One has $\log(11/6) > 0$ as a real number (equivalently $11/6 > 1$).
background
Item 8 in the Recognition Science verification stack concerns a unified sub-leading correction to sector mass ratios on the $\varphi$-ladder. The module builds the smallest precise theorem framework that would close the open quark sub-leading item and make the all-sector generalization falsifiable.
The lepton residual signature uses a fixed generation-step ratio $11/6$. The associated log-asymmetry is $\log(11/6)$. Downstream residual and refined-family constructions need this quantity to be nonzero (and, for orientation of inequalities, positive) so that denominators involving $\ln(s_{12}/s_{23})$ and sign-split coefficients remain well-defined.
No deep RS forcing (T5–T8, RCL) is invoked here; the statement is pure real analysis on a concrete rational greater than one.
proof idea
Tactic proof in two steps. First establish $1 < 11/6$ by norm_num. Then apply Real.log_pos, which states that $\log x > 0$ whenever $x > 1$. No Recognition-specific lemmas are used.
why it matters
Feeds the immediate parent leptonLogAsym_ne_zero, which upgrades positivity to $\log(11/6) \neq 0$ via ne_of_gt. That nonzero fact is the arithmetic gate for lepton residual orientation and for any refined-family coefficient formulas that divide by the generation-step log.
Within Item 8 closure, the module already has structural rigidity (consistency_of_ratioFamily), closed-form $\eta$ identities, and $\exists!$ solvability/uniqueness for refined families on signed sectors. A positive lepton log-asymmetry is a tiny but necessary numerical hinge so those algebraic closures apply cleanly to the lepton signature rather than stalling on a zero denominator.
It does not itself close Item 8 for quarks; it only clears the lepton log step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.