Masses Jcost Perturbation

Mass-Layer J-Cost Perturbation

Mass-layer J-cost perturbation is the study of how the recognition cost function J changes when its argument is shifted slightly from unity, written as J(1 + α). The core forcing theorem proves that the two-channel coefficient is unique: 2·J(1 + α) = α² + 12α³, with no free parameter left undetermined. This α² + 12α³ decomposition is the radiative correction structure used in the refined shift of the mass ledger.

The module upstreams this perturbative closure into the Masses namespace, tying it to canonical lepton-step definitions. It certifies three things: the J(1 + α) perturbative channel form, the explicit α² + 12α³ radiative decomposition used in refined_shift, and exact geometric evaluations of the zeroth-order constants in the same path. The constants that appear are not fitted; they are forced by the structure of the ledger and the cost function.

The theorems force specific numerical coefficients from the assumption that a step takes a particular affine form. For the electron-muon step, the passive energy term E_passive plus 1/(4π) minus a correction term forces the correction coefficient to be 1 and the denominator to be 4. For the muon-tau step, the cube faces term 6 minus a coefficient times α forces that coefficient to be 37/2 and the denominator to be 2. These are not measurements; they are derivations from the form of the step and the cost function.

The ledger fraction (W + E_total)/(k·E_passive) forces k = 4, and the weight split a + b = 2 forces a = 1 and b = 1, meaning the work and total energy contribute equally. The refined shift, built from the base shift plus the radiative correction, forces its coefficient u = 2 and c = 12. The module thus establishes that the lepton mass steps are not arbitrary: their perturbative coefficients are uniquely determined by the recognition cost function and the ledger structure.

THEOREM jcost_two_channel_coeff_unique · IndisputableMonolith/Masses/JCostPerturbation.lean

THEOREM step_e_mu_invpi_quadratic_forced · IndisputableMonolith/Masses/JCostPerturbation.lean

THEOREM step_mu_tau_full_affine_forced_from_face_term · IndisputableMonolith/Masses/JCostPerturbation.lean

THEOREM ledger_fraction_denominator_forced · ledger_fraction_weight_split_forced · IndisputableMonolith/Masses/JCostPerturbation.lean

THEOREM refined_shift_full_affine_forced_from_base_role · IndisputableMonolith/Masses/JCostPerturbation.lean

What this page does not claim

This answer does not claim that any lepton mass value is derived, only that the perturbative coefficients in the step forms are forced. This answer does not claim that the fine-structure constant α is derived; its seed is an identification, not a derived coupling. This answer does not claim that the physical recognition-to-linking bridge is closed; that bridge remains open.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/JCostPerturbation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: