Mathlib's Extreme Value Theorem, imported (labeled scaffolding, not ours)

The command greps for this fact's own marker line rather than trusting the exit status, so a suite that compiles to zero tests -- this repository's signature defect -- fails instead of exiting 0. `lean4export_census` reports 2171 declaration records / 2486 admitted declarations for the transitive dependency closure of `IsCompact.exists_isMaxOn` at Mathlib commit c5ea00351c28e24afc9f0f84379aa41082b1188f (module: see MANIFEST.json), all admitted by `Kernel::add_declaration` with ZERO declines. `Kernel::render_lean` of the admitted type is `formal.statement` verbatim. the constructive substitute (approximate, non-attaining) is F:creal-evt-approx-max (row 1), the boundary reduction is F:creal-evt-attained-max-decides-sign (row 2).

`Kernel::axiom_footprint` over the imported environment reports [Classical.choice, Quot, Quot.lift, Quot.mk, Quot.sound, String.Internal.append, propext, wrapped._@.Mathlib.Topology.Defs.Filter.2998874748._hygCtx._hyg.2] -- eight names, not Lean's own three (`#print axioms` reports [propext, Classical.choice, Quot.sound] for both theorems at this pinned commit, per docs/formalized-math-2026-08/08-ivt-and-evt-measured-against-mathlib.md section 3). The extra five are this kernel's finer-grained classification of the Quotient package (Quot itself, Quot.lift and Quot.mk alongside Quot.sound -- documented in fact.schema.json's proof_route field as 'must not be silently reconciled to Lean's'), plus two names this specific dependency closure reaches that the three hand-picked Init/Std imports never did: a String.Internal.append opaque and a wrapped._@.Mathlib.Topology.Defs.Filter opaque wrapper from a well-founded-recursion definition somewhere in the Filter machinery both theorems' proofs transitively use. Neither is a defect in the translation; both are real trusted declarations Mathlib's own proof rests on for this statement, and Kernel::axiom_footprint is reporting them faithfully. The first three entries in this array are the assumptions the IMPORT ROUTE adds on top: that the exporter faithfully rendered Lean's environment, that this crate's NDJSON-to-kernel-term translation preserves meaning, and that the delivered bytes are the producer's intended export (format 3.1 has no footer, so completion is relative to the bytes handed over).