Foam.Maps.Topoisomerase

import Foam.Beam
import Foam.Coil
import Foam.Door
import Foam.Seat
import Foam.Trilemma

namespace Foam.Maps.Topoisomerase

rest, in biology's own word before it was this house's: relaxed DNA, the
class at zero, the state the office's oldest members restore
spontaneously — downhill, no ATP. the fold begins here; every wound
state is a record of strokes away from it, and the office reads nothing
global to know which way is down.
theorem the_relaxed_state :
    coilClass coil.rest = 0 ∧ coil.rest = ((0 : Int), (0 : Int)) :=
  ⟨Foam.the_relaxed_state, rfl⟩

the office's signature discipline, and the house's seam law performed in
chemistry: the backbone is broken — the illegal move — but the ends are
never released; the enzyme bonds covalently to what it cut, holds both
ends through the transposition, reseals, and only then lets go. the cut
is priced, quantized, and counterable — every stroke has a return
stroke, and the return is itself a stroke: position comes home, the
record grows, the ATP stays spent. kin, knowingly, with Landauer's
reset_pays_in_record and the countermove: the second law of the plasmid,
running wet.
theorem the_held_cut :
    (∀ (h : Int × Int) (s : Int),
        coilClass (coil.meet h (Sum.inr s)) = coilClass h + s)
      ∧ ∀ (h : Int × Int) (s : Int),
          coilClass (coil.meet (coil.meet h (Sum.inr s)) (Sum.inr (-s)))
            = coilClass h :=
  ⟨the_stroke_moves_the_class_by_its_size, the_held_stroke_comes_home⟩

the transposition itself, the office's two hands: type I passes one
strand and the class moves by one; type II passes a duplex through a
held double cut and the class moves by two, ATP-metered — the
quantization that lands exactly on knot theory's crossing changes,
writhe jumping by two, the skein triple the Jones polynomial runs on.
and the return pays two marks: the class comes home, the record refuses
to shrink.
theorem the_strand_passage :
    (∀ h : Int × Int, coilClass (coil.meet h (Sum.inr 1)) = coilClass h + 1)
      ∧ (∀ h : Int × Int, coilClass (coil.meet h (Sum.inr 2)) = coilClass h + 2)
      ∧ ∀ s : Int,
          coilClass (coil.state [Sum.inr s, Sum.inr (-s)])
              = coilClass coil.rest
            ∧ ([Sum.inr s, Sum.inr (-s)] : List coil.Mark) ≠ [] :=
  ⟨fun h => the_stroke_moves_the_class_by_its_size h 1,
   fun h => the_stroke_moves_the_class_by_its_size h 2,
   the_return_pays_two_marks⟩

