227 ⟨alphaCoordinateFixationCert⟩ 228 229end 230 231/-! ## Summary 232 233The branch-selection chain now reads: 234 235``` 236RCL family (translation theorem) 237 ↓ branch selection (BranchSelection.lean) 238bilinear α-family with α ≥ 1 239 ↓ second-derivative calibration (constant in α: blind) 240 ↓ fourth-derivative calibration (this module) 241α = 1, hence F = J 242``` 243 244`J` is now the unique calibrated cost on the bilinear branch under the 245combined operator-level encoding plus the higher-derivative calibration. 246The α-coordinate freedom is closed. 247 248The other two §5 candidate fixations (generator calibration, 249action-functional minimisation) remain open as alternative routes for 250separate modules, but the present module gives one Lean-backed route to 251canonical J. 252-/ 253 254end AlphaCoordinateFixation 255end Foundation 256end IndisputableMonolith
depends on (26)
Lean names referenced from this declaration's body.