The divisional, compressing nature of names

[void4]

Naming a proof (theorem)/defining a short reference to a longer thing (proof tree, token sequence...) gives one the ability to make the proofs that depend on them shorter. Like a function name in programming, it can be reused because it has outputs and (sometimes) inputs (like axiom schemas or theorems were the assumptions can be substituted for something).

Terrible figure follows:

Say, "2" is defined to be equivalent to the set {{},{{}}}
So naming has a compression effect, if a name is used many times.
Which leads me to the question: What is the optimal choice of names?
Like, if all proofs were extended to just using axioms and the modus ponens deduction rule

Number of the log of expanded (including duplicate) proof steps vs number of subtheorems:

(https://github.com/void4/mmplot)

is there a shorter set of names? Or does the set of names we humans use really lead to the shortest number of proof steps overall?
Maybe there's something "between the names", a specific subtree of some proof or pattern that is often used, but unnamed?
I guess this is equivalent to asking "what is the optimal choice of instructions for a virtual machine".
For all possible programs, there is no single optimal set, thanks to Kolmogorov and the pidgeonhole principle, every choice constrains the space somehow, which programs are shorter/"closer" and which are longer.
Language is mostly a tool for communication (now also for formalization and persistence), so some concepts that are commonplace might have no name yet.
Or someone might have thought of the name but has not communicated it.

Mathematicians seem to like to name theorems after the people who invented/discovered them. But are there also names for some more detailed aspects of the work? There are names that refer to different types of proof like

"direct proof"
"proof by induction"
"proof by contraposition"
"proof by contradiction"

etc.

But are there ones for more fine grained patterns of deduction that are/can be communicated even though they are more intuitive/unconscious?

A name creates a division, a detailed definition defines the boundary of an object and the world it is in.

Names also have a causal nature. Only when a previous name was defined can it be used to build more things that can be named again, see Wolframs notes on "All Possible Theorems"

With all the theorems written out in “order of complexity”, I tried seeing which theorems I could prove just from theorems earlier in the list. Many were easy to prove. But some simply couldn’t be proved. And it turned out that these were essentially precisely the “named theorems”:

https://writings.stephenwolfram.com/2020/09/the-empirical-metamathematics-of-euclid-and-beyond/