Large Signal Model · Lean source
PerturbedOperatorFixture.lean
Declared contract recorded Coverage and evidence
The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (1)
KomorebiLSM/PerturbedOperatorFixture.lean327 lines
Original source path
Lean/KomorebiLSM/PerturbedOperatorFixture.leanSkip declarations and read code
1 import KomorebiLSM.RationalLorentzMatrix
2
3 /-! Literal rational Section88 fixtures. The nominal arrays are tied to the declared perturb-and-reset recipe. -/
4 set_option autoImplicit false
5 set_option maxHeartbeats 1200000
6 set_option maxRecDepth 4000
7 namespace Komorebi.LSM.PerturbedOperatorFixture
8 open scoped BigOperators
9 open RationalBernsteinMargin LorentzCylinder RationalLorentzMatrix
10 noncomputable section
11
12 def proposedTransform : RationalMatrix := (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix)
13
14 def proposedInverse : RationalMatrix := (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
15
16 def comparisonTransform : RationalMatrix := (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix)
17
18 def comparisonInverse : RationalMatrix := (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
19
20 def physicalReset : RationalMatrix := (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix)
21
22 def errorCoefficient : Fin 3 → RationalMatrix := (fun k => match k.val with | 0 => (![![(0/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-1/1 : ℚ),(2/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/1 : ℚ),(-1/1 : ℚ)]] : RationalMatrix) | 1 => (![![(0/1 : ℚ),(1/1 : ℚ),(-1/1 : ℚ)],![(1/1 : ℚ),(0/1 : ℚ),(1/1 : ℚ)],![(1/1 : ℚ),(-1/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix) | _ => (![![(0/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(-1/1 : ℚ),(1/1 : ℚ)],![(1/1 : ℚ),(0/1 : ℚ),(1/1 : ℚ)]] : RationalMatrix))
23
24 def referenceOriginal (a : Bool) : Fin 3 → RationalMatrix :=
25 if a then (fun k => match k.val with | 0 => (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(1/4 : ℚ)],![(1/10 : ℚ),(-1/4 : ℚ),(3/10 : ℚ)]] : RationalMatrix) | 1 => (![![(-2/1 : ℚ),(0/1 : ℚ),(4/1 : ℚ)],![(-7/16 : ℚ),(0/1 : ℚ),(2/1 : ℚ)],![(-53/80 : ℚ),(0/1 : ℚ),(2/1 : ℚ)]] : RationalMatrix) | _ => (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(9/4 : ℚ)],![(0/1 : ℚ),(9/4 : ℚ),(0/1 : ℚ)]] : RationalMatrix))
26 else (fun k => match k.val with | 0 => (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/4 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(1/4 : ℚ)]] : RationalMatrix) | 1 => (![![(-2/1 : ℚ),(4/1 : ℚ),(0/1 : ℚ)],![(-7/16 : ℚ),(2/1 : ℚ),(0/1 : ℚ)],![(-53/80 : ℚ),(2/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix) | _ => (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(9/4 : ℚ),(0/1 : ℚ)],![(9/10 : ℚ),(27/10 : ℚ),(-9/4 : ℚ)]] : RationalMatrix))
27
28 def fittedOriginal (a : Bool) : Fin 3 → RationalMatrix :=
29 if a then (fun k => match k.val with | 0 => (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2000 : ℚ),(-1/1000 : ℚ),(1/4 : ℚ)],![(1/10 : ℚ),(-501/2000 : ℚ),(601/2000 : ℚ)]] : RationalMatrix) | 1 => (![![(-2/1 : ℚ),(-1/2000 : ℚ),(8001/2000 : ℚ)],![(-219/500 : ℚ),(0/1 : ℚ),(3999/2000 : ℚ)],![(-663/1000 : ℚ),(1/2000 : ℚ),(2/1 : ℚ)]] : RationalMatrix) | _ => (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/2000 : ℚ),(4499/2000 : ℚ)],![(-1/2000 : ℚ),(9/4 : ℚ),(-1/2000 : ℚ)]] : RationalMatrix))
30 else (fun k => match k.val with | 0 => (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-1/2000 : ℚ),(251/1000 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/2000 : ℚ),(499/2000 : ℚ)]] : RationalMatrix) | 1 => (![![(-2/1 : ℚ),(8001/2000 : ℚ),(-1/2000 : ℚ)],![(-437/1000 : ℚ),(2/1 : ℚ),(1/2000 : ℚ)],![(-331/500 : ℚ),(3999/2000 : ℚ),(0/1 : ℚ)]] : RationalMatrix) | _ => (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(4499/2000 : ℚ),(1/2000 : ℚ)],![(1801/2000 : ℚ),(27/10 : ℚ),(-4499/2000 : ℚ)]] : RationalMatrix))
31
32 def correctedOriginal (a : Bool) : Fin 3 → RationalMatrix :=
33 if a then (fun k => match k.val with | 0 => (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1007/16000 : ℚ),(-7/8000 : ℚ),(7/32 : ℚ)],![(3/20 : ℚ),(-3507/16000 : ℚ),(4207/16000 : ℚ)]] : RationalMatrix) | 1 => (![![(-7/4 : ℚ),(-7/16000 : ℚ),(56007/16000 : ℚ)],![(-1533/4000 : ℚ),(0/1 : ℚ),(27993/16000 : ℚ)],![(-4641/8000 : ℚ),(7/16000 : ℚ),(7/4 : ℚ)]] : RationalMatrix) | _ => (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(7/16000 : ℚ),(31493/16000 : ℚ)],![(-7/16000 : ℚ),(63/32 : ℚ),(-7/16000 : ℚ)]] : RationalMatrix))
34 else (fun k => match k.val with | 0 => (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(993/16000 : ℚ),(1757/8000 : ℚ),(0/1 : ℚ)],![(1/16 : ℚ),(7/16000 : ℚ),(3493/16000 : ℚ)]] : RationalMatrix) | 1 => (![![(-7/4 : ℚ),(56007/16000 : ℚ),(-7/16000 : ℚ)],![(-3059/8000 : ℚ),(7/4 : ℚ),(7/16000 : ℚ)],![(-2317/4000 : ℚ),(27993/16000 : ℚ),(0/1 : ℚ)]] : RationalMatrix) | _ => (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(31493/16000 : ℚ),(7/16000 : ℚ)],![(12607/16000 : ℚ),(189/80 : ℚ),(-31493/16000 : ℚ)]] : RationalMatrix))
35
36 def referenceComparison (a : Bool) : Fin 3 → RationalMatrix :=
37 if a then (fun k => match k.val with | 0 => (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(3/20 : ℚ),(1/5 : ℚ)],![(0/1 : ℚ),(-1/5 : ℚ),(3/20 : ℚ)]] : RationalMatrix) | 1 => (![![(0/1 : ℚ),(0/1 : ℚ),(3/2 : ℚ)],![(6/5 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(9/10 : ℚ),(0/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix) | _ => (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(-27/20 : ℚ),(9/5 : ℚ)],![(0/1 : ℚ),(9/5 : ℚ),(27/20 : ℚ)]] : RationalMatrix))
38 else (fun k => match k.val with | 0 => (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/4 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(1/4 : ℚ)]] : RationalMatrix) | 1 => (![![(0/1 : ℚ),(6/5 : ℚ),(9/10 : ℚ)],![(6/5 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(9/10 : ℚ),(0/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix) | _ => (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(63/100 : ℚ),(54/25 : ℚ)],![(0/1 : ℚ),(54/25 : ℚ),(-63/100 : ℚ)]] : RationalMatrix))
39
40 def rawComparison (a : Bool) : Fin 3 → RationalMatrix :=
41 if a then (fun k => match k.val with | 0 => (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1493/10000 : ℚ),(1991/10000 : ℚ)],![(0/1 : ℚ),(-501/2500 : ℚ),(751/5000 : ℚ)]] : RationalMatrix) | 1 => (![![(0/1 : ℚ),(-3/20000 : ℚ),(60003/40000 : ℚ)],![(599/500 : ℚ),(-1/5000 : ℚ),(-9/10000 : ℚ)],![(1349/1500 : ℚ),(3/5000 : ℚ),(1/5000 : ℚ)]] : RationalMatrix) | _ => (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(3/2000 : ℚ),(-2699/2000 : ℚ),(14401/8000 : ℚ)],![(-1/500 : ℚ),(9/5 : ℚ),(2699/2000 : ℚ)]] : RationalMatrix))
42 else (fun k => match k.val with | 0 => (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(2507/10000 : ℚ),(9/10000 : ℚ)],![(0/1 : ℚ),(1/2500 : ℚ),(1249/5000 : ℚ)]] : RationalMatrix) | 1 => (![![(0/1 : ℚ),(24003/20000 : ℚ),(35997/40000 : ℚ)],![(601/500 : ℚ),(1/5000 : ℚ),(9/10000 : ℚ)],![(1351/1500 : ℚ),(-3/5000 : ℚ),(-1/5000 : ℚ)]] : RationalMatrix) | _ => (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-3/2000 : ℚ),(1259/2000 : ℚ),(17279/8000 : ℚ)],![(1/500 : ℚ),(54/25 : ℚ),(-1259/2000 : ℚ)]] : RationalMatrix))
43
44 def rawProposed (a : Bool) : Fin 3 → RationalMatrix :=
45 if a then (fun k => match k.val with | 0 => (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(3069/20500 : ℚ),(160649/806600 : ℚ)],![(0/1 : ℚ),(-673511/3362000 : ℚ),(12283/82000 : ℚ)]] : RationalMatrix) | 1 => (![![(0/1 : ℚ),(-37/246000 : ℚ),(984049/654000 : ℚ)],![(35311/29600 : ℚ),(-33/164000 : ℚ),(-14537/16132000 : ℚ)],![(147041/164000 : ℚ),(4033/6724000 : ℚ),(33/164000 : ℚ)]] : RationalMatrix) | _ => (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(3/2000 : ℚ),(-110959/82000 : ℚ),(579221/322640 : ℚ)],![(-327/164000 : ℚ),(12099/6724 : ℚ),(110959/82000 : ℚ)]] : RationalMatrix))
46 else (fun k => match k.val with | 0 => (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(7709/30750 : ℚ),(59/65400 : ℚ)],![(0/1 : ℚ),(4033/10086000 : ℚ),(61451/246000 : ℚ)]] : RationalMatrix) | 1 => (![![(0/1 : ℚ),(98679/82000 : ℚ),(197317/218000 : ℚ)],![(35429/29600 : ℚ),(33/164000 : ℚ),(14537/16132000 : ℚ)],![(147259/164000 : ℚ),(-4033/6724000 : ℚ),(-33/164000 : ℚ)]] : RationalMatrix) | _ => (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-3/2000 : ℚ),(51259/82000 : ℚ),(6403/2960 : ℚ)],![(327/164000 : ℚ),(36297/16810 : ℚ),(-51259/82000 : ℚ)]] : RationalMatrix))
47
48 def nominalComparison (a : Bool) : Fin 3 → RationalMatrix :=
49 if a then (fun k => match k.val with | 0 => (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(10451/80000 : ℚ),(13937/80000 : ℚ)],![(0/1 : ℚ),(-3507/20000 : ℚ),(5257/40000 : ℚ)]] : RationalMatrix) | 1 => (![![(0/1 : ℚ),(-21/160000 : ℚ),(420021/320000 : ℚ)],![(4193/4000 : ℚ),(-7/40000 : ℚ),(-63/80000 : ℚ)],![(9443/12000 : ℚ),(21/40000 : ℚ),(7/40000 : ℚ)]] : RationalMatrix) | _ => (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(21/16000 : ℚ),(-18893/16000 : ℚ),(100807/64000 : ℚ)],![(-7/4000 : ℚ),(63/40 : ℚ),(18893/16000 : ℚ)]] : RationalMatrix))
50 else (fun k => match k.val with | 0 => (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(17549/80000 : ℚ),(63/80000 : ℚ)],![(0/1 : ℚ),(7/20000 : ℚ),(8743/40000 : ℚ)]] : RationalMatrix) | 1 => (![![(0/1 : ℚ),(168021/160000 : ℚ),(251979/320000 : ℚ)],![(4207/4000 : ℚ),(7/40000 : ℚ),(63/80000 : ℚ)],![(9457/12000 : ℚ),(-21/40000 : ℚ),(-7/40000 : ℚ)]] : RationalMatrix) | _ => (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-21/16000 : ℚ),(8813/16000 : ℚ),(120953/64000 : ℚ)],![(7/4000 : ℚ),(189/100 : ℚ),(-8813/16000 : ℚ)]] : RationalMatrix))
51
52 def nominalProposed (a : Bool) : Fin 3 → RationalMatrix :=
53 if a then (fun k => match k.val with | 0 => (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(21483/164000 : ℚ),(1124543/6452800 : ℚ)],![(0/1 : ℚ),(-4714577/26896000 : ℚ),(85981/656000 : ℚ)]] : RationalMatrix) | 1 => (![![(0/1 : ℚ),(-259/1968000 : ℚ),(6888343/5232000 : ℚ)],![(247177/236800 : ℚ),(-231/1312000 : ℚ),(-101759/129056000 : ℚ)],![(1029287/1312000 : ℚ),(28231/53792000 : ℚ),(231/1312000 : ℚ)]] : RationalMatrix) | _ => (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(21/16000 : ℚ),(-776713/656000 : ℚ),(4054547/2581120 : ℚ)],![(-2289/1312000 : ℚ),(84693/53792 : ℚ),(776713/656000 : ℚ)]] : RationalMatrix))
54 else (fun k => match k.val with | 0 => (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(53963/246000 : ℚ),(413/523200 : ℚ)],![(0/1 : ℚ),(28231/80688000 : ℚ),(430157/1968000 : ℚ)]] : RationalMatrix) | 1 => (![![(0/1 : ℚ),(690753/656000 : ℚ),(1381219/1744000 : ℚ)],![(248003/236800 : ℚ),(231/1312000 : ℚ),(101759/129056000 : ℚ)],![(1030813/1312000 : ℚ),(-28231/53792000 : ℚ),(-231/1312000 : ℚ)]] : RationalMatrix) | _ => (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-21/16000 : ℚ),(358813/656000 : ℚ),(44821/23680 : ℚ)],![(2289/1312000 : ℚ),(254079/134480 : ℚ),(-358813/656000 : ℚ)]] : RationalMatrix))
55
56 @[simp] theorem referenceOriginal_false_0 : referenceOriginal false 0=(![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/4 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(1/4 : ℚ)]] : RationalMatrix) := rfl
57 @[simp] theorem referenceOriginal_false_1 : referenceOriginal false 1=(![![(-2/1 : ℚ),(4/1 : ℚ),(0/1 : ℚ)],![(-7/16 : ℚ),(2/1 : ℚ),(0/1 : ℚ)],![(-53/80 : ℚ),(2/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix) := rfl
58 @[simp] theorem referenceOriginal_false_2 : referenceOriginal false 2=(![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(9/4 : ℚ),(0/1 : ℚ)],![(9/10 : ℚ),(27/10 : ℚ),(-9/4 : ℚ)]] : RationalMatrix) := rfl
59 @[simp] theorem referenceOriginal_true_0 : referenceOriginal true 0=(![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(1/4 : ℚ)],![(1/10 : ℚ),(-1/4 : ℚ),(3/10 : ℚ)]] : RationalMatrix) := rfl
60 @[simp] theorem referenceOriginal_true_1 : referenceOriginal true 1=(![![(-2/1 : ℚ),(0/1 : ℚ),(4/1 : ℚ)],![(-7/16 : ℚ),(0/1 : ℚ),(2/1 : ℚ)],![(-53/80 : ℚ),(0/1 : ℚ),(2/1 : ℚ)]] : RationalMatrix) := rfl
61 @[simp] theorem referenceOriginal_true_2 : referenceOriginal true 2=(![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(9/4 : ℚ)],![(0/1 : ℚ),(9/4 : ℚ),(0/1 : ℚ)]] : RationalMatrix) := rfl
62 @[simp] theorem fittedOriginal_false_0 : fittedOriginal false 0=(![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-1/2000 : ℚ),(251/1000 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/2000 : ℚ),(499/2000 : ℚ)]] : RationalMatrix) := rfl
63 @[simp] theorem fittedOriginal_false_1 : fittedOriginal false 1=(![![(-2/1 : ℚ),(8001/2000 : ℚ),(-1/2000 : ℚ)],![(-437/1000 : ℚ),(2/1 : ℚ),(1/2000 : ℚ)],![(-331/500 : ℚ),(3999/2000 : ℚ),(0/1 : ℚ)]] : RationalMatrix) := rfl
64 @[simp] theorem fittedOriginal_false_2 : fittedOriginal false 2=(![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(4499/2000 : ℚ),(1/2000 : ℚ)],![(1801/2000 : ℚ),(27/10 : ℚ),(-4499/2000 : ℚ)]] : RationalMatrix) := rfl
65 @[simp] theorem fittedOriginal_true_0 : fittedOriginal true 0=(![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2000 : ℚ),(-1/1000 : ℚ),(1/4 : ℚ)],![(1/10 : ℚ),(-501/2000 : ℚ),(601/2000 : ℚ)]] : RationalMatrix) := rfl
66 @[simp] theorem fittedOriginal_true_1 : fittedOriginal true 1=(![![(-2/1 : ℚ),(-1/2000 : ℚ),(8001/2000 : ℚ)],![(-219/500 : ℚ),(0/1 : ℚ),(3999/2000 : ℚ)],![(-663/1000 : ℚ),(1/2000 : ℚ),(2/1 : ℚ)]] : RationalMatrix) := rfl
67 @[simp] theorem fittedOriginal_true_2 : fittedOriginal true 2=(![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/2000 : ℚ),(4499/2000 : ℚ)],![(-1/2000 : ℚ),(9/4 : ℚ),(-1/2000 : ℚ)]] : RationalMatrix) := rfl
68 @[simp] theorem correctedOriginal_false_0 : correctedOriginal false 0=(![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(993/16000 : ℚ),(1757/8000 : ℚ),(0/1 : ℚ)],![(1/16 : ℚ),(7/16000 : ℚ),(3493/16000 : ℚ)]] : RationalMatrix) := rfl
69 @[simp] theorem correctedOriginal_false_1 : correctedOriginal false 1=(![![(-7/4 : ℚ),(56007/16000 : ℚ),(-7/16000 : ℚ)],![(-3059/8000 : ℚ),(7/4 : ℚ),(7/16000 : ℚ)],![(-2317/4000 : ℚ),(27993/16000 : ℚ),(0/1 : ℚ)]] : RationalMatrix) := rfl
70 @[simp] theorem correctedOriginal_false_2 : correctedOriginal false 2=(![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(31493/16000 : ℚ),(7/16000 : ℚ)],![(12607/16000 : ℚ),(189/80 : ℚ),(-31493/16000 : ℚ)]] : RationalMatrix) := rfl
71 @[simp] theorem correctedOriginal_true_0 : correctedOriginal true 0=(![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1007/16000 : ℚ),(-7/8000 : ℚ),(7/32 : ℚ)],![(3/20 : ℚ),(-3507/16000 : ℚ),(4207/16000 : ℚ)]] : RationalMatrix) := rfl
72 @[simp] theorem correctedOriginal_true_1 : correctedOriginal true 1=(![![(-7/4 : ℚ),(-7/16000 : ℚ),(56007/16000 : ℚ)],![(-1533/4000 : ℚ),(0/1 : ℚ),(27993/16000 : ℚ)],![(-4641/8000 : ℚ),(7/16000 : ℚ),(7/4 : ℚ)]] : RationalMatrix) := rfl
73 @[simp] theorem correctedOriginal_true_2 : correctedOriginal true 2=(![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(7/16000 : ℚ),(31493/16000 : ℚ)],![(-7/16000 : ℚ),(63/32 : ℚ),(-7/16000 : ℚ)]] : RationalMatrix) := rfl
74 @[simp] theorem referenceComparison_false_0 : referenceComparison false 0=(![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/4 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(1/4 : ℚ)]] : RationalMatrix) := rfl
75 @[simp] theorem referenceComparison_false_1 : referenceComparison false 1=(![![(0/1 : ℚ),(6/5 : ℚ),(9/10 : ℚ)],![(6/5 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(9/10 : ℚ),(0/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix) := rfl
76 @[simp] theorem referenceComparison_false_2 : referenceComparison false 2=(![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(63/100 : ℚ),(54/25 : ℚ)],![(0/1 : ℚ),(54/25 : ℚ),(-63/100 : ℚ)]] : RationalMatrix) := rfl
77 @[simp] theorem referenceComparison_true_0 : referenceComparison true 0=(![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(3/20 : ℚ),(1/5 : ℚ)],![(0/1 : ℚ),(-1/5 : ℚ),(3/20 : ℚ)]] : RationalMatrix) := rfl
78 @[simp] theorem referenceComparison_true_1 : referenceComparison true 1=(![![(0/1 : ℚ),(0/1 : ℚ),(3/2 : ℚ)],![(6/5 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(9/10 : ℚ),(0/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix) := rfl
79 @[simp] theorem referenceComparison_true_2 : referenceComparison true 2=(![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(-27/20 : ℚ),(9/5 : ℚ)],![(0/1 : ℚ),(9/5 : ℚ),(27/20 : ℚ)]] : RationalMatrix) := rfl
80 @[simp] theorem rawComparison_false_0 : rawComparison false 0=(![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(2507/10000 : ℚ),(9/10000 : ℚ)],![(0/1 : ℚ),(1/2500 : ℚ),(1249/5000 : ℚ)]] : RationalMatrix) := rfl
81 @[simp] theorem rawComparison_false_1 : rawComparison false 1=(![![(0/1 : ℚ),(24003/20000 : ℚ),(35997/40000 : ℚ)],![(601/500 : ℚ),(1/5000 : ℚ),(9/10000 : ℚ)],![(1351/1500 : ℚ),(-3/5000 : ℚ),(-1/5000 : ℚ)]] : RationalMatrix) := rfl
82 @[simp] theorem rawComparison_false_2 : rawComparison false 2=(![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-3/2000 : ℚ),(1259/2000 : ℚ),(17279/8000 : ℚ)],![(1/500 : ℚ),(54/25 : ℚ),(-1259/2000 : ℚ)]] : RationalMatrix) := rfl
83 @[simp] theorem rawComparison_true_0 : rawComparison true 0=(![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1493/10000 : ℚ),(1991/10000 : ℚ)],![(0/1 : ℚ),(-501/2500 : ℚ),(751/5000 : ℚ)]] : RationalMatrix) := rfl
84 @[simp] theorem rawComparison_true_1 : rawComparison true 1=(![![(0/1 : ℚ),(-3/20000 : ℚ),(60003/40000 : ℚ)],![(599/500 : ℚ),(-1/5000 : ℚ),(-9/10000 : ℚ)],![(1349/1500 : ℚ),(3/5000 : ℚ),(1/5000 : ℚ)]] : RationalMatrix) := rfl
85 @[simp] theorem rawComparison_true_2 : rawComparison true 2=(![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(3/2000 : ℚ),(-2699/2000 : ℚ),(14401/8000 : ℚ)],![(-1/500 : ℚ),(9/5 : ℚ),(2699/2000 : ℚ)]] : RationalMatrix) := rfl
86 @[simp] theorem rawProposed_false_0 : rawProposed false 0=(![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(7709/30750 : ℚ),(59/65400 : ℚ)],![(0/1 : ℚ),(4033/10086000 : ℚ),(61451/246000 : ℚ)]] : RationalMatrix) := rfl
87 @[simp] theorem rawProposed_false_1 : rawProposed false 1=(![![(0/1 : ℚ),(98679/82000 : ℚ),(197317/218000 : ℚ)],![(35429/29600 : ℚ),(33/164000 : ℚ),(14537/16132000 : ℚ)],![(147259/164000 : ℚ),(-4033/6724000 : ℚ),(-33/164000 : ℚ)]] : RationalMatrix) := rfl
88 @[simp] theorem rawProposed_false_2 : rawProposed false 2=(![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-3/2000 : ℚ),(51259/82000 : ℚ),(6403/2960 : ℚ)],![(327/164000 : ℚ),(36297/16810 : ℚ),(-51259/82000 : ℚ)]] : RationalMatrix) := rfl
89 @[simp] theorem rawProposed_true_0 : rawProposed true 0=(![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(3069/20500 : ℚ),(160649/806600 : ℚ)],![(0/1 : ℚ),(-673511/3362000 : ℚ),(12283/82000 : ℚ)]] : RationalMatrix) := rfl
90 @[simp] theorem rawProposed_true_1 : rawProposed true 1=(![![(0/1 : ℚ),(-37/246000 : ℚ),(984049/654000 : ℚ)],![(35311/29600 : ℚ),(-33/164000 : ℚ),(-14537/16132000 : ℚ)],![(147041/164000 : ℚ),(4033/6724000 : ℚ),(33/164000 : ℚ)]] : RationalMatrix) := rfl
91 @[simp] theorem rawProposed_true_2 : rawProposed true 2=(![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(3/2000 : ℚ),(-110959/82000 : ℚ),(579221/322640 : ℚ)],![(-327/164000 : ℚ),(12099/6724 : ℚ),(110959/82000 : ℚ)]] : RationalMatrix) := rfl
92 @[simp] theorem nominalComparison_false_0 : nominalComparison false 0=(![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(17549/80000 : ℚ),(63/80000 : ℚ)],![(0/1 : ℚ),(7/20000 : ℚ),(8743/40000 : ℚ)]] : RationalMatrix) := rfl
93 @[simp] theorem nominalComparison_false_1 : nominalComparison false 1=(![![(0/1 : ℚ),(168021/160000 : ℚ),(251979/320000 : ℚ)],![(4207/4000 : ℚ),(7/40000 : ℚ),(63/80000 : ℚ)],![(9457/12000 : ℚ),(-21/40000 : ℚ),(-7/40000 : ℚ)]] : RationalMatrix) := rfl
94 @[simp] theorem nominalComparison_false_2 : nominalComparison false 2=(![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-21/16000 : ℚ),(8813/16000 : ℚ),(120953/64000 : ℚ)],![(7/4000 : ℚ),(189/100 : ℚ),(-8813/16000 : ℚ)]] : RationalMatrix) := rfl
95 @[simp] theorem nominalComparison_true_0 : nominalComparison true 0=(![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(10451/80000 : ℚ),(13937/80000 : ℚ)],![(0/1 : ℚ),(-3507/20000 : ℚ),(5257/40000 : ℚ)]] : RationalMatrix) := rfl
96 @[simp] theorem nominalComparison_true_1 : nominalComparison true 1=(![![(0/1 : ℚ),(-21/160000 : ℚ),(420021/320000 : ℚ)],![(4193/4000 : ℚ),(-7/40000 : ℚ),(-63/80000 : ℚ)],![(9443/12000 : ℚ),(21/40000 : ℚ),(7/40000 : ℚ)]] : RationalMatrix) := rfl
97 @[simp] theorem nominalComparison_true_2 : nominalComparison true 2=(![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(21/16000 : ℚ),(-18893/16000 : ℚ),(100807/64000 : ℚ)],![(-7/4000 : ℚ),(63/40 : ℚ),(18893/16000 : ℚ)]] : RationalMatrix) := rfl
98 @[simp] theorem nominalProposed_false_0 : nominalProposed false 0=(![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(53963/246000 : ℚ),(413/523200 : ℚ)],![(0/1 : ℚ),(28231/80688000 : ℚ),(430157/1968000 : ℚ)]] : RationalMatrix) := rfl
99 @[simp] theorem nominalProposed_false_1 : nominalProposed false 1=(![![(0/1 : ℚ),(690753/656000 : ℚ),(1381219/1744000 : ℚ)],![(248003/236800 : ℚ),(231/1312000 : ℚ),(101759/129056000 : ℚ)],![(1030813/1312000 : ℚ),(-28231/53792000 : ℚ),(-231/1312000 : ℚ)]] : RationalMatrix) := rfl
100 @[simp] theorem nominalProposed_false_2 : nominalProposed false 2=(![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-21/16000 : ℚ),(358813/656000 : ℚ),(44821/23680 : ℚ)],![(2289/1312000 : ℚ),(254079/134480 : ℚ),(-358813/656000 : ℚ)]] : RationalMatrix) := rfl
101 @[simp] theorem nominalProposed_true_0 : nominalProposed true 0=(![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(21483/164000 : ℚ),(1124543/6452800 : ℚ)],![(0/1 : ℚ),(-4714577/26896000 : ℚ),(85981/656000 : ℚ)]] : RationalMatrix) := rfl
102 @[simp] theorem nominalProposed_true_1 : nominalProposed true 1=(![![(0/1 : ℚ),(-259/1968000 : ℚ),(6888343/5232000 : ℚ)],![(247177/236800 : ℚ),(-231/1312000 : ℚ),(-101759/129056000 : ℚ)],![(1029287/1312000 : ℚ),(28231/53792000 : ℚ),(231/1312000 : ℚ)]] : RationalMatrix) := rfl
103 @[simp] theorem nominalProposed_true_2 : nominalProposed true 2=(![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(21/16000 : ℚ),(-776713/656000 : ℚ),(4054547/2581120 : ℚ)],![(-2289/1312000 : ℚ),(84693/53792 : ℚ),(776713/656000 : ℚ)]] : RationalMatrix) := rfl
104
105 theorem proposed_inverse : qmul proposedTransform proposedInverse=1 ∧ qmul proposedInverse proposedTransform=1 := by
106 constructor <;> ext i j <;> simp only [qmul,Matrix.one_apply]
107 all_goals fin_cases i <;> fin_cases j <;>
108 norm_num [proposedTransform,proposedInverse,qmul,Fin.sum_univ_succ,Matrix.cons_val]
109
110 theorem comparison_inverse : qmul comparisonTransform comparisonInverse=1 ∧ qmul comparisonInverse comparisonTransform=1 := by
111 constructor <;> ext i j <;> simp only [qmul,Matrix.one_apply]
112 all_goals fin_cases i <;> fin_cases j <;>
113 norm_num [comparisonTransform,comparisonInverse,qmul,Fin.sum_univ_succ,Matrix.cons_val]
114
115 theorem referenceComparison_construction (a : Bool) (k : Fin 3) :
116 referenceComparison a k=qmul (qmul comparisonTransform (referenceOriginal a k)) comparisonInverse := by
117 cases a
118 · fin_cases k
119 ·
120 change (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/4 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(1/4 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/4 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(1/4 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
121 ext i j
122 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
123 ·
124 change (![![(0/1 : ℚ),(6/5 : ℚ),(9/10 : ℚ)],![(6/5 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(9/10 : ℚ),(0/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(-2/1 : ℚ),(4/1 : ℚ),(0/1 : ℚ)],![(-7/16 : ℚ),(2/1 : ℚ),(0/1 : ℚ)],![(-53/80 : ℚ),(2/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
125 ext i j
126 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
127 ·
128 change (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(63/100 : ℚ),(54/25 : ℚ)],![(0/1 : ℚ),(54/25 : ℚ),(-63/100 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(9/4 : ℚ),(0/1 : ℚ)],![(9/10 : ℚ),(27/10 : ℚ),(-9/4 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
129 ext i j
130 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
131 · fin_cases k
132 ·
133 change (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(3/20 : ℚ),(1/5 : ℚ)],![(0/1 : ℚ),(-1/5 : ℚ),(3/20 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(1/4 : ℚ)],![(1/10 : ℚ),(-1/4 : ℚ),(3/10 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
134 ext i j
135 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
136 ·
137 change (![![(0/1 : ℚ),(0/1 : ℚ),(3/2 : ℚ)],![(6/5 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(9/10 : ℚ),(0/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(-2/1 : ℚ),(0/1 : ℚ),(4/1 : ℚ)],![(-7/16 : ℚ),(0/1 : ℚ),(2/1 : ℚ)],![(-53/80 : ℚ),(0/1 : ℚ),(2/1 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
138 ext i j
139 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
140 ·
141 change (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(-27/20 : ℚ),(9/5 : ℚ)],![(0/1 : ℚ),(9/5 : ℚ),(27/20 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(9/4 : ℚ)],![(0/1 : ℚ),(9/4 : ℚ),(0/1 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
142 ext i j
143 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
144
145 theorem rawComparison_construction (a : Bool) (k : Fin 3) :
146 rawComparison a k=qmul (qmul comparisonTransform (fittedOriginal a k)) comparisonInverse := by
147 cases a
148 · fin_cases k
149 ·
150 change (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(2507/10000 : ℚ),(9/10000 : ℚ)],![(0/1 : ℚ),(1/2500 : ℚ),(1249/5000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-1/2000 : ℚ),(251/1000 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/2000 : ℚ),(499/2000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
151 ext i j
152 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
153 ·
154 change (![![(0/1 : ℚ),(24003/20000 : ℚ),(35997/40000 : ℚ)],![(601/500 : ℚ),(1/5000 : ℚ),(9/10000 : ℚ)],![(1351/1500 : ℚ),(-3/5000 : ℚ),(-1/5000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(-2/1 : ℚ),(8001/2000 : ℚ),(-1/2000 : ℚ)],![(-437/1000 : ℚ),(2/1 : ℚ),(1/2000 : ℚ)],![(-331/500 : ℚ),(3999/2000 : ℚ),(0/1 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
155 ext i j
156 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
157 ·
158 change (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-3/2000 : ℚ),(1259/2000 : ℚ),(17279/8000 : ℚ)],![(1/500 : ℚ),(54/25 : ℚ),(-1259/2000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(4499/2000 : ℚ),(1/2000 : ℚ)],![(1801/2000 : ℚ),(27/10 : ℚ),(-4499/2000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
159 ext i j
160 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
161 · fin_cases k
162 ·
163 change (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1493/10000 : ℚ),(1991/10000 : ℚ)],![(0/1 : ℚ),(-501/2500 : ℚ),(751/5000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2000 : ℚ),(-1/1000 : ℚ),(1/4 : ℚ)],![(1/10 : ℚ),(-501/2000 : ℚ),(601/2000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
164 ext i j
165 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
166 ·
167 change (![![(0/1 : ℚ),(-3/20000 : ℚ),(60003/40000 : ℚ)],![(599/500 : ℚ),(-1/5000 : ℚ),(-9/10000 : ℚ)],![(1349/1500 : ℚ),(3/5000 : ℚ),(1/5000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(-2/1 : ℚ),(-1/2000 : ℚ),(8001/2000 : ℚ)],![(-219/500 : ℚ),(0/1 : ℚ),(3999/2000 : ℚ)],![(-663/1000 : ℚ),(1/2000 : ℚ),(2/1 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
168 ext i j
169 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
170 ·
171 change (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(3/2000 : ℚ),(-2699/2000 : ℚ),(14401/8000 : ℚ)],![(-1/500 : ℚ),(9/5 : ℚ),(2699/2000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/2000 : ℚ),(4499/2000 : ℚ)],![(-1/2000 : ℚ),(9/4 : ℚ),(-1/2000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
172 ext i j
173 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
174
175 theorem rawProposed_construction (a : Bool) (k : Fin 3) :
176 rawProposed a k=qmul (qmul proposedTransform (fittedOriginal a k)) proposedInverse := by
177 cases a
178 · fin_cases k
179 ·
180 change (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(7709/30750 : ℚ),(59/65400 : ℚ)],![(0/1 : ℚ),(4033/10086000 : ℚ),(61451/246000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix) (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-1/2000 : ℚ),(251/1000 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/2000 : ℚ),(499/2000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
181 ext i j
182 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
183 ·
184 change (![![(0/1 : ℚ),(98679/82000 : ℚ),(197317/218000 : ℚ)],![(35429/29600 : ℚ),(33/164000 : ℚ),(14537/16132000 : ℚ)],![(147259/164000 : ℚ),(-4033/6724000 : ℚ),(-33/164000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix) (![![(-2/1 : ℚ),(8001/2000 : ℚ),(-1/2000 : ℚ)],![(-437/1000 : ℚ),(2/1 : ℚ),(1/2000 : ℚ)],![(-331/500 : ℚ),(3999/2000 : ℚ),(0/1 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
185 ext i j
186 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
187 ·
188 change (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-3/2000 : ℚ),(51259/82000 : ℚ),(6403/2960 : ℚ)],![(327/164000 : ℚ),(36297/16810 : ℚ),(-51259/82000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix) (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(4499/2000 : ℚ),(1/2000 : ℚ)],![(1801/2000 : ℚ),(27/10 : ℚ),(-4499/2000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
189 ext i j
190 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
191 · fin_cases k
192 ·
193 change (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(3069/20500 : ℚ),(160649/806600 : ℚ)],![(0/1 : ℚ),(-673511/3362000 : ℚ),(12283/82000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix) (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2000 : ℚ),(-1/1000 : ℚ),(1/4 : ℚ)],![(1/10 : ℚ),(-501/2000 : ℚ),(601/2000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
194 ext i j
195 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
196 ·
197 change (![![(0/1 : ℚ),(-37/246000 : ℚ),(984049/654000 : ℚ)],![(35311/29600 : ℚ),(-33/164000 : ℚ),(-14537/16132000 : ℚ)],![(147041/164000 : ℚ),(4033/6724000 : ℚ),(33/164000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix) (![![(-2/1 : ℚ),(-1/2000 : ℚ),(8001/2000 : ℚ)],![(-219/500 : ℚ),(0/1 : ℚ),(3999/2000 : ℚ)],![(-663/1000 : ℚ),(1/2000 : ℚ),(2/1 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
198 ext i j
199 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
200 ·
201 change (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(3/2000 : ℚ),(-110959/82000 : ℚ),(579221/322640 : ℚ)],![(-327/164000 : ℚ),(12099/6724 : ℚ),(110959/82000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix) (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/2000 : ℚ),(4499/2000 : ℚ)],![(-1/2000 : ℚ),(9/4 : ℚ),(-1/2000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
202 ext i j
203 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
204
205 theorem nominalComparison_construction (a : Bool) (k : Fin 3) :
206 nominalComparison a k=qmul (qmul comparisonTransform (correctedOriginal a k)) comparisonInverse := by
207 cases a
208 · fin_cases k
209 ·
210 change (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(17549/80000 : ℚ),(63/80000 : ℚ)],![(0/1 : ℚ),(7/20000 : ℚ),(8743/40000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(993/16000 : ℚ),(1757/8000 : ℚ),(0/1 : ℚ)],![(1/16 : ℚ),(7/16000 : ℚ),(3493/16000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
211 ext i j
212 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
213 ·
214 change (![![(0/1 : ℚ),(168021/160000 : ℚ),(251979/320000 : ℚ)],![(4207/4000 : ℚ),(7/40000 : ℚ),(63/80000 : ℚ)],![(9457/12000 : ℚ),(-21/40000 : ℚ),(-7/40000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(-7/4 : ℚ),(56007/16000 : ℚ),(-7/16000 : ℚ)],![(-3059/8000 : ℚ),(7/4 : ℚ),(7/16000 : ℚ)],![(-2317/4000 : ℚ),(27993/16000 : ℚ),(0/1 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
215 ext i j
216 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
217 ·
218 change (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-21/16000 : ℚ),(8813/16000 : ℚ),(120953/64000 : ℚ)],![(7/4000 : ℚ),(189/100 : ℚ),(-8813/16000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(31493/16000 : ℚ),(7/16000 : ℚ)],![(12607/16000 : ℚ),(189/80 : ℚ),(-31493/16000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
219 ext i j
220 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
221 · fin_cases k
222 ·
223 change (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(10451/80000 : ℚ),(13937/80000 : ℚ)],![(0/1 : ℚ),(-3507/20000 : ℚ),(5257/40000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1007/16000 : ℚ),(-7/8000 : ℚ),(7/32 : ℚ)],![(3/20 : ℚ),(-3507/16000 : ℚ),(4207/16000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
224 ext i j
225 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
226 ·
227 change (![![(0/1 : ℚ),(-21/160000 : ℚ),(420021/320000 : ℚ)],![(4193/4000 : ℚ),(-7/40000 : ℚ),(-63/80000 : ℚ)],![(9443/12000 : ℚ),(21/40000 : ℚ),(7/40000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(-7/4 : ℚ),(-7/16000 : ℚ),(56007/16000 : ℚ)],![(-1533/4000 : ℚ),(0/1 : ℚ),(27993/16000 : ℚ)],![(-4641/8000 : ℚ),(7/16000 : ℚ),(7/4 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
228 ext i j
229 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
230 ·
231 change (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(21/16000 : ℚ),(-18893/16000 : ℚ),(100807/64000 : ℚ)],![(-7/4000 : ℚ),(63/40 : ℚ),(18893/16000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-2/3 : ℚ),(10/3 : ℚ),(-2/1 : ℚ)],![(-4/3 : ℚ),(0/1 : ℚ),(8/3 : ℚ)]] : RationalMatrix) (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(7/16000 : ℚ),(31493/16000 : ℚ)],![(-7/16000 : ℚ),(63/32 : ℚ),(-7/16000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(3/10 : ℚ),(9/40 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(3/8 : ℚ)]] : RationalMatrix)
232 ext i j
233 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
234
235 theorem nominalProposed_construction (a : Bool) (k : Fin 3) :
236 nominalProposed a k=qmul (qmul proposedTransform (correctedOriginal a k)) proposedInverse := by
237 cases a
238 · fin_cases k
239 ·
240 change (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(53963/246000 : ℚ),(413/523200 : ℚ)],![(0/1 : ℚ),(28231/80688000 : ℚ),(430157/1968000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix) (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(993/16000 : ℚ),(1757/8000 : ℚ),(0/1 : ℚ)],![(1/16 : ℚ),(7/16000 : ℚ),(3493/16000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
241 ext i j
242 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
243 ·
244 change (![![(0/1 : ℚ),(690753/656000 : ℚ),(1381219/1744000 : ℚ)],![(248003/236800 : ℚ),(231/1312000 : ℚ),(101759/129056000 : ℚ)],![(1030813/1312000 : ℚ),(-28231/53792000 : ℚ),(-231/1312000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix) (![![(-7/4 : ℚ),(56007/16000 : ℚ),(-7/16000 : ℚ)],![(-3059/8000 : ℚ),(7/4 : ℚ),(7/16000 : ℚ)],![(-2317/4000 : ℚ),(27993/16000 : ℚ),(0/1 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
245 ext i j
246 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
247 ·
248 change (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-21/16000 : ℚ),(358813/656000 : ℚ),(44821/23680 : ℚ)],![(2289/1312000 : ℚ),(254079/134480 : ℚ),(-358813/656000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix) (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(31493/16000 : ℚ),(7/16000 : ℚ)],![(12607/16000 : ℚ),(189/80 : ℚ),(-31493/16000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
249 ext i j
250 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
251 · fin_cases k
252 ·
253 change (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(21483/164000 : ℚ),(1124543/6452800 : ℚ)],![(0/1 : ℚ),(-4714577/26896000 : ℚ),(85981/656000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix) (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1007/16000 : ℚ),(-7/8000 : ℚ),(7/32 : ℚ)],![(3/20 : ℚ),(-3507/16000 : ℚ),(4207/16000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
254 ext i j
255 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
256 ·
257 change (![![(0/1 : ℚ),(-259/1968000 : ℚ),(6888343/5232000 : ℚ)],![(247177/236800 : ℚ),(-231/1312000 : ℚ),(-101759/129056000 : ℚ)],![(1029287/1312000 : ℚ),(28231/53792000 : ℚ),(231/1312000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix) (![![(-7/4 : ℚ),(-7/16000 : ℚ),(56007/16000 : ℚ)],![(-1533/4000 : ℚ),(0/1 : ℚ),(27993/16000 : ℚ)],![(-4641/8000 : ℚ),(7/16000 : ℚ),(7/4 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
258 ext i j
259 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
260 ·
261 change (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(21/16000 : ℚ),(-776713/656000 : ℚ),(4054547/2581120 : ℚ)],![(-2289/1312000 : ℚ),(84693/53792 : ℚ),(776713/656000 : ℚ)]] : RationalMatrix) = qmul (qmul (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-49/74 : ℚ),(123/37 : ℚ),(-2/1 : ℚ)],![(-109/82 : ℚ),(0/1 : ℚ),(109/41 : ℚ)]] : RationalMatrix) (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(7/16000 : ℚ),(31493/16000 : ℚ)],![(-7/16000 : ℚ),(63/32 : ℚ),(-7/16000 : ℚ)]] : RationalMatrix)) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(37/123 : ℚ),(74/327 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(41/109 : ℚ)]] : RationalMatrix)
262 ext i j
263 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
264
265 theorem fitted_construction (a : Bool) (k : Fin 3) :
266 fittedOriginal a k=qadd (referenceOriginal a k) (qscale (if a then (-1/2000 : ℚ) else 1/2000) (errorCoefficient k)) := by
267 cases a
268 · fin_cases k
269 ·
270 change (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-1/2000 : ℚ),(251/1000 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/2000 : ℚ),(499/2000 : ℚ)]] : RationalMatrix) = qadd (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/4 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(1/4 : ℚ)]] : RationalMatrix) (qscale (1/2000 : ℚ) (![![(0/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-1/1 : ℚ),(2/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/1 : ℚ),(-1/1 : ℚ)]] : RationalMatrix))
271 ext i j
272 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
273 ·
274 change (![![(-2/1 : ℚ),(8001/2000 : ℚ),(-1/2000 : ℚ)],![(-437/1000 : ℚ),(2/1 : ℚ),(1/2000 : ℚ)],![(-331/500 : ℚ),(3999/2000 : ℚ),(0/1 : ℚ)]] : RationalMatrix) = qadd (![![(-2/1 : ℚ),(4/1 : ℚ),(0/1 : ℚ)],![(-7/16 : ℚ),(2/1 : ℚ),(0/1 : ℚ)],![(-53/80 : ℚ),(2/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix) (qscale (1/2000 : ℚ) (![![(0/1 : ℚ),(1/1 : ℚ),(-1/1 : ℚ)],![(1/1 : ℚ),(0/1 : ℚ),(1/1 : ℚ)],![(1/1 : ℚ),(-1/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix))
275 ext i j
276 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
277 ·
278 change (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(4499/2000 : ℚ),(1/2000 : ℚ)],![(1801/2000 : ℚ),(27/10 : ℚ),(-4499/2000 : ℚ)]] : RationalMatrix) = qadd (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(9/4 : ℚ),(0/1 : ℚ)],![(9/10 : ℚ),(27/10 : ℚ),(-9/4 : ℚ)]] : RationalMatrix) (qscale (1/2000 : ℚ) (![![(0/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(-1/1 : ℚ),(1/1 : ℚ)],![(1/1 : ℚ),(0/1 : ℚ),(1/1 : ℚ)]] : RationalMatrix))
279 ext i j
280 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
281 · fin_cases k
282 ·
283 change (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2000 : ℚ),(-1/1000 : ℚ),(1/4 : ℚ)],![(1/10 : ℚ),(-501/2000 : ℚ),(601/2000 : ℚ)]] : RationalMatrix) = qadd (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(1/4 : ℚ)],![(1/10 : ℚ),(-1/4 : ℚ),(3/10 : ℚ)]] : RationalMatrix) (qscale (-1/2000 : ℚ) (![![(0/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-1/1 : ℚ),(2/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/1 : ℚ),(-1/1 : ℚ)]] : RationalMatrix))
284 ext i j
285 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
286 ·
287 change (![![(-2/1 : ℚ),(-1/2000 : ℚ),(8001/2000 : ℚ)],![(-219/500 : ℚ),(0/1 : ℚ),(3999/2000 : ℚ)],![(-663/1000 : ℚ),(1/2000 : ℚ),(2/1 : ℚ)]] : RationalMatrix) = qadd (![![(-2/1 : ℚ),(0/1 : ℚ),(4/1 : ℚ)],![(-7/16 : ℚ),(0/1 : ℚ),(2/1 : ℚ)],![(-53/80 : ℚ),(0/1 : ℚ),(2/1 : ℚ)]] : RationalMatrix) (qscale (-1/2000 : ℚ) (![![(0/1 : ℚ),(1/1 : ℚ),(-1/1 : ℚ)],![(1/1 : ℚ),(0/1 : ℚ),(1/1 : ℚ)],![(1/1 : ℚ),(-1/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix))
288 ext i j
289 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
290 ·
291 change (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/2000 : ℚ),(4499/2000 : ℚ)],![(-1/2000 : ℚ),(9/4 : ℚ),(-1/2000 : ℚ)]] : RationalMatrix) = qadd (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(0/1 : ℚ),(9/4 : ℚ)],![(0/1 : ℚ),(9/4 : ℚ),(0/1 : ℚ)]] : RationalMatrix) (qscale (-1/2000 : ℚ) (![![(0/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(-1/1 : ℚ),(1/1 : ℚ)],![(1/1 : ℚ),(0/1 : ℚ),(1/1 : ℚ)]] : RationalMatrix))
292 ext i j
293 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
294
295 theorem corrected_construction (a : Bool) (k : Fin 3) :
296 correctedOriginal a k=qadd (qscale (7/8 : ℚ) (fittedOriginal a k))
297 (if k=0 then qscale (1/8 : ℚ) physicalReset else 0) := by
298 cases a
299 · fin_cases k
300 ·
301 change (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(993/16000 : ℚ),(1757/8000 : ℚ),(0/1 : ℚ)],![(1/16 : ℚ),(7/16000 : ℚ),(3493/16000 : ℚ)]] : RationalMatrix) = qadd (qscale (7/8 : ℚ) (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(-1/2000 : ℚ),(251/1000 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/2000 : ℚ),(499/2000 : ℚ)]] : RationalMatrix)) (qscale (1/8 : ℚ) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix))
302 ext i j
303 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
304 ·
305 change (![![(-7/4 : ℚ),(56007/16000 : ℚ),(-7/16000 : ℚ)],![(-3059/8000 : ℚ),(7/4 : ℚ),(7/16000 : ℚ)],![(-2317/4000 : ℚ),(27993/16000 : ℚ),(0/1 : ℚ)]] : RationalMatrix) = qadd (qscale (7/8 : ℚ) (![![(-2/1 : ℚ),(8001/2000 : ℚ),(-1/2000 : ℚ)],![(-437/1000 : ℚ),(2/1 : ℚ),(1/2000 : ℚ)],![(-331/500 : ℚ),(3999/2000 : ℚ),(0/1 : ℚ)]] : RationalMatrix)) ((0 : RationalMatrix))
306 ext i j
307 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
308 ·
309 change (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(31493/16000 : ℚ),(7/16000 : ℚ)],![(12607/16000 : ℚ),(189/80 : ℚ),(-31493/16000 : ℚ)]] : RationalMatrix) = qadd (qscale (7/8 : ℚ) (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(4499/2000 : ℚ),(1/2000 : ℚ)],![(1801/2000 : ℚ),(27/10 : ℚ),(-4499/2000 : ℚ)]] : RationalMatrix)) ((0 : RationalMatrix))
310 ext i j
311 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
312 · fin_cases k
313 ·
314 change (![![(11/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1007/16000 : ℚ),(-7/8000 : ℚ),(7/32 : ℚ)],![(3/20 : ℚ),(-3507/16000 : ℚ),(4207/16000 : ℚ)]] : RationalMatrix) = qadd (qscale (7/8 : ℚ) (![![(1/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2000 : ℚ),(-1/1000 : ℚ),(1/4 : ℚ)],![(1/10 : ℚ),(-501/2000 : ℚ),(601/2000 : ℚ)]] : RationalMatrix)) (qscale (1/8 : ℚ) (![![(1/1 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(1/2 : ℚ),(0/1 : ℚ),(0/1 : ℚ)]] : RationalMatrix))
315 ext i j
316 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
317 ·
318 change (![![(-7/4 : ℚ),(-7/16000 : ℚ),(56007/16000 : ℚ)],![(-1533/4000 : ℚ),(0/1 : ℚ),(27993/16000 : ℚ)],![(-4641/8000 : ℚ),(7/16000 : ℚ),(7/4 : ℚ)]] : RationalMatrix) = qadd (qscale (7/8 : ℚ) (![![(-2/1 : ℚ),(-1/2000 : ℚ),(8001/2000 : ℚ)],![(-219/500 : ℚ),(0/1 : ℚ),(3999/2000 : ℚ)],![(-663/1000 : ℚ),(1/2000 : ℚ),(2/1 : ℚ)]] : RationalMatrix)) ((0 : RationalMatrix))
319 ext i j
320 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
321 ·
322 change (![![(63/32 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(7/16000 : ℚ),(31493/16000 : ℚ)],![(-7/16000 : ℚ),(63/32 : ℚ),(-7/16000 : ℚ)]] : RationalMatrix) = qadd (qscale (7/8 : ℚ) (![![(9/4 : ℚ),(0/1 : ℚ),(0/1 : ℚ)],![(0/1 : ℚ),(1/2000 : ℚ),(4499/2000 : ℚ)],![(-1/2000 : ℚ),(9/4 : ℚ),(-1/2000 : ℚ)]] : RationalMatrix)) ((0 : RationalMatrix))
323 ext i j
324 fin_cases i <;> fin_cases j <;> norm_num [qmul,qadd,qscale,Fin.sum_univ_succ]
325
326 end
327 end Komorebi.LSM.PerturbedOperatorFixture
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: 8f5426e4034c9879d59652701acbd9c29dfeb4a2b25f45e2ae16f997e90fc196