What makes a proof assistant a proof assistant?

Question

You open a code editor, define a syntax with lambdas, a few primitives. Then you invent some nice computation rules, some cool typing rules, and write a corresponding interpreter and "type checker". Congratulations! You just built a proof assistant! Now you can formalize all of mathematics on it! Or can you? After all, what makes the thing you built a valid "proof assistant"? What constitutes a "type checker"? As far as I'm concerned, you could have actually implemented Tetris, claimed that blocks are terms, their shapes are types, and the game loop is the computation rule. Who has authority to argue you're wrong?

When it comes to implementing a "programming language", the definition is much more clear. Just invent a syntax, a set of reduction rules and prove your thing Turing-complete. Then it is as good as a programming language is expected to be. When it comes to implementing a proof assistant, I have no idea. Sure, there are common things I see present in proof assistants, so, intuitively, I know what they are. They have lambdas and the corresponding dependent function space, they have inductive datatypes and their introductions and eliminations, and they must be consistent, which mean at least some type is uninhabited. But what if my "proof assistant" has no lambdas nor datatypes? It could have for example just combinators. I don't have a precise definition of what makes a "type theory" a "type theory".

What, formally, makes a program a valid proof assistant, in the same sense that Agda/Coq are? What is a precise and complete definition of a type theory? And what one must do to "justify" his syntax, reduction and typing rules? I'm making this specifically because, while I feel like I can, given enough time, implement something like A Cosmology of Datatypes, I do not feel the freedom to make any change, even minimal, to whatever the author did, because I do not know what justifies those things he did.