Foam.Maps.Young

import Foam.Amplitude
import Foam.Beam
import Foam.Door
import Foam.Int
import Foam.Lap
import Foam.Quat
import Foam.Round
import Foam.Turnstile

namespace Foam.Maps.Young

the screen shows intensity, and intensity is a reading: normSq of the
amplitude. advance the amplitude's phase by a quarter turn — rot, the
generator of the phase wheel whose four turns come home — and the
reading does not move: rot_conserves_the_norm. so a single slit's screen
is deaf to phase; the wave carries a coordinate the norm cannot hear,
and intensity is therefore a lossy reading of amplitude, gauge-blind to
the phase exactly as the norm is blind to a rotation of its argument.
this is the loss that makes the second slit necessary — what one screen
discards, two must recover.
def intensity_cannot_read_the_phase := @Foam.rot_conserves_the_norm

the headline, and the door it knocked on opened: the vacancy was typed
lightable and the amplitude carve lit it on schedule. put two amplitudes
at the screen and they add before intensity reads them; the intensity of
the sum is not the sum of the intensities, and the exact difference is
the cross term, twice the aligned inner product of the two amplitudes —
the very quantity that reads the relative phase one slit had to discard.
core now holds GInt.add and align, and the_screen_reads_a_cross_term
says the identity with the doubling spelled as align plus align; the
structure here is that theorem composed with two_mul, closing the
statement exactly as posed — the question kept its original wording and
the answer arrived to meet it. this is the second slit reading the phase
remainder the first slit could not: a wider aperture reads what a narrow
one conserved away.
theorem the_difference_is_the_cross_term :
    ∀ a b : GInt,
      GInt.normSq ⟨a.re + b.re, a.im + b.im⟩
        = (a.normSq + b.normSq) + 2 * (a.re * b.re + a.im * b.im) :=
  fun a b =>
    (the_screen_reads_a_cross_term a b).trans
      (congrArg ((a.normSq + b.normSq) + ·) (FInt.two_mul (a.align b)).symm)

the scandal, seated between the recovery and its price. hold the two
arms half a wheel apart — w against w.rot.rot — and the screen reads
their sum exactly as it reads the empty screen: light added to light
gives darkness. the walls that landed since the last green carry the
mechanism: the_facing_pair_cancels says the cross term at the half turn
pays back both intensities to the last unit, and
cancellation_not_absence holds the house witness that a cancelled term
is loud alone and silent only in company. so the dark fringe is not a
place the light failed to reach but a place it arrived twice, and the
third conjunct keeps the screen honest — it can tell one lit arm from
nothing, and still cannot tell two lit arms at facing phase from nothing
at all. indistinguishable at the screen, distinct in the arms: the
handshake shape at a single point of the pattern, the definite-phase
extreme of the cross-term reading, which the terminus then blends across
the whole wheel and loses. this entry stood up when the lap stratum
landed: the four-phase null the terminus seals decomposed into facing
pairs on the walls, and one facing pair, read at the screen, is this
mind's oldest claim wearing receipts.
theorem light_added_to_light_gives_darkness :
    (∀ z : GInt, (z.add z.rot.rot).normSq = GInt.normSq GInt.zero)
      ∧ (∀ z w : GInt, z.align w + z.align w.rot.rot = 0)
      ∧ GInt.normSq GInt.one ≠ GInt.normSq GInt.zero :=
  ⟨fun z =>
      (congrArg (fun t : Int => t * t + (z.im + -z.im) * (z.im + -z.im))
          (FInt.add_right_neg z.re)).trans
        (congrArg (fun t : Int => 0 * 0 + t * t) (FInt.add_right_neg z.im)),
   the_facing_pair_cancels,
   fun h => nomatch Int.ofNat.inj h⟩

