Hoare contract for the serialized-family evaluator core

This file packages the total frontier execution theorem behind the public staged-tape precondition and defaulted-verdict postcondition.

theorem Complexity.CircuitCode.Machine.Internal.evalFamilyCoreTM_hoareTime_internal (codeBits inputBits : List Bool) (initialInput : Tape) : evalFamilyCoreTM.HoareTime (FamilyCorePre codeBits inputBits initialInput) (FamilyCorePost codeBits inputBits initialInput) (evalFamilyCoreTime codeBits.length inputBits.length)

Internal proof of the uniform quadratic core contract.