`IndisputableMonolith.RRF.Theorems`

IndisputableMonolith/RRF/Theorems.lean · 32 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.RRF.Theorems.MonotoneArgmin
   2import IndisputableMonolith.RRF.Theorems.OctaveTransfer
   3import IndisputableMonolith.RRF.Theorems.OrderPreservation
   4
   5/-!
   6# RRF Theorems
   7
   8Umbrella file for RRF theorems.
   9
  10These are proven mathematical facts about RRF structures.
  11No physical hypotheses here—just pure logic.
  12
  13## Contents
  14
  15- `MonotoneArgmin`: Argmin invariance under monotone transforms
  16- `OrderPreservation`: Rank and ordering preservation
  17- `OctaveTransfer`: Properties that transfer between equivalent octaves
  18-/
  19
  20
  21namespace IndisputableMonolith
  22namespace RRF
  23
  24/-!
  25## RRF Theorems Status
  26
  27RRF Theorems are proven mathematical facts, not hypotheses.
  28-/
  29
  30end RRF
  31end IndisputableMonolith
  32

source mirrored from github.com/jonwashburn/shape-of-logic