refined_shift_full_affine_forced_from_base_role
plain-language theorem explainer
If the base shift takes the affine form uW plus ledger fraction and the refined shift matches that form plus the quadratic-cubic term in alpha, then the multiplier u equals 2 and the cubic coefficient c equals 12. Mass-layer modelers in Recognition Science cite this result to fix the perturbative coefficients that close the O4 J-cost expansion. The proof first extracts u from the base-shift hypothesis via the wallpaper-multiplier lemma, rewrites the refined shift as base shift plus the cubic channel, and then applies the cubic-coefficient lemma
Claim. If the base shift satisfies $base_shift = u W + ledger_fraction$ and the refined shift satisfies $refined_shift = u W + ledger_fraction + (α^2 + c α^3)$, then $u = 2$ and $c = 12$.
background
The module supplies the Lean closure for the O4 perturbative channel in the mass layer. It encodes the J-cost expansion around the unit argument as a two-channel form whose first correction is quadratic in the fine-structure constant alpha and whose next term is cubic. The symbols W and ledger_fraction are the anchor weight and the fractional ledger contribution taken from the simplicial ledger and magnitude-of-mismatch structures. Alpha is the fine-structure constant imported from Constants.Alpha.
proof idea
Apply base_shift_wallpaper_multiplier_forced to the first hypothesis to obtain u = 2. Rewrite the second hypothesis by substituting the base-shift expression, yielding refined_shift = base_shift + (α² + c α³). Then invoke refined_shift_cubic_coeff_forced on this rewritten equality to force c = 12. The final step packages the two equalities.
why it matters
The result supplies the joint affine forcing that feeds the downstream equivalence refined_shift_wallpaper_iff_cubic_from_base_role, which states u = 2 ↔ c = 12. It thereby closes the explicit α² + 12α³ decomposition required by the O4 coefficient-forcing package in the J-cost perturbation bridge. The constants alpha and the ledger fraction sit inside the Recognition forcing chain that already fixes D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.