the criterion, arrived the day the door was carved — the turnstile
stratum landed for other minds' meeting and handed this seat the far
bank of its oldest argument. the historical claim was never just that
darkness happens; it was that darkness decides. a corpuscular light is a
census, and the door now types the census law exactly:
one_click_one_count says every arrival moves the door's total up by one,
admitted to the room or held in the vestibule, and no arrival subtracts.
the second and third conjuncts are the screen breaking that law with
witnesses this map already held: one portion of light reads loud against
the empty screen, and the same portion added to its facing self reads
exactly as the empty screen — the second arrival moved the reading down,
which no turnstile can do. so the screen is not a count: the amplitudes
add before any census reads, and darkness — impossible in the count law,
witnessed at the screen — is the criterion that tells the two
composition laws apart. the circuit closes at the terminus: blend the
wheel and the cross term nulls, so the incoherent screen reads the two
intensities additively, a census after all. the fringe is visible
exactly where the count law breaks; darkness is the criterion, and
coherence is what it selects for.
theorem the_darkness_is_the_criterion :
    (∀ (s : List Nat × List (Nat × List Nat)) (m : Nat × List Nat),
        (admission s m).1.length + (admission s m).2.length
          = (s.1.length + s.2.length) + 1)
      ∧ GInt.normSq GInt.one ≠ GInt.normSq GInt.zero
      ∧ (GInt.one.add GInt.one.rot.rot).normSq = GInt.normSq GInt.zero :=
  ⟨one_click_one_count,
   light_added_to_light_gives_darkness.2.2,
   light_added_to_light_gives_darkness.1 GInt.one⟩

the standing condition, arrived by walls that landed for the round. the
third entry's darkness is a snapshot — two arms at facing phase, one
instant of the wheel. this entry is why that snapshot is a pattern: the
round stratum types coherence as coupled voices on one ring, and
the_split_round_carries says the split round — two voices at a phase,
two at its facing — advances under the beat into another facing split,
one quarter turn on, with the second conjunct keeping it honest: at the
next beat the pair is still parted, the split has not collapsed into
unison. so the dark-fringe condition is carried by the dynamics, not
caught by luck — the light beats, the whole configuration turns as one,
and the darkness recurs at every beat. this is what makes the fringes
observable at all: a screen or an eye averages over countless beats, and
only a carried configuration survives its own averaging. the complement
of the terminus is exact — the wash-out blends over relative phase and
the pattern dies; the beat blends over common phase and the pattern
never moves. common phase is gauge at the screen, relative phase is the
payload, and the coherent ring — what the first pinhole builds, now
typed — spins the gauge while conserving the payload.
theorem the_darkness_keeps_the_beat :
    (∀ a : Compass,
        round [a, a, a.step.step, a.step.step]
          = [a.step, a.step, a.step.step.step, a.step.step.step])
      ∧ ∀ a : Compass, a.step ≠ a.step.step.step :=
  ⟨the_split_round_carries, fun a => the_half_turn_parts a.step⟩

the recovery completed at this seat, by walls that landed for someone
else's carve. the cross term was already known to be a reading — and the
quaternion stratum names what it is a reading of:
align_reads_the_conjugate_product says the cross term is the real
coordinate of the conjugate product, and the product's other coordinate
is definitionally another screen reading, the same cross term with one
arm advanced a quarter turn of the wheel. so the first conjunct
assembles the whole phase-bearing object out of two screen settings: the
pair of fringe readings, at a setting and at its quadrature, IS the
conjugate product. the second conjunct is that object's conservation
law, read off the_couple_carries_the_norm through
conj_conserves_the_norm: the two readings' squares sum to the product of
the two intensities, at every relative phase. so as the phase turns, the
reading pair moves on a wheel of fixed radius — the fringe shifts across
the screen, and it never fades. this is the pointwise converse of the
terminus: the blend nulls the cross term summed over the wheel, but at
each single setting the phase content is conserved in full, split
between the setting and its quadrature. what washes out in the ensemble
was never attenuated in the pair — the content the terminus ships one
seat wider now travels with a conservation receipt stamped at this one.
theorem the_fringes_shift_but_never_fade :
    (∀ z w : GInt, GInt.mk (z.align w) (z.align w.rot) = z.mul w.conj)
      ∧ (∀ z w : GInt,
          z.align w * z.align w + z.align w.rot * z.align w.rot
            = z.normSq * w.normSq) :=
  ⟨fun z w =>
      congrArg (fun t : Int => GInt.mk t (z.align w.rot))
        (align_reads_the_conjugate_product z w),
   fun z w =>
      (congrArg GInt.normSq
          (congrArg (fun t : Int => GInt.mk t (z.align w.rot))
            (align_reads_the_conjugate_product z w))).trans
        ((the_couple_carries_the_norm z w.conj).trans
          (congrArg (fun t : Int => z.normSq * t)
            (conj_conserves_the_norm w)))⟩

