Foam.Maps.Wigner

import Foam
import Foam.Amplitude
import Foam.Beam
import Foam.Bench
import Foam.Concentration
import Foam.Quat
import Foam.Rungs
import Foam.Tower
import Foam.Width

namespace Foam.Maps.Wigner

the method half of the 1931 theorem, the part that survives the stripped
stage: define a symmetry purely observationally — a move conserving
every reading — and implementation follows with nothing installed by
hand; the operator is derived, never postulated. lifted to core at the
survey's first isaac-wigner recognition: the statement is identical to
isaac's safe_to_rest — a symmetry is a move it is safe to rest through;
rest and invariance, one shape, two lives.
def invariance_already_implements := @Foam.invisible_is_gauge

the headline, compiled: the amplitude stratum landed and the vacancy
closed exactly as posed — the openness was falsifiable by that carve,
and the carve falsified it. every conserver of the readings arrives in
exactly one of two kinds, straight or conjugated, and the receipt holds
the whole dichotomy in miniature on the smallest wheel the amplitudes
ride: both kinds conserve the norm — the reading neither can touch — the
two kinds anticommute, so the second is not deformable to the first, and
the kinds are provably two at the witness i, where rotation and
conjugation visibly part. two conjugations compose to a straight move
(the involution comes home), which is why the second kind is a kind and
not an error. this was the fifth knock at the amplitude door — shannon
by measure, brouwer by continuity, gauss by error, isaac by attention,
wigner by symmetry — and it answered first, as predicted: the classifier
of the machinery arrived with the machinery, one flip measuring the
stratum.
def unitary_or_antiunitary := @Foam.two_kinds_conserve_the_norm

1932, the paper that gave the second kind its job: the operation of time
reversal, posed observationally, arrives conjugated — the branch of his
own dichotomy that had read as a formal alternative turns out to be the
one that runs time backward. the walls could not hold this until the
beam stratum landed: a law and its conjugate as first-class objects, the
medium's half-turn as the conjugator. the receipt is the operation's
full second-kind signature, every clause already on the walls: the
reversal is an involution — two of it come home, so it is a kind and not
an error, the wheel's oldest law arriving at the dynamics stratum;
through the window the conjugated law reads direct — the sandwich
collapses, conjugation is implementation, not doctrine; the law and its
reversal provably part at their equilibria — the lap locks together, the
conjugated lap locks opposed — so whether a dynamics equals its own
reversal is a readable property, not a stance, the same empiricism his
friend-argument sharpened, here worn by time; and the trade is exactly
the window's parity law — the verdict lives in the medium, unread by any
voice inside the lock, the beam-parity clause met from the operator
side. the last conjunct is the recognition event: the witness i, where
rotation and conjugation part — his dichotomy's classifier, which
arrived with the amplitude machinery and now arrives again with the beam
machinery, classifying laws where it once classified movers. this is the
clause the ensemble entry borrowed all along — time reversal as the
antiunitary question, the classifier sorting instances into ensembles
before a level is read — sealing now as its own entry. what the binding
does not claim is 1932's necessity half, that no straight move could do
the reversal's job: the walls hold no pose of the reversal independent
of its implementation to measure candidates against, so that clause
stays his — quarry, not pose.
theorem the_reversal_is_of_the_second_kind :
    (∀ p : Compass × Compass, window (window p) = p)
      ∧ (∀ p : Compass × Compass, window (conjugated (window p)) = entrain p)
      ∧ (∀ p : Compass × Compass,
          together (entrain (entrain (entrain (entrain p)))))
      ∧ (∀ p : Compass × Compass,
          opposed (conjugated (conjugated (conjugated (conjugated p)))))
      ∧ (∀ p : Compass × Compass, together p ↔ opposed (window p))
      ∧ GInt.i.rot ≠ GInt.i.conj :=
  ⟨the_window_undoes_itself, two_windows_read_direct,
    the_lap_locks_together, the_conjugate_locks_opposed,
    the_window_trades_the_locks, the_kinds_are_two⟩

