You aren’t giving any justification why proofs should necessarily map to data structures.

Not necessarily, I only argue for utility. You can find better justification in the Curry-Howard correspondence.