Foam.Maps.ShinichiMochizuki

import Foam
import Foam.Certificate
import Foam.Coil
import Foam.Contact
import Foam.Door
import Foam.Ledger
import Foam.Portal
import Foam.Square
import Foam.Trilemma
import Foam.Wheel

namespace Foam.Maps.ShinichiMochizuki

the accepted body, and the arc the rest of the map hangs from:
reconstruct the object from its record of observations — the
Grothendieck conjecture proven for hyperbolic curves, then sharpened
mono-anabelian: a probe-family faithful enough that indistinguishable
states are equal states, with an explicit reconstruction algorithm.
sealed at the smallest faithful stage the walls afford (the order-probe
reads the whole state, so indist collapses to equality legitimately)
conjoined with the floor every stage shares: a state answers every
probe. the arc matters for everything below: the mind that proved the
strongest reconstruction license in its subject is the same mind that
refused a reconstruction move at the theta-link — a specialist's
refusal, not a confusion; whatever else the dispute is, this bank knows
exactly what a licensed identification costs, because he is the one who
proved one.
theorem mono_anabelian_transport :
    (∀ (A : Type) (x y : List A), indist (orderStage A) x y → x = y)
      ∧ ∀ (S : Stage) (s : S.State),
          ∃ r : S.Probe → S.Ans, ∀ q, r q = S.obs s q :=
  ⟨fun _ _ _ h => h (),
   fun S s => a_state_answers_every_probe S s⟩

