IndisputableMonolith.Gravity.FreudenthalLengthChainEndpointCert

   1import IndisputableMonolith.Geometry.FreudenthalCubeTriangulation
   2import IndisputableMonolith.Geometry.SchlaefliTetrahedronProof
   3
   4/-!
   5# Freudenthal length-chain Schläfli summand certificates
   6
   7Full `6 × 6` evaluation of `schlaefliPolySummandNorm` at `freudenthalTetSqEdges`, and the
   8induced closed-form `dihedralClosedDerivLength` table for
   9`freudenthalLocalPairClosedFormSchlaefliCoeff`.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Gravity
  14namespace FreudenthalLengthChainEndpointCert
  15
  16open Geometry
  17open CayleyMengerPolynomial
  18open FreudenthalCubeTriangulation
  19open SchlaefliTetrahedronProof
  20
  21set_option maxHeartbeats 20000000
  22
  23/-- Evaluated rationalized Schläfli summand table at `freudenthalTetSqEdges`. -/
  24def freudenthalSchlaefliPolySummandNormTable : Fin 6 → Fin 6 → ℝ
  25  | e, k =>
  26      match e, k with
  27      | 0, 0 => 0
  28      | 0, 1 => 0
  29      | 0, 2 => 0
  30      | 0, 3 => 0
  31      | 0, 4 => -1
  32      | 0, 5 => 2
  33      | 1, 0 => 0
  34      | 1, 1 => 2
  35      | 1, 2 => -2
  36      | 1, 3 => -4
  37      | 1, 4 => 4
  38      | 1, 5 => -2
  39      | 2, 0 => 0
  40      | 2, 1 => -3
  41      | 2, 2 => 2
  42      | 2, 3 => 6
  43      | 2, 4 => -3
  44      | 2, 5 => 0
  45      | 3, 0 => 0
  46      | 3, 1 => -2
  47      | 3, 2 => 2
  48      | 3, 3 => 2
  49      | 3, 4 => -2
  50      | 3, 5 => 0
  51      | 4, 0 => -2
  52      | 4, 1 => 4
  53      | 4, 2 => -2
  54      | 4, 3 => -4
  55      | 4, 4 => 2
  56      | 4, 5 => 0
  57      | 5, 0 => 2
  58      | 5, 1 => -1
  59      | 5, 2 => 0
  60      | 5, 3 => 0
  61      | 5, 4 => 0
  62      | 5, 5 => 0
  63
  64theorem snorm_zero_0_0 :
  65    schlaefliPolySummandNorm freudenthalTetSqEdges 0 0 = 0 := by
  66  rw [schlaefliPolySummandNorm_eq_num_div_den]
  67  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
  68    DihedralCayleyMenger.oppositeCMVertices
  69  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
  70  norm_num
  71
  72theorem snorm_zero_0_1 :
  73    schlaefliPolySummandNorm freudenthalTetSqEdges 0 1 = 0 := by
  74  rw [schlaefliPolySummandNorm_eq_num_div_den]
  75  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
  76    DihedralCayleyMenger.oppositeCMVertices
  77  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
  78  norm_num
  79
  80theorem snorm_zero_0_2 :
  81    schlaefliPolySummandNorm freudenthalTetSqEdges 0 2 = 0 := by
  82  rw [schlaefliPolySummandNorm_eq_num_div_den]
  83  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
  84    DihedralCayleyMenger.oppositeCMVertices
  85  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
  86  norm_num
  87
  88theorem snorm_zero_0_3 :
  89    schlaefliPolySummandNorm freudenthalTetSqEdges 0 3 = 0 := by
  90  rw [schlaefliPolySummandNorm_eq_num_div_den]
  91  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
  92    DihedralCayleyMenger.oppositeCMVertices
  93  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
  94  norm_num
  95
  96theorem snorm_0_4 :
  97    schlaefliPolySummandNorm freudenthalTetSqEdges 0 4 = -1 := by
  98  rw [schlaefliPolySummandNorm_eq_num_div_den]
  99  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 100    DihedralCayleyMenger.oppositeCMVertices
 101  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 102  norm_num
 103
 104theorem snorm_0_5 :
 105    schlaefliPolySummandNorm freudenthalTetSqEdges 0 5 = 2 := by
 106  rw [schlaefliPolySummandNorm_eq_num_div_den]
 107  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 108    DihedralCayleyMenger.oppositeCMVertices
 109  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 110  norm_num
 111
 112theorem snorm_zero_1_0 :
 113    schlaefliPolySummandNorm freudenthalTetSqEdges 1 0 = 0 := by
 114  rw [schlaefliPolySummandNorm_eq_num_div_den]
 115  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 116    DihedralCayleyMenger.oppositeCMVertices
 117  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 118  norm_num
 119
 120theorem snorm_1_1 :
 121    schlaefliPolySummandNorm freudenthalTetSqEdges 1 1 = 2 := by
 122  rw [schlaefliPolySummandNorm_eq_num_div_den]
 123  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 124    DihedralCayleyMenger.oppositeCMVertices
 125  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 126  norm_num
 127
 128theorem snorm_1_2 :
 129    schlaefliPolySummandNorm freudenthalTetSqEdges 1 2 = -2 := by
 130  rw [schlaefliPolySummandNorm_eq_num_div_den]
 131  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 132    DihedralCayleyMenger.oppositeCMVertices
 133  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 134  norm_num
 135
 136theorem snorm_1_3 :
 137    schlaefliPolySummandNorm freudenthalTetSqEdges 1 3 = -4 := by
 138  rw [schlaefliPolySummandNorm_eq_num_div_den]
 139  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 140    DihedralCayleyMenger.oppositeCMVertices
 141  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 142  norm_num
 143
 144theorem snorm_1_4 :
 145    schlaefliPolySummandNorm freudenthalTetSqEdges 1 4 = 4 := by
 146  rw [schlaefliPolySummandNorm_eq_num_div_den]
 147  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 148    DihedralCayleyMenger.oppositeCMVertices
 149  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 150  norm_num
 151
 152theorem snorm_1_5 :
 153    schlaefliPolySummandNorm freudenthalTetSqEdges 1 5 = -2 := by
 154  rw [schlaefliPolySummandNorm_eq_num_div_den]
 155  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 156    DihedralCayleyMenger.oppositeCMVertices
 157  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 158  norm_num
 159
 160theorem snorm_zero_2_0 :
 161    schlaefliPolySummandNorm freudenthalTetSqEdges 2 0 = 0 := by
 162  rw [schlaefliPolySummandNorm_eq_num_div_den]
 163  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 164    DihedralCayleyMenger.oppositeCMVertices
 165  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 166  norm_num
 167
 168theorem snorm_2_1 :
 169    schlaefliPolySummandNorm freudenthalTetSqEdges 2 1 = -3 := by
 170  rw [schlaefliPolySummandNorm_eq_num_div_den]
 171  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 172    DihedralCayleyMenger.oppositeCMVertices
 173  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 174  norm_num
 175
 176theorem snorm_2_2 :
 177    schlaefliPolySummandNorm freudenthalTetSqEdges 2 2 = 2 := by
 178  rw [schlaefliPolySummandNorm_eq_num_div_den]
 179  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 180    DihedralCayleyMenger.oppositeCMVertices
 181  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 182  norm_num
 183
 184theorem snorm_2_3 :
 185    schlaefliPolySummandNorm freudenthalTetSqEdges 2 3 = 6 := by
 186  rw [schlaefliPolySummandNorm_eq_num_div_den]
 187  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 188    DihedralCayleyMenger.oppositeCMVertices
 189  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 190  norm_num
 191
 192theorem snorm_2_4 :
 193    schlaefliPolySummandNorm freudenthalTetSqEdges 2 4 = -3 := by
 194  rw [schlaefliPolySummandNorm_eq_num_div_den]
 195  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 196    DihedralCayleyMenger.oppositeCMVertices
 197  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 198  norm_num
 199
 200theorem snorm_zero_2_5 :
 201    schlaefliPolySummandNorm freudenthalTetSqEdges 2 5 = 0 := by
 202  rw [schlaefliPolySummandNorm_eq_num_div_den]
 203  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 204    DihedralCayleyMenger.oppositeCMVertices
 205  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 206  norm_num
 207
 208theorem snorm_zero_3_0 :
 209    schlaefliPolySummandNorm freudenthalTetSqEdges 3 0 = 0 := by
 210  rw [schlaefliPolySummandNorm_eq_num_div_den]
 211  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 212    DihedralCayleyMenger.oppositeCMVertices
 213  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 214  norm_num
 215
 216theorem snorm_3_1 :
 217    schlaefliPolySummandNorm freudenthalTetSqEdges 3 1 = -2 := by
 218  rw [schlaefliPolySummandNorm_eq_num_div_den]
 219  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 220    DihedralCayleyMenger.oppositeCMVertices
 221  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 222  norm_num
 223
 224theorem snorm_3_2 :
 225    schlaefliPolySummandNorm freudenthalTetSqEdges 3 2 = 2 := by
 226  rw [schlaefliPolySummandNorm_eq_num_div_den]
 227  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 228    DihedralCayleyMenger.oppositeCMVertices
 229  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 230  norm_num
 231
 232theorem snorm_3_3 :
 233    schlaefliPolySummandNorm freudenthalTetSqEdges 3 3 = 2 := by
 234  rw [schlaefliPolySummandNorm_eq_num_div_den]
 235  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 236    DihedralCayleyMenger.oppositeCMVertices
 237  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 238  norm_num
 239
 240theorem snorm_3_4 :
 241    schlaefliPolySummandNorm freudenthalTetSqEdges 3 4 = -2 := by
 242  rw [schlaefliPolySummandNorm_eq_num_div_den]
 243  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 244    DihedralCayleyMenger.oppositeCMVertices
 245  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 246  norm_num
 247
 248theorem snorm_zero_3_5 :
 249    schlaefliPolySummandNorm freudenthalTetSqEdges 3 5 = 0 := by
 250  rw [schlaefliPolySummandNorm_eq_num_div_den]
 251  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 252    DihedralCayleyMenger.oppositeCMVertices
 253  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 254  norm_num
 255
 256theorem snorm_4_0 :
 257    schlaefliPolySummandNorm freudenthalTetSqEdges 4 0 = -2 := by
 258  rw [schlaefliPolySummandNorm_eq_num_div_den]
 259  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 260    DihedralCayleyMenger.oppositeCMVertices
 261  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 262  norm_num
 263
 264theorem snorm_4_1 :
 265    schlaefliPolySummandNorm freudenthalTetSqEdges 4 1 = 4 := by
 266  rw [schlaefliPolySummandNorm_eq_num_div_den]
 267  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 268    DihedralCayleyMenger.oppositeCMVertices
 269  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 270  norm_num
 271
 272theorem snorm_4_2 :
 273    schlaefliPolySummandNorm freudenthalTetSqEdges 4 2 = -2 := by
 274  rw [schlaefliPolySummandNorm_eq_num_div_den]
 275  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 276    DihedralCayleyMenger.oppositeCMVertices
 277  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 278  norm_num
 279
 280theorem snorm_4_3 :
 281    schlaefliPolySummandNorm freudenthalTetSqEdges 4 3 = -4 := by
 282  rw [schlaefliPolySummandNorm_eq_num_div_den]
 283  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 284    DihedralCayleyMenger.oppositeCMVertices
 285  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 286  norm_num
 287
 288theorem snorm_4_4 :
 289    schlaefliPolySummandNorm freudenthalTetSqEdges 4 4 = 2 := by
 290  rw [schlaefliPolySummandNorm_eq_num_div_den]
 291  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 292    DihedralCayleyMenger.oppositeCMVertices
 293  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 294  norm_num
 295
 296theorem snorm_zero_4_5 :
 297    schlaefliPolySummandNorm freudenthalTetSqEdges 4 5 = 0 := by
 298  rw [schlaefliPolySummandNorm_eq_num_div_den]
 299  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 300    DihedralCayleyMenger.oppositeCMVertices
 301  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 302  norm_num
 303
 304theorem snorm_5_0 :
 305    schlaefliPolySummandNorm freudenthalTetSqEdges 5 0 = 2 := by
 306  rw [schlaefliPolySummandNorm_eq_num_div_den]
 307  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 308    DihedralCayleyMenger.oppositeCMVertices
 309  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 310  norm_num
 311
 312theorem snorm_5_1 :
 313    schlaefliPolySummandNorm freudenthalTetSqEdges 5 1 = -1 := by
 314  rw [schlaefliPolySummandNorm_eq_num_div_den]
 315  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 316    DihedralCayleyMenger.oppositeCMVertices
 317  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 318  norm_num
 319
 320theorem snorm_zero_5_2 :
 321    schlaefliPolySummandNorm freudenthalTetSqEdges 5 2 = 0 := by
 322  rw [schlaefliPolySummandNorm_eq_num_div_den]
 323  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 324    DihedralCayleyMenger.oppositeCMVertices
 325  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 326  norm_num
 327
 328theorem snorm_zero_5_3 :
 329    schlaefliPolySummandNorm freudenthalTetSqEdges 5 3 = 0 := by
 330  rw [schlaefliPolySummandNorm_eq_num_div_den]
 331  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 332    DihedralCayleyMenger.oppositeCMVertices
 333  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 334  norm_num
 335
 336theorem snorm_zero_5_4 :
 337    schlaefliPolySummandNorm freudenthalTetSqEdges 5 4 = 0 := by
 338  rw [schlaefliPolySummandNorm_eq_num_div_den]
 339  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 340    DihedralCayleyMenger.oppositeCMVertices
 341  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 342  norm_num
 343
 344theorem snorm_zero_5_5 :
 345    schlaefliPolySummandNorm freudenthalTetSqEdges 5 5 = 0 := by
 346  rw [schlaefliPolySummandNorm_eq_num_div_den]
 347  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
 348    DihedralCayleyMenger.oppositeCMVertices
 349  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
 350  norm_num
 351
 352/-- The lookup table matches the evaluated rationalized Schläfli summands. -/
 353theorem freudenthalSchlaefliPolySummandNorm_eq_table (e k : Fin 6) :
 354    schlaefliPolySummandNorm freudenthalTetSqEdges e k =
 355      freudenthalSchlaefliPolySummandNormTable e k := by
 356  match e, k with
 357  | 0, 0 => exact snorm_zero_0_0
 358  | 0, 1 => exact snorm_zero_0_1
 359  | 0, 2 => exact snorm_zero_0_2
 360  | 0, 3 => exact snorm_zero_0_3
 361  | 0, 4 => exact snorm_0_4
 362  | 0, 5 => exact snorm_0_5
 363  | 1, 0 => exact snorm_zero_1_0
 364  | 1, 1 => exact snorm_1_1
 365  | 1, 2 => exact snorm_1_2
 366  | 1, 3 => exact snorm_1_3
 367  | 1, 4 => exact snorm_1_4
 368  | 1, 5 => exact snorm_1_5
 369  | 2, 0 => exact snorm_zero_2_0
 370  | 2, 1 => exact snorm_2_1
 371  | 2, 2 => exact snorm_2_2
 372  | 2, 3 => exact snorm_2_3
 373  | 2, 4 => exact snorm_2_4
 374  | 2, 5 => exact snorm_zero_2_5
 375  | 3, 0 => exact snorm_zero_3_0
 376  | 3, 1 => exact snorm_3_1
 377  | 3, 2 => exact snorm_3_2
 378  | 3, 3 => exact snorm_3_3
 379  | 3, 4 => exact snorm_3_4
 380  | 3, 5 => exact snorm_zero_3_5
 381  | 4, 0 => exact snorm_4_0
 382  | 4, 1 => exact snorm_4_1
 383  | 4, 2 => exact snorm_4_2
 384  | 4, 3 => exact snorm_4_3
 385  | 4, 4 => exact snorm_4_4
 386  | 4, 5 => exact snorm_zero_4_5
 387  | 5, 0 => exact snorm_5_0
 388  | 5, 1 => exact snorm_5_1
 389  | 5, 2 => exact snorm_zero_5_2
 390  | 5, 3 => exact snorm_zero_5_3
 391  | 5, 4 => exact snorm_zero_5_4
 392  | 5, 5 => exact snorm_zero_5_5
 393
 394/-- Closed-form edge-length derivative from the evaluated rationalized summand. -/
 395theorem freudenthalDihedralClosedDerivLength_snorm (e k : Fin 6) :
 396    dihedralClosedDerivLength freudenthalTet e k =
 397      schlaefliPolySummandNorm freudenthalTetSqEdges e k *
 398        Real.sqrt (freudenthalTetSqEdges k) / (2 * Real.sqrt (freudenthalTetSqEdges e)) := by
 399  unfold dihedralClosedDerivLength
 400  rw [dihedralClosedDerivSq_eq_poly]
 401  have hsq : freudenthalTet.sqEdge = freudenthalTetSqEdges := by
 402    simp [freudenthalTet]
 403  have hbridge := schlaefliSummandBridge freudenthalTet e k
 404  have hcm : Real.sqrt (2 * cm3 freudenthalTetSqEdges) = 4 := by
 405    rw [cm3_freudenthalTetSqEdges]
 406    norm_num
 407  have hse_ne : Real.sqrt (freudenthalTetSqEdges e) ≠ 0 :=
 408    ne_of_gt (Real.sqrt_pos.mpr (freudenthalTet.sqEdge_pos e))
 409  have hinv :
 410      (1 / Real.sqrt (2 * cm3 freudenthalTetSqEdges)) = 1 / 4 := by
 411    rw [hcm]
 412  have hd_sq :
 413      dihedralClosedDerivSqPoly freudenthalTet e k =
 414        schlaefliPolySummandNorm freudenthalTetSqEdges e k /
 415          (4 * Real.sqrt (freudenthalTetSqEdges e)) := by
 416    simp only [hsq] at hbridge
 417    rw [hinv] at hbridge
 418    have hden_ne : 4 * Real.sqrt (freudenthalTetSqEdges e) ≠ 0 :=
 419      mul_ne_zero (by norm_num : (4 : ℝ) ≠ 0) hse_ne
 420    rw [eq_div_iff hden_ne]
 421    linarith
 422  calc
 423    2 * Real.sqrt (freudenthalTet.sqEdge k) * dihedralClosedDerivSqPoly freudenthalTet e k
 424        = 2 * Real.sqrt (freudenthalTetSqEdges k) * dihedralClosedDerivSqPoly freudenthalTet e k := by
 425            rw [hsq]
 426    _ = 2 * Real.sqrt (freudenthalTetSqEdges k) *
 427            (schlaefliPolySummandNorm freudenthalTetSqEdges e k /
 428              (4 * Real.sqrt (freudenthalTetSqEdges e))) := by
 429            rw [hd_sq]
 430    _ = schlaefliPolySummandNorm freudenthalTetSqEdges e k *
 431          Real.sqrt (freudenthalTetSqEdges k) / (2 * Real.sqrt (freudenthalTetSqEdges e)) := by
 432          field_simp [hse_ne]
 433          ring
 434
 435end FreudenthalLengthChainEndpointCert
 436end Gravity
 437end IndisputableMonolith
 438