Rulial multiway system

There is only one full rulial multiway system (up to reparametrization based on the underlying model of computation). A particular multiway system is a fiber of this rulial multiway graph.
​
Full rulial multiway system is all possible mathematicses....
To reduce to a single fiber, as opposed to having to look at the whole rulial multiway system.
JG: Axiom system is a set of relations on the free rulial topos
Free topos: full rulial multiway system
Axiom system: relations imposed
If you always have to show your work, there would be no conclusions in mathematics

Completion in space vs branchial space

A completion is the squashing to zero of an entanglement cone or an elementary light cone....
The fact that the completion is possible is a consequence of univalence
Wick rotation in rulial space: completion is a crushing of a rulial elementary cone.
Observation in QM is like theorem proving in math [theorem proving conflates equivalent expressions]

Observational equivalence ↔ identity

Set theory

Axiom of extensionality: sets are equal if they have the same elements

Univalence Axiom

It claims to say there is only one type of equivalence
(A equivalent to B) equivalent to (A = B)
The middle equivalence is a completion, so you can apply the axiom again to that equivalence
This implies that you can implement the equivalence relation by adding rules....

The Observer in Mathematics

Causal Invariance ↔ no need to show your work

The ability to make measurements is an ability to crush cones

In mathematics, there are useful decidable equivalences
The crushing of cones by systematic means requires not too much wildness in their topology
​
Crucial point: the same observer can observe many things....

There is a possibility of a universal observer

The topology can’t be too wild (e.g. there can’t be an event horizon)

Proofs are geodesics in rulial space

Claim: model theory is to proof theory as geometry is to topology

Claim: model theory coordinatizes statements

f[f[a,b],c]
Proof multiway system defines a partial order on statements
Total order corresponds to a specific model

A model defines equivalences between statements

Time dilation : different models give proofs of different lengths
(some things are easier to prove over the rationals than over the integers)

What are causal edges?

They are the dashed lines of FindEquationalProof

Lemma dependency edges are the analog of causal edges

Energy ~ abstraction

Amount of use of previous results that you have to make ; AKA the height of the abstraction tower

The higher the amount of abstraction, the more geodesics are deflected, and so are longer: so the more abstraction there is, the longer the proofs are.

Gravity in mathematics: proofs become longer as a result of the presence of abstraction.

If you go near a part of statement space that involves lots of abstraction, then your proof path is attracted to the region of abstraction ... because all those causal edges give you a freeway in statement space.

Singularities

A model-like singularity is a decidable statement that can prove in finite time....

What is the analog of the gravitational constant?

There is a notion of volume in statement space

Density of independent mathematical facts relative to the number of all combinatorially possible statements

Tμν is related to the density of non-redundant / useful statements

Branchings in proof per unit volume

Represents tradeoff between computational effort and abstraction

Expansion of statement space

Mathematics is only effective insofar as it builds up a bolus of abstraction .... i.e. that the statement universe is expanding. Otherwise you might as well just follow a free-space geodesic of computational operations, without any shortcutting.