IndisputableMonolith.Masses.JCostPerturbation
The module upstreams the two-channel form of the J-cost perturbation for (1+α) in the masses domain. Researchers deriving masses via the phi-ladder and ledger topology would cite it to access the decomposed channel structure. It consists of a sequence of definitions establishing the form, coefficient uniqueness, and ledger fraction relations.
claimThe two-channel form decomposes the J-cost perturbation as $J(1+α) = c_1 J(x_1) + c_2 J(x_2)$ where the coefficients $c_i$ are unique and satisfy the ledger-fraction relations forced by the Recognition Composition Law.
background
Recognition Science defines the J-cost via the functional equation $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$, with $J(x) = (x + x^{-1})/2 - 1$. The module imports the RS time quantum τ₀ = 1 tick from Constants and the constructive derivation of α^{-1} from cubic-ledger geometry in AlphaDerivation, which obtains 4π from Gauss-Bonnet applied to vertex deficits of Q₃.
proof idea
This is a definition module, no proofs. It sequences definitions for the two-channel form, uniqueness of coefficients, and forced ledger-fraction denominators, each building directly on the imported constants and alpha geometry.
why it matters in Recognition Science
The module supplies the channel decomposition required for mass derivations on the phi-ladder. It feeds the mass-topology counts and ledger-fraction equations that appear among its siblings. It fills the upstreamed J-cost(1+α) step that connects the alpha derivation to the mass sector.
scope and limits
- Does not derive the numerical value of α or any mass.
- Does not extend beyond the two-channel decomposition.
- Does not invoke the forcing chain T5-T8 or spatial dimension D=3.
- Does not address Berry creation thresholds or dream fractions.
depends on (2)
declarations in this module (89)
-
theorem
jcost_two_channel_form -
theorem
jcost_two_channel_coeff_unique -
def
jcost_two_channel_coeff -
theorem
jcost_two_channel_coeff_spec -
theorem
jcost_two_channel_coeff_iff -
theorem
mass_topology_counts -
theorem
ledger_fraction_eq_29_over_44 -
theorem
ratio_29_over_11k_forces_k_eq_four -
theorem
ledger_fraction_denominator_forced -
theorem
ledger_fraction_denominator_forced_no_hk -
theorem
ledger_fraction_denominator_scale_forced -
theorem
ledger_fraction_denominator_scale_forced_no_hc_pos -
theorem
ledger_fraction_numerator_offset_forced -
theorem
ledger_fraction_weight_split_forced -
theorem
ledger_fraction_kn_forced_under_passive_bound -
theorem
ledger_fraction_kn_forced_under_passive_bound_no_hk -
theorem
base_shift_eq_34_plus_29_over_44 -
theorem
base_shift_wallpaper_multiplier_forced -
theorem
base_shift_denominator_forced -
theorem
base_shift_denominator_forced_no_hk -
theorem
base_shift_denominator_scale_forced_no_hc_pos -
theorem
base_shift_numerator_offset_forced -
theorem
base_shift_weight_split_forced -
theorem
base_shift_kn_forced_under_passive_bound -
theorem
base_shift_kn_forced_under_passive_bound_no_hk -
theorem
radiative_correction_channel_form -
theorem
refined_shift_channel_form -
theorem
radiative_cubic_coeff_forced -
theorem
refined_shift_cubic_coeff_forced -
theorem
refined_shift_full_affine_forced_from_base_role -
theorem
refined_shift_wallpaper_multiplier_forced_from_cubic_scale -
theorem
refined_shift_wallpaper_iff_cubic_from_base_role -
theorem
step_e_mu_channel_split -
theorem
step_e_mu_passive_term_forced -
theorem
step_e_mu_quadratic_scale_forced -
theorem
step_e_mu_invpi_quadratic_forced -
theorem
step_e_mu_invpi_quadratic_forced_no_hk -
theorem
step_e_mu_invpi_denominator_forced_from_quadratic_scale -
theorem
step_e_mu_invpi_denominator_forced_from_quadratic_scale_no_hk -
theorem
step_e_mu_full_mixed_family_forced_from_passive_and_channel -
theorem
step_e_mu_full_mixed_family_forced_from_passive_and_channel_no_hk -
theorem
step_e_mu_full_mixed_family_forced_from_passive_and_quadratic_scale -
theorem
step_e_mu_full_mixed_family_forced_from_passive_and_quadratic_scale_no_hk -
theorem
step_e_mu_denominator_iff_quadratic_scale -
theorem
step_e_mu_invpi_denominator_forced -
theorem
step_e_mu_invpi_denominator_forced_no_hk -
theorem
step_e_mu_denominator_iff_quadratic_scale_no_hk -
theorem
step_e_mu_invpi_scale_forced -
theorem
step_e_mu_invpi_scale_forced_no_hc_pos -
theorem
step_e_mu_full_family_forced_from_passive_term -
theorem
step_e_mu_full_family_forced_from_passive_term_no_hk -
theorem
step_e_mu_full_real_family_forced_from_passive_term -
theorem
step_e_mu_full_real_family_forced_from_passive_term_no_hc_pos -
theorem
step_e_mu_scale_iff_passive_term_no_hc_pos -
theorem
step_e_mu_full_family_forced_from_channel_match -
theorem
step_e_mu_full_family_forced_from_channel_match_no_hk -
theorem
step_mu_tau_linear_coeff_eq_37_over_2 -
theorem
step_mu_tau_channel_split -
theorem
step_mu_tau_face_term_forced -
theorem
step_mu_tau_face_count_forced -
theorem
step_mu_tau_linear_coeff_forced -
theorem
step_mu_tau_full_affine_forced_from_face_term -
theorem
step_mu_tau_coeff_forced_from_six_face_term -
theorem
step_mu_tau_denominator_forced -
theorem
step_mu_tau_scale_forced -
theorem
step_mu_tau_scale_forced_no_hc_pos -
theorem
step_mu_tau_full_real_family_forced_from_face_term_no_hc_pos -
theorem
step_mu_tau_scale_iff_face_count_no_hc_pos -
theorem
lepton_real_scale_iff_bundle_no_hc_pos -
theorem
step_mu_tau_numerator_offset_forced -
theorem
step_mu_tau_kn_forced_under_dim_bound -
theorem
step_mu_tau_kn_forced_under_dim_bound_no_hk -
theorem
step_mu_tau_denominator_iff_numerator_under_dim_bound -
theorem
step_mu_tau_denominator_iff_numerator_under_dim_bound_no_hk -
theorem
lepton_integer_slot_iff_bundle_no_hk -
theorem
step_mu_tau_coeff_iff_kn_under_dim_bound -
theorem
step_mu_tau_coeff_iff_kn_under_dim_bound_no_hk -
theorem
step_mu_tau_full_family_coeff_iff_under_dim_bound -
theorem
step_mu_tau_full_family_coeff_iff_under_dim_bound_no_hk -
theorem
step_mu_tau_coeff_iff_full_forced_under_dim_bound