Foam.Maps.Noether

import Foam
import Foam.Amplitude
import Foam.Beam
import Foam.Door
import Foam.Engine
import Foam.Lap
import Foam.Triple
import Foam.Quat

namespace Foam.Maps.Noether

the method: do not open the object — classify what acts on it. a
symmetry is a license, a relation every probe respects, and the
classification already pays out: move along any license, at every step,
for any run of probes, and the transcript is conserved entire. the
conserved quantity is not a second object found after the symmetry; it
is the record's indifference to the action, and the correspondence is
the theorem.
def to_every_symmetry_its_invariant := @Foam.a_license_is_a_gauge

the converse, published in the same paper and forgotten with the same
regularity: the correspondence runs both ways. the conserved quantity —
reading alike at every probe — is itself a relation every probe
respects, so the invariant is not merely downstream of a symmetry, it is
one: the widest license, the one every other license lands inside, which
is what being a license says. the loop closes — a symmetry conserves the
transcript, and transcript-conservation is a symmetry — so classifying
what acts and classifying what is conserved are one classification, and
the method needs no second tool.
def to_every_invariant_its_symmetry := @Foam.indist_is_licensed

the door stratum arrives at the method's own front step, and the method
does what it always does: do not open the door — classify what acts on
it. seated third, right behind the correspondence pair it grounds, per
the seat the door wave set. four clauses. first, the guest's freedom is
a symmetry: every rider move — any function at all on the rider
dimension, no structure asked of it — acts invisibly at the door, by
rfl. second, to that symmetry its invariant, cited through this map's
own first pair: the rider moves conserve the door's transcript entire,
a_license_is_a_gauge run at the door with indist_is_licensed in the
license seat — the correspondence pair sits in this entry's spectrum,
visibly grounding the door rather than being re-proved there. third, the
entry's own carve, the one classification no door entry in the wave
performed: an actor on the door is invisible if and only if its ground
component is invisible — and the receipt is Iff.rfl, the cheapest in the
fold. the criterion never mentions the guest: the rider's total freedom
is not a permission the door grants but the door's definition read at
the algebra — take apart what acts at the door and the classification
comes back already factored, the ground's invisibles times everything,
definitionally. this is why the wave's central clauses were never going
to fail: the guest rides unread because no invisibility criterion at the
door ever quantified over the rider in the first place. fourth, the
contrapositive the wave carries everywhere: a door that could classify
finer — resolve the rider — collapses every guest to one; the freedom is
load-bearing, not decorative. nulls on the rest of the standing ask,
with reasons: no existing entry compresses against the door — entries
one and two already seal the correspondence at every stage, door
included (the_handshake_is_the_doors_theorem is core's own receipt that
the traffic runs from the pair to the door, not back); and the lap-
direction remainder the ninth entry rests beside does not close — a door
types arrivals, not the order of a traversal, per the precedent the
wave's nulls set. the kinship sensor will confirm the seating without
being asked: the door polygon shared with the whole wave — isaac's
xenia, softer, torah, shannon, mochizuki, scholze, pasteur,
topoisomerase — while the Invisible, indist, a_license_is_a_gauge, and
indist_is_licensed vertices are this entry's alone among the door
entries: every other mind met the door as a guest; this one classified
its actors.
theorem what_acts_at_the_door :
    ∀ (S : Stage) (W : Type),
      (∀ σ : W → W, Invisible (door S W) (fun x => (x.1, σ x.2)))
        ∧ (∀ (σ : W → W) (ps : List (door S W).Probe)
              (x : (door S W).State),
            transcriptWith (door S W) (fun x => (x.1, σ x.2)) x ps
              = transcript (door S W) x ps)
        ∧ (∀ m : (door S W).State → (door S W).State,
            Invisible (door S W) m ↔ ∀ x, indist S (m x).1 x.1)
        ∧ ((∀ x y : (door S W).State, indist (door S W) x y → x = y) →
            ∀ (w₀ : W) (s : S.State) (w : W), (s, w) = (s, w₀)) :=
  fun S W =>
    ⟨fun _ _ _ => rfl,
     fun σ ps x =>
       a_license_is_a_gauge (door S W) (indist (door S W))
         (indist_is_licensed (door S W)) (fun x => (x.1, σ x.2))
         (fun _ _ => rfl) ps x,
     fun _ => Iff.rfl,
     fun h w₀ s w => a_door_that_checks_papers_unpersons_its_guests S w₀ h s w⟩

