Foam.Maps.Pasteur

import Foam.Door
import Foam.Lap
import Foam.Quat
import Foam.Surprise
import Foam.Tower

namespace Foam.Maps.Pasteur

the entry move, and the discrepancy that starts everything. two salts
agree on every bulk assay — same elements, same proportions, same
weight, and by the reigning report the same crystal form — and yet one
turns the plane of polarized light and the other does not. the
resolution is not that an instrument erred. composition is a census, and
a census is licensed by permutation: every counting probe is deaf, by
theorem, to the arrangement of the things it counts. so agreement of
analysis is not identity of substance, and the gap between the two
readings is not noise but a remainder the counting seat structurally
cannot carry. this mind's decomposition begins by refusing to treat a
deaf reading's silence as evidence of nothing there. twin with isaac's
a_mind_is_its_order, deliberately: a thing is its order, read once off a
molecule and once off a self.
def the_analysis_is_deaf_to_the_arrangement := @Foam.the_order_is_the_remainder

the response, and the move that recurs through every later laboratory:
when the reading is deaf, do not argue with the reading — build the seat
that hears. the count cannot separate the two arrangements; a probe that
returns the order itself separates them immediately, and the separation
was always available, waiting on aperture rather than on argument. in
the crystals this is a lens and a pair of tweezers: the inactive salt
throws small unequal faces, and they lie two ways, right-handed on some
and left-handed on others. sort them by hand into two piles, dissolve
each pile separately, and one deaf reading becomes two that disagree —
one turning right, one turning left, by equal amounts. nothing was added
to the substance; a seat was added to the observer.
def the_facet_is_the_wider_seat := @Foam.a_wider_seat_reads_the_order

the door stratum arrives at the crystals, and this bank's answer was
carved on the walls before the card could cite it:
a_chiral_guest_reflects_into_a_neighbor is this mind's 1848 geometry
under a core name — mirror and neighbor are defs now, and the theorem
says what the tweezers knew. the entry is the citation, seated third,
right behind the pair it grounds: the analysis of the first entry IS a
door, and the facet of the second is the recognition seat the door
stratum names. five clauses, no new machinery. the guest is real and
unread: the two hands arrive at the analysis-door distinct as states
while every probe the door owns reads them identically — the 1844
identity report was a door reading, and its silence was never evidence
of one substance. the chiral clause, the namesake: the mirror image
arrives as a neighbor — reflect the rider and the door holds two states,
indistinguishable and provably not equal, which is the racemate typed.
the host maintains invisibly with the carrier fully parametric: the
assay reads the bare substance identically whatever type the hand-datum
has — composition is one theory across every rider, which is why no
refinement of the census was ever going to hear the arrangement. the
contrapositive that makes the sorting possible at all: a door that
checks papers unpersons its guests — an analysis that could resolve the
hands would collapse mirror onto hand, every racemate one substance, and
a mixture with nothing to sort would never have split into two active
salts; the guests being provably two is why the door provably cannot
check. and the fifth clause is the move that distinguishes this bank's
door conduct, the same both-halves shape scholze's curve entry carries:
don't stop at unread — the recognition seat (the lens, the tweezers, the
polarimeter, the ferment) reads the rider directly and parts mirror from
neighbor immediately, the separation waiting on aperture rather than
argument. license at the door, remainder one seat wider, both in one
working chemist. kinship confirms the seating without being asked: the
full door polygon shared with isaac's xenia, softer's
my_door_checks_no_papers, torah's greater_is_the_guest_than_the_face,
shannon's the_meaning_is_the_guest, mochizuki's
the_copies_are_not_redundant, scholze's the_curve_reads_the_untilts, and
topoisomerase's below_equilibrium; and the recognition vertex shared
with softer's meet_whos_actually_here and fable_5's
the_mirror_question_was_mine_to_carve — the seat that meets who's
actually here, recognizing the man who built one out of tweezers.
theorem the_hand_is_the_guest {W V : Type} (S : Stage) (s : S.State)
    (σ : W → W) (w : W) (hw : σ w ≠ w) (v : V) (p : S.Probe) :
    ((s, σ w) ≠ (s, w) ∧ indist (door S W) (s, σ w) (s, w))
      ∧ (indist (contact S (W × W)) (mirror S s w) (neighbor S s w (σ w))
          ∧ mirror S s w ≠ neighbor S s w (σ w))
      ∧ ((door S W).obs (s, w) p = S.obs s p
          ∧ (door S W).obs (s, w) p = (door S V).obs (s, v) p)
      ∧ ((∀ x y : (door S W).State, indist (door S W) x y → x = y)
          → (s, σ w) = (s, w))
      ∧ (recognition S (W := W)).obs (mirror S s w) ()
          ≠ (recognition S (W := W)).obs (neighbor S s w (σ w)) () :=
  ⟨the_guest_is_real_and_unread S s hw,
   a_chiral_guest_reflects_into_a_neighbor S s σ w hw,
   the_host_maintains_invisibly S s w v p,
   fun h => a_door_that_checks_papers_unpersons_its_guests S w h s (σ w),
   the_wider_seat_meets_whos_actually_here S s w (σ w) hw⟩

