org/mpm.org

   1 #+TITLE:     Minipolymath 3 - core threads in LAK & IATC
   2 #+AUTHOR:    Joe Corneli
   3 #+DATE:      May 12, 2017
   4 #+DESCRIPTION: a "Rosetta Stone" for work on IATC
   5 #+KEYWORDS: mathematical argumentation
   6 #+LANGUAGE: en
   7 #+OPTIONS: H:3 num:t toc:t \n:nil @:t ::t |:t ^:nil -:t f:t *:t <:t
   8 #+OPTIONS: TeX:t LaTeX:nil skip:nil d:nil todo:t pri:nil tags:not-in-toc
   9 #+INFOJS_OPT: view:nil toc:nil ltoc:t mouse:underline buttons:0 path:http://orgmode.org/org-info.js
  10 #+EXPORT_SELECT_TAGS: export
  11 #+EXPORT_EXCLUDE_TAGS: noexport
  12 #+LINK_UP:
  13 #+LINK_HOME:
  14 #+HTML_HEAD: <link rel="stylesheet" type="text/css" href="http://metameso.org/~joe/solarized-css/build/solarized-light.css" />
  15 #+STARTUP: showeverything
  16
  17 * Thread 3: What is a line?
  18
  19 *ANONYMOUS*: If the points form a convex polygon, it is easy.
  20
  21 #+BEGIN_SRC
  22 LAK> a. P: Conjecture(‘statement holds in the convex polygon case’).
  23 LAK> b. P: Lemma(‘a windmill process walks around the vertices of the convex polygon’ L 3.1 )
  24 LAK> c. P: ProofDone.
  25 #+END_SRC
  26
  27 #+BEGIN_SRC
  28 IATC> perf[judge](value[easy](S_is_conv))
  29 #+END_SRC
  30
  31 *THOMAS H*: Yes. Can we do it if there is a single point not on the convex
  32 hull of the points?
  33
  34 #+BEGIN_SRC
  35 LAK> d. P: Conjecture(‘statement holds in the convex polygon plus point case’).
  36 #+END_SRC
  37
  38 #+BEGIN_SRC
  39 IATC> perf[agree](S_is_conv)
  40 IATC> perf[query](rel[has_property](convex_plus_point, cycle_spans_S)
  41 IATC> rel[instance_ofl](S, convex_plus_point)
  42 #+END_SRC
  43
  44 *JERZY*: Say there are four points: an equilateral triangle, and then one
  45 point in the center of the triangle.  No three points are collinear. It
  46 seems to me that the windmill can not use the center point more than
  47 once!  As soon as it hits one of the corner points, it will cycle
  48 indefinitely through the corners and never return to the center point. I
  49 must be missing something here...
  50
  51 #+BEGIN_SRC
  52 LAK> e. O: GlobalCounter(‘equilateral triangle plus point’, ‘statement holds in the convex polygon case’).
  53 #+END_SRC
  54
  55 #+BEGIN_SRC
  56 IATC> perf[assert](rel[instance_of](convex_plus_point, equi_tri))
  57 IATC> perf[assert](rel[instance_of](S, equi_tri))
  58 IATC> perf[assert](rel[has_property](equi_tri, not_colin))
  59 IATC> perf[challenge](problem, equi_tri_stuck)
  60 IATC> rel[structural](equi_tri, equi_tri_stuck)
  61 IATC> perf[judge](rel[not](value[plausible](equi_tri_stuck)))
  62 #+END_SRC
  63
  64 *JOE*: This isn’t true - it will alternate between the
  65 centre and each vertex of the triangle.
  66
  67 #+BEGIN_SRC
  68 LAK> f. P: MonsterBar(‘equilateral triangle plus point’, ‘statement holds in the convex polygon case’, ‘line is alternating’).
  69 #+END_SRC
  70
  71 #+BEGIN_SRC
  72 IATC> perf[challenge](equi_tri_stuck, alternate)
  73 #+END_SRC
  74
  75 *THOMAS H*: No, you’re not right. Let the corner points be A, B, C,
  76 clockwise, M the center. If you start in M, you first hit say A, then C,
  77 then M, then B, then A.
  78
  79 #+BEGIN_SRC
  80 LAK> g. P: PDefinition(‘equilateral triangle plus point’, ‘line is alternating’, ‘“line” extends in both directions’).
  81 #+END_SRC
  82
  83 #+BEGIN_SRC
  84 IATC> perf[challenge](equi_tri_stuck, alternate1)
  85 #+END_SRC
  86
  87 *JERZY*: Ohhh. . . I misunderstood the problem. I saw it as a half-line
  88 extending out from the last point, in which case you would get stuck on
  89 the convex hull.  But apparently it means a full line, so that the next
  90 point can be “behind” the previous point. Got it.
  91
  92 #+BEGIN_SRC
  93 LAK> h. O: MonsterAccept(‘equilateral triangle plus point’, ‘line is alternating’).
  94 #+END_SRC
  95
  96 #+BEGIN_SRC
  97 IATC> perf[retract](perf[challenge](problem, equi_tri_stuck))
  98 IATC> perf[assert](rel[not](half_line))
  99 IATC> rel[structural](line, half_line)
 100 #+END_SRC
 101
 102 * Thread 11: Hitting all the points
 103
 104 *ANONYMOUS*: One can start with any point (since every point of S
 105 should be pivot infinitely often), the direction of line that one
 106 starts with however matters!
 107
 108 #+BEGIN_SRC
 109 LAK> a. P: Lemma(‘we can start with any point’ L 11.1 ).
 110 #+END_SRC
 111
 112 #+BEGIN_SRC
 113 IATC> perf[assert](rel[equivalent](problem, forall_exists_problem))
 114 IATC> ???rel[structural](problem, forall_exists_problem)
 115 IATC> perf[assert](rel[not](rel[equivalent](problem, forall_forall_problem)))
 116 IATC> ???rel[structural](problem, forall_forall_problem)
 117 #+END_SRC
 118
 119 *NEMANJA*: In other words, we can start with any point and ‘just’ need
 120 to choose a second point through which will we draw a line.
 121
 122 #+BEGIN_SRC
 123 LAK> [Repetition of previous move.]
 124 #+END_SRC
 125
 126 #+BEGIN_SRC
 127 IATC> perf[assert](forall_exists_problem_detail)
 128 IATC> rel[structural](forall_exists_problem, forall_exists_problem_detail)
 129 #+END_SRC
 130
 131 *ANONYMOUS*: Perhaps even the line does not mat-
 132 ter! Is it possible to prove that any point and any line
 133 will do?
 134
 135 #+BEGIN_SRC
 136 LAK> b. P: Lemma(‘the line does not matter‘ L 11.2 ).
 137 LAK> c. P: ProofDone.
 138 #+END_SRC
 139
 140 #+BEGIN_SRC
 141 IATC> perf[query](forall_forall_problem)
 142 #+END_SRC
 143
 144 *THOMAS H*: No, if you start with two points on the convex hull (ordered
 145 in the right way) you stay on the convex hull.
 146
 147 #+BEGIN_SRC
 148 LAK> d. O: LocalCounter(‘two points on the convex hull’, L 11.2 )
 149 #+END_SRC
 150
 151 #+BEGIN_SRC
 152 IATC> perf[challenge](forall_forall_problem, two_conseq_hull)
 153 #+END_SRC
 154
 155 *NEMANJA*: It is not possible, two consecutive points on convex hull
 156 will not do.
 157
 158 #+BEGIN_SRC
 159 LAK> [Repetition of previous move.]
 160 #+END_SRC
 161
 162 #+BEGIN_SRC
 163 IATC> perf[assert](rel[wlog](problem, zero_angle), one_turn)
 164 #+END_SRC
 165
 166 *ZHECKA*: Sure a choice of line is important.  Imagine S is a set of
 167 vertices of a convex polygon P (triangle, say) plus one point inside
 168 P.
 169
 170 #+BEGIN_SRC
 171 LAK> [Repetition of previous move.]
 172 #+END_SRC
 173
 174 #+BEGIN_SRC
 175 IATC> perf[challenge](forall_forall_problem, convex_plus_point)
 176 #+END_SRC
 177
 178 *ANONYMOUS*: Only the starting point matters.  By the problem
 179 statement, it appears that the initial angle is irrelevant to the
 180 existence of a pivot point P∗ from which all of S is traversed. Every
 181 point in S is a pivot point, but only with a specific range of
 182 starting angle (e.g. those consistent with the cycle generating
 183 S). The union of these intervals must necessarily be [0, 2π), and thus
 184 we can assume WLOG that the start- ing angle is 0 (and thus we single
 185 out a specific point – or points in the case of |S| = 2).
 186
 187 #+BEGIN_SRC
 188 LAK> e. P: LocalLemmaInc(‘two points on the convex hull’, L 11.2 , ‘the initial angle is irrelevant within a specific range’).
 189 #+END_SRC
 190
 191 #+BEGIN_SRC
 192 IATC> perf[assert](rel[wlog](problem, zero_angle), one_turn)
 193 #+END_SRC
 194
 195 * Thread 14 (first part): Splitting in two sets, conclusion
 196
 197 *ANONYMOUS*: I’m not sure but as no three points are collinear, one can
 198 always find a line which splits the points into two sets whose number
 199 of elements differ at most one?
 200
 201 #+BEGIN_SRC
 202 LAK> a. P: Lemma(‘we can separate the points in two parts of roughly equal size’ L 14.1 ).
 203 #+END_SRC
 204
 205 #+BEGIN_SRC
 206 IATC> perf[assert](forall_split, rel[has_property](S, not_colin))
 207 #+END_SRC
 208
 209 *THOMAS H*: That is surely true. How could this help us?
 210
 211 #+BEGIN_SRC
 212 LAK> [Not coded.]
 213 #+END_SRC
 214
 215 #+BEGIN_SRC
 216 IATC> perf[agree](forall_split)
 217 IATC> perf[query](value[useful](forall_split))
 218 #+END_SRC
 219
 220 *ANONYMOUS*: Something like one can find this no matter how we choose
 221 the first point. Then in some time the windmill must be parallel to
 222 the line through these points. This line must be unique or else it
 223 splits the points such that number of elements differ at least two.
 224
 225 #+BEGIN_SRC
 226 LAK> [Not coded.]
 227 #+END_SRC
 228
 229 #+BEGIN_SRC
 230 IATC> perf[assert](value[useful](forall_split))
 231 IATC> perf[assert](meta[auxiliary](parallel_line, forall_split))
 232 IATC> rel[structural](parallel_line, l)
 233 #+END_SRC
 234
 235 *JUSTIN W SMITH*: It appears that the number of points to the “left” or
 236 “right” of the line is constant through the entire process!
 237
 238 #+BEGIN_SRC
 239 LAK> [Not coded.]
 240 #+END_SRC
 241
 242 #+BEGIN_SRC
 243 IATC> perf[assert](half_thepoints)
 244 #+END_SRC
 245
 246 *GARF*: I think this solves the problem. Start with a line which
 247 separates the points into two parts of roughly same size (their
 248 cardinal differ by at most one, not counting the point to which the
 249 line is attached).  Then run the process until the line is
 250 “upside-down”, and so has turn by exactly π. Every point has gone from
 251 the right of the line to the left of the line (easy to see is the
 252 number of point is odd, you have to be a bit more crafty if it is
 253 even), and no point can go from left to right or right to left without
 254 touching the line. Add the previous remarks (the process will always
 255 come back to its initial configuration), and every point will be
 256 visited infinitely often.
 257
 258 #+BEGIN_SRC
 259 LAK> b. P: Lemma(‘we can run the process until the line is upside down’ L 14.2 ).
 260 LAK> c. P: Lemma(‘every point goes from right to left’ L 14.3 ).
 261 LAK> d. P: Lemma(‘no point can go from left to right without touching the line’ L 14.4 ).
 262 LAK> e. P: Lemma(‘the process will return to its initial configuration’ L 14.5 ).
 263 LAK> f. P: Lemma(‘each point will be visited infinitely often’ L 14.6 ).
 264 LAK> g. P: ProofDone.
 265 #+END_SRC
 266
 267 #+BEGIN_SRC
 268 IATC> perf[define](init_line, init_line_def)
 269 IATC> rel[structural](init_line_def, forall_split)
 270 IATC> proof_sugg := perf[assert](rel[equivalent](init_turn_by_pi, points_switched_sides))
 271 IATC> perf[assert](problem, proof_sugg, half_thepoints)
 272 IATC> *** or perf[assert](rel[stronger](proof_sugg, problem))???
 273 IATC> perf[assert](rel[instance_of](parallel_line, init_turn_by_pi))
 274 IATC> rel[structural]((init_turn_by_pi, init_line)
 275 #+END_SRC
 276
 277 *GAL*: Very nice! Don’t we run into problems with a convex hull though?
 278 Take a square with a point in the middle (M) and pass the diagonal of
 279 the square (not through M) – it seems to me M is never visited (though
 280 I may be wrong here). I think we should be more specific in our
 281 initial choice of line, maybe?
 282
 283 #+BEGIN_SRC
 284 LAK> h. O: HybridCounter(‘point inside square’, ‘problem statement
 285 holds’, L 14.6 ).
 286 #+END_SRC
 287
 288 #+BEGIN_SRC
 289 IATC> perf[judge](value[beautiful](proof_sugg))
 290 IATC> perf[challenge](proof_sugg, convex_ex_5)
 291 IATC> rel[structural](convex_ex_5, S)
 292 IATC> rel[structural](convex_ex_5, l)
 293 IATC> rel[structural](convex_ex_5, P)
 294 #+END_SRC
 295
 296 *GAL*: No. This example is false :)
 297
 298 #+BEGIN_SRC
 299 LAK> i. P: HybridLemmaInc(‘point inside square’, L 14.6 ,).
 300 LAK> j. P: Conjecture(‘problem statement holds, even for point inside square’).
 301 LAK> k. P: ProofDone.
 302 #+END_SRC
 303
 304 #+BEGIN_SRC
 305 IATC> perf[retract](convex_ex_5)
 306 #+END_SRC
 307
 308 *ZHECKA*: Yes, it seems to be a correct solution!
 309
 310 #+BEGIN_SRC
 311 LAK> [Repetition of previous moves.]
 312 #+END_SRC
 313
 314 #+BEGIN_SRC
 315 IATC> perf[agree](proof_sugg)
 316 IATC> perf[assert](rel[stronger](proof_sugg, problem))
 317 #+END_SRC
 318
 319 *GAL*: This seems to be right, but there something I don’t
 320 understand. Please see if you can help me with it: Start with a square
 321 and a point inside it (M): start with a tangent to the square (your
 322 solution demands a more equal division of points, I know). When we get
 323 to the opposite vertex of the square all points moved from one side of
 324 the line to the other, but not all points have been visited (M will
 325 never be visited). The argu- ment is almost exactly the same, so it
 326 seems that the equal division of points plays a crucial role, but I
 327 don’t understand what role exactly. Can we pin it down pre- cisely?
 328
 329 #+BEGIN_SRC
 330 LAK> O: LocalCounter(‘M is never visited’, L 14.4 ).
 331 #+END_SRC
 332
 333 #+BEGIN_SRC
 334 IATC> perf[assert](half_points_essential, convex_ex_6)
 335 IATC> perf[assert](rel[instance_of](S, convex_ex_6))
 336 IATC> rel[structural](convex_ex_6, l)
 337 IATC> perf[assert](rel[has_property](convex_ex_6, rel[not](has_cycle)))
 338 IATC> perf[assert](rel[has_property](convex_ex_6, points_switched_sides))
 339 IATC> perf[queryE](why_half_points_essentia(X))
 340 IATC> rel[structural](why_half_points_essential, half_points_essential)
 341 #+END_SRC
 342
 343 *GARF*: If I understand well your example: the problem is that you must
 344 give an orientation to the line.  Then, left and right are defined
 345 with respect to this orientation: if the line has made half a turn,
 346 then left and right are reversed. In your example, I think most of the
 347 points move from, say, the part at the top of the line to the part at
 348 the bottom of the line, but always stay at the right of the line.
 349
 350 #+BEGIN_SRC
 351 LAK> m. P: LocalLemmaInc(‘M is never visited’, L 14.4 , ‘left and
 352 right must be reversed after a rotation’).
 353 #+END_SRC
 354
 355 #+BEGIN_SRC
 356 IATC> perf[challenge](rel[has_property](convex_ex_6, points_switched_sides))
 357 #+END_SRC
 358
 359 *GAL*: Got it! Kind of like a turn number in topology.  Thanks! :)
 360
 361 #+BEGIN_SRC
 362 LAK> [Not coded.]
 363 #+END_SRC
 364
 365 #+BEGIN_SRC
 366 IATC> perf[agree](perf[challenge](rel[has_property](convex_ex_6, points_switched_sides)))
 367 #+END_SRC