`IndisputableMonolith.Foundation.OperatorCore.ComplexStructureForcing`

IndisputableMonolith/Foundation/OperatorCore/ComplexStructureForcing.lean · 36 lines · 17 declarations

Explainer status: ready · generated 2026-08-13 16:59:19.594406+00:00

   1import IndisputableMonolith.Foundation.ComplexStructureForcing
   2
   3namespace IndisputableMonolith
   4namespace Foundation
   5namespace OperatorCore
   6
   7noncomputable section
   8
   9/-- Authoritative IM alias for the 8-tick complex carrier. -/
  10abbrev Signal8 := IndisputableMonolith.Foundation.ComplexStructureForcing.Signal8
  11
  12abbrev nextIdx := IndisputableMonolith.Foundation.ComplexStructureForcing.nextIdx
  13abbrev shift := IndisputableMonolith.Foundation.ComplexStructureForcing.shift
  14abbrev shiftIter := IndisputableMonolith.Foundation.ComplexStructureForcing.shiftIter
  15abbrev ζ := IndisputableMonolith.Foundation.ComplexStructureForcing.ζ
  16abbrev eigenvalue := IndisputableMonolith.Foundation.ComplexStructureForcing.eigenvalue
  17abbrev dft8 := IndisputableMonolith.Foundation.ComplexStructureForcing.dft8
  18abbrev idft8 := IndisputableMonolith.Foundation.ComplexStructureForcing.idft8
  19abbrev inner8 := IndisputableMonolith.Foundation.ComplexStructureForcing.inner8
  20abbrev JcostC := IndisputableMonolith.Foundation.ComplexStructureForcing.JcostC
  21abbrev totalModeCost := IndisputableMonolith.Foundation.ComplexStructureForcing.totalModeCost
  22abbrev UnitaryEvolution := IndisputableMonolith.Foundation.ComplexStructureForcing.UnitaryEvolution
  23
  24abbrev shift_period_8 := IndisputableMonolith.Foundation.ComplexStructureForcing.shift_period_8
  25abbrev complexification_forced := IndisputableMonolith.Foundation.ComplexStructureForcing.complexification_forced
  26abbrev dft8_preserves_inner := IndisputableMonolith.Foundation.ComplexStructureForcing.dft8_preserves_inner
  27abbrev jcost_phase_invariant := IndisputableMonolith.Foundation.ComplexStructureForcing.jcost_phase_invariant
  28abbrev mode_cost_phase_invariant := IndisputableMonolith.Foundation.ComplexStructureForcing.mode_cost_phase_invariant
  29abbrev cost_phase_duality := IndisputableMonolith.Foundation.ComplexStructureForcing.cost_phase_duality
  30
  31end
  32
  33end OperatorCore
  34end Foundation
  35end IndisputableMonolith
  36

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