cert
plain-language theorem explainer
The definition cert assembles a Muong23Cert structure by supplying the zero-cost condition at equal arguments, non-negativity of domain cost for positive inputs, and positivity of the canonical threshold. Physicists modeling the muon g-2 anomaly inside Recognition Science would cite it as the structural certificate for the J-cost derivation of Delta a_mu. It is built by direct assignment to the lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
Claim. Let domainCost$(m,e)$ be the J-cost of the ratio $m/e$ and canonicalThreshold the positive threshold. The structure Muong23Cert requires domainCost$(r,r)=0$ for all $r≠0$, domainCost$(m,e)≥0$ for $m>0$ and $e>0$, and canonicalThreshold$>0$. Then cert is the instance obtained by applying the corresponding lemmas.
background
In the Muon g-2 from J-Cost module the Recognition Science derivation of the anomalous magnetic moment deviation rests on the J-cost function. domainCost is the J-cost of the mass-to-energy ratio and is non-negative by the general cost_nonneg theorem from ObserverForcing. canonicalThreshold is shown positive by unfolding and applying phi_gt_onePointFive from the RecognitionLattice3 layer.
proof idea
This is a definition that constructs the Muong23Cert structure by direct field assignment to the three pre-proved lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No tactics beyond the structure constructor are required.
why it matters
This definition supplies the concrete certificate for the muon g-2 calculation inside the Recognition Science framework. It occupies the structural placeholder slot noted in the module documentation, where the computed Delta a_mu exceeds the experimental value by roughly two orders of magnitude. The construction closes the interface to the J-cost and phi-ladder machinery without resolving the scaling discrepancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.