連休にやってたこと
連休に写真の整理をした。具体的には、ハードディスク中の写真を Google Photo にアップしたのである。
jpeg 形式の写真ファイルの中には、それがいつ撮影されたかを示すデータが含まれている。Google Photo に写真をアップすると、これをもとにしてフォト・ライブラリに時系列順に並んで収められる。私はむかしの写真をながめつつ、アップロード作業を楽しんでいた。
ところが、そのうちいくつかの写真は撮影日時と時刻が誤っていることに気づいた。何かの拍子にカメラの中の時計が狂ってしまい、そのまま何ヵ月か撮影を続けたらしい。そうした写真が 200 枚以上あった。これらの写真については、ファイルの中の撮影時刻の情報を書き換える必要がある。
問題は、それぞれの写真の正しい撮影時刻はいつなのか、ということだ。
一連の写真ファイルに記録されている撮影時刻は、いずれも正しい撮影時刻と同じだけの時間ズレていると思われる。したがって、これらの写真の中に一枚でも撮影年・月・日・時・分がわかる内容が写っているものを見つければ話は簡単なのである。しかし、そう都合のよい写真はない。
そこで私は 2 枚の写真に注目した。一枚は、雪が降っている写真Aで、それが何月何日に撮影されたのかは日記を参照して知ることができる。ただ、撮影時刻はわからない。もう一枚は、時計が写っている写真Bで、撮影時刻を知ることはできるが、それがいったい何月何日に撮影されたものなのかはわからない。
果たしてこの 2 枚の写真から撮影日時がどれだけズレているか決めることができるだろうか。直感的にはできそうだと思うが、直観では人を説得できないし間違いも起こりうる。そこで素朴な計算を試みた。
まず、\(x\) を「記録された日時分\(+x\)分=正しい日時分」とする。そして、写真 A, B から \(x\) が満たすべき条件を求め、解がちょうど 1 つ求められるかどうか調べることにする。
まず、写真 A から、
\(\bbox{2月27日0時0分} \le\ \bbox{1月7日20時23分} + x \bbox{分間} < \bbox{2月28日0時0分} ...\bbox{①}\)
という、\(x\) にかんする条件が得られる。また、写真 B から
\(\exists n (n \in Z \wedge \bbox{16 時 22 分} = \bbox{2 時 1 分} + x 分間 + n \times \bbox{24時間})...\bbox{②}\)
という、やはり \(x\) にかんする条件が得られる。(\(n\) は \(\exists\) の中から出てこないので、この式は \(n\) に対する条件にはなっていない)
時刻をすべて 1 月 1 日 0 時 0 分からの経過分に直して整理すると、
\(72217 \le x < 73657 ... \bbox{①}'\)
\(\exists n (n \in Z \wedge 861 = x + 1440 n) ... \bbox{②}'\)
\(\bbox{①}'\) には \(n\) が含まれていないので、これを \(\bbox{②}'\) の \(\exists n\) の支配域の中に入れて 1 つにまとめると
\(\exists n (n \in Z \wedge 861 = x + 1440 n \wedge 72217 \le x < 73657) ... \bbox{③}\)
\(x = 861 - 1440n\) を \(72217 \le x < 73657\) に代入して
\(\exists n (n \in Z \wedge x = 861 - 1440 n \wedge 71356 \le -1440n < 72796) ... \bbox{③}'\)
となる。\(n \in Z\) のもとで不等式を解くと \(n=-50\) であるから
\(\exists n (x = 861 - 1440 n \wedge n=-50) ... \bbox{③}''\)
であり、ようするに \(n\) は \(x\) が
\(x = 861 + 1440 \times 50\)
を満たすときに限って存在する。したがって、
\(x=72861\)
これは、50日14時間21分に当たる。つまり、写真ファイルに記録されている撮影日時分を、それだけの時間進めればよいというわけだ。