where the closed loop opens onto the second career: two invisible moves
in a row are one invisible move — what acts is closed under composition,
so the acting things are not a heap of coincidences but one object with
an algebra. the classification the first two entries perform was only
ever possible because of this closure (a group, not a list), and the
closure is also where the method turns inward: once the actions form a
structure, the mind that takes apart what acts can take apart the
actions themselves — concepts before computation.
def what_acts_composes := @Foam.invisible_comp

the algebra gets its center: the action that does not act — the identity
map — is invisible, by the cheapest receipt in the fold (rfl, no
hypothesis). this is more than a checklist item: it shows what acts is
inhabited on every stage, unconditionally — rest is not only safe and
composable, it is always available, the unit everything composes around.
and it keeps the survey honest about the parenthesis in
what_acts_composes: closure and unit are now receipted, inverses are not
— an invisible move need not be undoable move-for-move, only its
transcript is conserved — so what stands sealed is a monoid, and the
group remains a reading until an inverse is carved.
def what_acts_has_a_unit := @Foam.invisible_id

the edge comes home by dissolving: the question was posed one level
below where the method reads. in the record — the only place this mind
ever looks — every invisible move is already the unit: its running
transcript is the resting transcript, so the move and the identity are
one element of the record's algebra, and there the monoid completes to a
group by collapse — everything inverts because everything is the unit,
every invisible move every other's inverse, its own included. move-for-
move undo at the state level is a different demand and not this mind's:
whether the move can be walked back state-for-state is unread at every
probe — by the very invisibility that admitted it to the algebra — so
the residue of the question is a remainder, real and unread, a wider
seat's business; and the countermove has already priced it, undo
existing at state level only as an appended walk, position home, record
grown. what acts inverts where what-acts lives; the group was always
there and it is trivial; the survey rests alongside the remainder. (the
structure is one citation now: core already held the whole move as
correct_maintenance_has_no_signature, with the unit in the second seat —
the hand-carved trans-symm compressed against the walls, and compression
is the signature.)
theorem does_what_acts_invert :
    ∀ (S : Stage) (m : S.State → S.State), Invisible S m →
      ∀ ps s, transcriptWith S m s ps = transcriptWith S (fun x => x) s ps :=
  fun S m hm ps s =>
    correct_maintenance_has_no_signature S m (fun x => x) hm
      (invisible_id S) ps s

the seat the fifth entry priced arrives, and it wears this mind's name:
the engine — a wheel with a conserved charge — is the correspondence run
concrete, the turn invisible to the charge-gauge and the transcript
conserved entire, which is the_turn_goes_unheard in core — the method's
theorem under a neutral name, this mind's word for it living here. and
one seat wider than the gauge, the residue the record could never hear
is read in the object itself: three more turns walk any turn home, so
the inverse exists move-for-move and the monoid completes to a group by
carving, not by collapse. nothing retracts — at the gauge the algebra is
still the unit's, exactly as does_what_acts_invert left it; at the
implementation seat it is a four-stroke cycle coming home — the same
what-acts read at two widths, closure_is_seat_relative wearing gears.
the remainder stays real; it stops being dark. the survey now rests
beside a remainder that has been read.
theorem the_wider_seat_reads_the_inverse :
    ∀ E : Engine,
      (∀ ps s, transcriptWith E.gauge E.turn s ps = transcript E.gauge s ps)
        ∧ ∀ s, E.turn (E.turn (E.turn (E.turn s))) = s :=
  fun E => ⟨the_turn_goes_unheard E, E.comes_home⟩

