Expose literature inputs as explicit hypotheses

[kim-em]

The presentation proof uses nine classical results from the literature. Until now they were available only as global Lean axioms, which made the core proof appear unconditional and prevented clients such as Palomar from supplying those results as explicit assumptions.

This PR bundles the nine results in LiteratureInputs and makes the dependent proof graph take [LiteratureInputs] as an ordinary hypothesis. The binder is written directly on each declaration that needs it, so the dependency is locally visible without ambient include/omit plumbing.

The existing public API remains compatible. Generic _of_inputs declarations use only the standard three Lean axioms, while legacy capstones keep their original names and statements and uniformly print all nine literature axioms. GQ2.Foundations.AxiomInstance provides that compatibility layer by assembling the historical axioms into an instance.

The PR also adds explicit-input Palomar entry points and audits for both trust models. One encoding detail is that a Lean structure field cannot quantify over a fresh universe level, so the bundled B7 field uses M : Type, which covers every consumer here; the legacy B7 axiom retains its original M : Type* statement.

[roed314]

Thanks!