IndisputableMonolith.Foundation.OperatorCore.ComplexStructureForcing
IndisputableMonolith/Foundation/OperatorCore/ComplexStructureForcing.lean · 36 lines · 17 declarations
show as:
view math explainer →
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