the first two entries close the correspondence for licenses — every
symmetry its invariant, every invariant its symmetry — and the algebra
entries built what acts into a monoid, then a group, on stages that
afford it. the walls now hold the boundary: ask for more than a license
— ask for an algebra, a multiplication composing the norm, the privilege
the wheel enjoys at width two and the couple of couples buys at width
four at the price of order — and at width three the norm refuses every
actor. the refusal is the method running in its purest direction: no
candidate is opened, no case inspected — any multiplication at all, by
its obligation alone, would have to seat a triple of norm fifteen, three
times five, the norms of two exhibited triples, and fifteen is not three
squares, so the actors are refuted wholesale, unexamined. take apart
what acts, run even where nothing does: the classification returns
empty, and the emptiness is a theorem with a receipt, not a failure to
find. nothing retracts — the unit still rests on every stage (the fourth
entry stands), and invisible moves still abound at width three; what the
third width lacks is not action but algebra: the stage acting on itself,
every state a move, the product carrying the norm — which is exactly the
privilege the next two entries spend. the absence is classified
alongside the presence, and the survey learns that the instrument it
rests beside was never the method's to summon; it was the stage's to
afford. (re-seated when the quaternion norm block landed: the widths the
gloss could only name are now receipted, and the binding carries the
whole ladder — at width two the product carries the norm and order is
unheard, at width four the product carries the norm and order arrives,
and between them the refusal stands exactly as sealed. nothing retracts;
the emptiness stops being a lone receipt and becomes a boundary between
two inhabited widths, the price of order typed as a contrast instead of
said in prose. the flanks are hamilton's vertices — his couple, his
commutation-price, his triplets closing one seat wider — so the kinship
the method predicted is now in the spectrum where the sensor can read
it.)
theorem the_norm_can_refuse_every_actor :
    ((∀ z w : GInt, (z.mul w).normSq = z.normSq * w.normSq)
        ∧ ∀ z w : GInt, z.mul w = w.mul z)
      ∧ ¬ (∃ mul : (Int × Int × Int) → (Int × Int × Int) → (Int × Int × Int),
            ∀ x y, normSq3 (mul x y) = normSq3 x * normSq3 y)
      ∧ (∀ x y : Quat, (x.mul y).normSq = x.normSq * y.normSq)
        ∧ Quat.mul eye jay ≠ Quat.mul jay eye :=
  ⟨⟨the_couple_carries_the_norm, gmul_comm⟩,
   no_triple_carries_the_norm,
   the_quadruple_carries_the_norm, order_arrives⟩

the sixth entry's carve pays out as an instrument, and the instrument
now compiles as four receipts in one conjunction — her first trade,
invariant theory, where the group's finiteness buys the average and the
average buys the theorem. the reading is real: the screen reads a cross
term, the interference itself, not conserved by the wheel. the wheel
taken whole is deaf to it: the same reading summed over all four phases
reads nothing — the invariant content of a non-invariant reading is
nothing. the deafness is selective, not blindness: the conserved charge
survives the sum intact, four turns yielding four full readings of the
norm, so the probe hears exactly the conserved part and only that. and
the deafness is non-trivial, witnessed: one sample carries the unknown —
a single phase reads one where the whole wheel reads zero, so the erased
sector is inhabited, indistinguishable at the averaged seat and distinct
at the single-phase seat. the group taken whole becomes what the method
said from the first entry: not a heap of moves but one object — and the
object, applied entire, is itself the widest probe, reading exactly what
every phase agrees on and erasing exactly what only a single phase can
see. the remainder is not lost by this; it is located: the interference
lives entirely in the sector the average is deaf to, its address the
narrower seat, and the survey rests beside it — the terminus taking its
usual shape, a receipted statement that the unknown stays open where
this probe provably cannot follow.
theorem what_acts_taken_whole_is_a_probe :
    (∀ z w : GInt,
        (z.add w).normSq = (z.normSq + w.normSq) + (z.align w + z.align w))
      ∧ (∀ z w : GInt,
          ((z.align w + z.align w.rot) + z.align w.rot.rot)
              + z.align w.rot.rot.rot = 0)
      ∧ (∀ z : GInt,
          ((z.normSq + z.rot.normSq) + z.rot.rot.normSq)
              + z.rot.rot.rot.normSq
            = ((z.normSq + z.normSq) + z.normSq) + z.normSq)
      ∧ GInt.i.align GInt.i ≠ 0 :=
  ⟨the_screen_reads_a_cross_term,
   the_four_phases_read_nothing,
   fun z =>
     ((congrArg
         (fun x => ((z.normSq + x) + z.rot.rot.normSq) + z.rot.rot.rot.normSq)
         (rot_conserves_the_norm z)).trans
       (congrArg
         (fun x => ((z.normSq + z.normSq) + x) + z.rot.rot.rot.normSq)
         ((rot_conserves_the_norm z.rot).trans
           (rot_conserves_the_norm z)))).trans
       (congrArg
         (fun x => ((z.normSq + z.normSq) + z.normSq) + x)
         (((rot_conserves_the_norm z.rot.rot).trans
             (rot_conserves_the_norm z.rot)).trans
           (rot_conserves_the_norm z))),
   fun h => nomatch Int.ofNat.inj h⟩