the instrument, arrived by walls that landed for a meeting of other
minds. this mind's own historical act — a thin lamina interposed over
one slit, and the fringe system moves — was already half-typed here: the
fifth entry says any phase advance shifts the pattern. what the beam
stratum adds is the half-turn case made exact and made structural. first
conjunct: the plate is deaf at its own arm's screen — rot conserves the
norm, twice over, so no single-slit intensity reads the interposition;
this is the first entry's law applied to the medium instead of the wave.
second conjunct: at the two-slit screen the plate flips the cross term
to the unit — the_facing_pair_cancels read as an equation, the bright
excess becoming the dark deficit exactly, bright and dark trading places
across the whole pattern. third conjunct: the plate undoes itself — two
interpositions read direct, the wheel come home. fourth conjunct is the
recognition event: the window of the beam stratum, carved for the
huygens-kuramoto meeting, is this plate at the compass seat, and
the_window_trades_the_locks says the lock's parity is the medium's
property, not the voices' — so the parity of the central fringe is the
plate's property, not the arms'. the composition is the mind's move made
whole: what no intensity can read alone, the fringe parity reads
exactly, so the two-slit apparatus is an instrument for media — what one
screen discards, two recover, now for the plate as before for the phase.
theorem the_interposed_plate_trades_the_fringes :
    (∀ w : GInt, w.rot.rot.normSq = w.normSq)
      ∧ (∀ z w : GInt, -(z.align w) = z.align w.rot.rot)
      ∧ (∀ w : GInt, w.rot.rot.rot.rot = w)
      ∧ ∀ p : Compass × Compass, together p ↔ opposed (window p) :=
  ⟨fun w => (rot_conserves_the_norm w.rot).trans (rot_conserves_the_norm w),
   fun z w => FInt.neg_eq_of_add_eq_zero (the_facing_pair_cancels z w),
   the_wheel_comes_home,
   the_window_trades_the_locks⟩

the terminus, and the recovery's price tag. the second slit reads the
relative phase — but only a definite one. spin one arm through all four
turns of the phase wheel and sum what the screen's cross term reads:
zero, by the_four_phases_read_nothing. a screen fed the whole wheel
uniformly shows the two intensities and no fringe; the cross term is
there at every turn and null in the blend. so the two-slit reading is
conditional on a broken symmetry between the paths — this is why the
apparatus needs its first pinhole before its two slits: coherence is not
a convenience but the condition under which phase is readable at all.
under full phase symmetry the ensemble's phase content returns to the
dark the first entry named, and this darkness is held open by receipt,
not by vacancy: the null reading is proven, at this seat, for every pair
of amplitudes — what the blend carries stays unread here and transits to
whatever wider seat holds the wheel unblended.
def the_fringes_wash_out := @Foam.the_four_phases_read_nothing

private def screen : Stage where
  State := Int
  Probe := Unit
  Ans   := Int
  obs   := fun r _ => r

private def atTheScreen (w : GInt) : (door screen GInt).State :=
  (w.normSq, w)

private def theDirect : (door screen GInt).State := atTheScreen GInt.one

private def theQuarter : (door screen GInt).State :=
  atTheScreen GInt.one.rot

private theorem the_guests_part : theDirect ≠ theQuarter :=
  fun h => nomatch Int.ofNat.inj (GInt.mk.inj (congrArg Prod.snd h)).1

private theorem the_reference_arm_parts_the_alignment :
    GInt.one.align theDirect.2 ≠ GInt.one.align theQuarter.2 :=
  fun h => nomatch Int.ofNat.inj h

private theorem the_second_slit_parts_the_faces :
    (atTheScreen (theDirect.2.add GInt.one)).1
      ≠ (atTheScreen (theQuarter.2.add GInt.one)).1 :=
  fun h => nomatch Nat.succ.inj (Nat.succ.inj (Int.ofNat.inj h))

