This is coming to you from Yiwei LI (PhD, Applied math), Taiyuan University of Science and Technology  (TYUST) Taiyuan, China

It's going on here for the third round of learning of Birkar's BAB-paper (v2), with scenarios of chess stories. No profession implications. 

The key lost is the "camera" from the memory for the general perspective...

Th 2.15    Th 1.8            ♖    ♘

     ↓   ↖     ↓

Th 1.1      Th 1.6            ♔    ♗

    Mathematics vs Palace stories.(v2)

------

Note: technical theorem is not on the board.

♙ ℂ ℍ ℕ ℙ ℚ ℝ ℤ ℭ ℜ I|φ∪∩∈ ⊆ ⊂ ⊇ ⊃ ⊄ ⊅ ≤ ≥ Γ Θ α Δ δ μ ≠ ⌊ ⌋ ∨∧∞Φ⁺⁻⁰ 1

(not continued) So, I need to find back the perspective...by reviewing the past notes*. I decide to start from 7a(foresee by overlook) ——

.

Step 7, Para one ——

In this step, we introduce Λ and show that it satisfies the properties listed in the theorem.

---- One will see in para two Λ be defined as B + R.

---- The task of this para one is to form R.

---- As hinted by the appearance, one may expect R is related to Rs.

---- Recall Rs is built at the beginning of Step 6.

---- In particular, Rs is just the difference between Bs⁺ and Bs.

.

New comments: The final goal is to formulate R, yet the way is through Rs.

---- R and S are the elements of the "camera", while Rs hints the connection.

---- Remember that R is just nominal at this moment.

---- Actually, Rs is also nominal at present.

---- I expect that Rs will be formulated first, which would pave the way for the formulation of R.

---- R|s = Rs is also expected.

---- Let's check them out...

.

Let L, P, G be the pushdowns to X of L', P', G'.

---- L', P', and G' are the main outputs of Steps 4 ~ 6.

---- Now, their images in X are of concern.

.

New comments: G' will play a key role (through Gs') in the formulation of Rs (through Rs'), if I remember right.

---- L' appears the key structure related to G'.

.

By the definition of L', by the previous step, and by the exceptionality of P', we have (n + 2)M - nKx - nE - ⌊(n + 1)Δ⌋ = L = L + P ~ G ≥ 0.

---- This is all clear.

---- P' is the image of P (= 0).

---- The net effect is to reach L ~ G.

.

Comments: It appears (it is) the proper position to recall the "formation" of L'.

---- As identified earlier, n·c'(M) is the prototype of L'.

---- c'(M) is the shorthand for M' - (Kx' + B').

---- So, n·c'(M) = nM' - n(Kx' + B').

---- Now, B' is divided into E' + Δ' by some rule.

---- Hence n·c'(M) = nM' - nKx' - nE' - nΔ'.

---- For some reason, nM' is replaced by (n + 2)M', and nΔ' by ⌊(n + 1)Δ'⌋.

---- That is, n·c'(M) is modified into the form (n + 2)M' - nKx' - nE' - ⌊(n + 1)Δ'⌋.

---- Now, give the later a notation of L'.

---- So, L' = (n + 2)M' - nKx' - nE' - ⌊(n + 1)Δ'⌋.

---- One sees n·c(M') and L' not the same thing.

---- L' can be viewed a modified version of n·c'(M).

---- At last, one is reminded the notation c'(M) homemade.

---- One can compare L' and L in forms.

.

New comment: L' is a key construction closely related to the "camera".

.

Since nB is integral,  ⌊(n + 1)Δ⌋ = nΔ, so (n + 2)M - n(Kx + B) = (n + 2)M - nKx - nE - nΔ = L ~ G ≥ 0. So defines nR: = G.

---- Nothing is changed but to use ⌊(n + 1)Δ⌋ = nΔ.

---- I slightly modify the later part to make it "natural".

---- Why nR: = G ?

---- The hint is in Step 6, near the end of para one.

.

Comments (why nR: = G ?) ——

---- One can answer this question by [the] calculation[s] in Step 6:

(L' + P')|s' = (2M' + nN' + d'n + P')|s ~ nRs' + d'n|s' + Ps'.

---- After that, it is defined Gs': = nRs' + d'n|s' + Ps'.

---- If one neglect s' and return to X, one has

---- G = nR, for P = 0 and dn = 0.

---- I call this approach "foresee by overlook".

.

New comments: The presence of (n + 2)M - n(Kx + B) appears not natural...

---- It appears just to simplify the expression of L by using ⌊(n + 1)Δ⌋ = nΔ.

---- After that, one has L = (n + 2)M - n(Kx + B).

---- The form (n + 2)M - n(Kx + B) is needed to account for the "relative" complement.

---- That is, one expects n(Kx + B⁺) ~ bounded quantity, instead of ~ 0.

---- Coincidentally, (n + 2)M - n(Kx + B) = L ~ G.

---- That is, n(Kx + B) + G ~ (n + 2)M.

---- So, it is natural to let nR:= G, so that n(Kx + B⁺) ~ (n + 2)M.

---- This also gives a better (acctually natural) explanation for "why nR:=G ?"

.

Summary comment: To move fast, keep things light.

.

↑↓ ℭ ℜ I|φ∪∩∈ ⊆ ⊂ ⊇ ⊃ ⊄ ⊅ ≤ ≥ Γ Θ α Δ δ μ ≠ ⌊ ⌋ ⌈ ⌉ ∨∧∞Φ⁺⁻⁰ 1

Calling graph for the technical theorem (Th1.9) ——

.

Th1.9

    |

[5, 2.13(7)]   Lem 2.26   Pro4.1   Lem2.7

                                                          |

.....................................................Lem2.3   

Note: Th1.9 is only called by Pro.5.11, one of the two devices for Th1.8, the executing theorem.

Pro4.1                                                    

    |

[5, ?]   [37, Pro3.8]   [5, Lem3.3]   Th2.13[5, Th1.7]   [16, Pro2.1.2]  [20]  [25, Th17.4]

Completed notes of the first round learning for v2 Pro.4.1 are packaged on RG.

.

Special note: Original synthesized scenarios in Chinese for the whole proof of v1 Th1.7, the technical theorem.

*It's now largely revised* due to new understandings.

.

See also: Earlier comments in Chinese* (v1).

.

.

It is my hope that this action would not be viewed from the usual perspective that many adults tend to hold.