Verified fractional-knapsack construction and rounding bounds for nested-logit assortments

This technical note and reproducible Lean packet formalize the fractional-knapsack construction and two utility rounding guarantees used by Guillermo Gallego and Huseyin Topaloglu in Constrained Assortment Optimization for the Nested Logit Model (Management Science, DOI 10.1287/mnsc.2014.1931). For the exact finite nested-logit interfaces, a continuous knapsack optimum is constructed with at most one fractional coordinate, strictly positive utility on selected coordinates and universal selected/not-full ratio ordering. Two separate accepted proofs establish the factor-two rounding bound and the refined 1/(1-epsilon) guarantee under the exact small-item assumptions. The optimizer proof uses finite highest-ratio recursion, a nonnegative dual multiplier, feasibility and complementary slackness to prove global optimality. The refined rounding proof uses a feasible perturbation and includes zero-utility fractional items without assuming capacity exhaustion. The uniform quadratic-size candidate-family construction and the complete assortment-revenue approximation theorem remain open and are outside the completed claim. The archive contains three exact Prove2Me-accepted source files, complete independent target audits with autoImplicit=false, all three required platform definition modules, immutable Lean 4.33.1 and Mathlib dependency pins, the established archive verifier, fresh staged reproduction logs, and rejecting controls for a changed proof byte, a weaker candidate statement and an added local axiom. Allowed axioms are only propext, Classical.choice and Quot.sound. Pinned third-party compiled caches remain trusted inputs; this is not a bootstrap verification. Original mathematics belongs to Gallego and Topaloglu; the shared instance model also credits James M. Davis. The target cites a September 11, 2013 manuscript; the inspected author-hosted revision is dated September 18, 2013, and no original-PDF hash is claimed. mikedeng1 supplied platform interfaces and statements; Shuze Chen reviewed the statements. Lean/Mathlib and the specific reused proof infrastructure retain credit. Alexander Richard Towell directed the work. Substantial OpenAI Codex assistance in proof development, verification and documentation is disclosed. No mathematical novelty, source-author endorsement or independent human proof review is claimed. All three proofs were publicly submitted on October 20, 2026. The earlier central v1.0 metadata record covered two rounding bounds; this first archival edition, v1.1.0, adds the complete optimizer construction. Exact original disclosures are recorded separately from this archive publication. The owning development repository remains private. This is one coherent Prove2Me contribution.