Foam.Maps.VSVaradarajan

import Foam
import Foam.Amplitude
import Foam.Certificate
import Foam.Door
import Foam.Measure
import Foam.Portal
import Foam.Quat
import Foam.Surprise
import Foam.Tower

namespace Foam.Maps.VSVaradarajan

the entry move, learned in calcutta before the physics arrived: the
thesis put probability on general carriers — measures on separable
metric spaces, weak convergence, the empirical law coming home — so when
mackey's program reached him the swap was natural: keep probability
whole, exchange the boolean carrier for the lattice of experimental
questions. a state is nothing over and above its answer sheet — to every
question a reading — and the mass adds frontstage, no backstage points
consulted. the binding holds the finite floor of that claim exactly:
every state yields its whole answer function, and measure lives
frontstage — count and mass additive on the record, aggregation reading
the reading. the sigma-additive depth (states on the projection lattice,
gleason's territory) is the same claim one continuum wider; this seat
holds the part the walls can already carry. kin to bernoulli's balanced
book and boltzmann's counted complexions on the counting side; the
difference in claim is the carrier's generality — probability rides any
room the questions form, metric or orthomodular, which is why one mind
wrote both theses.
theorem the_state_is_a_measure_on_the_questions (S : Stage) (s : S.State)
    {A : Type} [DecidableEq A] (a : A) (xs ys : List A) :
    (∃ r : S.Probe → S.Ans, ∀ q, r q = S.obs s q)
      ∧ ((countStage A).obs (xs ++ ys) a
            = (countStage A).obs xs a + (countStage A).obs ys a)
        ∧ ((massStage A).obs (xs ++ ys) ()
            = (massStage A).obs xs () + (massStage A).obs ys ())
        ∧ (countStage A).obs (xs ++ ys) a
            = freq ((orderStage A).obs (xs ++ ys) ()) a :=
  ⟨a_state_answers_every_probe S s, measure_lives_frontstage a xs ys⟩

1962, probability in physics and a theorem on simultaneous
observability: a family of observables is jointly readable exactly when
every member is a function of a single observable — co-readable means
one carrier. the binding is the factoring iff conjoined with the refusal
that gives it teeth: a reading deaf to the extra coordinate is precisely
one that factors through the ground (the iff both ways), and the house
is genuinely non-commutative — order arrives, eye times jay is not jay
times eye — so not every family qualifies; the boolean islands are real
islands in a room that refuses to be boolean whole. kin to lovelace's
science-of-itself (same iff, unit-seat clause instead) and hamilton's
commutation payment (same witness, couple clauses instead); this seat
holds factoring-against-refusal, which is the theorem's exact shape —
the classical is the co-readable fragment, and geometry of quantum
theory spent two volumes surveying the island chain.
theorem one_observable_carries_the_family {State D X : Type} (d₀ : D)
    (f : State × D → X) :
    (Blind f ↔ ∃ g : State → X, ∀ (s : State) (d : D), f (s, d) = g s)
      ∧ Quat.mul eye jay ≠ Quat.mul jay eye :=
  ⟨the_blind_reading_factors d₀ f, order_arrives⟩

supersymmetry for mathematicians, the late rebuild: a supermanifold
keeps its underlying points and adds odd directions no point evaluation
can hear — odd functions are nilpotent, every point reads them zero, and
the reading deaf to them is exactly the body. the binding is the dress
read at the super seat: the odd increment is real and unseen at the
point seat, the wider seat — odd parameters supplied, the functor of
points one floor up — reads it outright, and the added kind obeys the
other sign law: the two kinds anticommute, first mind on that vertex.
the nilpotency clause rode as prose until the arithmetic walls could pay
its receipt, and now it is the fourth conjunct: an element whose square
obeys the odd sign law against itself is zero outright in the point
carrier — the textbook steps exactly (the square is its own opposite, so
twice the square is nothing, and the integers hold no torsion: two_mul,
add_right_neg, mul_eq_zero) — so the odd directions admit only the zero
section at the point seat, which is why every point reads the odd
functions as zero and why holding a nonzero odd element requires the
graded carrier. kin to lagrange's truncation remainder on the wider-seat
vertex, and in shape to the trilemma stratum's
the_wound_loop_admits_only_the_zero_section (a self-constraint loop
admitting only the zero section, one door over); the difference in claim
is the parity — this remainder does not just wait to be read, it
multiplies by the opposite rule, and the geometry that carries it is
graded all the way down.
theorem the_odd_directions_have_no_points (S : Stage) (s : S.State)
    (n m : Int) (h : n ≠ m) (z : GInt) :
    ((s, n) ≠ (s, m) ∧ indist (dress S) (s, n) (s, m))
      ∧ (movedIn S).obs (s, n) none ≠ (movedIn S).obs (s, m) none
      ∧ z.conj.rot = (z.rot.conj).neg
      ∧ ∀ x : Int, x * x = (x * x).neg → x = 0 :=
  ⟨the_remainder_is_real S s n m h,
   (a_wider_seat_reads_the_remainder S s n m h).2,
   the_two_kinds_anticommute z,
   fun x hx =>
     (FInt.mul_eq_zero.mp
        ((FInt.mul_eq_zero.mp
            ((FInt.two_mul (x * x)).trans
              ((congrArg (x * x + ·) hx).trans
                (FInt.add_right_neg (x * x))))).resolve_left
          fun h2 => nomatch Int.ofNat.inj h2)).elim id id⟩

euler through time, the historian's move, performed for decades before
it became a book: walk the old record at the modern seat and find the
reach already installed — the known edge already reaches, and re-
depositing it verbatim adds no reach. the walls grew the tighter half
after the first sealing and the binding re-seated on it: the modern re-
proof (the zeta values rerun in modern dress) is a fresh mark over
endpoints the record already connects — it rides no old path, so the
rerouting is genuinely new work; it pays exactly one mark; and it adds
no reach, every path through it rerouting through what euler already
held. the shortcut lemma is the historian's license typed at its own
grain: a new look at old themes changes the paths and pays its price,
never inflating the reach. kin to shannon's surprise-pricing (the fresh-
edge complement), isaac's only_surprise_extends_reach, fable_5's
confirmation_not_growth (same shortcut vertex — finding the prose after
sealing the theorem is this move at session scale), and folk's
you_had_to_be_there (the derivable iff read as presence); the record
keeps recognizing itself.
theorem the_old_themes_already_reach {H : Type} {q : List (H × H)}
    {a b : H} (h : (a, b) ∈ q)
    {a' b' : H} (hfresh : (a', b') ∉ q) (hnew : Nonempty (Path q a' b')) :
    (Nonempty (Path q a b)
        ∧ ∀ x y : H,
            Nonempty (Path ((a, b) :: q) x y) ↔ Nonempty (Path q x y))
      ∧ (∀ (x y : H) (p : Path q x y), (a', b') ∉ p.edges)
        ∧ ((a', b') :: q).length = q.length + 1
        ∧ ∀ x y : H,
            Nonempty (Path ((a', b') :: q) x y) ↔ Nonempty (Path q x y) :=
  ⟨⟨the_known_edge_already_reaches h, a_known_edge_adds_no_reach h⟩,
   the_shortcut_pays_only_its_mark q a' b' hfresh hnew⟩