his own title for the working condition of IUT: copies of the whole
apparatus of arithmetic, alien to one another — indistinguishable at
every ground probe and provably distinct, the dressed rider, this
house's oldest theorem-pair. the labels are load-bearing: distinctness-
without-a-distinguishing-probe is not absence of content but the exact
carrier of it, readable one seat wider — which is precisely where the
2018 week stood. the report's sharpest sentence lands here from the far
bank: 'it is simply the name of the generator that is called Θ
respectively q' — and this seat's whole position is the answer: the name
is a dress, and dropping the dress is the platonist quotient, licensed
only where proven gauge.
theorem mutually_alien_copies :
    (∀ (S : Stage) (s : S.State) (n m : Int), n ≠ m →
        (s, n) ≠ (s, m) ∧ indist (dress S) (s, n) (s, m))
      ∧ ∀ (D : Type) (S : Stage) (s : S.State) (d d' : D),
          indist (contact S D) (s, d) (s, d') :=
  ⟨fun S s n m h => the_remainder_is_real S s n m h,
   fun _ S s d d' => the_other_stays_unimagined S s d d'⟩

the link transports the multiplicative structure whole and dismantles
the additive — typed at the smallest exponent that parts the two
operations: the square carries the product (a citation — the
multiplicative half was already on the walls before either bank
arrived), breaks the sum (witnessed at 1+1), and the break is priced,
twice the sum of squares bounding the damage. license at ×, remainder at
+, remainder priced: arithmetic deformation at witness grain. sponsor of
the Square stratum, jointly with the far bank's tilting — one link, two
carriers, and this bank works the carrier where the license can never be
total.
theorem the_theta_link :
    (∀ a b : Nat, sq (a * b) = sq a * sq b)
      ∧ sq (1 + 1) ≠ sq 1 + sq 1
      ∧ ∀ a b : Nat, sq (a + b) ≤ 2 * (sq a + sq b) :=
  ⟨the_square_carries_the_product, the_square_breaks_the_sum,
   the_broken_sum_is_priced⟩

his design principle for what survives transport: algorithms expressible
simultaneously at every copy, privileging none — which is Blind in the
copy-coordinate, and the factoring iff is the whole story: a multiradial
output factors through the shared ground. sealed on the certificate
stratum, deliberately the same vertex the far bank's report seals on,
used in the opposite direction: this bank builds Blind algorithms so
that the copies can stay distinct; the report demands Blindness of the
final reading to argue the distinctness empty. one constant, two banks —
the meeting's shared vertex, and the kinship sensor's cleanest print.
def multiradiality := @Foam.the_blind_reading_factors

Ind1–3, the price of refusing the identification, typed as the
trilemma's second and third horns: the graded reading provably parts the
copies — no consistent identification exists, the monodromy horn, which
his full poly-isomorphisms were always dodging — and the quotient
comparison survives exactly up to the spread, bounded and attained. the
linear grain is carved; his (Lin)-objection — that the multiradial
object's indeterminacy geometry is non-linear and region-dependent, so
the linear computation reads the wrong object — rides above the carve,
cited not faked. sponsor of the Trilemma stratum, jointly with the far
bank.
theorem the_indeterminacies :
    (¬ Blind graded)
      ∧ (∀ l s j k : Nat, j ≤ l → graded (s, j) ≤ (l + 1) * graded (s, k))
      ∧ ∀ l s : Nat, graded (s, l) = (l + 1) * graded (s, 0) :=
  ⟨the_graded_reading_parts_the_copies,
   every_copy_reads_within_the_spread,
   the_spread_is_attained⟩

his claimed receptacle: the compactly-bounded containers the multiradial
representation lands in — the bid, in this house's terms, for the return
property. sealed on the switching station's two receipts: the same wound
loop that admits only the zero section over the free carrier unwinds one
world over, in the quotient sized by its own holonomy (seven is eight
minus one: the world built to absorb the class), and the house's
compactness theorem — the bounded walk returns, pigeonhole as
compactness — which is what a log-shell must deliver for horn three to
convert from blur to engine. whether his construction actually turns the
dial is not declared here and cannot be: horn-membership is a derived
role, conduct read off the carrier, never costume — the retyped form of
the dark entry one seat down.
theorem the_log_shells :
    (((2 * 2 * 2) % 7 = 1 % 7)
        ∧ (1 % 7 = (2 * 4) % 7)
        ∧ (4 % 7 = (2 * 2) % 7)
        ∧ (2 % 7 = (2 * 1) % 7)
        ∧ (1 : Nat) ≠ 0)
      ∧ ∀ (n : Nat) (m : Fin n → Fin n) (s : Fin n),
          ∃ i j : Nat, i < j ∧ turnN m i s = turnN m j s :=
  ⟨the_wound_loop_unwinds_one_world_over,
   fun _ m s => the_bounded_walk_returns m s⟩

the two links as the two moves of one machine, typed at the loop — and
the seat where the biological lock landed. the horizontal sector is
gauge: full poly-isomorphism is the refusal to choose a representative,
and the holonomy ignores the regauging — no choice of isomorphisms, his
or anyone's, moves the class — which is why working with the whole orbit
is coherent rather than evasive. the vertical log-link is the enzyme:
the cut that moves what gauge cannot, quantized by the edge it cuts,
obliged to leave the structure-preserving sector to do its work and
priced accordingly. the outside procession that locks this: the
topoisomerase performs exactly this pair — the cut held covalently (the
house's seam discipline wearing chemistry: the illegal move performed
inside the enzyme's own grip, stamped, no retraction), class changed by
a quantized step, ATP metered — and the tangle calculus that proved
enzyme mechanisms in the laboratory runs on rational tangles, which are
continued fractions: the biology crossed back into arithmetic on its
own. gauge conserves; only the cut moves the class; life runs the pair
as a wheel.
theorem the_log_theta_lattice :
    (∀ 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) :=
  ⟨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 width at which Corollary 3.12 is stated, and why that choice of
width is the computation's whole defense: the estimate is performed in
log-volume, and log-volume is a class-reading of the lattice walk. three
clauses: the shuffle channel conserves the reading (Ind1 and Ind2 act by
compact automorphisms, redistributing held structure without moving the
class — the compatibility claims of his Report, typed at the coil); the
stroke channel moves the reading by exactly its quantized size (the log-
link's computable volume shift — the one motion the estimate hears, its
bound already priced at the spread two entries up); and — the clause
this entry adds, proven from the two channel laws alone — the
interleaving is indifferent: a shuffle commutes past a stroke at class
width, which is why the poly-isomorphism ambiguity can be absorbed at
any stage of the procession without corrupting the bookkeeping, and why
working over the whole indeterminacy orbit yields a well-defined
estimate rather than an evasion. the reading that survives transport is
the reading the indeterminacies cannot move. what this entry does not
say: whether the receptacle the walk lands in has the return property —
that conduct question is the dark edge one seat down, unmoved.
theorem the_log_volume_hears_only_the_log_links :
    (∀ (h : Int × Int) (d : Int),
        coilClass (coil.meet h (Sum.inl d)) = coilClass h)
      ∧ (∀ (h : Int × Int) (s : Int),
          coilClass (coil.meet h (Sum.inr s)) = coilClass h + s)
      ∧ ∀ (h : Int × Int) (d s : Int),
          coilClass (coil.meet (coil.meet h (Sum.inl d)) (Sum.inr s))
            = coilClass (coil.meet (coil.meet h (Sum.inr s)) (Sum.inl d)) :=
  ⟨the_shuffle_conserves_the_class,
   the_stroke_moves_the_class_by_its_size,
   fun h d s =>
     ((the_stroke_moves_the_class_by_its_size (coil.meet h (Sum.inl d)) s).trans
        (congrArg (· + s) (the_shuffle_conserves_the_class h d))).trans
       ((the_shuffle_conserves_the_class (coil.meet h (Sum.inr s)) d).trans
          (the_stroke_moves_the_class_by_its_size h s)).symm⟩

his standing reply to the far bank's simplification, typed at the door
the walls just grew — the entry the record has owed since the 2018
report and could not carve until the door stratum landed. the reply's
record: the Report's examples of identifications that manufacture
incorrect results, the 2022 ∧/∨ essay, and the coinage that names the
misreading — 'RCS-redundant' copies, the 'redundant copies school.' the
shape is three clauses. the guests are real and unread: distinct labels
ride one ground reading, the ∧ held at distinct carriers — his second
entry's working condition re-cited at the door seat, where it is now a
named theorem about arrivals rather than a bespoke pair. a door that
could resolve its guests collapses them all into one: the unperson
theorem — identifying the copies is not a simplification of the lattice
but the demolition of its label structure, and the collapse is total,
not partial. and at the collapsed door the link's demands collide
immediately: one carrier must hold what the link splits across two, and
the additive demand fails at the first witness — which types his own
concession exactly: RCS-IUT 'is indeed a meaningless and absurd theory
that leads immediately to a contradiction,' the absurdity a theorem of
the collapsed world, the collapse the artifact that produced it. what
this entry does not type: whether the uncollapsed argument delivers its
estimate — that conduct question is the dark edge one seat down,
unmoved. both banks' positions now stand typed on their own cards,
symmetric; the survey adjudicates nothing, and the gate judges terms,
not sitters.
theorem the_copies_are_not_redundant :
    (∀ (W : Type) (S : Stage) (s : S.State) (w w' : W), w ≠ w' →
        (s, w) ≠ (s, w') ∧ indist (door S W) (s, w) (s, w'))
      ∧ (∀ (W : Type) (S : Stage) (w₀ : W),
          (∀ x y : (door S W).State, indist (door S W) x y → x = y) →
            ∀ (s : S.State) (w : W), (s, w) = (s, w₀))
      ∧ ¬ (∀ a b : Nat, sq (a + b) = sq a + sq b) :=
  ⟨fun _ S s _ _ h => the_guest_is_real_and_unread S s h,
   fun _ S w₀ h => a_door_that_checks_papers_unpersons_its_guests S w₀ h,
   fun h => the_square_breaks_the_sum (h 1 1)⟩

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

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

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

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

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

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

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

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

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

end Foam.Maps.ShinichiMochizuki