OAI/Computability/UniqueGames/Inverse/ShortcodeTheorem.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Grassmann theorem, chart retention, zero-factor correction, output-fiber extraction, and affine row/column slice construction yield the unconditional affine matrix inverse theorem.

  1. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeTheorem.inversePrinciple line 17

    Source documentation

    Full-factor sampling includes zero. The conclusion retains an affine intercept and applies to arbitrary matrix labelings without a folding premise.

    theorem inversePrinciple : Shortcode.InversePrinciple :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.InversePrinciple