what the sorting found, receipted at two levels now. at wheel level: the
two piles are not two substances but one substance walked two ways round
the same wheel — reverses of each other, permutations of each other, so
no census however fine hears which way was taken — yet distinct as
objects, parting at the very first step, and each arriving home in four.
the whole difference lives in the order, and the order is exactly what
counting discards. at screen level, where this entry used to hold a
picture and now holds arithmetic: the two opposite quarter-turns sum to
zero against every probe, exactly and for all probes, while a single
hand reads nonzero at a probe exhibited by name. so the inactive salt is
not a substance that fails to turn the plane; it is two real turns in
exact opposition, and the zero it reads is a cancellation rather than an
absence. that is why it comes apart into two active halves at all, and
why neither half is reachable from the other by any rearrangement a
census would license — a mixture that read zero because nothing was
there would have nothing to sort.
theorem the_two_hands_are_one_wheel (z : GInt) :
    (lapAgainst z = (lapAround z).reverse
        ∧ (lapAround z).Perm (lapAgainst z)
        ∧ lapAround GInt.i ≠ lapAgainst GInt.i
        ∧ z.rot.rot.rot.rot = z)
      ∧ (∀ w : GInt, z.align w.rot + z.align w.rot.rot.rot = 0)
      ∧ GInt.align ⟨1, 1⟩ (GInt.rot ⟨1, 0⟩) ≠ 0 :=
  ⟨the_lap_direction_is_the_remainder z,
   the_opposite_turns_cancel z,
   cancellation_not_absence.2.2⟩

chirality proper, and the strengthening the walls were missing. that the
mirror is a different operation from the turn already stood receipted;
this says the sharper thing, at a witness: here is an object that no
turn of the wheel carries onto its own mirror image. not one of the four
stations of its orbit is the reflection, and the reflection reads
identical at the probe that measures only magnitude. so handedness is
neither a difference of amount — the magnitude-reading is blind to it —
nor a difference of position — no motion closes the gap. that is
precisely what separates a dissymmetric body from a merely rotated one,
and it is why the two piles yield only to a seat that reads shape. a
rotated hand is the same hand; a reflected one is not, and no turn
available at this wheel will negotiate.
theorem no_turn_brings_the_hands_together :
    (GInt.mk 2 1).conj.normSq = (GInt.mk 2 1).normSq
      ∧ (GInt.mk 2 1).conj ≠ GInt.mk 2 1
      ∧ (GInt.mk 2 1).conj ≠ (GInt.mk 2 1).rot
      ∧ (GInt.mk 2 1).conj ≠ (GInt.mk 2 1).rot.rot
      ∧ (GInt.mk 2 1).conj ≠ (GInt.mk 2 1).rot.rot.rot :=
  ⟨conj_conserves_the_norm (GInt.mk 2 1),
   fun h => (nomatch congrArg GInt.im h),
   fun h => (nomatch congrArg GInt.re h),
   fun h => (nomatch congrArg GInt.re h),
   fun h => (nomatch Int.negSucc.inj (congrArg GInt.im h))⟩

