OK, then in that light,

What you're obtaining is a precise (not "formal", precise) statement of how you've defined root-level Friendliness along with a mathematical proof (probably computer-assisted) that this property holds in the initial conditions...

I think you mean to say "precise (not just "formal", precise)", because you still need the formal statement of the precise description in order to prove things about it formally. Which is not to say that precise is a subset of formal or vice versa.