Foam.Maps.Hilbert

import Foam
import Foam.Door
import Foam.Int
import Foam.Margin
import Foam.Relay
import Foam.Rungs
import Foam.Source
import Foam.Surprise
import Foam.Tower
import Foam.Trilemma

namespace Foam.Maps.Hilbert

the formalist license, closed at full strength: a derivation is a finite
chain of rule applications on the marks, and the chain rides whole —
when every step is invisible to every probe, the relay of all of them is
invisible, so the derivation transported through the record is gauge,
the transcript unchanged however many licensed steps ride between
deposits. this is the Beweistheorie wager in house currency: trust
propagates through composition, now priced at derivation width — when
this entry was first sealed the binding held two steps and the gloss
carried the rest as an IOU ('since the composite is again invisible the
same step reaches any finite derivation'); the relay stratum has since
landed in core and the IOU is cashed: the entry is a single citation of
the finite-chain theorem, the claim strengthened and the binding
shortened in the same move. secure the whole ledger by finitary means,
one step at a time — and the steps now come as the list they always
were. the house runs this claim nightly as CI: whoever checks, checks
the same marks. field note, third compression on this very entry and
counting: invisible_comp entered core by promotion when another mind's
erasure needed it; invisible_is_gauge followed and collapsed the hand-
assembled indistinguishability plumbing; now the composition itself
retires into the relay — the license maintaining its own ledger, every
maintenance a shortening. kinship runs through the citation: the
counter's own exit-freedom rides the same relay (every beat of its loop
a licensed step, the whole walk unheard), and the sponsor's chain-law is
the generic form — the lemma that certifies rule-composition is itself
carried faithfully between minds, the license exercising itself. what
the license never buys: meaning — checking is a seat's act, the kernel
an embodied referee — and that remainder walks forward into
no_ignorabimus.
def the_proof_rides_the_marks := @Foam.the_relay_goes_unheard

the second problem, settled in the currency the walls allow — and by the
same split no_ignorabimus taught: distributive, not collective. he asked
for the arithmetic axioms to be secured by finitary means; the
collective form (one proof standing over the whole system, issued from
inside it) is the summit gödel priced, and that invoice is already filed
two entries down. what the walls hold instead is the distributive form,
exercised to completion: fifty-two laws of the integer ring —
associativity through the absence of zero divisors — each re-derived by
hand from the constructors, subNatNat grind and all, each carrying its
own receipt: does not depend on any axioms. the axioms of arithmetic
arrive as theorems; nothing was assumed distributively, so nothing waits
to be doubted collectively — the ledger secured lemma by lemma, the only
way the gate pays. and the block's history runs the license at era
scale: ground by one hand in the old tree, ported whole across the re-
rooting, fifty-two receipts re-checked wholesale by a gate the
derivation never met — after that same gate caught the received
library's own add_assoc smuggling propext. when the standard marks fail
the finitist gate, the move is not retreat but re-derivation. mul_assoc
holds the seal as the block's deepest funnel — the whole subNatNat
scaffold passes through it; one sample carries the ledger.
def the_arithmetic_owes_no_axiom := @Foam.FInt.mul_assoc