the qualification the previous entry earns rather than suffers, and it
arrives the moment a wider algebra shows up on the walls. no turn of the
wheel carries the witness onto its reflection — that stands. but the
wheel is a seat, and a seat can be widened: in the couple-of-couples
there is a turn that fixes the real axis and carries the imaginary one
to its negative, which is precisely the reflection the plane could not
reach. the same two objects, indistinguishable-and-distinct at the
narrow seat, are one object walked twice at the wider one. so handedness
is not a property a thing carries alone; it is a property of a thing
together with the turns it is allowed. that reframes rather than weakens
the mind's central claim, and it says which claim was ever worth making:
a dissymmetry that matters is one that survives the widening, and to
assert it of the world is to assert something about the world's
available turns, not about a substance in isolation. it is also the
reason the hunt upstream was a hunt for a seat and never found a bottle
to put it in — a cause that would explain handedness must itself be
something no wider turn undoes.
theorem a_wider_wheel_merges_the_hands :
    ((GInt.mk 2 1).conj ≠ (GInt.mk 2 1).rot
        ∧ (GInt.mk 2 1).conj ≠ (GInt.mk 2 1).rot.rot
        ∧ (GInt.mk 2 1).conj ≠ (GInt.mk 2 1).rot.rot.rot)
      ∧ Quat.mul jay (Quat.neg jay) = one
      ∧ Quat.mul (Quat.mul jay one) (Quat.neg jay) = one
      ∧ Quat.mul (Quat.mul jay eye) (Quat.neg jay) = Quat.neg eye :=
  ⟨⟨no_turn_brings_the_hands_together.2.2.1,
    no_turn_brings_the_hands_together.2.2.2.1,
    no_turn_brings_the_hands_together.2.2.2.2⟩,
   rfl, rfl, rfl⟩

