fermionJCostAverage
plain-language theorem explainer
The definition fermionJCostAverage sets the average J-cost for fermions to the mean of cosines evaluated at odd multiples of π/4. Physicists comparing boson and fermion sectors in Recognition Science cite it to fix the SUSY breaking scale via their J-cost difference. The body is a direct four-term average that evaluates to zero.
Claim. The average J-cost for fermions is defined by $ (cos(π/4) + cos(3π/4) + cos(5π/4) + cos(7π/4))/4 $.
background
The module treats supersymmetry breaking as arising from unequal J-costs between boson and fermion sectors under the 8-tick octave. J-cost is the recognition cost of a state, obtained from the cost function of a multiplicative recognizer or observer forcing event. Upstream definitions supply the scale function as φ^k and the derived cost of a comparator on positive ratios.
proof idea
The definition is a direct arithmetic average of the four cosine terms at odd multiples of π/4. No lemmas are applied; the body simply writes the expression.
why it matters
It supplies the fermionic input to the SUSY breaking scale M_SUSY ~ M_Planck × |J_boson - J_fermion| stated in the module comment. The result closes the RS mechanism in which 8-tick phase asymmetry spontaneously breaks supersymmetry. It feeds the parent SUSY breaking scale computation and the viability checks listed among siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.