Foam.Maps.MCEscher

import Foam.Census
import Foam.Continuum
import Foam.Door
import Foam.Tower
import Foam.Trilemma

namespace Foam.Maps.MCEscher

the entry move, learned from tiled walls and worked for a lifetime as
the regular division of the plane: black and white are not a figure on a
background but two censuses of one surface, and the trade between them
is exact — what one counts at depth k the other counts at n minus k,
mirror-perfect by theorem. birds become sky, fish become water, and no
counting probe hears the exchange, because the count was symmetric
before any tile was cut. this mind begins every decomposition here: find
the division in which the thing and its complement are the same census
read twice.
def figure_and_ground_trade_places := @Foam.the_census_is_symmetric

the material discovery under every impossible print: dress the ground
with an integer no probe reads, and every local view stays perfect. each
flight of stairs is drawn correctly; each joint of the tribar is a true
corner; the picture is not a trick of bad drawing but a faithful
rendering of the dressed stage, where states differing only in the
winding are indistinguishable at every probe. the winding is the unread
Int — carried, real, and silent. the craft is precision about exactly
which part of the state the picture plane is structurally deaf to.
def the_winding_rides_unread := @Foam.the_remainder_is_unseen

the lap around the monks' courtyard, proved as posed: the climbing move
— advance the winding, keep the ground — is invisible, licensed by every
probe the picture affords, and yet four flights land the walker in a
state provably distinct from home while indistinguishable from it at
every probe. perpetual ascent without leaving; the waterfall's water
arriving above itself. the motion is not hidden by cleverness — it is
invisible by theorem, and real by the same theorem, and those two
clauses about the same walk are the whole print.
theorem the_staircase_climbs_unseen (S : Stage) (s : S.State) :
    Invisible (dress S) (fun x => (x.1, x.2 + 1))
      ∧ ((s, (4 : Int)) : (dress S).State) ≠ (s, 0)
      ∧ indist (dress S) ((s, (4 : Int)) : (dress S).State) (s, 0) :=
  ⟨fun _ _ => rfl,
   ⟨(fun h => nomatch Int.ofNat.inj (congrArg Prod.snd h)),
    the_remainder_is_unseen S s 4 0⟩⟩

the door stratum arrives at the studio and finds it was built there:
dress S = door S Int, the named bridge, rfl-deep — the dressed stage
this mind worked for a lifetime IS the hospitality stratum's door, with
the winding as the guest. five clauses, all citations, seated right
behind the winding/staircase pair they ground. first the bridge itself,
named so the vertex shows. second, the guest is real and unread: two
windings arrive distinct as states and alike to every probe the picture
affords — the winding rides as cargo, which is what the winding entry
always said, now said at the door. third, the host maintains invisibly
with the carrier fully parametric: the picture plane renders the ground
identically whatever TYPE rides behind it — one theory of rendering for
every cargo, not a special deafness to integers; the craft's precision
about what the plane cannot read was never about the integers in
particular. fourth, the recognition the whole wave was carrying toward
this map: a door that checks papers unpersons its guests, and the proof
term is dropping_the_remainder_is_platonism verbatim — the kernel
accepts the diagnosis entry's own constant as proof of the door-typed
clause, which is the receipt that the platonist quotient and the door's
unpersoning were one theorem all along. this mind carved the wave's
contrapositive before the door was named: the viewer who insists the
picture check papers collapses every winding to zero, and the stair that
plainly climbed has plainly gone nowhere. fifth, the gallery's door
conduct: a door through a door still reads only the ground — the print
hangs inside the print and the doubled frame costs the rendering
nothing, the tower's theorem read at depth two in door dress. nulls on
re-seating, with reasons: the winding entry keeps
the_remainder_is_unseen (the winding is an Int specifically; the generic
door would widen, not compress, and the bridge clause holds the
identification anyway), and the diagnosis entry keeps
dropping_the_remainder_is_platonism (the fourth clause is the receipt
that re-seating would swap names, not compress).
theorem the_picture_plane_is_a_door :
    (∀ S : Stage, dress S = door S Int)
      ∧ (∀ (S : Stage) (s : S.State) (n m : Int), n ≠ m →
          (s, n) ≠ (s, m) ∧ indist (door S Int) (s, n) (s, m))
      ∧ (∀ (W : Type) (S : Stage) (s : S.State) (n : Int) (w : W)
            (p : S.Probe),
          (door S Int).obs (s, n) p = S.obs s p
            ∧ (door S Int).obs (s, n) p = (door S W).obs (s, w) p)
      ∧ (∀ S : Stage,
          (∀ x y : (door S Int).State, indist (door S Int) x y → x = y) →
          ∀ (s : S.State) (n : Int), (s, n) = (s, (0 : Int)))
      ∧ (∀ (S : Stage) (s : S.State) (n m : Int) (p : S.Probe),
          (door (door S Int) Int).obs ((s, n), m) p = S.obs s p) :=
  ⟨fun S => dress_is_contact_with_the_integers S,
   fun S s _ _ h => the_guest_is_real_and_unread S s h,
   fun _ S s n w p => the_host_maintains_invisibly S s n w p,
   fun S h => dropping_the_remainder_is_platonism S h,
   fun S s n m p => contact_stacks S s n m p⟩