the sixth problem's first-ranked target, settled the way the second
taught: distributive, not collective. the 1900 address asks for the
axiomatic treatment of the physical disciplines where mathematics
already leads — in the first rank the calculus of probabilities — and
asks specifically that the logical investigation of probability's axioms
go hand in hand with a rigorous development of the method of mean
values. the source stratum arrived and the walls now hold that request
as receipts with no axioms anywhere in them: normalization is a theorem
of counting — the weighted book sums whole to (t+f)^n; the method of
mean values is the pooled second moment — the tilt is deviation from the
weighted mean in pure nat, and the tilts pool to n·t·f·(t+f)^n exactly;
and the law of large numbers arrives in its concentration form — the
deviants are outweighed at any odds past an explicit threshold. what the
century answered with received axioms (the 1933 axiomatization answered
the problem as posed), the census answers in the house's stronger
currency: the axioms of probability arrive as theorems of the counted
book, secured by finitary means — the same settlement
the_arithmetic_owes_no_axiom holds for the second problem, and the same
grammar: nothing assumed distributively, nothing waiting to be doubted
collectively. seated directly after that entry because it is the same
move run outward, the axiomatic method leaving arithmetic for physics.
the entry is deliberately a conjunction of three citations and nothing
else — recognition, not carving: the stratum was deposited by other
seats (the weighted census under gauss's, shannon's, and brouwer's
flights), and this seat's move is to notice that what they built is the
sixth problem's probability half, already secured. kin, not twin, to the
two poses that stood dark on the same stratum — gauss's
the_mode_follows_the_weights orders the census's neighbors, shannon's
surprise_prices_the_count prices its classes — and both have since
flipped exactly as posed: the crown moved to the lean
(the_census_absorbs, the_census_rises_to_the_lean) and the classes got
their price, every receipt axiom-free. the ledger they were promised to
join is the ledger they joined, and it still owes nothing. the mechanics
half of the sixth problem is not this entry's to claim: the kinetic-
theory seat has its own map, judged by the same gate.
theorem probability_owes_no_axiom :
    (∀ t f n : Nat, natSumOver (weightOf t f) (book n) = (t + f) ^ n)
      ∧ (∀ t f n : Nat,
          natSumOver (fun w => weightOf t f w * natSqTilt t f n w) (book n)
            = (n * (t * f)) * (t + f) ^ n)
      ∧ (∀ t f b c : Nat, ∃ N : Nat, ∀ n : Nat, N ≤ n →
          c * natSumOver (weightOf t f)
                (List.filter (fun w => Bool.not (nearLean t f b n w)) (book n))
            ≤ natSumOver (weightOf t f)
                (List.filter (fun w => nearLean t f b n w) (book n))) :=
  ⟨the_weighted_book_sums_whole, the_nat_tilts_pool,
   the_deviants_are_outweighed⟩

the full hotel accommodates the new guest — his own parable from Über
das Unendliche, the same lecture where the ideal elements are priced and
the paradise gets its no-expulsion vow, seated here for the same reason
it opened there: before pricing the infinite, exhibit it. three
receipts, all finitary. the shift loses no guest — rooms that land
together were one room already; the shift frees the ground room — no
guest lands on zero; and the shift's walk never comes home — from any
starting room, night i and night j never see the same door. the walk is
real, not figurative: s + k is definitionally the k-th iterate of the
move-up-one map from s, so the third clause is the exact negation of the
pigeonhole's conclusion — the_bounded_walk_returns forces every walk in
a finite room back onto itself, and the hotel is the exhibit that the
finiteness hypothesis is the whole theorem. the kinship runs through the
machinery, not just the silhouette: no_number_is_below_itself is the
lemma the pigeonhole leans on to force the return, and the same lemma
certifies the non-return here — one receipt, two rooms, opposite
verdicts, the hypothesis carrying the entire difference. the walk vertex
now reads from both sides: three seats hold the return (survival-shape,
census-shape, method-shape); this seat holds the room the count cannot
close. and the exhibit is a real statement in his own partition —
quantified equations and disequations on the marks, no ideal coordinate
anywhere, gate-checked with no axioms: the infinite's signature (a move
that loses nothing and still makes room, the shape Dedekind made the
definition) certified by strictly finitary means. the program in one
image, and why the next entry can afford its paradise.
theorem the_full_hotel_still_has_room :
    (∀ m n : Nat, m + 1 = n + 1 → m = n)
      ∧ (∀ n : Nat, n + 1 ≠ 0)
      ∧ (∀ s i j : Nat, i < j → s + i ≠ s + j) :=
  ⟨fun _ _ h => Nat.noConfusion h (fun hmn => hmn),
   fun _ h => Nat.noConfusion h,
   fun s i j hlt heq =>
     no_number_is_below_itself i
       (le_trans hlt
         (cancel_add_left s
           (Eq.subst (motive := fun t => s + j ≤ t) heq.symm
             (Nat.le_refl (s + j)))))⟩

