IndisputableMonolith.Gravity.TensorShearSector

declarations in this module (201)

• abbrev EdgePerturbation L34
• def conformalEdgeLogStrain L38
• def conformalEdgeLengthPerturbation L45
• theorem conformalEdgeLengthPerturbation_eq_sqrt_mul_logStrain L50
• def IsConformalEdgePerturbation L59
• theorem vertexConformal_rectangle_log_strain_forces_square L66
• theorem nontrivial_rectangle_shear_not_vertexConformal L77
• abbrev PeriodicVertex5 L90
• abbrev PeriodicEdge5 L93
• abbrev PeriodicTorus5 L97
• def periodicExternalVertexOfIndex5 L102
• def periodicExternalVertexIndex5 L109
• def periodicExternalEdgeOfEncodedIdx5 L116
• def periodicExternalEdgeIndex5 L123
• abbrev periodicVertexEquiv5 L127
• def periodicAddFin5 L132
• def periodicTranslateVertex5 L136
• def periodicTranslateEncodedVertexIdx5 L142
• theorem periodicTorus5_edgeVerts_symm_eq_endpoints L149
• abbrev PeriodicEdgePerturbation5 L162
• abbrev EncodedEdgePerturbation5 L166
• def encodedToPeriodicEdgePerturbation5 L170
• def periodicToEncodedEdgePerturbation5 L175
• def periodicEdgePerturbationEquiv5 L181
• structure RawEdgePerturbationSplitting L197
• def PeriodicFreudenthalTTDecompositionTargetAtN5 L208
• def periodicRawSplittingOfEncoded5 L217
• def periodicEdgeInnerProduct5 L238
• theorem periodicEdgeInnerProduct5_symm L242
• theorem periodicEdgeInnerProduct5_zero_left L250
• theorem periodicEdgeInnerProduct5_zero_right L255
• theorem periodicEdgeInnerProduct5_add_right L260
• theorem periodicEdgePerturbation5_eq_zero_of_inner_self_eq_zero L274
• def PeriodicConformalLogSubspace5 L291
• theorem periodicConformalLogSubspace5_zero L296
• def encodedVertexDeltaPotential5 L303
• def periodicConformalGenerator5 L309
• theorem periodicConformalGenerator5_apply_endpoint L316
• theorem periodicConformalLogSubspace5_spanned_by_encodedVertexGenerators L328
• def PeriodicGaugeSubspace5 L346
• def PeriodicTTOrthogonal5 L353
• theorem periodicTTOrthogonal5_zero L362
• def PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5 L374
• structure PeriodicTTProjectorData5 L385
• theorem periodicEdgeInnerProduct5_linear_combo_right L401
• structure PeriodicTTFiniteGeneratorProjectorData5 L428
• def periodicGaugeGeneratorMap5 L456
• def periodicConformalGeneratorMap5 L464
• theorem periodicConformalGeneratorMap5_apply_endpoint L470
• theorem periodicConformalGeneratorMap5_mem L482
• theorem periodicGaugeSubspace5_spanned_by_generatorMap L496
• abbrev PeriodicLongitudinalGaugeIdx5 L507
• def periodicTranslateLongitudinalGaugeIdx5 L511
• def periodicDispCoord5 L518
• def periodicLongitudinalGaugeGenerator5 L528
• def periodicLongitudinalGaugeMap5 L537
• theorem periodicLongitudinalGaugeMap5_apply_endpoint L543
• theorem periodicLongitudinalGaugeMap5_eq_generatorMap L557
• abbrev PeriodicLongitudinalTTSubspace5 L563
• theorem periodicGaugeSubspace5_spanned_by_longitudinalGeneratorMap L570
• structure PeriodicTTGaugeGeneratorProjectorData5 L584
• structure PeriodicTTGeneratorMapProjectorData5 L607
• structure PeriodicTTLongitudinalProjectorData5 L627
• structure PeriodicTTLongitudinalCoefficientProjectorData5 L648
• def periodicLongitudinalCoefficientResidual5 L667
• structure PeriodicTTLongitudinalCoefficientSolutionData5 L679
• abbrev PeriodicTTNormalEquationIdx5 L699
• def periodicTranslateTTNormalEquationIdx5 L705
• def periodicTTNormalEquationGenerator5 L712
• def periodicTTNormalEquationConformalCoeff5 L719
• def periodicTTNormalEquationGaugeCoeff5 L725
• def periodicTTNormalEquationGeneratorMap5 L731
• def periodicExternalDispCoordNat5 L737
• def periodicExternalEdgeHeadIndex5 L746
• def periodicExternalTTNormalEquationGeneratorMatrixEntry5 L753
• def periodicExternalTTNormalEquationGeneratorMatrixDot5 L770
• def periodicExternalTTNormalEquationGeneratorSparseDot5 L778
• theorem periodicTTNormalEquationGeneratorMap5_eq_split L796
• def periodicTTNormalEquationLoad5 L812
• def periodicTTNormalEquationGramApply5 L818

… and 121 more