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. 

In the proof of a formal theorem, there must be one existed theorem to serve as the pillar or captain (掌门), favored by a beam or cheif mate (大副), the another existed theorem...

.

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 or continued) Previously, one arrives at L' + P' ~ G'. Recall that L' is constructed as a "pre-construction" (or "resolvent") of G in the X'-space, evolving from the prototype n·c(M) hinted by the form of "n·divisor" which is originated from the mode inherent in the definition of "n-complement". In mathematics, definitions are the sources of modes, while practices are the sources of definitions (TOM). But, why is this c(M) chosen as the proper divisor? To answer this question, I introduce the concept of "candidate set" where the candidate objects are included. These candidate objects are either invented by the author or encountered in the references along the journey. When a researcher enters the right domain for the solution of a problem, he or she faces a scene of dominoes of finite trials (TOR). In such a scene, the player moves ahead by striking the right trial. The objects in the candidate set have a nature that induces the player's strike, while the right trial may return certain positive feedback to the player.

.

To proceed, recall that P' presents as an aide to form a plt-Eve pair needed by the KV vanishing theorem (cf. "looking at..."). Functionally, the KV vanishing theorem is to suggest the construction of a "plt type" divisor O (or O' in the scene of X'-space here). As this happens in the context of n-complement, it is expectant that O' contains L' as a major component. One can view the matter this way: both "n-complement" and "KV"  suggest the construction of certain divisors —— Under this common context, it is expectant that the desired divisors share a "common component" from both threads. Meanwhile, in the context of "construction", a pre-construction is usually expected (cf. high view). Jointly, L' can also be viewed as the pre-construction (or "resolvent") of O'.

.

The philosophy of "common component" is also applied in the construction of the "plt-Eve type boundary" motivated/ needed by the KV vanishing theorem. A plt-Eve type boundary ฿ is the boundary of a plt-Eve pair, such that the removal of Eve from ฿ transforms the original pair into a klt pair (see KV vanishing theorem). In order to construct a plt-Eve type boundary, one uses the boundary of a plt-Eve pair as the seed which is given as the auxiliary items in Pro.4.1 (search "auxiliary items" here ). In the scene of X'-space, this seed is just Γ'. The common component from the thread of n-complement is taken as d'n from L' (why d'n?)*. So, the pre-construction of the plt-Eve type boundary takes the form of Γ' + d'n.

* This question is asked in the sense of Theory Of Mathematics (TOM).

.

So far, L' is viewed as the pre-construction of O', while Γ' + d'n is viewed as the pre-construction of ฿ (or Θ in the paper). To activate the KV vanishing theorem, one can temporarily assume that (X', Γ' + d'n) is plt-Eve(S'), such that (X', Γ' + d'n - S') is klt, and [·] is nef and big such that L' - [·] = Kx' + (Γ' + d'n). However, at some point, one checks that Γ' + d'n does not satisfy the non-negative requirement for any boundary. To mend this problem, one uses Γ' + d'n - ⌊Γ' + d'n⌋\S' as the plt-Eve type boundary. For clarity,  - ⌊Γ' + d'n⌋\S' is denoted as P'. Applying this mending backward, one has L' + P' - [·] = Kx' + (Γ' + d'n + P'). Here, P' plays a double role, to help form O' (= L' + P'). Nevertheless, P' just presents in O' incidentally. It is notable that, the second auxiliary item, concerning c(α·M), is only essentially used in the context of KV vanishing theorem.

.

Now, one needs to figure out the term [·], a nef and big divisor —— c(α·M) enters the game only to settle down this divisor. But, how did the thoughts of c(α·M) occur to the author? To look ahead, the additional term of 2M' in L' arises in this context. Recall L' = (n + 2)M' - nKx' - nE' - ⌊(n + 1)Δ'⌋ = 2M' + n·c'(M) + d'n. To understand the presence of 2M', I remove it from L' and denote such modified L' as (L'). That is to say, I have ——

.

(L') = n·c'(M) + d'n. 

.

Now, replace L' in the expression of L' + P' - [·] with (L'), one has ——

.

               (L') + P' - [·] = Kx' + (Γ' + d'n + P') ==>

n·c'(M) + d'n + P' - [·] = Kx' + (Γ' + d'n + P') ==>

                n·c'(M) - [·] = Kx' + Γ'.

.

The right-hand side is the operation form of the pair (X', Γ'). One can solve for [·] as ——

.

[·] = n·c'(M) - (Kx' + Γ').

.

It is given* that c'(M) is nef and big, but there is no information concerning the attribution of Kx' + Γ'. Also, it appears not convenient to prescribe Kx' + Γ' as nef and big. However, as the attribution of "nef and big" of c'(M) is out of prescribing, it is convenient to apply the similar philosophy by constructing a "confrontation" involving Kx' + Γ'. Actually, the author introduces a scaled** version of M', namely α·M', which is more flexible (or more general in form). So, one has ——

* Clearly, c(M) is prescribed to be "nef and big" due to the KV vanishing theorem. 

** Such scaled version of M' arises naturally in the final proof of Theorem 1.9.

.

[·] = n·c'(M) + α·M' - (Kx' + Γ') - α·M' ==>

[·] = n·c'(M) + c(α·M')Γ' - α·M'.

.

Now, one can prescribe c(α·M')Γ' to be "nef and big", or more strongly "ample", for the reason seen in move one. Finally, one needs to deal with the term - α·M'. It is given that M' is semi-ample, while α falls in (0, 2) due to move one. So introduces the term 2M' into (L') to form a positive term (2 - α)M', which favors the desired attribution of "nef and big" of [·]. In retrospect, 2M' is the common component from KV in the construction of L'.

.

In summary, it is the KV vanishing theorem that has dominated the construction of L' and P', jointly favored by the mode from n-complement in the case of L'. (From another angle, the constructions are conducted like a duet).

.

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

.

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.