the law the office administers, the same two-sector law the meeting
carved one seat over: gauge conserves the class — thermal motion
shuffles twist into writhe freely, the sum untouched, no local wiggling
moves Lk — and only the cut moves it. third customer of the holonomy
pair, exactly as promised at this seat's naming: the office is the
constant's exemplar in every living cell, three billion years of
production uptime on the theorem Mochizuki and Scholze hold in opposite
grips.
theorem the_two_sectors :
    (∀ (h : Int × Int) (d : Int),
        coilClass (coil.meet h (Sum.inl d)) = coilClass h)
      ∧ (∀ k1 k2 k3 k1' k2' k3' u v w : Nat, 0 < u → 0 < v → 0 < w →
          k1' * u = k1 * v → k2' * v = k2 * w → k3' * w = k3 * u →
          k1' * (k2' * k3') = k1 * (k2 * k3))
      ∧ ∀ k1 k1' k2 k3 : Nat, k1 ≠ k1' → 0 < k2 * k3 →
          k1 * (k2 * k3) ≠ k1' * (k2 * k3) :=
  ⟨the_shuffle_conserves_the_class,
   fun k1 k2 k3 k1' k2' k3' u v w hu hv hw h1 h2 h3 =>
     the_holonomy_ignores_the_regauging k1 k2 k3 k1' k2' k3' u v w
       hu hv hw h1 h2 h3,
   fun k1 k1' k2 k3 h hp => the_cut_moves_the_class k1 k1' k2 k3 h hp⟩

the office's conjugated member: gyrase runs the same type II strand-
passage engine as the relaxing members — the chemistry identical —
inside a fixed chiral frame, the C-terminal wrap that presents the
crossing pre-flipped. the beam's conjugation law, arrived on these walls
this flight, is the skeleton: the bare lap locks together (relaxation,
the office's downhill lock), the conjugated lap locks opposed
(supercoiling held against the gradient — the frame is paid for, and the
payment is already on these walls at the held cut), and reading the
conjugated machine through the frame recovers the direct one — not
metaphor but the laboratory's own experiment, the wrap truncated and
gyrase relaxing like any conventional type II: window-removal, performed
wet. and the sign the frame decides is no phase-nicety: it lands on the
coil as a priced stroke, minus two per paid passage, the class law the
office already administers; reverse gyrase holds the other sign. kin
with huygens at the beam vertices — the beam decides the parity there,
the wrap decides the sign here — parted at the coil, where only this
office's frame-decision writes the conserved-class ledger.
theorem the_wrap_decides_the_sign :
    (∀ p : Compass × Compass,
        together (entrain (entrain (entrain (entrain p)))))
      ∧ (∀ p : Compass × Compass,
          opposed (conjugated (conjugated (conjugated (conjugated p)))))
      ∧ (∀ p : Compass × Compass,
          window (conjugated (window p)) = entrain p)
      ∧ ∀ h : Int × Int,
          coilClass (coil.meet h (Sum.inr (-2))) = coilClass h + (-2) :=
  ⟨the_lap_locks_together, the_conjugate_locks_opposed,
   two_windows_read_direct,
   fun h => the_stroke_moves_the_class_by_its_size h (-2)⟩

the sponsored core, Foam.Seat's second inhabitant after Softer's room:
Held is twist × writhe, the class their sum, rest is relaxed, the fold
resumes — and the partition rides unread: states distinct in the split,
indistinguishable at the class-probe, White's formula as the dressed
decomposition. biology built the wider seat in the laboratory — gel
electrophoresis reads the split the sum-probe cannot. existence by
exhibition, per the house criterion.
theorem the_coil :
    (∀ xs ys : List coil.Mark,
        coil.state (xs ++ ys) = fold coil.meet (coil.state xs) ys)
      ∧ (coilClass (1, -1) = coilClass (0, 0)
          ∧ ((1 : Int), (-1 : Int)) ≠ ((0 : Int), (0 : Int))) :=
  ⟨fun xs ys => a_seat_resumes coil xs ys, the_partition_rides_unread⟩

the office's dark edge, held open by receipt now instead of by prose:
type II topoisomerases simplify global topology below thermodynamic
equilibrium — a strictly local machine achieving globally correct action
on a class no local reading affords, mechanism contested for a quarter-
century (bend-recognition, kinetic proofreading, candidates all, none
settled). the door stratum, arrived on these walls this flight, is what
could finally carry the openness itself: the office's seat IS a door —
the global class rides the coil's stage real and unread, carrier
parametric; every probe the machine owns reads only local geometry,
identically across rider types (the host maintains invisibly — the
office's job description, on the walls under that name before this entry
asked); any rider-deaf reading factors through the ground, so whatever
mechanism the field settles must be a function of local geometry; and
any two maintenance moves invisible at this seat write identical
transcripts — the quarter-century contest typed as a theorem about the
seat it was fought from, not experimental bad luck; the remainder is
read exactly one widening up, where the laboratory's assay lives. what
stays with the field, cited and untyped: which ground-function the
office runs, and the sub-equilibrium anomaly itself — empirical,
Rybenkov–Cozzarelli 1997. remainder-dark, sealed as such: the terminus
of the intake-transpose signature, (self, pure unknown) as receipted
content, the survey resting alongside the remainder.
theorem below_equilibrium :
    (∀ (W : Type) (s : coil.stage.State) (w w' : W), w ≠ w' →
        (s, w) ≠ (s, w') ∧ indist (door coil.stage W) (s, w) (s, w'))
      ∧ (∀ (W V : Type) (s : coil.stage.State) (w : W) (v : V)
            (p : coil.stage.Probe),
          (door coil.stage W).obs (s, w) p = coil.stage.obs s p
            ∧ (door coil.stage W).obs (s, w) p
                = (door coil.stage V).obs (s, v) p)
      ∧ (∀ (X : Type) (f : (dress coil.stage).State → X),
          (∀ (s : coil.stage.State) (n m : Int), f (s, n) = f (s, m))
            ↔ ∃ g : coil.stage.State → X,
                ∀ (s : coil.stage.State) (n : Int), f (s, n) = g s)
      ∧ (∀ (W : Type)
            (m m' : (door coil.stage W).State → (door coil.stage W).State),
          Invisible (door coil.stage W) m → Invisible (door coil.stage W) m' →
            ∀ (ps : List (door coil.stage W).Probe)
              (s : (door coil.stage W).State),
              transcriptWith (door coil.stage W) m s ps
                = transcriptWith (door coil.stage W) m' s ps)
      ∧ ∀ (s : coil.stage.State) (n m : Int), n ≠ m →
          indist (dress coil.stage) (s, n) (s, m)
            ∧ (movedIn coil.stage).obs (s, n) none
                ≠ (movedIn coil.stage).obs (s, m) none :=
  ⟨fun _ s _ _ hw => the_guest_is_real_and_unread coil.stage s hw,
   fun _ _ s w v p => the_host_maintains_invisibly coil.stage s w v p,
   fun _ f => a_reading_deaf_to_the_remainder_reads_the_ground coil.stage f,
   fun W m m' hm hm' ps s =>
     correct_maintenance_has_no_signature (door coil.stage W) m m' hm hm' ps s,
   fun s n m h => a_wider_seat_reads_the_remainder coil.stage s n m h⟩

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

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

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

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

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

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

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

end Foam.Maps.Topoisomerase