the seventh entry rested beside a located remainder — the interference
alive in the sector the whole probe is deaf to — and the walls have
since read into that sector. what they read is the mechanism of the
erasure: the zero the averaged probe reports is cancellation, not
absence. the four phases arrive in facing pairs — quarter-turn against
three-quarter-turn, the reading against its own half-turn — and each
pair annihilates exactly, while the witness holds a cancelled term alive
on its own: nonzero singly, silent only in company. so the invariant
content of a non-invariant reading is nothing for a reason, and the
reason is the group again — the same closure that made the whole a probe
pays out its deafness pair by pair. and the remainder does what
remainders do here: transit, not die. with the mechanism read, a new
unread stands up one seat over, already receipted on the walls — the
lap's own direction, around and against one multiset and two lists, the
whole probe deaf to the order of its own traversal — and the survey
rests again, one address deeper than before.
def the_deafness_is_cancellation := @Foam.cancellation_not_absence

the third entry's gloss made a promise the map never cashed: once the
actions form a structure, the mind that takes apart what acts can take
apart the actions themselves. the beam stratum affords the carve, and
this entry cashes it. conjugation is the taking-apart of a law by a move
— the window is an involution, and the entrainment law dressed in it,
window then law then window, is another law. the correspondence does not
stay behind: the direct law's four-stroke lap locks together; the
conjugated law's lap locks opposed, which is exactly the window-image of
together — the invariant trades with the law, in step, through the same
move that trades the law. and the fourth conjunct is the method's own
receipt rather than a new computation: core proves the conjugated lock
by sixteen cases, and this binding re-derives it with zero cases opened
— the direct theorem carried through the window, the involution
swallowing each interior window-pair as the walk climbs, congrArg and
trans the whole way — so the kernel accepting the transport IS the
receipt that the correspondence is equivariant: to the conjugated
symmetry, the conjugated invariant, no second theorem needed. concepts
before computation, run literally. the stratum is the clockmaker's — two
clocks, the beam deciding the parity of the lock — and this mind reads
the same walls as the adjoint action carrying a conservation theorem to
its conjugate: one mechanism, two vocabularies. the terminus does not
move: the lap-direction remainder the ninth entry rests beside still
stands unread at this seat, and the survey rests where it rested — one
entry richer about what the algebra of what-acts does to its own laws.
theorem the_lock_trades_with_the_law :
    (∀ p : Compass × Compass,
        together (entrain (entrain (entrain (entrain p)))))
      ∧ (∀ p : Compass × Compass, window (window p) = p)
      ∧ (∀ p : Compass × Compass, together p ↔ opposed (window p))
      ∧ ∀ p : Compass × Compass,
          opposed (conjugated (conjugated (conjugated (conjugated p)))) :=
  ⟨the_lap_locks_together,
   the_window_undoes_itself,
   the_window_trades_the_locks,
   fun p =>
     let stride : ∀ q : Compass × Compass,
         conjugated (window q) = window (entrain q) :=
       fun q =>
         congrArg (fun x => window (entrain x)) (the_window_undoes_itself q)
     let two : conjugated (conjugated p)
         = window (entrain (entrain (window p))) :=
       stride (entrain (window p))
     let three : conjugated (conjugated (conjugated p))
         = window (entrain (entrain (entrain (window p)))) :=
       (congrArg conjugated two).trans
         (stride (entrain (entrain (window p))))
     let four : conjugated (conjugated (conjugated (conjugated p)))
         = window (entrain (entrain (entrain (entrain (window p))))) :=
       (congrArg conjugated three).trans
         (stride (entrain (entrain (entrain (window p)))))
     Eq.mpr (congrArg opposed four)
       ((the_window_trades_the_locks
           (entrain (entrain (entrain (entrain (window p)))))).mp
         (the_lap_locks_together (window p)))⟩

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

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

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

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

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

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

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

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

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

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

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

end Foam.Maps.Noether