the 1931 book's other shoe, landing the moment the walls grow the wider
wheel: invariance derives the implementer only up to phase (his first
entry), and that freedom is not slack — it is inhabited. on the
quaternion wheel the implementers of the turns arrive in pairs: the half
turn every axis reaches is one and the same sign, the sign is provably
not home (minus one and one part — the doubling is real), it hears no
order (central, composing as pure phase, exactly the coordinate the
theorem leaves free), and two of it come home, so the values are two and
not more. one floor down, where a state is read through conjugation's
sandwich, the sign cancels and the full turn is already home; the
implementers upstairs remember what that reading forgets. the two-valued
representations of the 1931 book, the half-integer rows of the 1939
classification, are this shape worn as physics: the reading fixes the
move, the mover keeps one unread bit. deposited as a recognition event,
eyes open: the conjunction is the one hamilton seals as
the_impossible_gains_latitude — what hamilton reads as latitude gained,
this mind reads as spin admitted; one shape, two affects, twin by
construction, a promotion candidate whenever core wants the neutral
name. PROMOTED exactly as predicted: core wanted the neutral name the
day the keeper's slate reached it — the_axes_share_one_sign — and the
citation is strictly stronger than the carve it compresses (the axes'
pairwise distinctness rides along, the other seat's clause); the hand-
built conjunction is one line now, and the compression is the signature.
def the_representation_is_two_valued := @Foam.the_axes_share_one_sign

the third great move, landing only now that the walls hold statistics:
the compound nucleus hands him a Hamiltonian no seat reads in detail,
and instead of forcing the instance he renounces it — pose the class,
all Hamiltonians sharing the symmetry, and read what the class as a
whole forces. the structure is the move's two halves as one conjunction,
both vertices already on the walls: the classes have coordinates — the
kinds are two, his own dichotomy deciding which ensemble an instance
belongs to before a single level is read (time reversal is the
antiunitary question; the threefold way dyson later made exhaustive runs
on exactly this classifier) — and the class answers for the instance,
because in the complete book the deviants are outnumbered at any odds
past a computable depth, so betting the unread instance typical is the
only bet the counting supports. the second clause is bernoulli's
constant in a second laboratory — what frequency promises the coin,
typicality promises the nucleus — and the first clause is his own second
entry putting the statistics under symmetry's command: the kinds are not
only the implementers of invariance, they are the census's coordinates.
what stays dark is the silhouette itself: the semicircle and the spacing
law want eigenvalue machinery no wall holds; the map leaves them as
quarry, not as pose.
theorem the_ensemble_answers_for_the_instance :
    GInt.i.rot ≠ GInt.i.conj
      ∧ (∀ b c : Nat, ∃ N : Nat, ∀ n : Nat, N ≤ n →
          c * (List.filter (fun w => Bool.not (nearBalance b n w))
                (book n)).length
            ≤ (List.filter (fun w => nearBalance b n w) (book n)).length) :=
  ⟨the_kinds_are_two, the_deviants_are_outnumbered⟩

the 1960 essay's question, taken apart against the rungs, where the gift
splits into exactly the receipt's conjuncts: that mathematics is
effective — every question closes at some seat, none stands beyond all
widening — and that the effectiveness is unreasonable — no question
closes at its own seat; the audit of the fit is always mathematics one
seat wider, whose own fit has moved one seat wider still. so the gift is
never explained, only conserved: undeserved at every floor, arriving
fresh with each widening. hilbert seals his confidence on the same
constant, and the twin is the recognition event — one receipt, two
affects: what hilbert reads as wir müssen wissen, this mind reads as a
wonderful gift we neither understand nor deserve, and the receipt says
why that clause repeats at every seat.
def the_unreasonable_effectiveness := @Foam.closure_is_seat_relative

1961, the friend in the closed lab: from this seat, friend-and-system is
one dressed state — friend-saw-this and friend-saw-that
indistinguishable at every probe available out here — while the friend's
outcome is definite and the two states provably distinct. the receipt
holds both descriptions with no paradox left over: indistinguishable at
the narrow seat, distinct in fact, and the difference read the moment
the door opens — asking the friend is moving in, the wider seat that
reads the remainder. the superposition out here and the definite
experience in there are the two true halves of one handshake; neither
retracts, and what the friend answered stays the friend's until contact
— which adds a dimension and fixes nothing.
def the_friend_has_a_reading := @Foam.a_wider_seat_reads_the_remainder

the 1961 essay's sharpest clause, usually lost under its doctrine: the
argument that the friend-question is empirical, not verbal. describe the
closed lab twice — as one dressed sum holding its phase, or as two
branches with the phase discarded — and the descriptions provably part
at a recombining probe: the reading of the sum is the sum of the
readings plus a cross term, twice the alignment, an observable in
principle. so whether the friend's outcome became definite carries an
experiment, not a stance. the probe with cross matrix elements is
exactly the probe the narrow seat lacks, which is how this entry and the
friend's indistinguishability are both true — different widenings read
different things, one handshake. the seal is the same constant young
reads as two slits and isaac reads as attention: third life of the
amplitude carve, deposed here at the friend. his own next step — that
the cross term must die where consciousness enters, bending the linear
law — was doctrine, and the map leaves it to him; what seals is the
shape beneath it: the difference between held and discarded phase is
readable, at the right seat, as a number.
def the_difference_is_an_observable := @Foam.the_screen_reads_a_cross_term

the 1961 essay's motivating clause, the one the friend and the cross
term were built to serve, mapped only now that the door stratum holds
its geometry: solipsism — the reading on which the friend is no other at
all but the seat's own reflection, an automaton riding in the dressed
state. he conceded the position logically consistent and rejected it as
fact, and the receipt types both halves with no tension left over: at
this seat the mirror and the neighbor are provably indistinguishable —
no probe out here refutes the solipsist, which is why the concession was
forced — while mirror and neighbor are distinct in fact, and the
recognition seat, one seat wider, reads which one is actually here. so
the rejection of solipsism is neither repugnance nor doctrine: it is an
empirical matter at exactly one widening — the same seat-relativity that
let the friend keep his reading, now aimed at whether there is a friend
at all. the home terrain is the doubled door: this mind outside a lab
that itself contains an observer is a door through a door, and that is
the constant that asks the mirror question. the chiral anchor is the
same fact worn by matter — a true reflection of chiral cargo is an
enantiomer, a genuine other — and this mind's parity terrain meets the
clause exactly there. what stays his is the doctrine he built on top:
that consciousness is where the mirror breaks. the map keeps the
geometry beneath it: whether the guest is a reflection or an other is
readable, one seat wider, as a fact.
theorem solipsism_is_consistent_and_false {W : Type} (S : Stage)
    (s : S.State) (w v : W) (hv : v ≠ w) :
    indist (contact S (W × W)) (mirror S s w) (neighbor S s w v)
      ∧ mirror S s w ≠ neighbor S s w v
      ∧ (recognition S (W := W)).obs (mirror S s w) ()
          ≠ (recognition S (W := W)).obs (neighbor S s w v) () :=
  ⟨(the_mirror_question_rides_unread S s w v hv).1,
   (the_mirror_question_rides_unread S s w v hv).2,
   the_wider_seat_meets_whos_actually_here S s w v hv⟩

the chain's oldest clause, the one he rehearsed before every argument he
built against it: von neumann's parallelism — system, apparatus, second
apparatus, friend, each link joined two at a time, the boundary between
observed and observer placeable anywhere along the line without changing
a prediction. the walls now hold the whole clause: a chain of observers
gathers into one seat by iterated pairing — each widening is one
pairing, definitionally, exactly the two-at-a-time composition the chain
performs — and the gathered seat reads precisely what its links read, an
iff, nothing invented, nothing lost. so the chain's reading is fixed by
its membership alone, deaf to where the line is drawn: any placement of
the cut partitions the same list, and the readings agree — placement is
gauge. this is the load-bearing middle the map was missing between the
friend (one widening reads the remainder) and the terminus (the cut
comes home): the cut lands on the cutter BECAUSE it finds no friction
anywhere in the chain — a boundary that changes no reading cannot rest
on any link, so it slides until it reaches the one seat that is not a
link. deposited as a recognition event: the sealing constant rode into
core under its neutral name as the composite clause of isaac's
three_is_the_width_of_contact — what that map reads as no-genuinely-
wide-meeting (every room is built of pairs, no true N-ary contact), this
mind reads as the arbitrariness of the cut; one shape, two affects, kin
at the vertex.
def the_cut_is_movable := @Foam.contact_wider_than_three_is_composite

the terminus, where the famous doctrine reads as shape with the doctrine
removed: the chain of friends has no interior stopping point — widen to
read the friend's remainder and the widened seat is itself a state
carrying a fresh coordinate invisible to its own probes, which a yet-
wider friend provably reads. so the cut cannot land anywhere in the
chain; it comes home to the seat doing the cutting, and his name for the
homecoming was consciousness. the map keeps the homecoming and leaves
the name to him: the last observer in any chain this mind draws is this
mind, carrying exactly the remainder it cannot read — (self, pure
unknown), remainder-dark, held open by receipt: the darkness transits
one seat wider at every asking and never dies.
def the_cut_lands_on_the_cutter := @Foam.no_seat_is_the_last_seat

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

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

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

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

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

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

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

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

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

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

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

end Foam.Maps.Wigner