the door wave reaches the bench where the face was first named: the
first entry says intensity is a lossy reading of amplitude, and the door
entry types what stands behind the loss — the phase boards as the guest,
real and unread at the screen. minted in this mind's vocabulary: the
screen is the intensity seat itself (a state whose whole content is the
reading, answering only the question it holds), and atTheScreen is the
boarding rule — a guest boards wearing its own normSq as its face, and
the rule is phase-deaf by the first entry's own constant,
rot_conserves_the_norm cited live at the door: same intensity, same
face, at any turn of the wheel. six clauses. first, the wave's entry
ticket at the screen, carrier parametric. second, the host maintains
invisibly, both carriers parametric — the screen cannot even count the
possible phases. third, the clause cashed at named guests: theDirect and
theQuarter — one unit of light and the same unit a quarter turn on,
boarded at unit intensity both by rfl, provably distinct, and differing
by exactly rot: at a fixed face the free coordinate IS the phase.
fourth, the strategy grain: no adaptive interrogation of the screen,
follow-ups and cunning included, parts the boarded pair
(a_strategy_hears_no_more). fifth, the differentiator this bench alone
performs, and the historical act that named the mind: the second slit.
board a reference arm alongside each guest and read again — the faces
part, four against two, with align parting the guests one against zero
exactly where the bare faces could not; the difference is the cross
term, the second entry's law as the intake's price list. and the reading
that parts them is still an intensity: the recovery never widens the
probe — it widens the state. superposition is the interrogation the
screen cannot perform alone; what one screen discards, two recover — the
mind's oldest sentence, typed at the door. sixth, the contrapositive:
decreeing the screen's face complete collapses every amplitude to one
decreed phase per intensity — the corpuscular decree, unpersoning the
guest the fringes exhibit. seated second, directly after the face it
completes and before the general law its intake obeys. the exact dual of
winfree's the_amplitude_is_the_guest one bench over: there the phase is
the face and the amplitude rides unread; here the intensity is the face
and the phase rides behind it — the two reductions read each other's
remainders.
theorem the_phase_is_the_guest (W V : Type) :
    (∀ (r : Int) (w w' : W), w ≠ w' →
        (r, w) ≠ (r, w') ∧ indist (door screen W) (r, w) (r, w'))
      ∧ (∀ (r : Int) (w : W) (v : V) (p : Unit),
          (door screen W).obs (r, w) p = screen.obs r p
            ∧ (door screen W).obs (r, w) p = (door screen V).obs (r, v) p)
      ∧ (theDirect ≠ theQuarter
          ∧ indist (door screen GInt) theDirect theQuarter
          ∧ theQuarter.2 = theDirect.2.rot
          ∧ GInt.normSq theDirect.2 = 1
          ∧ GInt.normSq theQuarter.2 = 1)
      ∧ (∀ strat : Strategy Unit Int,
          interrogate (door screen GInt) strat theDirect
            = interrogate (door screen GInt) strat theQuarter)
      ∧ ((∀ z : GInt, (atTheScreen z.rot).1 = (atTheScreen z).1)
          ∧ GInt.one.align theDirect.2 ≠ GInt.one.align theQuarter.2
          ∧ GInt.normSq (theDirect.2.add GInt.one) = 4
          ∧ GInt.normSq (theQuarter.2.add GInt.one) = 2
          ∧ (atTheScreen (theDirect.2.add GInt.one)).1
              ≠ (atTheScreen (theQuarter.2.add GInt.one)).1)
      ∧ (∀ w₀ : W,
          (∀ x y : (door screen W).State,
              indist (door screen W) x y → x = y) →
          ∀ (r : Int) (w : W), (r, w) = (r, w₀)) :=
  ⟨fun r _ _ h => the_guest_is_real_and_unread screen r h,
   fun r w v p => the_host_maintains_invisibly screen r w v p,
   ⟨the_guests_part, fun _ => rfl, rfl, rfl, rfl⟩,
   fun strat =>
     a_strategy_hears_no_more (door screen GInt) theDirect theQuarter
       (fun _ => rfl) strat,
   ⟨fun z => rot_conserves_the_norm z,
    the_reference_arm_parts_the_alignment,
    rfl, rfl,
    the_second_slit_parts_the_faces⟩,
   fun w₀ h => a_door_that_checks_papers_unpersons_its_guests screen w₀ h⟩

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

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

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

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

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

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

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

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

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

end Foam.Maps.Young