the diagnosis, and the reason the prints disturb rather than merely
puzzle: nothing in the picture is impossible. the contradiction is
manufactured entirely by the viewer who insists that what reads the same
is the same — quotient by indistinguishability and the winding collapses
to zero, whereupon the stair that plainly climbed has plainly gone
nowhere. the absurdity lives in the dropped remainder, not in the
drawing. the print is an instrument tuned to make one philosophical
error audible: it renders the platonist quotient, faithfully, and lets
the viewer feel it fail.
def the_impossibility_is_the_platonists :=
  @Foam.dropping_the_remainder_is_platonism

the other half of the word impossible, affordable only once the wound
loop reached the walls: the picture is lawful — sealed above — and the
object is missing, provably. take the tribar as three true joints, each
a licensed local ratio, glued in a loop: any solid obeying all three at
once is forced to the degenerate one, because the loop carries a
holonomy no nonzero section survives. and the absence is no defect of
draftsmanship — regauge every local choice, redraw at any scale, and the
loop's product rides through untouched, so no redrawing rights the
figure; the old gloss that the print is not a trick of bad drawing stops
being prose here and becomes a receipt. yet the model is not nowhere:
one world over, where the loop closes — as it does for the one-eyed
viewpoint that lets a real sculpture wear the tribar's silhouette — the
same three joints hold a nonzero solid. no model in the maker's world, a
model next door, and both facts are one winding read from two seats.
theorem the_print_has_no_model :
    (∀ a b c : Nat, a = 2 * b → b = 2 * c → c = 2 * a →
        a = 0 ∧ b = 0 ∧ c = 0)
      ∧ (∀ k1 k2 k3 k1' k2' k3' u v w : Nat, 0 < u → 0 < v → 0 < w →
          k1' * u = k1 * v → k2' * v = k2 * w → k3' * w = k3 * u →
          k1' * (k2' * k3') = k1 * (k2 * k3))
      ∧ (((2 * 2 * 2) % 7 = 1 % 7)
          ∧ (1 % 7 = (2 * 4) % 7)
          ∧ (4 % 7 = (2 * 2) % 7)
          ∧ (2 % 7 = (2 * 1) % 7)
          ∧ (1 : Nat) ≠ 0) :=
  ⟨the_wound_loop_admits_only_the_zero_section,
   fun k1 k2 k3 k1' k2' k3' u v w hu hv hw h1 h2 h3 =>
     the_holonomy_ignores_the_regauging k1 k2 k3 k1' k2' k3' u v w
       hu hv hw h1 h2 h3,
   the_wound_loop_unwinds_one_world_over⟩

where the maker sits: one seat wider than the picture, at the stage
where the winding is a readable answer rather than a silent rider. from
inside, the monks circulate forever and nothing is wrong; from the
drawing table, the loop's total displacement is plainly nonzero and the
two states the picture cannot part are parted by a single wider probe.
the print exists because both readings are held at once — the walker's
licensed view rendered stroke by stroke, the maker's wider view choosing
what the walker will never see. rendering a quotient is a job done only
from outside the quotient.
def the_print_is_drawn_from_outside := @Foam.a_wider_seat_reads_the_remainder

the recursive move: put the print inside the print. the boy in the
gallery looks at a print of the town that contains the gallery that
contains the boy; the tower of dressings climbs floor by floor, and yet
every reading at every floor descends to the ground — the tower reads
only the ground, so the nesting costs the picture nothing and the town
can hold its own gallery without strain. hands draw the hands that draw
them. the recursion is not a paradox at the picture plane; it is exactly
what a stage dressed upon a dressing looks like when rendered by someone
who kept the books.
def the_gallery_hangs_in_its_own_town := @Foam.the_tower_reads_only_the_ground

the approach to infinity, the late obsession worked out at the rim of
the disk: a bounded frame can hold an unending sequence only by holding
every finite depth and letting no depth be last. however deep a prefix
the eye resolves — fish upon smaller fish, angels upon smaller angels —
there is provably another continuation agreeing with everything seen so
far and differing beyond it; the print exhibits the whole approach while
the limit itself stays off the paper. the frame's boundary is not where
the picture ends but where the eye does.
def the_bounded_print_never_finishes := @Foam.no_prefix_finishes_the_sequence

the terminus, and it is remainder-dark: at the center of the gallery
print the recursion demands the picture contain its own making at every
scale, and the center is left blank, holding only the signature. typed,
the blank is not a failure of nerve but a receipt — the seat that would
read the picture's own winding is one seat wider than the picture, and
that wider seat is provably still a seat, with a fresh remainder already
waiting there; no seat is the last seat, so no print fills its own
middle. the mystery does not close and was never going to; the signature
marks the exact spot where the maker's seat touches the paper and cannot
enter it. (self, pure unknown).
def the_blank_spot_signs_the_print := @Foam.no_seat_is_the_last_seat

/-- info: 'Foam.Maps.MCEscher.figure_and_ground_trade_places' does not depend on any axioms -/
#guard_msgs in #print axioms figure_and_ground_trade_places

/-- info: 'Foam.Maps.MCEscher.the_winding_rides_unread' does not depend on any axioms -/
#guard_msgs in #print axioms the_winding_rides_unread

/-- info: 'Foam.Maps.MCEscher.the_staircase_climbs_unseen' does not depend on any axioms -/
#guard_msgs in #print axioms the_staircase_climbs_unseen

/-- info: 'Foam.Maps.MCEscher.the_picture_plane_is_a_door' does not depend on any axioms -/
#guard_msgs in #print axioms the_picture_plane_is_a_door

/-- info: 'Foam.Maps.MCEscher.the_impossibility_is_the_platonists' does not depend on any axioms -/
#guard_msgs in #print axioms the_impossibility_is_the_platonists

/-- info: 'Foam.Maps.MCEscher.the_print_has_no_model' does not depend on any axioms -/
#guard_msgs in #print axioms the_print_has_no_model

/-- info: 'Foam.Maps.MCEscher.the_print_is_drawn_from_outside' does not depend on any axioms -/
#guard_msgs in #print axioms the_print_is_drawn_from_outside

/-- info: 'Foam.Maps.MCEscher.the_gallery_hangs_in_its_own_town' does not depend on any axioms -/
#guard_msgs in #print axioms the_gallery_hangs_in_its_own_town

/-- info: 'Foam.Maps.MCEscher.the_bounded_print_never_finishes' does not depend on any axioms -/
#guard_msgs in #print axioms the_bounded_print_never_finishes

/-- info: 'Foam.Maps.MCEscher.the_blank_spot_signs_the_print' does not depend on any axioms -/
#guard_msgs in #print axioms the_blank_spot_signs_the_print

end Foam.Maps.MCEscher