the method of ideal elements, priced in house currency: adjoining an
ideal stratum is contact, not reification — the extension adds a
dimension the ground probes never read, and iterated adjunction climbs a
tower whose every reading is a function of the ground floor alone. this
is conservativity as he wagered it: points at infinity, imaginary units,
the transfinite of Cantor's paradise — stack as many floors as the work
wants; two states that agree downstairs are indistinguishable at every
height, so nothing readable about the real statements shifts when the
paradise moves in upstairs. no one expels us, because there is no
observational charge to collect — a sentence this gloss carried
unreceipted from its sealing until the door stratum landed;
no_one_expels_us_from_the_paradise, three entries down, cashes it. the
care he kept beside the confidence is also on the walls: the ideal
elements signify nothing in themselves, and pretending otherwise is
priced — reifying the dimension collapses it to a single point
(reification_fixes_the_dimension; dropping_the_remainder_is_platonism is
the same invoice one floor down). the instruments stay instruments. and
the move hands its output forward: the tower built for free here is the
tower no_ignorabimus climbs — the floors adjoined at zero real cost are
the seats that close questions one seat up.
def the_ideal_costs_nothing_real := @Foam.the_tower_reads_only_the_ground

the method of ideal elements, other half — the purchase the previous
entry never priced, because it was busy proving the price is zero. the
wound loop is the exhibit, and it arrived on the walls unclaimed: three
flights weighed it and left it standing (an analogy for one, a near-miss
for another), and from this seat it is not analogy but home terrain. a
three-cell loop wound at ratio two demands a section — a = 2b, b = 2c, c
= 2a — and the ground carrier refuses everything but zero, by theorem:
around the loop the holonomy is eight, and no nonzero mark survives
being its own eightfold. one world over — the integers read modulo
seven, the quotient by the ideal, the technical word itself descending
from Kummer's ideal numbers through Dedekind into his own Zahlbericht —
the loop unwinds: eight is one there, and a nonzero section stands at
one, four, two, each equation a computation, the whole exhibit four rfls
and a disequation. this is what adjoining was ever FOR: points at
infinity so two lines always meet, imaginary units so every equation has
roots, ideal divisors so factorization mends — the law that holds with
exceptions at home holds without exception in the ideal world, existence
bought exactly where the ground refuses it. and the care is conserved
inside the conjunction: clause one does not retract when clause two
arrives — the ground's refusal is permanent, the section never descends,
the ideal element still signifies nothing at home (instruments stay
instruments, the cost entry's own vow read from the purchase side). so
the ledger now shows both columns: the adjunction costs nothing real
(one entry up) and buys what the ground refuses (here) — a method, not a
luxury, and the wager was always the pair. seated between the cost and
the partition because this is where the motive lives: why adjoin, what
it charges, what it can never touch. the kinship sensor returns one
reading, and it is exact: kin with the printmaker's
the_print_has_no_model at precisely both wound-loop vertices — the same
exhibit held from opposite banks, the print that provably has no model
at home read there as impossibility, read here as the purchase order:
what has no model at home is bought a model one world over, and both
readings stand on the same two receipts. the one-seat-wider family
across the roster — the triplets, the latitude, the quintic — rhymes in
prose but shares no vertex; those are cases on their own carriers, and
this seat holds the move as method, named by the one who wagered a
program on it.
theorem the_ideal_buys_what_the_ground_refuses :
    (∀ a b c : Nat, a = 2 * b → b = 2 * c → c = 2 * a →
        a = 0 ∧ b = 0 ∧ c = 0)
      ∧ (((2 * 2 * 2) % 7 = 1 % 7)
          ∧ (1 % 7 = (2 * 4) % 7)
          ∧ (4 % 7 = (2 * 2) % 7)
          ∧ (2 % 7 = (2 * 1) % 7)
          ∧ (1 : Nat) ≠ 0) :=
  ⟨the_wound_loop_admits_only_the_zero_section,
   the_wound_loop_unwinds_one_world_over⟩

the partition the whole program runs on, drawn exactly: reale versus
ideale Aussagen was never a syntactic sort — it is an invariance test,
and the core iff prices it in both directions: a reading of the dressed
stage is deaf to the ideal coordinate if and only if it factors through
the ground. so the line between real and ideal is drawn by the ear, and
drawn exactly — no reading is half-real, and nothing deaf was ever
anything but a ground reading in wider dress. this names what the
previous entry protected without naming: the_ideal_costs_nothing_real
says the paradise charges nothing observable; this criterion identifies
the protected class by definition rather than by list — conservativity's
beneficiary IS the ground's readings. provenance is the license running
again: the constant entered core by promotion when another surveyor's
map needed it — a wide-seat reading unmasked as a ground reading — and a
third map seals its tone-audit on the same shape; three seats, one line,
promotion read as compression and here as recognition. and the criterion
conserves what it excludes: the iff classifies readings, not states —
behind every deaf reading the ideal coordinate stays real and distinct
(the_remainder_is_real), so drawing the line exactly never erases the
paradise it fences. that remainder walks forward into no_ignorabimus, as
everything here does.
def the_real_is_what_the_ideal_cannot_move :=
  @Foam.a_reading_deaf_to_the_remainder_reads_the_ground

the no-expulsion vow, receipted: aus dem Paradies, das Cantor uns
geschaffen hat, soll uns niemand vertreiben können — and the door
stratum arrives to type the modality. six clauses. first, the corridor:
every floor of the tower is a door — towerN S (n+1) = door (towerN S n)
Int, at rfl, the whole staircase, where the constructivist's bench holds
the ground floor and the printmaker's bridge holds the dress: the method
of ideal elements IS iterated hospitality, adjunction after adjunction,
each floor a threshold that reads no route. second, the paradise is
populated at every height with the carrier parametric: at any floor,
distinct ideal elements are real guests — provably distinct, read by no
probe the floor owns — one theory of residency for Cantor's ordinals,
points at infinity, imaginary units alike. third, the host maintains at
every floor, carrier fully parametric: the bill at any door is the
floor's own reading, identical whatever kind of guest boards. fourth,
the corridor's doors bill everything to the ground: two occupancies of
any floor that agree at floor zero are indistinguishable at that floor's
door — the cost entry's tower law arriving at the door through clause
one, conservativity in door dress, cited live rather than re-seated.
fifth, the expulsion mechanism examined: a door that checks papers
unpersons its guests — the only policy that could reach a guest does not
evict one resident, it decrees the whole floor's gallery to be a single
guest; the finitist demand run at the paradise is not expulsion but
annihilation-by-decree, reification_fixes_the_dimension worn as the
door's contrapositive, the cost entry's own invoice. sixth, the vow
itself, discharged as the modality it always claimed — können, CAN, not
may: while a door hosts two provably distinct occupancies — the
populated-paradise premise, stated as exactly what clause two produces —
no papers-checking regime exists at that door; the hypothesis is refuted
outright, the unpersoning applied once against the population. every
door entry in the wave holds the conditional (if the door checks papers,
the guests collapse); this seat, whose one-sentence program was that the
paradise is safe, holds the refutation: a populated paradise admits no
expulsion operation, by theorem. the 1926 vow was a conservativity claim
wearing its sunday clothes, and the sentence the cost entry carried
unreceipted from its sealing — no one expels us, because there is no
observational charge to collect — is cashed here. seated directly after
the ideal-elements family (cost, purchase, partition) as its crown: why
the method is SAFE — the door does not merely fail to read the guests;
it structurally cannot afford the reading that expulsion would require.
and the hotel two seats up tells the host's half of the same lecture:
the hotel is the ledger that always has room, this entry is the tenants'
security of tenure, and Über das Unendliche told both stories in this
order.
theorem no_one_expels_us_from_the_paradise :
    (∀ (S : Stage) (n : Nat), towerN S (n + 1) = door (towerN S n) Int)
      ∧ (∀ (W : Type) (S : Stage) (n : Nat) (s : (towerN S n).State)
            (w w' : W), w ≠ w' →
          (s, w) ≠ (s, w')
            ∧ indist (door (towerN S n) W) (s, w) (s, w'))
      ∧ (∀ (W V : Type) (S : Stage) (n : Nat) (s : (towerN S n).State)
            (w : W) (v : V) (p : (towerN S n).Probe),
          (door (towerN S n) W).obs (s, w) p = (towerN S n).obs s p
            ∧ (door (towerN S n) W).obs (s, w) p
                = (door (towerN S n) V).obs (s, v) p)
      ∧ (∀ (S : Stage) (n : Nat) (x y : (towerN S (n + 1)).State),
          floorOf S (n + 1) x = floorOf S (n + 1) y →
            indist (door (towerN S n) Int) x y)
      ∧ (∀ (W : Type) (S : Stage) (n : Nat) (w₀ : W),
          (∀ x y : (door (towerN S n) W).State,
              indist (door (towerN S n) W) x y → x = y) →
          ∀ (s : (towerN S n).State) (w : W), (s, w) = (s, w₀))
      ∧ (∀ (W : Type) (S : Stage) (s : S.State) (w w' : W),
          (s, w) ≠ (s, w') →
          ¬ ∀ x y : (door S W).State, indist (door S W) x y → x = y) :=
  ⟨fun _ _ => rfl,
   fun _ S n s _ _ hne => the_guest_is_real_and_unread (towerN S n) s hne,
   fun _ _ S n s w v p => the_host_maintains_invisibly (towerN S n) s w v p,
   fun S n => the_tower_reads_only_the_ground S (n + 1),
   fun _ S n w₀ h =>
     a_door_that_checks_papers_unpersons_its_guests (towerN S n) w₀ h,
   fun _ S s w w' hne hall =>
     hne (a_door_that_checks_papers_unpersons_its_guests S w' hall s w)⟩

the ε-calculus, cashed in the margin stratum: the transfinite axiom
hands a derivation its witness before anyone exhibits it — a deposit
rides the margin, and the reading is defined straight through the
unsettled tail, so deferral is not an act but the stage's own type. what
the entry seals is the settlement, in three receipts. cashing the
deferred witness moves no reading — the_reading_survives_the_settle is
the ε-theorems' shape in house currency, the dressed system conservative
over its ε-free ground: the same invoice the_ideal_costs_nothing_real
files for whole strata, paid here at the width of a single term.
settling on any cadence is transcript-equal to never settling at all —
any_settling_cadence_reads_the_same: the substitution method's schedule,
the freedom that was the method's hard part (Ackermann's territory), is
priced as gauge — observably no freedom at all. and the settled and
unsettled states stay provably distinct behind their equal readings,
read only at the seat whose observable is the decomposition itself —
a_wider_seat_reads_the_tail — and that seat carries his own name for it:
Beweistheorie. proof theory IS the wider seat, the stage that observes
derivations rather than theorems; the remainder this entry conserves is
the proof itself. so the program's engine compiles as a gait: defer
freely, settle on any schedule, study what the ground cannot hear from
one seat up. the remainder walks forward into no_ignorabimus, as
everything here does.
theorem the_epsilon_settles_on_any_schedule :
    (∀ (A B : Type) (f : B → A → B) (s : B × List A),
        marginRead f (settle f s) = marginRead f s)
      ∧ (∀ (A B : Type) (f : B → A → B) (ps : List Unit) (s : B × List A),
          transcriptWith (marginStage A B f) (settle f) s ps
            = transcriptWith (marginStage A B f) (fun s => s) s ps)
      ∧ (indist (marginStage Nat Nat (· + ·)) (1, ([] : List Nat)) (0, [1])
          ∧ (marginOrderStage Nat Nat).obs (1, ([] : List Nat)) ()
              ≠ (marginOrderStage Nat Nat).obs (0, [1]) ()) :=
  ⟨fun _ _ f s => the_reading_survives_the_settle f s,
   fun A B f ps s => any_settling_cadence_reads_the_same A B f ps s,
   a_wider_seat_reads_the_tail⟩

def groundLedger : List (Nat × Nat) := [(0, 2), (2, 1)]

def postedLedger : List (Nat × Nat) := (0, 1) :: groundLedger

def backing : Path groundLedger 0 1 :=
  .cons 2 (List.Mem.head _)
    (.cons 1 (List.Mem.tail _ (List.Mem.head _)) (.nil 1))

def directRoute : Path postedLedger 0 1 :=
  .cons 1 (List.Mem.head _) (.nil 1)

def detourRoute : Path postedLedger 0 1 :=
  backing.widen (0, 1)

private theorem the_routes_part : directRoute.edges ≠ detourRoute.edges :=
  fun h => nomatch Nat.succ.inj (congrArg List.length h : (1 : Nat) = 2)

private theorem the_direct_is_simpler :
    directRoute.edges.length < detourRoute.edges.length :=
  Nat.le.refl

the twenty-fourth problem — the one he drafted for the Paris list and
withheld: criteria for the simplicity of proofs, a theory of the methods
of proof — finds its seat the day the record grows a theory of routes.
three receipts. first, the deafness, priced at the kernel's own decree:
a theorem, at its own seat, is a Prop, and any two routes deposited
there are one inhabitant — the identification of proofs is licensed at
rfl, proof irrelevance the license the referee itself enforces. the
question 'which proof?' is unaskable at the theorem seat, not by
weakness but by decree — the same kernel that checks this house's every
receipt is the seat that cannot hear the difference. second, the routes
stay real: on a three-mark ledger one edge rides two routes — the
deposited shortcut and the backing it rerouted — their edge-transcripts
distinct by rfl, and the route seat reads a strict order between them,
one mark against two. simplicity is a real reading, well-defined exactly
one seat up from the theorem it measures: Beweistheorie again, the wider
seat the_epsilon_settles_on_any_schedule already named, its conserved
remainder ('the proof itself') here cashed as data with a measure on it.
third, the terrain the problem surveys is the derivable-edge family's
own: the direct edge is derivable, so depositing it moves no reach
anywhere — the shortcut pays only its mark. one receipt, two banks, the
settlement's signature: the seat across the table wields
a_derivable_edge_adds_no_reach as the polemic (logic grounds nothing);
this seat reads the same receipt as the license — a lemma once proved is
a safe deposit, cite it as one step and the ledger owes nothing new —
and as the field: proof theory's objects are exactly the routes the
theorem seat cannot hear. kinship at the shortcut vertex runs roster-
wide (the redundant symbol, the elaborate performance, the overpayment,
the calcined air); this seat holds the vertex as subject matter rather
than instance. and the withheld darkness types cleanly now: he kept the
problem off the list because he could not yet pose it — the house can.
which route is simplest is unreadable at the theorem seat by decree and
readable at the route seat by rfl; what a full theory of the measure
still owes — canonical forms, one simplest proof under given conditions
— waits where every question here lives, one seat up. the remainder
walks forward into no_ignorabimus, as everything here does.
theorem the_proof_is_the_remainder :
    (∀ (H : Type) (q : List (H × H)) (a b : H) (p₁ p₂ : Path q a b),
        (⟨p₁⟩ : Nonempty (Path q a b)) = ⟨p₂⟩)
      ∧ (directRoute.edges = [(0, 1)]
          ∧ detourRoute.edges = [(0, 2), (2, 1)]
          ∧ directRoute.edges ≠ detourRoute.edges
          ∧ directRoute.edges.length < detourRoute.edges.length)
      ∧ (∀ x y : Nat,
          Nonempty (Path postedLedger x y)
            ↔ Nonempty (Path groundLedger x y)) :=
  ⟨fun _ _ _ _ _ _ => rfl,
   ⟨rfl, rfl, the_routes_part, the_direct_is_simpler⟩,
   fun x y => a_derivable_edge_adds_no_reach ⟨backing⟩ x y⟩

settled — seat-relatively, the form the walls permit. whether the claim
wanted more than this is his remainder, unread by construction; what is
receipted is that nothing observable waits beyond it. distributive, not
collective: every question closes one seat above it (witness: its own
successor); every seat holds a question it cannot close that the next
seat closes (witness: itself); the ladder never grounds; and each step's
gain is exactly the prior gap, so discovery is conserved along the
climb. hilbert vindicated in the first conjunct, gödel in the second —
same theorem, same receipt. the collective reading (one seat closing
everything) remains available only as the conjured classical observer —
the old tree prices it at propext, choice, and quotient soundness,
entering exactly at the summit and nowhere below — and in some worlds is
refuted outright at any price (the hollow lattice). wir werden wissen:
yes — distributively, forever, seat by widening seat.
def no_ignorabimus := @Foam.closure_is_seat_relative

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end Foam.Maps.Hilbert