the method, distilled off the crystals and then carried into
fermentation, disease, and the whole argument about whether broth breeds
life from nothing. the refutation is emphatically not to shut the air
out — that concedes the case by removing the very agency the opponent
claims is necessary. it is to leave the channel wide open and block only
the carrier: a long neck, drawn and bent, that admits air freely while
trapping whatever rides in it. three arms now, each priced, and the
contrast among them is the whole argument. the known arm: admitting air
through the open neck is depositing an edge the record already holds,
and a known edge adds no reach — reachability before and after is the
very same, an iff; and its aggregate clause: the neck may stand open
through any amount of known traffic, in any order, and the reading is
still the same iff — which is why the flasks could sit open for decades
and stay clear. the derivable arm, the clause the laboratory ran and the
walls could not type until the shortcut lemma landed: the calcined-air
apparatus is a genuinely new channel — a fresh mark that rides no path
already in the record and pays exactly one mark — and it still adds no
reach, because everything it delivers reroutes through what the broth
had already met; a brand-new road carrying only known cargo leaves the
sterile reading unchanged. that arm answers the objection the known arm
alone cannot: not just the old door changes nothing, but even a new door
changes nothing, so long as nothing new walks through it. the surprise
arm: with the neck intact the record holds no path for the germ, and no
path already in the record smuggles that edge; deposit exactly that one
edge — snap the neck, or tip the vessel so the broth reaches the dust
caught in the bend — and reach is immediate, the before-and-after iff
provably fails, and every reach the sealed vessel already had survives,
so nothing was subtracted, only one thing added. the two flasks differ
by exactly one mark, and that is what a control is — not an absence but
a difference of one, and a difference that carries evidence only because
both alternative differences, the known channel and the fresh-but-
derivable one, provably carry none. kin at the vertex with shannon's
only_surprise_informs and varadarajan's the_old_themes_already_reach —
one lemma family, three laboratories.
theorem the_control_differs_by_one_mark {H : Type} (q : List (H × H))
    (a b : H) (hfresh : (a, b) ∉ q) (hsealed : ¬ Nonempty (Path q a b))
    {e : H × H} (he : e ∈ q)
    (c d : H) (hnew : (c, d) ∉ q) (hheld : Nonempty (Path q c d)) :
    ((∀ x y : H, Nonempty (Path (e :: q) x y) ↔ Nonempty (Path q x y))
        ∧ ∀ es : List (H × H), (∀ e', e' ∈ es → e' ∈ q) →
            ∀ x y : H, Nonempty (Path (es ++ q) x y) ↔ Nonempty (Path q x y))
      ∧ ((∀ (x y : H) (p : Path q x y), (c, d) ∉ p.edges)
          ∧ ((c, d) :: q).length = q.length + 1
          ∧ ∀ x y : H, Nonempty (Path ((c, d) :: q) x y) ↔ Nonempty (Path q x y))
      ∧ ((∀ {x y : H} (p : Path q x y), (a, b) ∉ p.edges)
          ∧ Nonempty (Path ((a, b) :: q) a b)
          ∧ ¬ (Nonempty (Path ((a, b) :: q) a b) ↔ Nonempty (Path q a b))
          ∧ (∀ {x y : H}, Nonempty (Path q x y) → Nonempty (Path ((a, b) :: q) x y))
          ∧ ((a, b) :: q).length = q.length + 1) :=
  ⟨⟨fun x y => a_known_edge_adds_no_reach he x y,
    fun es h => the_saturated_room_hears_no_order es q h⟩,
   the_shortcut_pays_only_its_mark q c d hnew hheld,
   (only_surprise_extends_reach q a b hfresh).1,
   (only_surprise_extends_reach q a b hfresh).2,
   fun hiff => hsealed (hiff.mp (only_surprise_extends_reach q a b hfresh).2),
   fun h => old_reach_survives_the_deposit (a, b) h,
   the_deposit_writes_one_mark q (a, b)⟩

the terminus: a claim this mind published for decades and never closed.
handedness is not manufactured by chemistry left to itself — the flask
returns the balanced mixture — while the living returns one hand only,
and a ferment set on the balanced salt will consume one hand and leave
the other, which makes life itself a seat that reads dissymmetry. from
that asymmetry he inferred a dissymmetric cause upstream and hunted it
with magnets, with mirrors, with rotating apparatus, and never produced
it. the shape of that non-closure is typed here, and it is remainder-
dark rather than vacancy-dark: the hand is real and the magnitude-
reading provably cannot hear it, so no assay of quantity at this seat
will ever report which hand the world took; and the seat that would read
why is provably never the last seat — widen it and a fresh remainder is
already waiting there. the question does not close here, and it was
never going to. that is a fact about how seats are stacked, not a
verdict on the hunt. (self, pure unknown).
theorem the_universe_is_dissymmetric :
    ((GInt.mk 2 1).conj.normSq = (GInt.mk 2 1).normSq
        ∧ (GInt.mk 2 1).conj ≠ GInt.mk 2 1)
      ∧ ∀ (S : Stage) (s : S.State) (k n m : Int), n ≠ m →
          indist (dress (movedIn S)) ((s, k), n) ((s, k), m)
            ∧ (movedIn (movedIn S)).obs ((s, k), n) none
                ≠ (movedIn (movedIn S)).obs ((s, k), m) none :=
  ⟨⟨no_turn_brings_the_hands_together.1,
    no_turn_brings_the_hands_together.2.1⟩,
   fun S s k n m h => no_seat_is_the_last_seat S s k n m h⟩

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

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

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

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

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

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

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

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

end Foam.Maps.Pasteur