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. 

Is it not surprising that mathematics has not formed an open source society ?

---- By "open", I refer to the "transparency" on every level.

.

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

(continued) camera level one = {R, S, '} ==> camera of level two {Rs, Rs', R', ...}.

.

Step 7, Para two (b) ——

Since nR' := G' - P' + ⌊(n + 1)Δ' ⌋ - nΔ' ~ L' +  ⌊(n + 1)Δ' ⌋ - nΔ' = 2M' + nN' ~Q 0/ X...

---- Recall, the target is to arrive at R|s = Rs; see Para two (a).

---- Recall, Rs is defined at the beginning of Step 6, and R is defined in Step 7, Para two (a).

---- Recall, L' + P' ~ G' is setup at the end of Step 6.

---- Where does the idea of defining nR' come from ?

---- The most close expression is (from Step 6) ——

(L' + P')|s' ~ Gs' := nRs' + nΔs' -  ⌊(n + 1)Δs'⌋ + Ps'.

---- By a rearrangement of terms, one arrives at nRs' = Gs' - Ps' + ⌊(n + 1)Δs'⌋ - nΔs'.

---- So far, one has Rs, Rs', and R.

---- Rs and R have similar shape.

---- For one thing, nR: = G; for another, B⁺ := B + R.

---- However, one cannot define nR' := G', for there is an "exceptional" matter.

---- So, one resorts to the expression for nRs'.

---- That is, to define nR' by overlooking s' in the expression.

---- Indeed, the expression G' - P' + ⌊(n + 1)Δ' ⌋ - nΔ' can stand.

---- So, let it be nR'.

---- So comes nR' := G' - P' + ⌊(n + 1)Δ' ⌋ - nΔ'.

---- The rest matter is straightforward, except for the last connection.

---- I cannot see 2M' + nN' ~Q 0/ X. (?)

.

New comments: The camera of nR' appears not apparent.

---- Perhaps, Rs, Rs' and R' should be added in the camera.

---- As Rs' is the pullback of Rs, one expects that R' is the pullback of R.

---- While the targe is of R|s = Rs, one needs to arrive there through R'|s' = Rs'.

---- So arises the need to define R'.

---- In regard of  R'|s' = Rs', one needs to "derive" R' through Rs'.

---- Actually, nRs' = Gs' - Ps' + ⌊(n + 1)Δs'⌋ - nΔs' by Step 6.

---- So, one derives nRs' = Gs' - Ps' +  ⌊(n + 1)Δs'⌋ - nΔs' = (G' - P' +  ⌊(n + 1)Δ'⌋ - nΔ')|s'.

---- It is desirable to have nR':= G' - P' +  ⌊(n + 1)Δ'⌋ - nΔ', In regard of  R'|s' = Rs'.

(It appears that "camera" is of targets).

.

... and since ⌊(n + 1)Δ ⌋ - nΔ = 0, we get φ* nR' = G = nR and that R' is the pullback of R.

---- To be complete, I would calculate ——

(Note: the star in " φ* " is a subscript.)

φ* nR' = φ* (G' - P' + ⌊(n + 1)Δ'⌋  - nΔ')

= φ* (G') - φ* (P') + φ* (⌊(n + 1)Δ'⌋ - nΔ')

= G + 0 + 0.

= nR.

.

New comment: This is to show that nR' is indeed the pullback of R (as desired).

.

That is, φ* nR' = nR, i.e. φ* R' = R. (So, R' is the pullback of R.)

.

Comment: It appears that the handle of principle behind the deduction stands out.

.

Now by Step 6, nRs' = Gs' - Ps' + ⌊(n + 1)Δs'⌋ - nΔs' = (G' - P' + ⌊(n + 1)Δ'⌋ - nΔ')|s' = nR'|s' which means Rs' = R'|s'...

---- The preceding two equations have no new elements.

---- The third one comes only after the definition of nR'.

---- The net effect is nRs' = nR'|s', i.e. Rs' = R'|s'.

.

New comment: The key is the expression nRs' = Gs' - Ps' + ⌊(n + 1)Δs'⌋ - nΔs'  (set up by Step 6), plus the desire to seperate s'.

.

...hence Rs and R|s both pull back to Rs' which implies Rs = R|s as required.

---- This can be clarified by ——

.

Rs' = R'|s' --> R|s

||                   ||

Rs' -----------> Rs

.

Summary comment: I expect to rewrite the proof in a different style.

.

New comment: It appears that one is assumed to take for grounded R'|s' as the pullback of R|s.

.

↑↓ ℭ ℜ 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.