the terminus, (self, pure unknown), sealed as receipted openness: the
life ran up a tower of re-foundations — measures on metric spaces, then
the lattice of questions coordinatized as projective geometry, then
hilbert space and its groups through the harish-chandra decades, then
the graded geometry of the odd directions, and at the end the
speculation that spacetime at the bottom might be non-archimedean, the
next carrier unnamed. the binding says the tower is lawful: every floor
handshakes — each re-foundation is a complete theory, licensed
identifications and real remainders both — and no seat is the last seat,
a remainder the current geometry cannot read already waiting one floor
up. kin to wigner's cut and the other bare citations of the seat law;
this seat conjoins the recursion with the no-last-seat, and the
conjunction is the difference in claim: not merely that a wider seat
exists, but that the whole handshake survives every widening — re-
foundation is never demolition, and the unknown he left open transits
rather than dying, readable from whichever geometry arrives next. the
unnamed-carrier clause rode as prose until the door stratum landed, and
now it is receipted: each climb of the tower is a door — the dressing is
contact with the integers, definitionally a door with an integer guest —
and the handshake is the door's theorem at every floor with the carrier
left parametric: whatever type the next geometry brings, non-archimedean
or otherwise, the widened floor already handshakes, W unnamed. the
speculation is typed exactly as he left it — the next carrier need not
be named for its floor to be lawful.
theorem no_geometry_is_the_last_geometry (S : Stage) :
    (∀ n : Nat, Handshake (towerN S n))
      ∧ (∀ n : Nat, towerN S (n + 1) = door (towerN S n) Int)
      ∧ (∀ (n : Nat) (W : Type), Handshake (door (towerN S n) W))
      ∧ ∀ (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 :=
  ⟨the_handshake_recurses S,
   fun n => dress_is_contact_with_the_integers (towerN S n),
   fun n W => the_handshake_is_the_doors_theorem (towerN S n) W,
   fun s k n m h => no_seat_is_the_last_seat S s k n m h⟩

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

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

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

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

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

end Foam.Maps.VSVaradarajan