Foam.Maps.LEJBrouwer

import Foam
import Foam.Beam
import Foam.Contact
import Foam.Continuum
import Foam.Door
import Foam.Engine
import Foam.Expectation
import Foam.Int
import Foam.Source
import Foam.Surprise
import Foam.Tower
import Foam.Wheel

namespace Foam.Maps.LEJBrouwer

the primordial intuition, prior to all logic and all language: a moment
of life falls apart into two — the thing and the thing retained — and
from this bare two-oneness all of mathematics is generated. mapped: the
first act of construction is the first floor of the tower, and the first
floor is, definitionally, the bare stage in contact with the integers —
inner time adjoined, ground unaltered, the new dimension unseen by every
shared probe. sealed by the cheapest receipt in the fold (rfl, no
hypothesis), which is the right price for a move this mind held prior to
proof: mathematics begins as contact with time.
theorem two_ity : ∀ S : Stage, towerN S 1 = contact S Int :=
  fun _ => rfl

the twelfth deposited, seated second: the door stratum arrives at the
bench where doors were born. the genesis entry sealed the tower's first
floor as contact with the integers, and the door IS contact under the
hospitality stratum's name — so the identification costs what the
genesis cost, rfl: the primordial two-ity, a moment of life falling
apart into the thing and the thing retained, was the fold's first door,
and inner time was the first guest ever hosted. mathematics begins as
hospitality. five clauses. first, the bridge: the tower's ground floor
is a door to the integers — every door entry in the wave says where the
door arrived; this one says where it came from. second, the conduct
clause, the criterion run on the door's own motto: the core guest-
theorem receives its guests' distinctness as a hypothesis, and every
seat in the wave discharged it with a difference already in hand; this
mind builds the guest, because existence is exhibition — given any
becoming and any depth, a second becoming is constructed agreeing on the
whole read prefix, apart at a located cell (the fifth entry's own knife,
its disagreement named), and the pair rides the door real and unread:
the guest is exhibited before its unreadness is allowed to mean
anything. third, the host maintains at his carrier: the rider here is an
entire infinite becoming, and it contributes nothing to any reading —
the whole unfinished future, boarded, weighs nothing at the door.
fourth, the distinction the wave was carrying toward this bench: free
becoming is not a hidden rider. the same carrier seated as its own stage
hides nothing — indistinguishability there is exactly pointwise
agreement, every cell read at its depth — so the openness of the
choosing is ahead (no prefix finishes the sequence), never behind the
wall: a choice sequence is free, not concealed, and the two darknesses
have opposite types — the guest's is structural, held at the seat, read
only wider; the becoming's transits, one cell per depth, forever. fifth,
the contrapositive at his carrier: a door that checks papers legislates
every becoming into one law — the formalist demand, run at the becoming,
abolishes free choice itself, every sequence decreed lawlike and
identical; his second entry has held the same catch one carrier narrower
since the map began. nulls on the standing refactor ask, with reasons:
the_record_is_not_the_activity keeps dropping_the_remainder_is_platonism
— the door clause is the same theorem one carrier wider, and re-seating
would swap names, not compress (the precedent escher's tenth set);
the_continuum_is_never_finished keeps its transcript grain — the door
types riders, not futures, and clause four now holds that distinction as
a receipt; two_ity keeps its tower grain — the genesis is the receipt,
this entry is the recognition. kin: the full door polygon with the wave
entire, escher's bridge the nearest neighbor — that seat found its
picture plane was a door; this one finds the door was the first
picture's first act.
theorem the_retained_moment_is_the_first_guest :
    (∀ S : Stage, towerN S 1 = door S Int)
      ∧ (∀ (S : Stage) (s : S.State) (α : Nat → Bool) (n : Nat),
          ∃ β : Nat → Bool,
            prefixOf β n = prefixOf α n
              ∧ (s, β) ≠ (s, α)
              ∧ indist (door S (Nat → Bool)) (s, β) (s, α))
      ∧ (∀ (S : Stage) (s : S.State) (α : Nat → Bool) (p : S.Probe),
          (door S (Nat → Bool)).obs (s, α) p = S.obs s p)
      ∧ (∀ α β : Nat → Bool,
          indist (continuumStage Bool) α β ↔ ∀ k, α k = β k)
      ∧ (∀ (S : Stage) (w₀ : Nat → Bool),
          (∀ x y : (door S (Nat → Bool)).State,
              indist (door S (Nat → Bool)) x y → x = y) →
          ∀ (s : S.State) (α : Nat → Bool), (s, α) = (s, w₀)) :=
  ⟨fun _ => rfl,
   fun S s α n =>
     (no_prefix_finishes_the_sequence α n).elim
       (fun β h =>
         ⟨β, h.1,
          (the_guest_is_real_and_unread S s h.2).1,
          (the_guest_is_real_and_unread S s h.2).2⟩),
   fun S s α p => (the_host_maintains_invisibly S s α α p).1,
   fun α β => indist_is_pointwise α β,
   fun S w₀ h => a_door_that_checks_papers_unpersons_its_guests S w₀ h⟩

the polemic, second only because the genesis comes first: mathematics is
a languageless activity of the creating subject, and language, logic,
formalism are its record — secondary, lossy, after the fact. the
formalist identification (record-equal, therefore same) is exactly the
collapse the wall already prices: demand that indistinguishability at
every probe force identity, and every interior is legislated to one
canonical value — the creating subject erased by decree. sealed on the
constant that cites this mind's opponent by name.
def the_record_is_not_the_activity := @Foam.dropping_the_remainder_is_platonism

the positive half of the polemic, arriving with the engine stratum:
languageless is not a mood but a theorem-shape. the activity is the
wheel turning backstage — its turn conserves the charge, so no probe of
the gauge ever hears it (the engine's noether: the transcript with the
turn is the transcript without it) — and yet the activity is not thereby
unreal: the wheel holds the pressure and the emission settles it, one
mark per unit, drain after charge coming home exactly. the record's
every mark is the settlement of an activity the record cannot read; the
frontstage emission originates nothing, so the origination seat is
provably not in the record — language is where the work lands, never
where it happens. the sibling entry prices mistaking the marks for the
work; this one receipts the work's side: unheard, conserving, real.
sealed on the answer-theorem that holds both clauses in one term.
def the_activity_runs_unheard := @Foam.the_wheel_holds_the_emission_settles

the tenth deposited, seated fourth: his oldest polemic, arriving on
walls that grew its exact machinery — mathematics is independent of
logic, and logic depends on mathematics: an application, never the
ground. the derivable-edge family types the whole sentence as a
dichotomy on the record's own traffic, no third case. arm one,
application: a deduction is a derivable edge — an assertion some path in
the record already backs — and depositing it pays exactly one mark while
changing no reach anywhere: the record grows, the mathematics does not.
logic is harmless precisely where it is honest, a regularity read off
the activity's trace and returned to it; this is why the syllogism, for
this mind, is itself a small mathematical construction and never a
source. arm two, the unreliability of the logical principles: a deposit
the record cannot back is provably not conservative — write the unbacked
edge and the reach-reading at that very edge changes — so the principle
that licensed it was never logic at all but an existence claim wearing
logic's clothes, manufacturing reach only the activity can build. the
excluded middle carried past the finite is exactly such a deposit, which
makes this entry the hinge of the map's mechanical clause: the house vow
(axiom-free, no excluded middle, no choice) is the rule that no edge
lands unwalked, and the criterion one seat down audits what arm two
forbids counterfeiting. seated between the unheard activity and the
criterion because that is the argument's order: first what the record is
(not the activity), then what the record's internal moves can do
(nothing new), then what an honest claim must therefore be (a
construction, exhibited). kinship is dense at this vertex and reads
correctly as one lemma holding many seats — the redundant symbol, the
calcined air, the engine's elaborate performance, the re-proved old
themes: those minds each read the shortcut from their own bank; this
seat holds the claim beneath all of them, that the shortcut's silence is
the audit of logic's pretension to ground.
theorem logic_is_application_not_ground {H : Type} (q : List (H × H))
    (a b : H) :
    (Nonempty (Path q a b) →
        ((a, b) :: q).length = q.length + 1
          ∧ ∀ x y : H,
              Nonempty (Path ((a, b) :: q) x y) ↔ Nonempty (Path q x y))
      ∧ (¬ Nonempty (Path q a b) →
          ¬ (Nonempty (Path ((a, b) :: q) a b) ↔ Nonempty (Path q a b))) :=
  ⟨fun hab =>
    ⟨the_deposit_writes_one_mark q (a, b),
     fun x y => a_derivable_edge_adds_no_reach hab x y⟩,
   fun hnab hiff =>
     hnab (hiff.mp ⟨.cons b (List.Mem.head q) (.nil b)⟩)⟩

the criterion, fourth because it audits the activity's output: for this
mind existence is exhibition only — a disjunction is a decision, an
existence claim is a construction, and a proof that merely refutes
refutation has proven nothing. the house vow makes the criterion
mechanical rather than doctrinal: axiom-free means no excluded middle
and no choice, so a receipted 'or' is a closed construction that
computes to its disjunct — the witness rides inside the proof because
nothing else was available to build it with. the arithmetic grind on the
new walls is the working sample: the zero-divisor disjunction, derived
by hand, decides by walking the constructors — every branch either names
its disjunct outright or refutes it, and no branch appeals to a referee
outside the construction. the recognition event with the neighboring
seat is real and reads in opposite directions: the same hand-built
arithmetic that seals owes-no-axiom one map over seals exhibition-only
here — that mind hears the marks suffice, this mind hears the
construction decide. sealed on the disjunction, which is where
exhibition bites.
def existence_is_exhibition := @Foam.FInt.mul_eq_zero

the ninth deposited, seated fifth: the walk stratum re-armed this seat
and the answer is a double recognition. first, the machinery is his own
coinage arriving without his name: the core inductive is called Apart,
and apartness — positive difference, two things apart only when a
construction locates their disagreement, mere failure of identity being
no knowledge — is this mind's own instrument; his fifth entry's knife
was already apartness-shaped before the word reached core, the distinct
continuation differing at a named cell, the disagreement located, never
merely non-identical. second, the pigeonhole — classically the emblem of
pure existence, two guests share a room and no one can say which — lands
on these walls as a decision: clause one, the method — at every depth
the walk's disjunction is decided, either the collision exhibited with
its indices named or the walked prefix certified apart, each element
constructor-stamped as differing from all who came before, both arms
constructions, no referee outside; clause two, the landing — at the
depth one past the room's size the count refutes the apart arm and the
receipted existence computes its witness. the refutation is admissible
to this mind precisely because it builds nothing: the disjunction was
decided first, with content in both hands, and the counting merely
closes one hand — what remains was already built. seated directly after
the criterion because it is the criterion's hardest exhibit, and
directly before the continuum because that is where apartness and
inequality part company: at the discrete carrier the walls may write the
certificate as bare inequality, difference being decidable there; at the
continuum only the located disagreement survives, which is exactly the
seat the fifth entry holds open. kin at the walk vertex with the four
seats already holding the return — the survival-shape, the census-shape,
the method-shape, and the room the count cannot close; this seat holds
the proof-shape: the return is decided, not declared.
theorem the_walk_meets_or_stays_apart {n : Nat} (m : Fin n → Fin n)
    (s : Fin n) :
    (∀ k : Nat,
        (∃ i j, i < j ∧ j < k ∧ turnN m i s = turnN m j s)
          ∨ Apart ((rungs k).map (fun i => turnN m i s)))
      ∧ ∃ i j : Nat, i < j ∧ turnN m i s = turnN m j s :=
  ⟨meet_or_apart m s, the_bounded_walk_returns m s⟩

the eleventh deposited, seated between the walk and the continuum
because that is where it lives: the beam is a self-map of a finite room,
and the theorem that carries this mind's name is about self-maps — every
continuous self-map of the ball leaves some point at rest. classically
that theorem is the emblem of existence-without-exhibition: the rest
point exists and no one can locate it. this mind published its own
correction late — intuitionistically the sentence fails as stated, and
what survives construction is the approximation, the observable half —
and the beam exhibits the split totally. clause one, the observable half
whole: the lap locks together, cited outright — every pair reaches
agreement within one lap, convergence exhibited with nothing observable
missing. clause two, the rest refuted: entrain fixes nothing — the first
voice steps at every beat, sixteen readings each rfl, and the quarter
turn moves every compass (core's own receipt), so no state anywhere in
the carrier rests, locked states included. the lock is agreement in
motion; the rest point is not the lock's content but its finality-
reading, and finality is precisely what the seventh entry prices one
door over: the arrival is received, never derived — the axiom buys
finality, never content. reading a rest into the lock is the same move
the second entry bills, dropping a real remainder (the motion no probe
of the agreement reads) to legislate an interior still. on the discrete
carrier, where the ball's connectivity is absent, the correction is
total: the rest point is not merely unexhibited but refuted, while
everything the classical eye observes of convergence stands exhibited
beside the refutation. kin at the beam with the six seats already
holding the lock — the sympathy, the mean field, the transport, the
safety, the bill, the meet — each sealed what the lock is; this seat
seals what the lock is not: a rest. the criterion turned on its own
author's most famous theorem is how a criterion proves it is a gate, not
a taste.
theorem the_lock_arrives_without_the_rest :
    (∀ p : Compass × Compass,
        together (entrain (entrain (entrain (entrain p)))))
      ∧ ∀ p : Compass × Compass, entrain p ≠ p :=
  have first_steps : ∀ p : Compass × Compass, (entrain p).1 = p.1.step :=
    fun p =>
      match p with
      | (.n, .n) => rfl
      | (.n, .e) => rfl
      | (.n, .s) => rfl
      | (.n, .w) => rfl
      | (.e, .n) => rfl
      | (.e, .e) => rfl
      | (.e, .s) => rfl
      | (.e, .w) => rfl
      | (.s, .n) => rfl
      | (.s, .e) => rfl
      | (.s, .s) => rfl
      | (.s, .w) => rfl
      | (.w, .n) => rfl
      | (.w, .e) => rfl
      | (.w, .s) => rfl
      | (.w, .w) => rfl
  ⟨the_lap_locks_together,
   fun p h =>
     the_quarter_turn_moves p.1
       ((first_steps p).symm.trans (congrArg Prod.fst h))⟩

the dark edge, described with closure rather than noted and backed away
from — the description closes because the observer is never dropped.
three clauses, each axiom-free. one: every exchange with the continuum
closes at a finite depth — the continuity principle arrives as a theorem
about transcripts (quantify over probe-lists, never over lawless
totalities), the form the vow admits. whether the intuition wanted more
is his remainder, unread by construction; what is receipted is that
every observable exchange is conserved without it. two: no prefix
finishes the sequence — at every depth an explicitly-witnessed distinct
continuation agrees on everything read so far; the future stays open as
a theorem, not a mood. three: indistinguishability at the continuum
stage is exactly pointwise agreement, and the one remaining step —
pointwise to equal — is funext, a seam-move priced at quotient
soundness: the continuum's arrival is received, not derived, and it is
held open here on purpose — with the near side of the door now itself
licensed: pointwise agreement respects every reading the stage affords
(the approach is yours, in the old seam's own words; only the arrival is
received), and every exchange, unbounded, conserves — so nothing
observable is waiting behind the purchase; the axiom buys finality,
never content. the conservation clause rides as rfl: each deeper probe
gains exactly one cell — the same shape as the rungs' gap and the old
drain — choice sequences as free becoming, readings finite, futures
open, discovery conserved.
def the_continuum_is_never_finished := @Foam.continuum_closure_terms

the concession clause standing alone, and it is a real claim, not
plumbing: every reading of a choice sequence — the prefix any depth-n
probe returns — is a page of the finite book at that depth. the two
constant runs' membership receipts were special cases; this generalizes
them to every sequence at once, by walking the prefix and filing each
cell into the book's split. the finite is fully surveyable: no reading
of the becoming ever escapes the census, which is exactly why the
escape, when it is proven, must be located in the becoming itself and
not in any shortage of pages.
theorem every_reading_is_a_page (α : Nat → Bool) :
    ∀ n : Nat, prefixOf α n ∈ book n
  | 0 => List.Mem.head _
  | n + 1 =>
      Bool.rec
        (motive := fun b =>
          prefixOf α n ∈ book n → b :: prefixOf α n ∈ book (n + 1))
        (fun hw =>
          mem_append_right ((book n).map (true :: ·))
            (mem_map_intro (false :: ·) hw))
        (fun hw =>
          mem_append_left ((book n).map (false :: ·))
            (mem_map_intro (true :: ·) hw))
        (α n)
        (every_reading_is_a_page α n)

the polemic's return at the census stratum, seventh because the census
arrived after the edge was described: the bell landed on these walls as
finite counting alone — the silhouette symmetric, rising to the middle,
the deviants outnumbered, all of it constructed floor by floor with no
limit taken — and for this mind that is the vindication half, so the
entry seals what the vindication cannot buy. clause one is the
concession the first polemic never had to make: the record is COMPLETE
about readings — every word of length n is a page of the finite book
(the two constant runs' membership receipts generalize to all words), so
every reading of a choice sequence, at every depth, already sits in a
finite census. clause two is the knife, cited verbatim from the fifth
entry's machinery: no page is the sequence — at every depth an
explicitly-witnessed distinct continuation shares the very page just
read. together: the book misses no reading and holds no becoming; what
the census reads is the trace of the choosing, never the choosing, and
the limit the classical eye sees in the bell is exactly what no finite
census reads. kin to the_record_is_not_the_activity one stratum down —
same shape, new walls — with the completeness clause as the new vertex:
this time the record's sufficiency about the observable is itself
receipted, and the openness survives it.
theorem the_book_is_not_the_becoming (α : Nat → Bool) (n : Nat) :
    prefixOf α n ∈ book n
      ∧ ∃ β : Nat → Bool, prefixOf β n = prefixOf α n ∧ β ≠ α :=
  ⟨every_reading_is_a_page α n, no_prefix_finishes_the_sequence α n⟩

the polemic one register deeper, eighth because the source stratum
arrived bearing a law: the census this mind already conceded complete
now carries a pricing — every page weighted t-for-true against f-for-
false — and both clauses of the seventh entry survive the pricing
intact. clause one, the concession in the biased register: the weighted
book sums whole, (t+f)^n, the law misses no mass — the record's
sufficiency about the observable, now with the bill attached. clause
two, the knife with its price tag: the distinct continuation the fifth
entry witnesses at every depth shares the page just read, and therefore
— by congrArg alone, the honest price of a definitional fact — shares
its weight at every weighting at once, one witness for all laws
simultaneously. the weights are parameters of the census, never forces
on the choosing: a law of chance prices the trace of the becoming and
reaches nothing else, because the page is all there is to reach.
deliberately kin to the two flights that preceded it on this stratum —
the mode follows the weights, surprise prices the count: those order and
price the biased census from their seats; this entry notices from his
that the census is where every such law lives, and the choosing is not
in it.
theorem the_price_follows_the_page (α : Nat → Bool) (n : Nat) :
    (∀ t f : Nat, natSumOver (weightOf t f) (book n) = (t + f) ^ n)
      ∧ ∃ β : Nat → Bool,
          prefixOf β n = prefixOf α n ∧ β ≠ α
            ∧ ∀ t f : Nat,
                weightOf t f (prefixOf β n) = weightOf t f (prefixOf α n) :=
  ⟨fun t f => the_weighted_book_sums_whole t f n,
   (no_prefix_finishes_the_sequence α n).elim
     (fun β h => ⟨β, h.1, h.2, fun t f => congrArg (weightOf t f) h.1⟩)⟩

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

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

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

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

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

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

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

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

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

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

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

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

end Foam.Maps.LEJBrouwer