Glossary: D

Definitions in this project whose names start with D. The whole glossary has the other sections.

A · B · C · D · E · F · G · H · I · J · K · L · M · N · O · P · Q · R · S · T · U · V · W · X · Y · Z · Other

D def: Polynomial dependence on the concentration parameter after multiplying the physical derivative by delta squared. · OAI.ElasticityBoundaryProfile.D
D def: Constant-direction differentiation. All directions are real; the values may be real or complex, as in the source lemma. · OAI.ElasticityFiniteType.D
D abbrev: The actual finite-dimensional ordinary algebra and off-diagonal bimodule. · OAI.LittleFinitistic.SelectedOrdinaryAlgebra.D
D def: Its polar cross-terms. In characteristic two these equal Q (x + a) + Q x + Q a. · OAI.MaxCutGames.Quadratic.D
D def: Its polar cross-terms. In characteristic two these equal Q (x + a) + Q x + Q a. · OAI.UniqueGamesTheorem.Quadratic.D
D0Iso def: All three actual tensors have the primary H(Y) as homology in both selected degrees. · OAI.LittleFinitistic.SelectedChainHomology.D0Iso
damped def: The actual increment with an ambient-metric taper. The scalar transverse field is measured intrinsically, while this weight may use the unrestricted metric. · OAI.PlanarL1.Increment.damped
dampedMapMoment def: The actual weighted map-derivative sum left by the finite reindexing. · OAI.MaxCutGames.Appendix.A5Induction.dampedMapMoment
dampedMapMoment def: The actual weighted map-derivative sum left by the finite reindexing. · OAI.UniqueGamesTheorem.Appendix.A5Induction.dampedMapMoment
Dart def: Literal darts of the recursively substituted word; no quotient identifies any darts of distinct blocks. · OAI.FKCRT.Inventory.CoreTree.Dart
Dart abbrev: Original darts plus one radial pair for each face corner. Radial true is at the new face center, radial false at the original vertex. · OAI.TorsionFreeZeroDivisors.ConedMap.Dart
Dart abbrev: The source's outgoing half-edges, preserving their basepoints and letters. · OAI.TorsionFreeZeroDivisors.TypedGraphs.Dart
dart def: Positions remember their literal original dart, without a choice of orientation. · OAI.TorsionFreeZeroDivisors.RawDecomposition.dart
dartBlockEquiv def: A vertex's block consists of one adjacent orientation pair per word. · OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.dartBlockEquiv
dartBlockEquiv def: A vertex's block consists of one adjacent orientation pair per word. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.dartBlockEquiv
dartCloudEquiv def: Every original dart occurs in exactly one cloud. · OAI.MaxCutGames.Foundations.PCP.CloudPadding.dartCloudEquiv
dartCloudEquiv def: Every original dart occurs in exactly one cloud. · OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.dartCloudEquiv
dartCount def: Number of directed recorded-walk occurrences, including orientation. · OAI.MaxCutGames.Foundations.PCP.PoweringTables.dartCount
dartCount def: Number of directed recorded-walk occurrences, including orientation. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.dartCount
dartEquiv def: Executable vertex-major dart numbering, with adjacent orientations. · OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.dartEquiv
dartEquiv def: The port number is retained by the coordinate conversion. · OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv
dartEquiv def: Executable vertex-major dart numbering, with adjacent orientations. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.dartEquiv
dartEquiv def: The port number is retained by the coordinate conversion. · OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.dartEquiv
dartGraphEmbeddingIso def: Relabelling literal darts, without adding edges or collapsing nonzero original distances. · OAI.FKCRT.PermutationWedge.dartGraphEmbeddingIso
dartInsert def: Literal dart order for all successive corner insertions. · OAI.FKCRT.Inventory.dartInsert
dartMap def: Every candidate is injective on actual-image vertices; the letters uniquely specify the target ports before the random matching is chosen. · OAI.TorsionFreeZeroDivisors.PatternEmbeddings.dartMap
DartRow structure: The row itself is finite data; index bounds are checked while parsing. · OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.DartRow
DartRow structure: The row itself is finite data; index bounds are checked while parsing. · OAI.MaxCutGames.Foundations.PCP.GraphTables.DartRow
DartRow structure: The row itself is finite data; index bounds are checked while parsing. · OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.DartRow
DartRow structure: The row itself is finite data; index bounds are checked while parsing. · OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.DartRow
dartStart def: Start of one of the three subdivided segments of a signed old edge. · OAI.HyperbolicObstruction.FinitePolygonModel.Data.dartStart
dartVertexEquiv def: Exact quotient-graph relabelling for arbitrary finite dart carriers. · OAI.FKCRT.PermutationWedge.dartVertexEquiv
dartVertexEquiv def: The tuple permutation putting the vertex before its word and orientation. · OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.dartVertexEquiv
dartVertexEquiv def: The tuple permutation putting the vertex before its word and orientation. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.dartVertexEquiv
Data structure: A specified coordinate norm, with individually bounded coordinate evaluations. No bound on the norms of coordinate projections is imposed. · OAI.DiamondDistortion.CoordinateCompletion.Data
Data structure: Finite descending directions with literal word-length decrease. These combinatorial fields will be supplied by the checked Artin trace normal form. · OAI.EilenbergGanea.DescendingCube.Data
Data structure: Binary self-similarity data for a group, with the associativity laws in explicit multiplicative orientation. The concrete finite structural quotient supplies every field; this is not an assumption on the main theorem's input. · OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Data
Data structure: Combinatorial data of an actual one-vertex union. Distances are not part of these hypotheses; they are derived from the adjacency data below. · OAI.FKCRT.GraphWedge.Data
Data structure: An incidence constraint compares transported flags with their named quotients. Constant grade zero imposes full equality (e.g. a surface relation). Coarsening the grade imposes the unchanged direct-sum block at an interchange. · OAI.IntegralCharacterVarieties.FlagCircuit.Data
Data structure: The adjacent old flag terms and chosen subsystem. No splitting or exact-sequence data is an input. · OAI.IntegralCharacterVarieties.IntrinsicInterval.Data
Data structure: Chain representatives and all specified relation homotopies for the one fixed diagram. · OAI.LittleFinitistic.SelectedChainDiagram.Data
Data structure: All choices, arrows, relation-basis equations and equivariant identifications for the actual selecting algebra. No evaluation module is a parameter. · OAI.LittleFinitistic.SelectedFixedDiagram.Data
Data structure: Boundary data is a specification of physical tape contents, never part of the machine's finite control state. All eighteen core work tapes are empty. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Data
Data structure: Continuous dependence of a polynomial family and its complex differential. This is used only to obtain the uniform nonlinear bounds in the source sonic contraction, not as a replacement for construction of the shooting family. · OAI.SepticProfile.FamilyC1.Data
Data structure: Finite data of the preprocessed instance; geometric hypotheses are proved for the actual input construction below, not hidden in this record. · OAI.Superstring.Counts.Data
Data structure: The precise deformation data needed for a horn attachment. · OAI.Thomason.Construction.TopologicalDeformation.Data
Data structure: A path system in an ambient finite graph. The graph need not be the union of the paths; taking its literal supported image constructs the raw data. · OAI.TorsionFreeZeroDivisors.AmbientPattern.Data
Data structure: The literal finite pattern data. These are only combinatorial encoding bounds; none of the probability or realizability conclusions is a field. · OAI.TorsionFreeZeroDivisors.BoundedPattern.Data
Data structure: Full integer affine comparison geometry. The offset uses [-2H,2H]. · OAI.TorsionFreeZeroDivisors.ComparisonCoding.Data
Data structure: A purely finite lifted boundary certificate. The single unpaired marker records the break from the exterior endpoint y back to the prescribed root x. No surface map, cone filling, essentiality, or CW realization is asserted. · OAI.TorsionFreeZeroDivisors.FinitePicture.Data
Data structure: All non-label data of a bounded actual pattern. Proof fields are not encoded, while all data fields are. · OAI.TorsionFreeZeroDivisors.PatternCoding.Data
Data structure: The data of a literal bounded family of immersed graph paths. The finite image graph is arbitrary; only the source's bounds on path and comparison counts, total length and proportion of unpaired letters are stated here. · OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data
Data structure: The actual suppressed form of source paths. No bound on the resulting skeleton, chain lengths, multiplicities or number of traversals is assumed. · OAI.TorsionFreeZeroDivisors.SourcePattern.Data
Data structure: A finite lifted spherical boundary map; empty boundary components are not recorded. Unlike the disk certificate there is NO marked exceptional boundary. This is combinatorial data, not yet a claim about a continuous sphere map. · OAI.TorsionFreeZeroDivisors.SphericalPicture.Data
Data structure: Boundary data is a specification of physical tape contents, never part of the machine's finite control state. All eighteen core work tapes are empty. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Data
data def: Actual permutation-map insertion satisfies graph-wedge adjacency data. No metric or distance assertion is supplied as an assumption. · OAI.FKCRT.PermutationWedge.data
data def: The old adjacent interval, before any coordinate choice on U or Q. · OAI.IntegralCharacterVarieties.OldContactSlice.data
data def: The constructed atomic forcing relations instantiate the external quotient machinery on any specified set of name codes. · OAI.PartitionConsistency.SetForcingNames.AtomicForcing.data
DataArg def: Even builders accept a raw data element; odd builders accept a raw callback. · OAI.PureTypeSystem.LogicSetup.DataArg
dataCanonicalList def: A direct fixed-field validator: read field zero, test its supplied-factor CRT congruences, and check every other field and the unused word is zero. · OAI.ExactQuantumFactoring.dataCanonicalList
dataCanonicalResidue def: Checking the uniquely specified CRT residue needs only congruences against the supplied prime powers; no CRT search is hidden in the guess validator. · OAI.ExactQuantumFactoring.dataCanonicalResidue
dataChildPrimes def: Child lookup takes the first matching stored occurrence. It does not compute new children. Distinct parents deliberately retain separate occurrence data. · OAI.ExactQuantumFactoring.dataChildPrimes
dataLog def: Projection of the actual retained record, including dummy rows. No true factorization is used in constructing this projection. · OAI.ExactQuantumFactoring.NodeMachine.dataLog
DataMap def: An ordinary raw data callback. Its uniformity is a consequence of the already proved labelled substitution theorem. · PureTypeSystem.Labelled.DataMap
dataOrderPassed def: Test the same completed order slot using the later supplied node record. Unusable list entries (including out-of-range words) use the source dummy test. · OAI.ExactQuantumFactoring.dataOrderPassed
dataTests def: Retrospective evaluation on the actual split trace, with one verified read-only factor-data view for this physical node. The controller and all query words are the same ones used by the physical run. · OAI.ExactQuantumFactoring.NodeKernel.dataTests
dataTests def: Read-only postprocessing of the retained actual history. Each node receives only the flat row data at its actual runtime label. Occurrences are retained; lookup selects the first matching verified record, not a factorization oracle. · OAI.ExactQuantumFactoring.NodeMachine.dataTests
dataTotientPrimes def: phi factors are reconstructed from division against the supplied parent record and the supplied p−1 children. The p=2 contribution requires no child. · OAI.ExactQuantumFactoring.dataTotientPrimes
DataTree inductive: A prefix-encoded finite binary tree; every code is nonempty and uniquely self-delimiting. Working trees need no infinite-alphabet cells. · OAI.ParityWL.Complexity.DataTree
DataView def: Precisely the supplied local record and p−1 lookup facts consumed by the retrospective arithmetic. This is established below from actual verified rows. · OAI.ExactQuantumFactoring.DataView
DataWitnessContext structure: The data context has no proof-mode declarations. Its finite witness terms are literal all-data embeddings and their erased types are normal. · OAI.PureTypeSystem.Labelled.DataWitnessContext
DataWrapper inductive: A retained data path, with fixed tail codes and fixed positive witnesses. · OAI.PureTypeSystem.Labelled.DataWrapper
Daugavet def: Every rank-one operator has the form ell.smulRight v. · OAI.ExactModuli.Daugavet
DavidsonSzarekInput structure: The edge and integrable-tail consequences of DS2001, TheoremII.13. The rank-deficient case uses the exact zero eigenvalues of the Gram matrix. · OAI.InvariantIsing.DavidsonSzarekInput
dB def: deltas · OAI.GeneralMahler.ProjField.dB
dbar def: Conjugate Wirtinger derivative with the same normalization. · OAI.Mahler.dbar
dc def: The coefficient derivative and distribution derivative are genuine derivatives. · OAI.ElasticityDistribution.dc
dc def: The convention d^c u(v) = -D_R u(iv)/4. · OAI.Mahler.dc
dcForm def: The operator d^c as a real alternating one-form. · OAI.MahlerStokes.dcForm
dcLinear def: The operator d^c, bundled as a real continuous linear one-form. · OAI.Mahler.dcLinear
Dcoef def: Coefficients of the actual primitive; all are nonnegative on the side domain. Their estimates use size-derived logarithmic cancellation. · OAI.KServer.SideTracker.Dcoef
dCoefficient def: The coefficient of the parent input D, after analytic integration. · OAI.UniformKServer.SideStability.dCoefficient
dcOperator def: The linear operation taking a real derivative to d^c. · OAI.Mahler.dcOperator
ddcTwoJet def: The second derivative determines the actual exterior derivative of d^c. · OAI.Mahler.ddcTwoJet
de def: The square-zero algebra is only an algebraic way of reusing the physical compatibility identities: its genuine distribution component is never multiplied by another distribution. · OAI.ElasticityDistribution.de
death def: Death trials for one actual age increment, including the compulsory cutoff. Already absent records are assigned probability zero. · OAI.KServer.ShortRoster.death
decayingPhysical def: Physical Fourier ODE, retaining the normal derivatives instead of assigning a boundary symbol by definition. · OAI.ElasticityBoundarySymbol.decayingPhysical
decideConnected def: Consequently internal weak connectivity has a decision procedure that uses only the table and finite configuration data, not a halting oracle. · OAI.FiniteAlgebraicEnvelopes.Compiler.decideConnected
decideGap def: Rational comparison of the returned cut with a fixed rational factor B. No real-number oracle is used by this predicate. · OAI.UniformSparsestCut.decideGap
Decides def: The formalization proves $\mathsf L=\mathsf{RL}=\mathsf{BPL}$ for binary languages in an explicit Turing-machine model with logarithmic workspace. The randomized classes use polynomial time: $\mathsf{RL}$ never accepts a no-instance and … · OAI.ExactDerandomization.Machine.Decides
DecidesWithin def: Uniform genuine executions on every bit word, including malformed graph words. · OAI.WLIdentification.DecidesWithin
decisions def: All finite tuples are explicitly included, so this construction treats all parameters, not just sentences or quantifier-free formulas. · OAI.PartitionConsistency.Completeness.decisions
decisions def: Conditions deciding the fixed standard formula at a fixed tuple of names. · OAI.PartitionConsistency.ForcingQuotient.AtomicData.decisions
decisionThreshold def: A fixed constant can be chosen once for the finite program. · OAI.LowSpaceSubsetSum.decisionThreshold
decisionWeight def: A rejected box entry contributes zero. A valid completion contributes its cached integer multiplicity precisely when it reaches the target. · OAI.ContingencyTables.ProfilePrograms.decisionWeight
deckGroup def: The actual group of self-homeomorphisms over a covering projection. · OAI.EilenbergGanea.CoverTopology.deckGroup
Decl inductive: A literal list representation of the nodes and the (possibly incomplete) cache. The cache is not replaced by a search through all nodes. · OAI.ExactQuantumFactoring.NativeAIG.Decl
DeclRenaming def: A genuine variable renaming sends declarations to declarations, rather than merely to terms that happen to have convertible types. · OAI.PureTypeSystem.TypingTree.DeclRenaming
decode def: Decode the first w bits of a natural-number mask. · OAI.CycleClique.Construction.decode
decode def: From an injective natural coding on a fixed finite alphabet. · OAI.Fifths.SM.decode
decode def: An entirely literal decoder, including a final equality check. It does not assume that its input is a path or that any tag is clean. · OAI.FiniteAlgebraicEnvelopes.Compiler.Path.decode
decode def: Decoding the normal form respects the nonabelian multiplication. · OAI.PolycyclicRecognition.GroupExtensionSection.decode
decodeButterfly def: Decode an independent bit at every switch into the actual routing object. · OAI.CubeShuffle.decodeButterfly
decodeCap def: Saturated, genuine left-to-right binary decoding. It stays unary-bounded by c. · OAI.WLIdentification.WordExpressions.NatPoly.decodeCap
decodeColumnPattern def: An equality pattern contains no numerical label names. · OAI.TwoPointCorrelations.decodeColumnPattern
decodedBad def: Badness is computed from the actual base predicate and the decoded labels. · OAI.MaxCutGames.Foundations.PCP.PoweringTest.decodedBad
decodedBad def: Badness is computed from the actual base predicate and the decoded labels. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.decodedBad
decodeForestPaths def: A valid path code determines one family; invalid codes decode to empty lists. The proven uniqueness makes this choice independent of witnesses. · OAI.TwoPointCorrelations.decodeForestPaths
decodeFormula def: `decodeFormula input` parses the clause list with enough fuel and succeeds only when no trailing bits remain. · OAI.UniqueGamesTheorem.BinaryEncoding.decodeFormula
decodeIndex def: A total fixed decoder for a retained index. On supported (o,n) it is uniquely determined by the distinctness of the three names. · OAI.MaxCutGames.Soundness.ZeroInformation.decodeIndex
decodeIndex def: A total fixed decoder for a retained index. On supported (o,n) it is uniquely determined by the distinctness of the three names. · OAI.UniqueGamesTheorem.Soundness.ZeroInformation.decodeIndex
decodeMap def: This body exposes the decoded predicate as a data map on exact BP values. · OAI.PureTypeSystem.Labelled.DoubleCode.decodeMap
decodePairedEmission def: Three chronological streams, with side pairs independent across slots. This forgets flags but does not separate any marks inside the central list. · OAI.TraceReconstruction.decodePairedEmission
decodeProfile def: Failed candidates are discarded. Passing candidates retain all completion multiplicity through the original physical state type. · OAI.ContingencyTables.SmallGraphProfiles.decodeProfile
decoderSuccess def: Select independent Walsh masks by squared coefficients and uniform points in each support. The two selections use only the respective private tables. · OAI.MaxCutGames.Foundations.Hastad.decoderSuccess
decoderSuccess def: Select independent Walsh masks by squared coefficients and uniform points in each support. The two selections use only the respective private tables. · OAI.UniqueGamesTheorem.Foundations.Hastad.decoderSuccess
decodeRule def: Decode the indexed rule without adding any future-information input. · OAI.MatroidProphet.LabeledTransport.decodeRule
decodeSource def: A finite source decoder. It need not accept malformed configurations; on each guarded source cylinder it recovers the unique table row. · OAI.ForcedComputation.Balanced.decodeSource
decodeTuple def: Interpret a radix tuple using the declared domain and codomain numbering. · OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.decodeTuple
decodeTuple def: Interpret a radix tuple using the declared domain and codomain numbering. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.decodeTuple
decodeWeight def: Decode an integer weight code using the fixed mesh. · OAI.MetricEntropyDuality.decodeWeight
decompose def: Actual orbit--stabilizer decomposition, including its fiber cardinal factor. · OAI.CoordinateSweeps.PlacementInduction.Chart.decompose
decomposeBefore def: Decompose upstairs, then apply the quotient map to every component. · OAI.StableCoordinate.HomogeneousQuotient.decomposeBefore
decomposePolynomial def: Finite support is the actual polynomial support, not an assumption of a formal infinite homogeneous decomposition. · OAI.ReesProj.decomposePolynomial
decomposePolynomial def: Finite support is the actual polynomial support, not an assumption of a formal infinite homogeneous decomposition. · OAI.SectionCompletion.decomposePolynomial
decomposeQuotient def: The decomposition map on the quotient. · OAI.StableCoordinate.HomogeneousQuotient.decomposeQuotient
decomposition def: The block direct sum is linearly isomorphic to the entire actual count submodule. · OAI.DerivedBar.Multibar.Indexed.decomposition
decomposition def: A quotient by a homogeneous ideal has a direct-sum decomposition. · OAI.StableCoordinate.HomogeneousQuotient.decomposition
decorate def: A direct product of local coordinate copies of the acting group. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.decorate
decoratedBaker def: A baker element defined inside the finitely presented quotient, before any injectivity or table-presentation completeness theorem. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedBaker
decoratedColourTensor def: A binary tensor at any colour, constructed internally from the descended baker. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedColourTensor
decoratedRelations def: Finite structural laws together with the point stabilizer laws. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedRelations
Decoration structure: Facet names are attached to EACH local germ, even when their values repeat. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration
decoration def: The facet/strip names incident at every corner. A global use may map different A/B names to the same old facet without changing occurrences. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.decoration
decoration def: Decoration extracted from the actual old incidence, not chosen colors. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.decoration
decreasingEigenvalues def: The ordered spectrum, with the matrix cardinality reduced to its size. · OAI.Kaplansky.decreasingEigenvalues
DecreasingOrderLaw def: The reverse ordering has the same density. · OAI.JointDickman.DecreasingOrderLaw
decreasingStrip def: The reflected strip above the strict ordering diagonal. · OAI.JointDickman.decreasingStrip
defaultFormula def: Use a partial graph's value when it belongs to the codomain, and otherwise use the specified default. The variables are f,X,x₀,a,y, respectively. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.defaultFormula
defaultTargetAnswer def: A default actual target answer is used only for unsupported displayed questions, which never occur in the experiment. · OAI.MaxCutGames.Clean.AnswerBridge.defaultTargetAnswer
defaultTargetAnswer def: A default actual target answer is used only for unsupported displayed questions, which never occur in the experiment. · OAI.UniqueGamesTheorem.Clean.AnswerBridge.defaultTargetAnswer
defect def: Defect between two letter phases. · OAI.FourierLLogL.Compress.defect
defect def: Number of darts minus number of vertex cycles, including singleton cycles. The integer form avoids artificial truncated-subtraction side conditions. · OAI.HyperbolicObstruction.PictureSwitch.defect
defectCoefficient def: The defect coefficient H_d in equation (19). · OAI.PositiveEinsteinFour.Energy.defectCoefficient
defectConstant def: Exact source defect constant. It depends on the fixed parameters, not on alphabet size, the picture or fragment. · OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.defectConstant
defectIsometry def: The first component is the original contraction; the second accounts for exactly the lost squared norm. · OAI.KadisonKastler.defectIsometry
defectMap def: The linear extension of the point-probability defects. · OAI.ThompsonNonamenability.defectMap
defectPiece abbrev: The degree-n piece of the actual quotient T/S. · OAI.KLInvariance.Hilbert.defectPiece
defectSet def: The actual image of finite nonnegative probabilities under the defect map. · OAI.ThompsonNonamenability.defectSet
DefectSpace abbrev: The simultaneous defects use the ℓ¹ norm on the product index set. · OAI.ThompsonNonamenability.DefectSpace
deficiency def: The paper's deficiency, with logarithms in base two. · OAI.LowSpaceSubsetSum.deficiency
deficiencyVariance def: Variance for uniform sampling of exactly v indices, without replacement. · OAI.LowSpaceSubsetSum.deficiencyVariance
deficit def: Equation (1.4), defined also outside the interval for convenience. · OAI.InvariantIsing.deficit
deficit def: The one-sided deficit r_n, used on pairs of length n. · OAI.TreeEdit.BinaryLower.deficit
deficit def: One-sided deficit; used below only when the two lengths agree. · OAI.TreeEdit.deficit
deformation def: Shift only the fraction of mass specified by the interval coordinate. · OAI.Thomason.Construction.HornBarycentric.deformation
deg def: degree/shift arithmetic · OAI.GeneralMahler.HMode.deg
degenerateLift def: Fix the phase of the lift at the degenerate point. · OAI.ArnoldCounterexample.Construction.degenerateLift
degeneration def: A checked polynomial degeneration to the two matched convolution branches. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.degeneration
degree def: The degree is one absolute constant, independent of the input graph. · OAI.MaxCutGames.Foundations.PCP.Regularization.degree
degree def: Frequency degree: cardinality of the set of selected Boolean coordinates. · OAI.OptimalMaxCut.Analytic.degree
degree def: The number of support edges incident to a vertex. · OAI.Problem313.SupportCombinatorics.degree
degree def: The integer degree is the infimum of the layers containing an element. The lemmas below show that for a nonzero element this infimum is attained. · OAI.StableCoordinate.IntegerFiltration.degree
degree def: The degree is one absolute constant, independent of the input graph. · OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.degree
DegreeAtMost def: Fourier support is restricted to maps of rank at most d. · OAI.MaxCutGames.Appendix.DerivativeDegree.DegreeAtMost
DegreeAtMost def: Fourier support is restricted to maps of rank at most d. · OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.DegreeAtMost
degreeCastEuclidean def: The degree equality is explicit; this is transport along that equality, not an arbitrary permutation of the ordered real coordinates. · OAI.MahlerStokes.degreeCastEuclidean
degreeData opaque: A checked initialized degree avoids evaluating enormous fixed logarithms while applying polynomial identities. Its bound is part of the stored data. · OAI.MaxCutGames.Foundations.PCP.TableIteration.degreeData
degreeData opaque: A checked initialized degree avoids evaluating enormous fixed logarithms while applying polynomial identities. Its bound is part of the stored data. · OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.degreeData
degreeDerivativeEquiv def: The differential at the regular fiber is a real-linear isomorphism. · OAI.KervaireFixedSpace.degreeDerivativeEquiv
degreeDistance def: The degree-saving distance at slope (n-s)/(2*n). · OAI.Problem335.degreeDistance
degreeEquiv def: The outgoing darts at each new vertex are exactly its fixed port alphabet. · OAI.MaxCutGames.Foundations.PCP.Regularization.degreeEquiv
degreeEquiv def: The outgoing darts at each new vertex are exactly its fixed port alphabet. · OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.degreeEquiv
DegreeExponent def: Ternary exponent vectors with sum k. · OAI.Nagata.W02.DegreeExponent
degreeExponentEquiv def: Explicit finite enumeration by the genuine finsupp antidiagonal. · OAI.Nagata.W02.degreeExponentEquiv
degreeExponentsEquivSym def: Degree-exact exponent vectors are multisets of the indicated cardinality. · OAI.Problem335.degreeExponentsEquivSym
degreeForcedRoleEnergy def: A degree-r sum over the genuine pairs (selected leaves, roles), restricted only by deterministic allowed forced labels. · OAI.TraceReconstruction.degreeForcedRoleEnergy
DegreeForcedShape abbrev: Only the unlabeled ordered role shape is selected here; no child label or hidden orientation enters the forced choice. · OAI.TraceReconstruction.DegreeForcedShape
degreeGrading def: The degree grading associated to projections indexed from zero to n. · OAI.LeanBlast.GotsmanLinial.degreeGrading
degreeIdeal def: The descending coefficient filtration on the graded polynomial algebra. · OAI.SectionCompletion.degreeIdeal
degreeKernelEquiv def: The actual degreewise kernel, not merely an equality of dimensions. · OAI.KLInvariance.Hilbert.degreeKernelEquiv
DegreeLE def: A simultaneous degree bound for the four cleared coefficients and denominator. · OAI.Ostmann.PolynomialGiantRows.DegreeLE
DegreeLE def: Every homogeneous component above degree d vanishes. · OAI.StableCoordinate.LeadingComponent.DegreeLE
degreeLE def: Degree at most n means an R-linear combination of words of length at most n. This definition includes zero, constants, and linear terms. · OAI.LittleFinitistic.QuadraticPresentation.degreeLE
degreeMass def: Normalized degree measure is uniform dart mass pushed to vertices. · OAI.FKCRT.degreeMass
degreeOfColor def: Degree is already recoverable from a joint-update round, with two distinct slots. · OAI.WLIdentification.degreeOfColor
degreeOneConormalGenerator def: Degree-one section of the conormal line on the source X. · OAI.SourcePullbackChart.degreeOneConormalGenerator
degreeOneFraction abbrev: A homogeneous degree-one quotient. · OAI.AlgebraicGeometry.Proj.degreeOneFraction
degreeOneIdealGenerator def: degree-one global section of the Cartier ideal. · OAI.SourcePullbackChart.degreeOneIdealGenerator
DegreePositive def: Positivity is required only on the paper's valid subset degree. · OAI.ContingencyTables.BinaryContraction.DegreePositive
degreeWeight def: The one-factor bidegree weight used in the manuscript. · OAI.Problem335.degreeWeight
degreeZeroConstantBasis def: A basis of the actual section space with its single constant-one vector. · OAI.Nagata.W19.degreeZeroConstantBasis
degreeZeroSectionEquiv def: Evaluation at one is a genuine linear equivalence for actual sections. · OAI.Nagata.W19.degreeZeroSectionEquiv
degreeZeroSubalgebra def: The degree-at-most-zero part of a multiplicative integer filtration is a subalgebra. · OAI.StableCoordinate.FilteredRees.degreeZeroSubalgebra
dehomogenize def: The equation of a projective form in the affine chart X_c = 1. · OAI.Nagata.ProjectiveGeometry.dehomogenize
dehomogenize def: Literal degree-one dehomogenization of the section algebra into its actual homogeneous affine Proj chart, constructed as an algebra map. · OAI.SectionCompletion.dehomogenize
DekimpeLatticeRealizationInput def: The exact lattice-realization consequence of Dekimpe's Theorem 4.1 needed for the paper's lattice formulation. · OAI.PolycyclicRecognition.DekimpeLatticeRealizationInput
delay def: The time reserved for subsequent attaching deformations. · OAI.Thomason.Construction.TopologicalDeformation.Sequential.delay
delayColor def: Raise the final color of x to the color immediately after cut i. · OAI.TalagrandThreshold.Selector.delayColor
delayedFrame def: The literal two delayed target sides, retaining all old depth coordinates. · OAI.DilutedSpinGlass.ReducedTopology.delayedFrame
deletedCycle def: The edge-deleted product from the source; the missing edge is represented by 1, so the empty/one-node case is unambiguous. · OAI.CoordinateSweeps.deletedCycle
deletedMarks def: All marks lying on an occurring short-cycle attempt are discarded. · OAI.Release075.deletedMarks
DeletedSet def: All points of every bad row are removed. · OAI.MaxCutGames.Fourier.Deletion.DeletedSet
DeletedSet def: All points of every bad row are removed. · OAI.UniqueGamesTheorem.Fourier.Deletion.DeletedSet
deleteInterval def: The actual retained matching after a successful insertion is erased. · OAI.FKCRT.Inventory.StackMatching.deleteInterval
deletePrefix def: Delete, in the usual order of ℕ, the labels not reserved by the lower endpoint or by the finite prefix. · OAI.InfiniteMatroidCounterexample.deletePrefix
deletePrefix def: Delete an arbitrary prefix, costing zero. · OAI.Superstring.Hierarchical.Path.deletePrefix
deleteTail def: The limit after every eligible label has been deleted. · OAI.InfiniteMatroidCounterexample.deleteTail
deleteTuple def: Delete one entry of a weakly increasing tuple. · OAI.Thomason.Construction.SimplexComplex.deleteTuple
deletion def: A monotone deletion map, with an arbitrary choice only at the deleted vertex. · OAI.Thomason.Construction.HornBarycentric.deletion
delimiter def: A fixed one-bit push; the finite register is cleared before continuation. · OAI.MaxCutGames.BinaryHeaderMachine.delimiter
delimiter def: A fixed one-bit push; the finite register is cleared before continuation. · OAI.UniqueGamesTheorem.BinaryHeaderMachine.delimiter
delta def: The standard delta vector used for the finite trace. · OAI.KervaireRegular.delta
delta def: Change when adding one orthogonal line in a fixed mask. · OAI.PowerSaving.Binary.delta
delta def: The discrete derivative, retained as a function on the full cube. · OAI.Problem313.BiasedFourier.delta
delta def: The usual delta functions. · OAI.TorsionFreeBass.Regular.delta
demand def: Demand is fixed, not chosen by the reduction. · OAI.UniformSparsestCut.Graph.demand
den def: use identically clipped denominators on any input · OAI.ExactDerandomization.At.den
denominator def: Exact integer implementation of ceil(h / (a/b)). · OAI.MaxCutGames.Explicit.Rounding.denominator
denominator def: A concrete finite denominator, independent of proof-valued sieve parameters. · OAI.Problem337.GoldbachSelberg.denominator
denominator def: An executable exact common denominator, not the number of output copies. · OAI.UniqueGamesTheorem.Explicit.RationalWeights.denominator
denominator def: Exact integer implementation of ceil(h / (a/b)). · OAI.UniqueGamesTheorem.Explicit.Rounding.denominator
denominatorAlgebra def: The elements whose denominator is a power of the given source element. · OAI.FractionalAlgebraAway.denominatorAlgebra
denormalize def: Evaluate a nondegenerate simplex with specified barycentric coordinates. · OAI.Thomason.Construction.RealizationPrism.denormalize
Dense def: Strict density above the rational threshold p / q when q > 0. · OAI.MaxCutGames.Fourier.Deletion.Dense
Dense def: Stronger conditions are smaller. · OAI.PartitionConsistency.ForcingQuotient.Dense
Dense def: Strict density above the rational threshold p / q when q > 0. · OAI.UniqueGamesTheorem.Fourier.Deletion.Dense
denseAdditiveExtension def: The additive extension of bounded data from a dense subgroup. · OAI.KadisonSimilarity.denseAdditiveExtension
DenseAnchorCore def: A dense core consists of at least six selected anchor positions. Every opposite position has at most one zero on it, while a variable opposite position would have at most four ones. · OAI.Problem348.AnchorRigidity.DenseAnchorCore
DenseEgyptianFamily def: The exact dense-family input required by the elementary main upper reduction. No distinctness is asked of the supplied lists. · OAI.Problem337.DenseEgyptianFamily
denseEvent def: Union of all dense witnesses of a fixed vertex and prescription size. · OAI.TorsionFreeZeroDivisors.DiameterCounting.denseEvent
denseFamily def: Sets containing at least m distinct edges of the original family. · OAI.TalagrandDiscreteConvexity.Covering.denseFamily
denseFamilyIsometry def: The unique isometry sending a total family to a family with the same Gram matrix, constructed through finitely supported linear combinations. · OAI.KadisonSimilarity.denseFamilyIsometry
denseSubringRepresentation def: The uniform extension, retaining its ring structure. · OAI.KadisonSimilarity.denseSubringRepresentation
density def: The physical density lifted to the Euclidean kinetic domain of GLPS. · OAI.BoltzmannNonuniqueness.EuclideanFlight.density
density def: A positive density that makes the two mean constraints elementary. · OAI.ClosedSurfaceR4.CollarVelocity.density
DensityBadFamily structure: Explicit finite arithmetic data consumed by the density descent. No residue-distribution or divisor-moment estimate is asserted by this structure: these are the many_residues and moment_bound fields that must be supplied. · OAI.Problem337.DensityBadFamily
densityBridgeSlots def: Ordered identification of the normal slot and recursive boundary slots. · OAI.Mahler.densityBridgeSlots
DensityCRTData structure: A bounded density product with its proved local-mean-zero consequence. · OAI.Ostmann.DensityCRTData
densityCRTList def: This is the actual product of the centered functions, formed by CRT along the list of distinct prime factors. · OAI.Ostmann.densityCRTList
densityDivisorCount def: The truncated divisor count appearing in the shifted moment hypothesis. · OAI.Problem337.densityDivisorCount
DensityExpansionContract def: lem:density, including the convention of closing a nonflat argument. · OAI.MatroidProphet.DensityExpansionContract
densityFailure def: The bad pairs for one orientation of a radial kernel. · OAI.Falconer.densityFailure
densityG def: Rational functions used to obtain bounded approximants without bounded input norms. · OAI.TraceConeClassification.densityG
densityMeasure def: The ordinary Lebesgue-density measure. · OAI.LeanBlast.KLS.densityMeasure
densityMeasure def: Norm total-variation measure of an actual complex density. · OAI.LocalCancellation.densityMeasure
densityMeasure def: The probability distribution with the given density, restricted to its open interval. · OAI.Problem358.PositiveIntervalDensity.densityMeasure
densityMeasure def: Norm total-variation measure of an actual complex density. · OAI.SignedDisk.LocalCancellation.densityMeasure
densityMeasure def: Multiplication by a density, ignoring exceptional negative values on null sets. · OAI.WeakMTWTransport.densityMeasure
densityMomentParameter def: A common exponential size parameter for cutoffs and translated divisors. · OAI.Problem337.densityMomentParameter
densityNum def: Zero-based piece indexing: this is exactly the source M_1,...,M_6. · OAI.SharpPlanar.IntegerBasis.densityNum
densityPower def: Ordinary (not graded) tensor power of a one-site density, as in05. · OAI.CoordinateSweeps.SignedTensor.densityPower
densityProbabilityMeasure def: A nonnegative integrable density of mass one defines a probability. · OAI.PolycyclicRecognition.densityProbabilityMeasure
densityRatio def: The derivative dictated by successive conditional section densities. It is defined on all prefixes, including invalid prefixes of density zero. · OAI.Problem358.TriangularDensity.densityRatio
DensityResidueFamily structure: Raw residue data before the good sets are constructed. The terminal expansions, small-residue supply and shifted divisor moments are explicit inputs; all finite propagation is proved below. · OAI.Problem337.DensityResidueFamily
densityRoot def: The unique Hilbert--Schmidt vector realizing the positive density root. · OAI.NuclearUltrapower.densityRoot
departure def: The last level at which the vertex belongs to the nested giant. · OAI.WeakPinned.Hierarchy.Depth.departure
departureKey def: Departure reheats the fresh pair jointly and every other index separately. Orientation is retained in either case. · OAI.BoundedTreewidthL1.ExpandedParticleLaw.departureKey
Dependency inductive: A domain can be used after any finite number of continuation frames. · OAI.PureTypeSystem.PlainSpaces.Schema.Dependency
DependencyExpansion inductive: Node labels carry remaining physical depth and remaining rank. Children in the first and second arrays have distinct edge sorts. · OAI.EditApproximation.DependencyExpansion
dependencyPathBudget def: Overcount of dependency paths with at most depth descending edges and indices strictly earlier-index/pass edges. · OAI.EditApproximation.dependencyPathBudget
dependentProduct def: Independent observations at literal slot IDs, allowing different outcome types (side traces and old leaf oracles carry genuinely different data). · OAI.TraceReconstruction.FiniteLaw.dependentProduct
dependentRowEquiv def: Pullback along a surjection parametrizes the dependent rows exactly. · OAI.MaxCutGames.Inverse.KMSAnalytic.dependentRowEquiv
dependentRowEquiv def: Pullback along a surjection parametrizes the dependent rows exactly. · OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.dependentRowEquiv
DependsOn def: Dependence only on the listed coordinate values of a placement. · OAI.CoordinateSweeps.Placement.DependsOn
DependsOn def: Agreement on the named coordinates determines event membership. · OAI.MetricEntropyDuality.FiniteProductCounting.DependsOn
DependsOn def: A finite event is determined by the coordinates in its declared support. · OAI.QuantitativeVanDerWaerden.FiniteProbability.DependsOn
DependsOn def: A test depends only on the listed coordinates of the same configuration. · OAI.TwoPointCorrelations.DependsOn
DependsOnBoolean def: A function is constant on the cells cut out by the indicated coordinates. · OAI.PolycyclicRecognition.DependsOnBoolean
DependsOnlyOn def: A function inspects only the indicated coordinates of its input subset. · OAI.LeanBlast.SecondKahnKalai.DependsOnlyOn
DependsOutside def: A function is unchanged by modifications inside the indicated coordinates. · OAI.LeanBlast.SecondKahnKalai.DependsOutside
Depot structure: A row with bounded ports and virtual baseline. · OAI.ExactDerandomization.Stem.Depot
depth def: The first index at which a geometric scale reaches exp m. · OAI.Problem337.ResidueLevels.depth
depth def: Number of contractions reducing a logarithmic height S to one. · OAI.Problem337.TerminalDepth.depth
depth def: Distance, with the corner sign, from the chosen endpoint of a coordinate. · OAI.SharpLiebThirring.CubeFlags.Flag.depth
depth def: Only the maximum loop-nesting depth determines the number of counters. · OAI.Superstring.BitCode.Program.depth
depth def: AND/OR depth, with literals at depth zero. · OAI.TwoPointCorrelations.AC0Circuit.depth
depth def: Actual jointly defined hierarchy depth in the original complex plane. · OAI.WeakPinned.Grid.depth
depthCap def: The radial profile has only finitely many values, one per reachable column. This explicit cap bounds every node ever used by the pasted field. · OAI.PlanarL1.Columns.Model.Point.RadialTree.depthCap
depthCount def: Count of vertices at one depth, including unary vertices. · OAI.DilutedSpinGlass.PrescribedTree.depthCount
depthWeightedCount def: Charge every actual node by a function of its remaining physical depth, as needed for length-dependent initial-state evaluation. · OAI.EditApproximation.DependencyExpansion.depthWeightedCount
DerdzinskiHitchinInput def: The compact positive-curvature specialization of the published half-conformally-flat identification. · OAI.PositiveEinsteinFour.Geometry.DerdzinskiHitchinInput
derivation def: Its derivation is induced by the universal objectwise derivation. · OAI.ActualCotangent.derivation
derivation def: derivation of the structure sheaf extending the given affine coordinate derivation. · OAI.AffineDerivation.derivation
derivation def: Transfer one unit of polynomial degree from src to dst. Other blocks are spectator variables. · OAI.Problem346.PolynomialShift.derivation
derivation def: The coefficient of the action parameter is its infinitesimal derivation. · OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.derivation
derivationColumn def: Restrict the source of an operator-valued derivation to a closed summand. · OAI.KadisonSimilarity.derivationColumn
derivationEnergy def: The actual finite squared Euclidean energy of the entrywise derivation. · OAI.GrahamSpherical.derivationEnergy
derivative def: A spatial derivative loses exactly one order, with no increase of jet norm. · OAI.ForcedComputation.BoundedSpatialJets.derivative
derivativeBound def: A depth-independent bound on derivative order k; the total absolute one-step extension coefficient is the count of eligible old positions plus all sampled leaves. · OAI.DilutedSpinGlass.PrescribedTree.derivativeBound
derivativeCLM def: Bounded spatial differentiation between consecutive finite jet spaces. · OAI.ForcedComputation.BoundedSpatialJets.derivativeCLM
derivativeMatrix def: The block formula for the incidence derivative. · OAI.KervaireFixedSpace.derivativeMatrix
derivativeMatrix def: The matrix of derivatives in a fixed tangent direction. · OAI.PositiveEinsteinFour.Bianchi.derivativeMatrix
derivativePair def: Squared derivative columns, the pairs used in the one fixed compact set. · OAI.DoublingHilbert.derivativePair
derivativePairing def: Pairing with the corresponding derivative component of the gradient. · OAI.PositiveEinsteinFour.TraceHessian.derivativePairing
derivativeQuaternion def: Apply a quaternion only in the derivative slot of a matrix-valued tensor. · OAI.PositiveEinsteinFour.Bianchi.derivativeQuaternion
derivativeRatio def: The derivative of H relative to the derivative of the square root. · OAI.PositiveEinsteinFour.Variance.derivativeRatio
derivativeSlotForm def: Twice the diagonal curvature-block contribution on the derivative slots. · OAI.PositiveEinsteinFour.HighestHessian.derivativeSlotForm
derived def: The native derived tensor endofunctor of this one fixed bounded projective bimodule complex. · OAI.LittleFinitistic.BimoduleTotal.BoundedProjective.derived
derived def: The actual fixed bimodule tensor total descends to the native derived category of B-modules. · OAI.LittleFinitistic.BimoduleTotal.derived
derived abbrev: Tensor via the actual bounded right-projective Q_X, with the left D-action retained. · OAI.LittleFinitistic.SelectedOrdinaryResolution.derived
derivedBarSplitting def: Manuscript prop:bar-splitting, eq:bar-splitting: the balanced tensor of D with the verified free A-bar resolution is isomorphic, in the genuine integer derived category, to the actual coproduct of (F^r N)[r]. · OAI.DerivedBar.ParityBridge.derivedBarSplitting
derivedBaseChange abbrev: The actual left-derived balanced base-change functor on modules, viewed in the integer derived category. · OAI.DerivedBar.derivedBaseChange
derivedBimoduleTensor def: The actual Q_T tensor lift with the source's left B-action retained. · OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.derivedBimoduleTensor
derivedComparison def: This derived endofunctor is computed by the signed tensor total on every input complex. · OAI.LittleFinitistic.BimoduleTotal.derivedComparison
derivedCountCoproductIsColimit def: The original count direct sum, with its original inclusions, is an actual coproduct after passing to the genuine integer derived category. · OAI.DerivedBar.derivedCountCoproductIsColimit
derivedEmbedding def: The canonical derived-category functor on the actual bounded projective source. · OAI.LittleFinitistic.FiniteProjectiveHomotopy.derivedEmbedding
derivedEvenIterate def: Every even iterate is the first-block inflation of the corresponding actual P[b] tensor iterate. · OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedEvenIterate
derivedFiniteTotal def: Localization of the actual signed total tensor functor, justified by the proved preservation theorem. · OAI.LittleFinitistic.ComplexTensor.derivedFiniteTotal
derivedFiniteTotalComparison def: The explicit natural comparison with the actual chain-level total on every input complex. · OAI.LittleFinitistic.ComplexTensor.derivedFiniteTotalComparison
derivedFirst def: Native derived inflation on the first block of the product algebra. · OAI.LittleFinitistic.BlockModule.derivedFirst
derivedFirstComponent abbrev: The exact derived first-component functor on the whole product-ring derived category. · OAI.LittleFinitistic.BlockModule.derivedFirstComponent
derivedFirstComponentFactors def: On chain representatives, the composite is the identity localization. · OAI.LittleFinitistic.BlockModule.derivedFirstComponentFactors
derivedFirstIso def: The ordinary localization model is naturally the exact derived inflation. · OAI.LittleFinitistic.BlockModule.derivedFirstIso
derivedFirstRetraction def: Taking the first component recovers every derived object, naturally. · OAI.LittleFinitistic.BlockModule.derivedFirstRetraction
derivedInterval abbrev: The native B-valued derived tensor total on a chosen support interval. · OAI.LittleFinitistic.BimoduleTotal.derivedInterval
derivedIso def: The already proved chain comparison descends through the actual localization. · OAI.LittleFinitistic.BimoduleTotalPresentation.derivedIso
derivedIterateCongr def: All finite genuine iterations are compatible with the original bimodule equivalence. · OAI.DerivedBar.BimoduleTensor.derivedIterateCongr
derivedIterateFlatIso def: The flattened complex represents actual finite iteration of the constructed left derived tensor. This uses the previously proved derived universal property. · OAI.DerivedBar.derivedIterateFlatIso
derivedIterateIndexedIso def: Genuine derived tensor iteration represented by the exact indexed block complex. No count splitting or projective-dimension statement is assumed. · OAI.DerivedBar.RecursiveTotal.derivedIterateIndexedIso
derivedIterateLeadingBarIso def: The final leading D-bar resolution leaves the represented derived iterate unchanged. · OAI.DerivedBar.derivedIterateLeadingBarIso
derivedIterateMultibarIso def: The independent recursive multibar represents genuine finite derived iteration. · OAI.DerivedBar.derivedIterateMultibarIso
derivedIterateWeightShiftIso def: Each original count summand is the genuine [r] shift of the constructed finite derived tensor iterate. · OAI.DerivedBar.ParityBridge.derivedIterateWeightShiftIso
derivedObject abbrev: Actual derived object of a nonnegative chain complex, with degree n sent to -n. · OAI.LittleFinitistic.PDBar.derivedObject
derivedRestriction def: The derived restriction homomorphism on the coherent Grothendieck group. · OAI.ActualCartier.derivedRestriction
derivedSingleEvaluation def: Evaluation of the actual derived endofunctor on a degree-zero module is the native tensor complex in D(B-Mod). · OAI.LittleFinitistic.BimoduleTotal.derivedSingleEvaluation
derivedSquareComparison def: The actual native derived square comparison on every complex Z, with first-block support. Both tensor functors are the localization lifts of their verified bounded projective models. · OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedSquareComparison
derivedSquareObject def: The actual ordinary square on every native derived object, using essential surjectivity of Q. · OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedSquareObject
derivedTensor def: Left derived balanced tensor on the localization of nonnegative chain complexes. · OAI.DerivedBar.derivedTensor
derivedTensor def: The derived endofunctor obtained from the actual bounded resolution of X. · OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedTensor
derivedTensorBarSplitting def: The actual left-derived D tensor over A is the actual categorical coproduct of genuine shifted derived iterates. This proves the manuscript's bar-splitting proposition; projective-dimension detection is a separate result. · OAI.DerivedBar.ParityBridge.derivedTensorBarSplitting
derivedTensorCongr def: The same actual tensor equivalence descends to the genuine bar-derived functor. · OAI.DerivedBar.BimoduleTensor.derivedTensorCongr
derivedTensorExplicitIso def: The explicit two-sided total represents the genuine derived tensor of the input. · OAI.DerivedBar.derivedTensorExplicitIso
derivedTensorIterate def: Genuine derived functor iteration, with the manuscript's right-to-left order. · OAI.DerivedBar.derivedTensorIterate
derivedTensorIterateIso def: Successive resolve-and-tensor complexes represent iteration of the genuine left derived functor. No derived comparison is included as a hypothesis. · OAI.DerivedBar.derivedTensorIterateIso
derivedTotal def: Localization of the actual tensor total, retaining the outside action. · OAI.LittleFinitistic.BimoduleComplexTensor.derivedTotal
derivedUnderlyingComparison def: The existing finite derived evaluation agrees with canonical derived localization of the explicitly computed homotopy evaluation. · OAI.LittleFinitistic.QuadraticEncoding.derivedUnderlyingComparison
Derives inductive: Classical first-order natural deduction with equality. Hypotheses may be an infinite theory, but a derivation is a finite inductive proof. The allI and exE rules use a fresh last variable, and shift all assumptions to avoid capture. We … · OAI.PartitionConsistency.Derives
derivExponent def: Exponents of the variables acting by differentiation. · OAI.Problem335.derivExponent
Desc structure: Parameters included in the open-code guarantee. · OAI.PowerSaving.RAM.Desc
desc def: A map out of an additive image of the recursive total is specified on all literal nested terms. Only finite diagonal coproducts are distributed. · OAI.DerivedBar.RecursiveTotal.desc
desc def: The actual positive chain map specified by two matching cell tables. · OAI.Thomason.Construction.PastingGlobeBasis.desc
desc def: The map specified independently on the two ends. · OAI.Thomason.Construction.SimplicialCylinder.desc
desc def: Unique strict map with the prescribed four matching bounded cells. · OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.desc
desc def: Every matching pair determines its unique strict map from the pasting. · OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.desc
descApp def: Extend the two cell tables linearly on canonical bases. · OAI.Thomason.Construction.PastingGlobeBasis.descApp
descend def: Descent through the actual circle quotient, proved from its actual fibers. · OAI.ArnoldCounterexample.Quadric.descend
descend def: Descent of coefficient evaluation to the balanced tensor. · OAI.DerivedBar.Balanced.descend
descend def: The coefficient derivation obtained from a homogeneous Laurent derivation. · OAI.StableCoordinate.LaurentDescent.descend
descendantEnergyAt def: Proper-child covariance at the later first split, retaining the entire original evaluation prefix. These are genuine iterated kernel expectations. · OAI.DilutedSpinGlass.PrescribedTree.descendantEnergyAt
descendantFamily def: The descendant family using a section of the actual image. · OAI.MaxCutGames.Gadget.descendantFamily
descendantFamily def: The descendant family using a section of the actual image. · OAI.UniqueGamesTheorem.Gadget.descendantFamily
descendantFirst def: The first terminal-level descendant. · OAI.ReflexiveFixedPoints.OrderedTree.descendantFirst
descendantHi def: Exclusive upper endpoint of the descendant block. · OAI.ReflexiveFixedPoints.OrderedTree.descendantHi
descendantLast def: The last terminal-level descendant. · OAI.ReflexiveFixedPoints.OrderedTree.descendantLast
descendantLevelDefect def: Weighted map displacement on one level below a specified ancestor. Levels before the ancestor contribute zero. · OAI.ReflexiveFixedPoints.TreeEvaluation.descendantLevelDefect
descendantLo def: Inclusive lower endpoint of the descendant block. · OAI.ReflexiveFixedPoints.OrderedTree.descendantLo
descendants def: The later-level descendants of a node. · OAI.ReflexiveFixedPoints.OrderedTree.descendants
descendants def: Descendants are defined by the actual branch beyond the parent edge. · OAI.TorsionFreeZeroDivisors.TreeCentroid.descendants
descendAtomSources def: The first entry of the path is the root branch. Source indices count the previously reconstructed pivots in root-to-leaf order. · OAI.Ostmann.descendAtomSources
descendDerivation def: A specified function whose image intertwines a derivation through an injective algebra map automatically satisfies all derivation laws. · OAI.AbhyankarSathaye.CommutingDerivations.descendDerivation
descendedFactorAction def: An action on the first factor commuting with the second factor and fixing their actual intersection descends to an action on the whole group. · OAI.PolycyclicRecognition.descendedFactorAction
descendedFactorHom def: The induced endomorphism on the original group. · OAI.PolycyclicRecognition.descendedFactorHom
descending def: r (n-1) ... r i, with the empty product when n ≤ i. · OAI.FiniteAlgebraicEnvelopes.Adjacent.descending
DescendingParents structure: A predecessor system whose heights strictly decrease to its root. The well-foundedness here uses finiteness, not any discretization of real lengths. · OAI.PlanarL1.Weighted.DescendingParents
descendingRowPermutation def: Sort row sizes in nonincreasing order, with no restriction on ties. · OAI.Nagata.Workers.W10.descendingRowPermutation
descendPosetLabel def: Descend an actual strict ordered label through finite reflection. · OAI.Thomason.Construction.FiniteReflectionInput.descendPosetLabel
descendQuotientAction def: A group of automorphisms preserving the kernel acts on the quotient. · OAI.PolycyclicRecognition.descendQuotientAction
descendQuotientAutomorphism def: A kernel-preserving automorphism descends using any section of the surjective quotient map. Its value on a projected point is independent of the choice of section. · OAI.PolycyclicRecognition.descendQuotientAutomorphism
descendStarAlgHom def: Descend a proved compatible map through a surjective star-algebra map. · OAI.Generator.Tracial.descendStarAlgHom
Descent structure: Descending paths are actual attained shortest switching paths, with the manuscript's length domain and endpoint deficit, not assumed rays in a quotient. · OAI.PlanarL1.Columns.Model.Field.Descent
DescentSystem structure: Local combinatorial descending-cube data. All these fields will be supplied by the actual trace normal form, not by a geometric exactness assumption. · OAI.CubicalChains.DescentSystem
Description abbrev: Ordered padded row coefficients, row values, column coefficients, column values, affine coefficient, and affine intercept. Redundant descriptions are intentional: counting descriptions provides an upper bound on distinct slices. · OAI.MaxCutGames.Inverse.RowErasureDescriptions.Description
Description abbrev: Ordered padded row coefficients, row values, column coefficients, column values, affine coefficient, and affine intercept. Redundant descriptions are intentional: counting descriptions provides an upper bound on distinct slices. · OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.Description
DescriptorInverseSymbols structure: The exact factors delivered by the finite inverse calculation. · OAI.Falconer.DescriptorInverseSymbols
deshiftedCount def: The actual integer cochain count complex shifted by -r. · OAI.DerivedBar.ParityBridge.deshiftedCount
designatedPass def: The fixed solution chooses this residue only in the success analysis. · OAI.LowSpaceSubsetSum.CompressionSetup.designatedPass
designatedReciprocal def: The exact reciprocal coefficient of one lit/unlit designation, including the singleton atoms. · OAI.TwoPointCorrelations.designatedReciprocal
Desk structure: A predictable linear wager driven by the revealed output bit, with quadratic cost. · OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk
destination def: Decode the returned cloud index into its actual global padded dart. · OAI.MaxCutGames.Foundations.PCP.PreprocessingInternalRows.destination
destination def: Decode the returned cloud index into its actual global padded dart. · OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.destination
detach def: Detach an edge from both endpoint rotations. It then forms a separate one-edge component and can be discarded by restricting to its complement. · OAI.KaplanskyCounterexample.Planar.Ribbon.detach
detach def: A zero-weight edge can be detached without changing any nonzero balance. · OAI.KaplanskyCounterexample.Planar.WeakBalanced.detach
detectorSet def: The actual compact prediction detector, computed before the next map. · OAI.ReflexiveFixedPoints.CandidateContext.detectorSet
detectorSet def: The first k + 1 test points and every possible actual prediction limit. The sequence is supplied before the candidate map; density is only used later. · OAI.ReflexiveFixedPoints.Prediction.detectorSet
detectorSet def: The prescribed finite test prefix and all possible evaluated prediction limits. · OAI.ReflexiveFixedPoints.Prediction.Prefix.detectorSet
detectorSites def: The countable coordinate family used by the fixed representatives. · OAI.PartitionConsistency.TailSelector.TailData.detectorSites
DetectsPrefix def: One witness satisfies every nonroot detector on the path to a node. · OAI.ReflexiveFixedPoints.OrderedTree.DetectsPrefix
determinant def: Multiplication by uw-vs lands in the bounded pair space. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.determinant
determinant def: Multiplication by D = uw - vs after putting u = 1. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant
determinantBasepoint def: Evaluation at an actual determinant-one matrix supplies a scalar retraction. · OAI.StableCoordinate.Obstruction.determinantBasepoint
determinantEval def: Evaluate the determinant quotient at any point satisfying its defining relation. · OAI.StableCoordinate.Obstruction.determinantEval
determinantGrading def: The quotient grading for any weight vector satisfying the two determinant constraints. · OAI.StableCoordinate.Obstruction.determinantGrading
determinantIdeal def: Defining ideal of the determinant-one ring with coordinates (a,d,b,c,u). · OAI.StableCoordinate.BundleCharts.determinantIdeal
determinantMap def: The natural map from the determinant module to rational forms. · OAI.CanonicalCoordinates.determinantMap
determinantPiece abbrev: The induced weighted pieces in the determinant quotient. · OAI.StableCoordinate.Obstruction.determinantPiece
determinantRelation def: Variables are ordered a,d,b,c,u. · OAI.StableCoordinate.DeterminantDomain.determinantRelation
DeterminantRing abbrev: Coordinate ring of SL₂ × A¹, in the source's coordinate order. · OAI.StableCoordinate.BundleCharts.DeterminantRing
DeterminantRing abbrev: Coordinate ring of the determinant hypersurface, ordered a,d,b,c,u. · OAI.StableCoordinate.DeterminantDomain.DeterminantRing
determinantSqBound def: Factorwise rational upper bound for the determinant on the parameter disk. · OAI.DefocusingNLS.ProfileCertificate.determinantSqBound
DeterminedBy def: An event is determined by a finite set of coordinates. · OAI.KaplanskyCounterexample.FiniteLocalLemma.DeterminedBy
Deterministic def: The formalization proves $\mathsf L=\mathsf{RL}=\mathsf{BPL}$ for binary languages in an explicit Turing-machine model with logarithmic workspace. The randomized classes use polynomial time: $\mathsf{RL}$ never accepts a no-instance and … · OAI.ExactDerandomization.Machine.Deterministic
Deterministic def: At most one next-state/move pair at every state and scanned symbol. · OAI.TwoWayComplementation.TwoNFA.Deterministic
deterministicValue def: The actual game value is the maximum over all deterministic local strategies. · OAI.MaxCutGames.Reduction.IncidenceProbability.deterministicValue
deterministicValue def: The actual game value is the maximum over all deterministic local strategies. · OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.deterministicValue
deterministicVector def: Move the full mass of each row to its selected label. · OAI.MaxCutGames.Repetition.deterministicVector
deterministicVector def: Move the full mass of each row to its selected label. · OAI.UniqueGamesTheorem.Repetition.deterministicVector
detMultilinear def: The determinant as a continuous multilinear map in its rows. · OAI.GAD.detMultilinear
develop def: Takahashi's complete development, including type annotations. · OAI.PureTypeSystem.Expr.develop
develop def: Complete development contracts only matching-labelled redexes. · OAI.PureTypeSystem.Labelled.Expr.develop
deviation def: Midpoint deviations normalized by the lengths of the parent edges. · OAI.DiamondDistortion.Diamond.deviation
deviation def: The centered deficit contributed by one bit. · OAI.QuantitativeVanDerWaerden.FairBitTail.deviation
df def: The ambient differential of the polynomial. · OAI.ArnoldCounterexample.ThreePoints.df
DFTProgram def: Include an integer and address bound polynomial in n. Constants inside this bound are immaterial (a constant number of logarithmic sized words is allowed). W n is the work allowance, including the order program, one root primitive and the … · OAI.PowerSaving.DFTProgram
dfvs def: Minimum number of vertices of a feedback set. No weights or auxiliary cost oracle appear in this definition. · OAI.DirectedFeedback.Digraph.dfvs
dgen def: The five quotient generators (a,d,b,c,u). · OAI.StableCoordinate.BundleCharts.dgen
diagonal def: The diagonal of a real multilinear map, expanded in the fixed coordinates. · OAI.ElasticityBoundaryTaylorPolynomial.diagonal
diagonal def: The original diagonal tensor e tensor n in its actual fixed submodule. · OAI.ExternalTensor.Section4.ArrowVertex.diagonal
diagonal def: Two equal local copies in the coordinate halves. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.diagonal
diagonal def: Unit-valued diagonal, valid over the full coefficient ring. · OAI.IntegralCharacterVarieties.MatrixIso.diagonal
diagonal def: Restricting the separate action to the diagonal. · OAI.KadisonKastler.NonsingularAction.diagonal
diagonal def: The vertical differential on the finite direct sum of the columns. · OAI.LittleFinitistic.FiniteColumnComplex.diagonal
diagonal def: Diagonal substitution on the space with the prescribed degree bounds. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonal
diagonal def: Substitute the first variable pair into the second variable pair. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal
diagonal def: The diagonal characters with their actual unit values. · OAI.PolycyclicRecognition.PositiveTriangular.diagonal
diagonal def: The individual longitudinal derivative in each full-coordinate direction. · OAI.Problem358.TriangularDensity.diagonal
diagonalAdjoinedGroup def: The subgroup generated by A and a prescribed invariant subgroup. · OAI.DukePrimeDegree.diagonalAdjoinedGroup
diagonalAmplification def: The constant diagonal amplification of an element. · OAI.KadisonKastler.diagonalAmplification
diagonalBlocks def: Block direct sum with the line-label index first. · OAI.Release075.diagonalBlocks
diagonalColumnEquiv def: The diagonal vertex component of its own induced column is exactly N. · OAI.LittleFinitistic.CornerTensor.diagonalColumnEquiv
diagonalCommutatorVelocity def: The actual velocity of the diagonal commutator curve. · OAI.DukePrimeDegree.diagonalCommutatorVelocity
diagonalComplex def: Original insertion into a single induced column, degree by degree. · OAI.ExternalTensor.Section4.ArrowVertex.diagonalComplex
diagonalComplexIso def: On actual complexes, the diagonal vertex is the original complex via its specified insertion. · OAI.LittleFinitistic.VertexColumnComplex.diagonalComplexIso
diagonalCovariance def: On a diagonal block the cross-multiplicity word covariance is exactly the existing same-multiplicity covariance. · OAI.KadisonSimilarity.WordLevelMatrixActions.diagonalCovariance
diagonalCurvatureAction def: The matrix-slot curvature operator for a diagonal trace-free curvature block. · OAI.PositiveEinsteinFour.Bianchi.diagonalCurvatureAction
diagonalDAG def: A fixed diagonal layer charges exactly one multiplication per coordinate. · OAI.ExactFourier.ScalarConvolution.diagonalDAG
diagonalEquiv def: A column's own vertex is its original right module, with no replacement action. · OAI.LittleFinitistic.BimoduleVertex.diagonalEquiv
diagonalEquiv def: A diagonal corner has only its scalar trivial path. · OAI.LittleFinitistic.CornerSpaces.diagonalEquiv
diagonalExp def: The determinant-one exponential diagonal matrix. · OAI.DukePrimeDegree.diagonalExp
diagonalField def: A chosen genuine field for an operator in the diagonal commutant. · OAI.KadisonSimilarity.diagonalField
diagonalFlow def: Time t of the one-parameter diagonal flow associated with u. · OAI.DukePrimeDegree.diagonalFlow
diagonalFourierSum def: A diagonal phase sum, represented in the actual Euclidean Hilbert norm. · OAI.LipschitzHilbert.PhaseCombinatorics.diagonalFourierSum
diagonalGenerators def: The pointwise diagonal generating family from an exact cocycle. · OAI.KadisonKastler.diagonalGenerators
diagonalGradientPairing def: The diagonal matrix-slot form keeps both Bianchi arguments. · OAI.PositiveEinsteinFour.Bianchi.diagonalGradientPairing
diagonalHaarReference def: A normalized reference law allowing either a diagonal or a Haar draw. · OAI.FiniteFactor.CouplingParameters.diagonalHaarReference
diagonalHom def: The diagonal assignment respects the unit-group multiplication. · OAI.CoarseAssembly.Congruence.diagonalHom
diagonalHom def: The positive diagonal action, encoded as a homomorphism to the ambient group. · OAI.DukePrimeDegree.diagonalHom
diagonalL def: The fixed Frobenius-coordinate norm cost of the diagonal embedding. · OAI.HarmonicCounterexample.LinearODE.diagonalL
diagonalLabeling def: Use a single label function on both auxiliary sides, solely to share the already proved finite-average calculation. This does not change the v2 game. · OAI.MaxCutGames.Decoder.TableKeysCompleteness.diagonalLabeling
diagonalLabeling def: Use a single label function on both auxiliary sides, solely to share the already proved finite-average calculation. This does not change the v2 game. · OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.diagonalLabeling
diagonalLaplacianBlock def: The normalized weak Weyl equation in a diagonal frame. · OAI.PositiveEinsteinFour.TraceHessian.diagonalLaplacianBlock
diagonalMatrixConjugation def: Conjugation by the split real diagonal one-parameter subgroup. · OAI.DukePrimeDegree.diagonalMatrixConjugation
diagonalModulation def: Coordinatewise modulation by unit characters. · OAI.LipschitzHilbert.PhaseCombinatorics.diagonalModulation
diagonalModulationIsometry def: The common diagonal carrier as a complex linear isometry. · OAI.LipschitzHilbert.diagonalModulationIsometry
diagonalNatIso def: The diagonal insertion is natural in the original right module. · OAI.LittleFinitistic.VertexColumnComplex.diagonalNatIso
diagonalParameters def: Deleted-log-coordinate-free parametrization of the positive diagonal group. · OAI.DukePrimeDegree.diagonalParameters
diagonalPolynomial def: The diagonal polynomial, formed from the actual ordered-tuple expansion. · OAI.MetricEntropyDuality.diagonalPolynomial
diagonalPolynomial def: The one-variable polynomial obtained by restricting a multilinear form to an affine diagonal. · OAI.Problem346.diagonalPolynomial
diagonalProduct def: Recursive product of the canonical sampler's longitudinal derivatives. · OAI.Problem358.TriangularDensity.diagonalProduct
diagonalRegularMultiplier def: other i is the fixed denominator consisting of the outside and all small slots other than the regular prime i. The two giants are retained. · OAI.Ostmann.diagonalRegularMultiplier
diagonalRemainderFrequency def: Frequencies after the distinguished child's diagonal carrier is removed. · OAI.LipschitzHilbert.diagonalRemainderFrequency
diagonalRepresentation def: Restrict the actual product representation to the diagonal group. · OAI.KadisonKastler.StandardTracialPosition.diagonalRepresentation
diagonalSecond def: The second derivative in one direction, expressed without choosing coordinates on the space of bilinear maps. · OAI.RegularPointCoordinates.diagonalSecond
diagonalSpecialization def: Substitute y=x, leaving x,u,v as three variables. · OAI.Paper170.diagonalSpecialization
diagonalSquareBlock def: The actual trace-free square of a diagonal Weyl block. · OAI.PositiveEinsteinFour.TraceHessian.diagonalSquareBlock
diagonalStarAlgHom def: The diagonal star representation of a finite product of C⋆-algebras. · OAI.KadisonKastler.diagonalStarAlgHom
diagonalToDegreeLT def: Diagonal substitution with both the domain and codomain degree bounded. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonalToDegreeLT
diagonalTrace def: The trace of diag(t^n,t^(-n),1), expressed using a unit so that the inverse is available in an arbitrary commutative ring. · OAI.CoarseAssembly.diagonalTrace
diagonalTraceHull def: Closed convex hull in the supplied trace Hilbert space. · OAI.KadisonKastler.diagonalTraceHull
diagonalUnit def: A diagonal unit is represented by a genuine invertible diagonal matrix. · OAI.PolycyclicRecognition.diagonalUnit
Diagram structure: A full finite decorated tree pair, including the entire leaf bijection. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram
Diagram structure: The finite oriented boundary cycles contain each side occurrence exactly once. Their successor is the one constructed from the allowed vertices. No cycle is discarded if a facet or a seam appears repeatedly. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram
Diagram structure: An actual injective diagram on all of the monoid, with no finite or rank cutoff. Stronger diagrams are the larger diagrams in the translation order. · OAI.PartitionConsistency.DiagramForcing.Diagram
Diagram structure: Four boundary relations; the direction distinguishes the two copies of Fin m. · OAI.TwoWayComplementation.Diagram
diagram abbrev: The labelled diagram has the original orientals as underlying objects. · OAI.Thomason.Construction.CosieveSimplex.diagram
diagram abbrev: The actual topological simplices indexing a realization. · OAI.Thomason.Construction.RealizationPrism.diagram
diagram abbrev: The labelled diagram has the original orientals as underlying objects. · OAI.Thomason.Construction.SieveSimplex.diagram
diagram def: The identity-extension diagram of maps from the actual globe images. · OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.diagram
diagramCutoff def: One cutoff simultaneously enforces the original-letter linear filling and unbounded closed-picture chain vanishing. It is selected before each alphabet and realization. · OAI.HyperbolicObstruction.IncidenceTemplate.diagramCutoff
diameterBadA def: The A-side actual diameter-failure event, still conditioned on girth. · OAI.TorsionFreeZeroDivisors.TypedDiameter.diameterBadA
DiameterLE def: Every pair of points in a set is at distance at most the given radius. · OAI.Tingley.DiameterLE
Diameters def: Both exact component diameter conclusions, including disconnected graphs. · OAI.TorsionFreeZeroDivisors.GraphSample.Diameters
diameterScale def: The deterministic scale exp(m(ν) - m(τ)) from the normalization lemma. · OAI.MetricMeasureLimits.DiameterCenter.diameterScale
diamond def: Countably branching diamonds, all current edges of length one. · OAI.ForestSpace.Diamond.diamond
DiamondEdges inductive: The entirely unlabelled closure used in graph reconstruction. Its completeness for Bruhat graphs is a separate obligation; this definition neither changes Bruhat order nor defines the R/KL polynomials. · OAI.KLInvariance.DiamondEdges
dice def: Uniform conditional law on a block (total default law if not fitting). · OAI.FourierLLogL.Dyadic.Node.dice
DicksonTwoBound def: The norm-two specialization of Dickson (2014), Lemma 2.9, Eq. (19), including its column form obtained by taking adjoints. · OAI.KadisonSimilarity.DicksonTwoBound
dictator def: The honest assignment is an actual Boolean cut (coordinate dictators). · OAI.OptimalMaxCut.LongCode.Game.dictator
difference def: Difference of two paths ending at the same basepoint. · OAI.HyperbolicObstruction.HSpacePathObstruction.difference
difference def: This is √3 * s̃; using it avoids divisions by a square root in the coordinate inverse. · OAI.PositiveEinsteinFour.Bianchi.difference
differenceBall def: The entire closed unit ball of the difference span, viewed in X. · OAI.ReflexiveFixedPoints.differenceBall
differenceBit def: Boolean full-subtractor gate. · OAI.RationalHitting.StackLanguage.differenceBit
differenceLaw def: The relative difference law uses two independent samples of the same conditional probability law; it is not an independent marginal difference. · OAI.EuclideanFiveColor.RelativeCenters.differenceLaw
differenceList def: The literal difference list, including any duplicated outputs only once. · OAI.MetricEntropyDuality.SignedCompression.differenceList
differenceParameters def: First samples minus second samples, with the same fixed order of letters. · OAI.PolycyclicRecognition.differenceParameters
differenceSpan def: The norm-closed linear span of the actual differences. · OAI.ReflexiveFixedPoints.differenceSpan
differencingBudget def: The elementary square-root budget obtained from repeated differencing. · OAI.Problem337.differencingBudget
differencingPhase def: The unit complex phase with frequency one. · OAI.Problem337.differencingPhase
Differential structure: A finite-column total differential, recorded independently of a chosen direct-sum presentation. · OAI.LittleFinitistic.FiniteColumnComplex.Differential
differential def: Recursive alternating face differential. No A-flatness of N is required. · OAI.DerivedBar.differential
differential def: Independently recursive differential on the flattened direct sum. Its construction uses only the original functor differentials, finite-sum distribution, and the previously constructed inner differential, never the total differential. · OAI.DerivedBar.RecursiveTotal.differential
differential def: The actual signed differential, now linear for the outside algebra. · OAI.LittleFinitistic.BimoduleComplexTensor.differential
differential def: The B-extended resolution differential is left multiplication by 1 tensor c. · OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.differential
differential def: The actual tensor differential retains both B-actions. · OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.differential
differential def: Differential on the free abelian groups of canonical bases. · OAI.Thomason.Construction.PastingGlobeBasis.differential
differential def: Differential of lambda, defined on the quotient rather than postulated. · OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.differential
differentialAlgebraic def: Extension to an arbitrary algebraic field extension in characteristic zero. · OAI.GrahamSpherical.AlgebraicExtension.differentialAlgebraic
differentiate def: Only the base-map slot is differentiated. The new direction is one of the three variation slots, so a third variation uses no extra map slots. · OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.differentiate
diffK def: Dirichlet profile minus rescaled approximate Hilbert profile modulated by sine. · OAI.FourierLLogL.Period.diffK
digitColor def: A digit is identified with its residue, so an extra remainder is redundant. · OAI.QuantitativeVanDerWaerden.digitColor
digitInTime def: A composable actual-time witness for any well-formed positive-radix digit. · OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.digitInTime
digitInTime def: A composable actual-time witness for any well-formed positive-radix digit. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.digitInTime
digitPower def: Locate the unique power of two having the requested binary digit index. Search is bounded by n+1; no exponentially large unary number is ever built. · OAI.OptimalMaxCut.CounterMachine.Expr.digitPower
digitProd def: Matrix tensor product indexed by digit tuples. · OAI.PowerSaving.digitProd
digitSteps def: The exact step count for one digit, including its possible reset. · OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.digitSteps
digitSteps def: The exact step count for one digit, including its possible reset. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.digitSteps
Digraph structure: Finite loopless digraph. Opposite arcs are permitted. Every arc is listed explicitly. No symmetric closure or undirected-cycle convention is used. · OAI.DirectedFeedback.Digraph
dihedralArcProjection def: The open centered angular arc, expressed as a spectral cut of the real part. · OAI.KadisonSimilarity.dihedralArcProjection
dihedralGroupWordVectors def: All ordinary dihedral rotation and reflection-coset vectors. · OAI.KadisonSimilarity.TracialCornerGeometry.dihedralGroupWordVectors
dihedralHalfProjection def: The corner of a symmetry, written algebraically. · OAI.KadisonSimilarity.dihedralHalfProjection
dihedralNormalization def: The actual normalization factor t⁻¹ᐟ². · OAI.KadisonSimilarity.dihedralNormalization
DihedralSpectralArc structure: Exactly the spectral data of the centered arc used in the argument. · OAI.KadisonSimilarity.DihedralSpectralArc
DihedralSpectralArcInput def: The local bounded Borel functional calculus specialization. In its application C is the dihedral von Neumann algebra and τ its normal trace. · OAI.KadisonSimilarity.DihedralSpectralArcInput
dihedralWordIsometry def: Isometric inclusion of the completed tracial base space as the k-th actual dihedral word space. · OAI.KadisonSimilarity.dihedralWordIsometry
dihedralWordMap def: The unnormalized algebraic word inclusion. · OAI.KadisonSimilarity.dihedralWordMap
dilate def: The normalized dilation is appropriate to the two-dimensional chart. · OAI.ClosedSurfaceR4.FiniteOrderSmoothing.dilate
dilate def: Change physical units by a positive factor. This scales the actual switch sets and vertical path lengths; the cyclic link graph is not changed. · OAI.PlanarL1.Columns.Model.dilate
dilate def: Field values have length units too. The vertical Lipschitz constant does not change on passing to new physical units. · OAI.PlanarL1.Columns.Model.Field.dilate
dilate def: Change a cut system's physical units by the same factor as its columns. The measure, height-coordinate variables, and every scalar chart are all scaled; there is no implicit normalization of label mass. · OAI.PlanarL1.Columns.Model.SetSystem.dilate
dilate def: Exact dilation transports all measurable prefixes, generator amplitudes and endpoints. The chain length and prefix radius are unchanged. · OAI.PolycyclicRecognition.CartanWordModel.BoxProbeChains.dilate
dilate def: Extend f(m/a) by zero away from multiples of a. · OAI.TwoPointCorrelations.dilate
dilatedNuclei def: Rescaling the nuclear positions leaves all nuclear charges unchanged. · OAI.ContinuumCoulomb.dilatedNuclei
dilationPrimes def: The primes up to the short-period cutoff. · OAI.QuantitativeVanDerWaerden.dilationPrimes
dimension def: The least universal coordinate dimension. The theorem also asserts that this least dimension has the defining property, ruling out an empty infimum. · OAI.SubpolynomialLp.dimension
dimensionLanguage def: A malformed word is rejected: membership requires a valid nonempty simple matrix and k>0. · OAI.WLIdentification.dimensionLanguage
DimensionLE def: A cell has dimension at most n precisely when its n-boundaries are itself. Higher identity extensions require no extra cell data. · OAI.Thomason.Construction.StrictOmegaCategory.DimensionLE
dimensionSpectralValue def: This is a constructed scalar value on self-adjoint operators; it is not yet packaged as a linear functional. · OAI.Generator.Tracial.dimensionSpectralValue
DimensionwiseGenerated def: The exact dimensionwise generation hypothesis used in Steiner's normalization argument. It follows from exists_bounded_expression for the positive-table comparisons. · OAI.Thomason.Construction.StrictOmegaCategory.DimensionwiseGenerated
Dipole structure: The six oriented incidences of two faces which cancel across their common edge. Outside partners may reconnect arbitrarily elsewhere in the filling. · OAI.Release075.TriangleFilling.Dipole
dipoleClassesEquiv def: Exactly the two face classes, not an arbitrary assumed two-cell subset. · OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces.dipoleClassesEquiv
dipoleFace def: Two oppositely oriented triangular faces. · OAI.Release075.PermCycles.dipoleFace
dir def: dir = false means ascending · OAI.ExactDerandomization.Counter.dir
dir def: Forward directional factor. · OAI.PowerSaving.Binary.dir
diracDefect def: Translation defect of the point probability at g. · OAI.ThompsonNonamenability.diracDefect
dirDeriv def: A fixed-direction derivative, used only as notation for the actual Fréchet derivative. · OAI.AffineBernstein.dirDeriv
directChartHom def: Actual dehomogenization in chart c, with the two surviving coordinates ordered by Fin.succAbove. · OAI.Nagata.W27.directChartHom
directedComplex abbrev: The augmented directed simplex complex with its differential identity. · OAI.Thomason.Construction.SimplexComplex.directedComplex
directedEdgeEmbedding def: A vertex and a direction identify a unique ordered cube edge. · OAI.LeanBlast.GotsmanLinial.directedEdgeEmbedding
directedIntegerEdge def: The increasing-edge coefficient, including the two endpoint cutoffs. The auxiliary extra predicate carries the remaining vertex deletions. · OAI.TwoPointCorrelations.directedIntegerEdge
directedSup def: Directed unions do not add factors or conditional joins. · OAI.PartitionConsistency.ConservativeMonoids.Subobject.directedSup
DirectedSystem structure: The displayed algebraic hypotheses of Section 3, Lemma directed-bound. The field and algebra are unital; zero idempotents are allowed by the source. · OAI.LittleFinitistic.DirectedBound.DirectedSystem
directedSystem def: The actual chain algebra has the source's directed vertex system, including l=0. · OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.directedSystem
directedSystem def: A concrete linear extension of the source's product order, with exactly 3n vertices. · OAI.LittleFinitistic.OrdinarySimulation.TensorDirected.directedSystem
directGradS def: The actual gradient convolution, as a bounded linear differential. · OAI.TriangularBilliards.directGradS
direction def: The redundant compact group has a canonically chosen horizontal frame. · OAI.KervaireIncidenceCurrent.direction
direction def: The projective direction of the literal blowup of affine 3-space at its origin; no line-bundle or regularity identification is assumed. · OAI.KummerSourceModel.direction
direction def: The linear part of the affine parametrization. · OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.direction
direction def: The linear part of the affine parametrization. · OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.direction
directionalCurvatureMatrix def: Contract the two Jacobi directions before choosing the normal basis. · OAI.PositiveEinsteinFour.Geometry.directionalCurvatureMatrix
directionalDerivativeCLM def: One directional derivative loses one order and has norm at most the direction norm. · OAI.ForcedComputation.BoundedSpatialJets.directionalDerivativeCLM
directionalIterate def: Repeated constant directional differentiation as a genuine derivative operator. · OAI.Nagata.W19.directionalIterate
directionalMeanConstant def: The directional mean constant is the Fekete limit of mean passage times along a lattice ray, with the infimum taken over positive indices. · OAI.GammaFPP.directionalMeanConstant
directionalPath def: Differentiate a continuous jet path pointwise. · OAI.ForcedComputation.PlaneScalarMild.directionalPath
directionalVisitPath def: The outward-switch-return path using an explicitly prescribed Cartan direction. · OAI.PolycyclicRecognition.CartanWordModel.directionalVisitPath
directionBox def: A packet's spatial box expressed in a fixed comparison direction. · OAI.LipschitzHilbert.PacketLatticeData.directionBox
directionBox def: A packet's spatial box expressed in a fixed comparison direction. · OAI.LipschitzHilbert.SourceLabeledLattice.directionBox
directionEquiv def: The concrete simultaneous slice is exactly an affine copy of Hom(domain / columnSpan, commonRowKernel). · OAI.MaxCutGames.Inverse.Shortcode.Slice.directionEquiv
directionEquiv def: The concrete simultaneous slice is exactly an affine copy of Hom(domain / columnSpan, commonRowKernel). · OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.directionEquiv
Directions abbrev: Free directions of a row/column slice, intrinsically as quotient maps. · OAI.MaxCutGames.Inverse.Shortcode.Slice.Directions
Directions abbrev: Free directions of a row/column slice, intrinsically as quotient maps. · OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.Directions
directionSet def: A direction is ordered by its full underlying point set. Slopes are just coordinates for all of the one-dimensional subspaces, including the vertical one. · OAI.KaplanskyCounterexample.Prescription.directionSet
directS def: The direct Euclidean convolution term on one copy of the table. · OAI.TriangularBilliards.directS
directSumComplex def: The direct sum of module chain complexes, with the componentwise actual differential. · OAI.DerivedBar.directSumComplex
directSumComplexInclusion def: The canonical summand map into the already constructed chain direct sum. · OAI.DerivedBar.directSumComplexInclusion
directSumComplexIsColimit def: The native componentwise chain direct sum is the actual categorical coproduct. · OAI.DerivedBar.directSumComplexIsColimit
directSumComplexProjection def: Projection from the original chain direct sum to its r-th complex. · OAI.DerivedBar.directSumComplexProjection
dirichlet def: Unscaled form: each site has a rate-one clock. · OAI.SKGap.dirichlet
dirichletMatrix def: The Dirichlet matrix with diagonal blocks D and both off-diagonals -1. · OAI.PositiveEinsteinFour.Jacobi.dirichletMatrix
dirichletSolution def: A definition by choice, not a wellposedness assumption. The fallback is irrelevant once the Dirichlet problem has been proved solvable. · OAI.Elasticity.dirichletSolution
dirichletSource def: Integration against an actual L² source on the Dirichlet space. · OAI.RegularPointCoordinates.dirichletSource
dirtyEval def: Each internal gate starts at an arbitrary dirty value, and its computed linear combination is added to that value. The literal zero remains literal zero. · OAI.ExactFourier.Program.dirtyEval
disagreement def: The weight of a disagreement for two independent draws (not necessarily normalized). · OAI.UniformSparsestCut.FiniteWeights.disagreement
disagreementFiberEquiv def: A cloud disagreement is the same actual internal dart in global coordinates. · OAI.MaxCutGames.Foundations.PCP.CloudRounding.disagreementFiberEquiv
disagreementFiberEquiv def: A cloud disagreement is the same actual internal dart in global coordinates. · OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.disagreementFiberEquiv
discardInTime def: The same exact trace packaged for composition with ambient machine phases. · OAI.MaxCutGames.Foundations.Complexity.MachineLookup.discardInTime
discardInTime def: The same exact trace packaged for composition with ambient machine phases. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.discardInTime
discrepancy def: The discrepancy between twice-localizing and conjugating a localization. · OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.discrepancy
discrepancy def: The number of V layers minus ρ times the number of U layers. · OAI.Problem335.BalancedSchedule.discrepancy
discreteCoproductCocone def: The chosen coproduct also presents a discrete diagram not syntactically written as Discrete.functor. · OAI.Thomason.Construction.discreteCoproductCocone
discreteCoproductIsColimit def: Its universal property follows directly from the coproduct universal property. · OAI.Thomason.Construction.discreteCoproductIsColimit
discreteCoproductIso def: Comparison from the chosen coproduct to any colimit of the same diagram. · OAI.Thomason.Construction.discreteCoproductIso
DiscreteE def: A separate synonym ensures that the dual uses the discrete topology, not the Euclidean topology inherited by the embedded algebraic field. · OAI.PlaneFiveColor.Spectral.DiscreteE
discreteGap def: Rayleigh quotient definition of the uniform-site discrete heat-bath gap. · OAI.SKGap.discreteGap
discreteGoodMass def: Gibbs mass of realized initial states still farther than 1 / 4 after k attempts. · OAI.CriticalSK.discreteGoodMass
discriminantSign def: Determinant character of the nondegenerate radical quotient, including rank zero (where the empty determinant is one). · OAI.SidorenkoCounterexample.discriminantSign
DisjointFour def: Four selections are disjoint in their natural union order. · OAI.LowSpaceSubsetSum.RepresentationUniverse.DisjointFour
disjointLists def: Only disjoint lists are used as bad-event witnesses. · OAI.MetricEntropyDuality.DirectionSampling.disjointLists
DisjointSupports def: Different tuples in the list use disjoint sets of indices. · OAI.MetricEntropyDuality.DisjointSupports
disjointWordSubsetEquiv def: Disjoint columns in one row are precisely the fixed-size subsets of the complement of that row. · OAI.KadisonKastler.disjointWordSubsetEquiv
diskAnnulus def: Exception annuli for exact unit distances from the small closed disks. · OAI.EuclideanFiveColor.diskAnnulus
DiskAtlas structure: Disjoint relator disks in a larger ribbon diagram. The other darts may belong to an outside word or be isolated markers from previous cancellations. · OAI.KervaireRibbon.DiskAtlas
diskAtRadius def: The actual compact disk mass at the indicated logarithmic radius level. Infinite radius times use the already constructed terminal measure. · OAI.SLEExactGauge.Multipoint.CanonicalMass.diskAtRadius
DiskCore structure: A literal finite polyline core in a bounded convex disk, with specified leaf ports on its boundary. These data are constructed by the surgeries. · OAI.PlanarL1.Topology.DiskCore
diskDerivativeWeight def: A formula for the derivative weight which is measurable at every real angle and agrees with the disk chart derivative on the natural angle interval. · OAI.SLEExactGauge.diskDerivativeWeight
DiskEuler def: The disk Euler estimate for the actual circle rotation and word matching. The empty word is distinguished, since it has no boundary occurrences. · OAI.TorsionFreeZeroDivisors.WordPairing.DiskEuler
DiskHomotopy inductive: A disk certificate obtained by elementary triangle attachments/removals, with spurs/collapses allowed. The index is the number of triangular faces. · OAI.HyperbolicObstruction.FiniteComplex.DiskHomotopy
diskKernel def: The normalized open-disk kernel, without an absolute value on the input. · OAI.SignedDisk.SobolevBand.diskKernel
DiskMove inductive: An elementary disk move. A noncollapsed triangular face costs one; a spur or a collapsed edge costs zero. Contexts are unchanged. · OAI.HyperbolicObstruction.FiniteComplex.DiskMove
DiskRLP def: The concrete disk-boundary right lifting property. · OAI.GroupRingTopology.Cellular.DiskRLP
diskSubspace def: Lower U fibers, read from the old solution, including the initial fiber and last-to-first edge. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.diskSubspace
disorderReplicaLaw def: Keeping the external disorder in the sampled space is essential: projected overlaps depend on the same rotation as the Gibbs measure. · OAI.InvariantIsing.disorderReplicaLaw
dispatch def: Edges are listed in decreasing schedule order, so the chronologically last transfer is the outermost one. · OAI.KLInvariance.SchedulePaths.dispatch
dispatcher def: Pop the one-bit match result. Only a match pops the remaining local rank. Every completed skipped row separately pushes the global position. · OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.dispatcher
dispatcher def: Reuse the RHS vector already loaded by MachineRhsLoad; dispatch takes one real transition, and resets only the optional temporary bit. · OAI.MaxCutGames.Reduction.MachineOutcomeRows.dispatcher
dispatcher def: Pop the one-bit match result. Only a match pops the remaining local rank. Every completed skipped row separately pushes the global position. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.dispatcher
dispatcher def: Reuse the RHS vector already loaded by MachineRhsLoad; dispatch takes one real transition, and resets only the optional temporary bit. · OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.dispatcher
dispersionModel def: The model polynomial S(u). · OAI.CubicFirstMoment.dispersionModel
dispersionPolynomial def: The polynomial F_u(a) in the corrected-dispersion argument. · OAI.CubicFirstMoment.dispersionPolynomial
displacementMap def: Negative radial normalization of the concrete nonvanishing correction. · OAI.ThompsonNonamenability.Analytic.displacementMap
displacementScalar def: The literal finite source displacement scalars: nine zeros, followed by Pi(z_j). · OAI.Nagata.W06.TorusConfiguration.displacementScalar
displayCopyEquiv def: The actual finite display, reindexed fibre by fibre by its exact copy count. · OAI.ContingencyTables.LabelledFactorial.displayCopyEquiv
distance def: Distance in the weighted support norm; on a nonempty finite set it is a minimum. · OAI.CoboundaryExpanders.Complex.distance
distance def: Distance in the source norm. On a nonempty subspace of this finite cochain space the infimum is a minimum; no closure or cocycle relaxation is used. · OAI.CoboundaryExpanders.Complex.distance
distance def: Full-permutation total variation, with the source's factor one half. · OAI.CubeShuffle.distance
distance def: Final edges have length 2⁻ᵏ: this is the shortest-path metric of the normalized graph. · OAI.DiamondDistortion.Diamond.distance
distance def: A notation for the actual original all-edge distance of a typed matching. · OAI.FKCRT.Inventory.StackMatching.distance
distance def: The shortest-path distance, via Mathlib's actual graph distance. · OAI.ForestSpace.Diamond.distance
distance def: Infimum of smooth path lengths, the intrinsic Riemannian distance. · OAI.HarmonicCounterexample.distance
distance def: The genuine extended shortest-path distance, including infinity. · OAI.MetricEntropyDuality.PartitionGraph.distance
distance def: The pairwise distances of the five centers. · OAI.Problem356.CenterCertificate.distance
distanceDatum def: The canonical compact squared-distance datum at this source scale. · OAI.RegularPointCoordinates.DyadicDistanceReplacements.distanceDatum
distanceError def: The pretentious-distance error in the published complex estimate. · OAI.JointDickman.PublishedInputs.distanceError
distanceLayer def: The exact-distance layer within the root component. · OAI.CycleClique.Construction.distanceLayer
distanceLength def: The group length associated to the left-invariant metric used in the Lie-group application. · OAI.PolycyclicRecognition.distanceLength
distanceSet def: Original Euclidean distances; auxiliary projections are not used here. · OAI.Falconer.distanceSet
distanceShell def: A finite distance layer, also useful for weights indexed by ordered pairs. · OAI.LeanBlast.GotsmanLinial.distanceShell
distanceSq def: The continuous squared distance to one on the spectrum. · OAI.KervaireSpectral.distanceSq
distanceWeight def: The weight in the classical threshold argument, and in the spherical stationary-phase normalization, is dist ^ (-(d-1)/2). · OAI.Falconer.distanceWeight
distinct def: The forced children are distinct at every split. Central restrictions are separate deterministic predicates, not conditioning events. · OAI.TraceReconstruction.BinaryWindowLabels.distinct
DistinctAnchorGroups def: A selected family uses each anchor group at most once. · OAI.Problem348.AnchorRigidity.DistinctAnchorGroups
distinctDerivative def: The distinct-coordinate pairing in a derivative layer. · OAI.Problem335.FactorialExpansion.distinctDerivative
distinctMultiplication def: The distinct-coordinate pairing in a multiplication layer. · OAI.Problem335.FactorialExpansion.distinctMultiplication
distinctProductNet def: A quadratic comparison scan counts every runtime prime only once. No sorting primitive or mathematical finset operation is used by the circuit. · OAI.ExactQuantumFactoring.BitArithmetic.distinctProductNet
distinctSumCount def: The count N(V) used in the paper's deficiency. · OAI.LowSpaceSubsetSum.distinctSumCount
distinctSums def: Distinct integer values of subset sums on the index domain V. · OAI.LowSpaceSubsetSum.distinctSums
DistinctThroughLabel abbrev: Multisets containing a prescribed label, with no repeated label. · OAI.KadisonKastler.DistinctThroughLabel
distinctThroughLabelEquiv def: Distinct multisets are exactly finite subsets with the same cardinality. · OAI.KadisonKastler.distinctThroughLabelEquiv
distinguished def: Constant tables give compatible distinguished parameters with no additional choice of an inhabitant at any recursive node. · OAI.PureTypeSystem.PlainSpaces.Schema.distinguished
distortion def: The product of the two maximal distance ratios. · OAI.EditDistortion.distortion
distortion def: The product of the two maximal pairwise distance ratios. · OAI.TreeEdit.BinaryLower.distortion
distortion def: Product of the two maximal ratios. On the finite nontrivial metric spaces used below each displayed supremum is a maximum. · OAI.TreeEdit.BinaryLower.distortion
distortion def: Product of the two maximal pairwise distance ratios. · OAI.TreeEdit.distortion
distribution def: The regularized spectral distribution attached to an actual positive matrix. · OAI.Kaplansky.CuntzDimensionState.distribution
divBody def: Remainder 0, denominator 5, unread MSD numerator 6, quotient 7. · OAI.RationalHitting.StackLanguage.divBody
Divergence inductive: The deepest reference prefix and its forbidden reference-containing children. This describes the whole compatible choice set, including both old unused leaves and fresh divergences in reference-free subtrees. · OAI.DilutedSpinGlass.PrescribedTree.Divergence
divergence def: Relative entropy, used only when q is positive on the positive support of p. · OAI.CliqueFreeIndependence.FiniteEntropy.divergence
divergence def: Euclidean divergence in the orthonormal coordinate frame. · OAI.CubicTorus.divergence
divergence def: Literal sum of corner phases on each boundary circle. · OAI.KervaireFlow.divergence
divergence def: Quaternionic divergence in each matrix column. · OAI.PositiveEinsteinFour.Bianchi.Tensor.divergence
divergence def: Bianchi is imposed on each fixed outer derivative, using the original quaternion action on the inner derivative and matrix slots. · OAI.PositiveEinsteinFour.HighestHessian.divergence
divergence def: Cartesian divergence at points where the field is differentiable. · OAI.StationaryNS.divergence
divide def: Binary division starts with numerator in 0 and denominator in 5. The original denominator is retained; quotient is placed in 7, remainder in 0. Every other register is cleared. · OAI.RationalHitting.StackLanguage.divide
dividedAnalyticFamily def: Finite divided normal family; every exponent is a natural number, so the formula defines an actual function at the central parameter zero. · OAI.Nagata.Workers.W28.dividedAnalyticFamily
divideDigits def: Long division, scanning the original numerator most-significant-bit first. The quotient and remainder registers remain ordinary little-endian words. · OAI.RationalHitting.StackLanguage.divideDigits
dividedIterate def: The factorially divided nth iterate of a derivation. · OAI.StableCoordinate.LNDExponential.dividedIterate
dividedNormalCenter def: Actual center in the rescaled normal chart for an affine moving point. · OAI.Nagata.Workers.W28.dividedNormalCenter
dividedNormalCoordinate def: The actual divided normal coordinate, extended at zero by the derivative. · OAI.Nagata.Workers.W28.dividedNormalCoordinate
divisionRing abbrev: An actual division ring containing all ordered quantum-monomial series; no finite-dimensional-domain or external division-algebra theorem is assumed. · OAI.RationalHitting.QuantumSeries.divisionRing
divisionState def: The common row state at a division boundary, with its local residue reset. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionState
divisionState def: The common row state at a division boundary, with its local residue reset. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionState
divisionStates def: The residue and the emitter's unit field are just permuted; no tape is read or written by this static change of finite state coordinates. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionStates
divisionStates def: The residue and the emitter's unit field are just permuted; no tape is read or written by this static change of finite state coordinates. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionStates
DivisorDense def: A positive integer has a divisor within a factor of m below each scale. · OAI.Problem337.DivisorDense
divisorEulerFactor def: A local Euler factor, in the indexing convenient for Rankin's trick. · OAI.Problem337.divisorEulerFactor
divisorHarmonicWeight def: The multiplicative weight occurring in divisor harmonic moments. · OAI.Problem337.divisorHarmonicWeight
divisorMomentWeight def: The multiplicative weight used in harmonic and Rankin divisor moments. · OAI.Problem337.DivisorMoment.divisorMomentWeight
divisorMultiples def: Positive integers up to Y divisible by at least one member of A. · OAI.Problem337.SparseBadDivisorTail.divisorMultiples
divisorNet def: Supplied divisor computed from exactly this run's retained quantum bits. All guarded arithmetic is explicit, including full rare-branch order guesses. · OAI.ExactQuantumFactoring.FixedSplit.divisorNet
divisorPointwiseError def: An explicit uniform error coefficient for the pointwise truncated-divisor estimate. · OAI.Problem337.divisorPointwiseError
divisorPrimes def: Divide a subfactor from the parent's prime list, in bounded time: there is at most one division per prime occurrence in the already supplied list. · OAI.ExactQuantumFactoring.divisorPrimes
divisorQuadraticScalar def: The v divisor is part of the original modular quadratic argument. · OAI.Ostmann.divisorQuadraticScalar
divisorResidueEnergy def: The normalized residue-fiber energy of the complete positive divisor list. · OAI.Problem337.divisorResidueEnergy
divisors def: Search each possible small divisor once, stopping at the first divisor. The numeric square-root bound is a parameter to this counted inner loop. · OAI.LowSpaceSubsetSum.SamplerAttempts.divisors
divisorsBits def: A bit-bounded trial-division implementation. The loop bound is a power of two determined by the candidate width, so no square-root oracle is used. Squares beyond the candidate are discarded by an ordinary multiplication and comparison … · OAI.LowSpaceSubsetSum.SamplerAttempts.divisorsBits
divisorsOK def: Need a uniform computation yielding a modulus with Δ < p-1. · OAI.Fifths.Modulus.divisorsOK
divisorSplitSet def: Replace one denominator, keeping the other denominators in T. · OAI.Problem337.divisorSplitSet
divisorSplitSmall def: The two replacement denominators associated to a proper divisor. · OAI.Problem337.divisorSplitSmall
divisorSplitUpper def: The larger denominator in the split of 1 / n indexed by d ∣ n. · OAI.Problem337.divisorSplitUpper
divisorTupleCount def: Ordered positive factor tuples, expressed by Dirichlet powers of zeta. · OAI.Problem337.SelbergError.divisorTupleCount
DixmierExponentialInput def: The global-chart specialization of Dixmier's real-root criterion. · OAI.PolycyclicRecognition.DixmierExponentialInput
DM abbrev: The fixed denominator constant from the residue construction. · OAI.Problem337.RawDensityParameters.DM
DN def: The weak displacement-to-traction pairing; definition (physical-dn). · OAI.Elasticity.DN
Dom def: Least data needed for a "big-O with +1" natural work budget convenience. · OAI.PowerSaving.RAM.Dom
dom def: dominance formulated without choosing minima · OAI.GeneralMahler.Scarf.dom
domain def: Actual closed full-column update domain. · OAI.PlanarL1.Columns.Model.MainCell.domain
domain def: The literal closed union of radius-R seed balls, on each vertical column. · OAI.PlanarL1.Columns.Model.SecondaryCell.domain
domainEquiv def: Domain coordinates, with the first coordinate literally in range X. · OAI.MaxCutGames.Appendix.CoordinateTransport.domainEquiv
domainEquiv def: Domain coordinates, with the first coordinate literally in range X. · OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.domainEquiv
domains def: Preliminary domains are unrestricted for the polynomial potentials and are the actual chart sources for the two supporting-value potentials. · OAI.Problem356.FiveComponentGeometry.domains
domainSort def: Scan the ambient indices in order. The quadratic charge includes membership tests against a list representation of the finite domain. · OAI.LowSpaceSubsetSum.RepresentationLeaf.domainSort
domainSplit def: A dual Fourier index on a product is exactly its two restrictions. · OAI.MaxCutGames.Fourier.SplitMaps.domainSplit
domainSplit def: A dual Fourier index on a product is exactly its two restrictions. · OAI.UniqueGamesTheorem.Fourier.SplitMaps.domainSplit
domainU def: An ambient open carrier of the exact local expression's relative coordinate domain. It is NOT a smooth extension of the expression. · OAI.SmoothObstruction.ManifoldCoordinates.domainU
dome def: label cutoff by reference radius · OAI.FourierLLogL.Dyadic.Thermal.dome
dominant def: Exact dominant selection; the same reference, hence the same mark, is held until a wholesale event. · OAI.KServer.EpochSchedule.dominant
dominated def: Positivity on support condition. · OAI.FourierLLogL.Law.dominated
Dominates def: Entrywise complex modulus bounds, retaining the two-term matrix product. · OAI.DefocusingNLS.ProfileCertificate.Dominates
Domination def: Exact signed-density domination05 eq13, expressed for every irreducible (including absent ones whose projection is zero). The mixture is a genuine probability measure on the source's even density matrices, not an unproved positive operator … · OAI.CoordinateSweeps.SignedTensor.Domination
dot def: Missing coordinates are zero. The loop runs over the vector's length. · OAI.ContingencyTables.IntegerMatrixPrograms.dot
dot def: The normalized site contraction used in sections/decorrelation.tex. · OAI.DilutedSpinGlass.FiniteLaw.dot
dot def: Field dot product, with all three coordinates displayed. · OAI.MaxCutGames.Quadratic.dot
dot def: Field dot product, with all three coordinates displayed. · OAI.UniqueGamesTheorem.Quadratic.dot
dotCharacter def: The additive character obtained by pairing against a binary vector. · OAI.MaxCutGames.Fourier.MatrixNoise.dotCharacter
dotCharacter def: The additive character obtained by pairing against a binary vector. · OAI.UniqueGamesTheorem.Fourier.MatrixNoise.dotCharacter
dotFunctional abbrev: A coordinate vector as a linear functional, for the standard dot pairing. · OAI.MaxCutGames.Inverse.MatrixChart.dotFunctional
dotFunctional abbrev: A coordinate vector as a linear functional, for the standard dot pairing. · OAI.UniqueGamesTheorem.Inverse.MatrixChart.dotFunctional
dotLinear def: The dot-product functional over the large field. · OAI.MaxCutGames.Quadratic.dotLinear
dotLinear def: The dot-product functional over the large field. · OAI.UniqueGamesTheorem.Quadratic.dotLinear
double def: Double an open band and sew every non-short-end interface across the two copies. Exactly four short ends remain. This is an exhaustive whole-port construction, not merely a list of proposed endpoints. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double
double abbrev: nesting scans for 3 chunk coordinates. · OAI.PowerSaving.RAM.Bench.Engrave.double
doubleAssembly def: All longitudinal and transverse whole seams are present, with precisely matching original ordered color occurrences. No independent child-germ matching is used. Short ends here are closed against their mirror copies; splicing them into the … · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleAssembly
doubleBergRotation def: Two simultaneous corner rotations. The right corner is moved first. · OAI.WeakPureInfiniteness.doubleBergRotation
doubled def: Both copies are aligned, but the two occurrences are different vertices. · OAI.DilutedSpinGlass.PrescribedTree.doubled
doubledComputableInPolyTime def: Reinterpret the existing producer using the proved exact codec equality. · OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.doubledComputableInPolyTime
doubledComputableInPolyTime def: Reinterpret the existing producer using the proved exact codec equality. · OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.doubledComputableInPolyTime
doubledCornerLinear def: Duplicate the upper-left matrix entry. · OAI.WeakPureInfiniteness.doubledCornerLinear
doubledOverlap def: The overlap of every old leaf, with two complete independent descendant sides retained. This is also the normalized full leaf product. · OAI.DilutedSpinGlass.PrescribedTree.doubledOverlap
doubleDualIso def: Functoriality of the literal structure-sheaf double dual. · OAI.CoherentModelActual.doubleDualIso
doubledWiring def: Identifying matching short ends supplies an honest closed occurrence assembly; the external matching is itself equal-arity, as required. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.doubledWiring
doubleFixedMap def: Both traversal blocks have the same fixed space dimension, without a spectral-theorem assumption or a nonzero complement assumption. · OAI.KervaireFixed.doubleFixedMap
doubleFlow def: Unit-speed geodesic flow of the oriented double in the two interior charts. · OAI.TriangularBilliards.doubleFlow
DoubleInternal abbrev: Index bookkeeping for the literal doubled patch. The first two summands are the two longitudinal sewings; the last two are ALL transverse branches. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.DoubleInternal
doubleIso def: Reversing twice recovers the original object in the slice. · OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.doubleIso
doubleKernel def: Kernel integration on the two physical triangle copies, with the exact unnormalized Euclidean spatial integral and normalized phase pairing. · OAI.TriangularBilliards.doubleKernel
doubleLastVertexPiece def: The compatible comparison prism attached to each original simplex. · OAI.Thomason.Construction.doubleLastVertexPiece
doubleLift def: Pullback from the billiard phase space preserves L² exactly. · OAI.TriangularBilliards.doubleLift
doubleOppositeIso def: The double opposite has exactly the original strict cells. · OAI.Thomason.Construction.StrictOmegaCategory.doubleOppositeIso
doubleOutgoingVariation def: The derivative when the first normal varies through unit vectors. The normal component of its variation is included, so the formula also applies to the radially normalized extension off the sphere. · OAI.BoltzmannNonuniqueness.CollisionCompactness.doubleOutgoingVariation
doubleRotate def: Rotation in the oriented tangent circle; the negative copy has the opposite physical rotation, exactly as in a conjugate Euclidean chart. · OAI.TriangularBilliards.doubleRotate
doubletonBranchCount def: The number of two-vertex branches. · OAI.HadwigerMatching.doubletonBranchCount
doubleTriangle def: The sphere consisting of two oppositely oriented triangles. · OAI.ArtinCAT0.TriangleMesh.doubleTriangle
DoublingAtMost def: Intrinsic open-ball doubling with a specified integer bound and centers in the subset. · OAI.DoublingHilbert.DoublingAtMost
doublingTuple def: Two scaled orthogonal inclusions, padded by twenty-two zero maps. These algebraic hypotheses are discharged by the actual sum coordinates. · OAI.Kaplansky.doublingTuple
down def: A snap (rounding down). · OAI.FourierLLogL.Dyadic.down
down def: Shift one unit of degree from the first coordinate block to the second. · OAI.Problem346.PolynomialShift.down
downTensor def: The down-center tensor, with the ordinary, not conjugate, contraction on the internal edge. The order m,n is essential for the snake identity. · OAI.CriticalHoneycomb.Transfer.PhysicalTiles.downTensor
DownToken abbrev: Each copy of an actual base down edge is a distinct token. · OAI.Superstring.Counts.Data.DownToken
doZ def: knobs player. · OAI.HadwigerCounterexample.doZ
DPath def: Conveniently prove the shear and inverse-transpose shear together. · OAI.PowerSaving.Cluster.DPath
dProbe def: The block-density difference d_m^T(X). · OAI.InfiniteMatroidCounterexample.dProbe
drainBody def: All symbols of one source stack flow to a number of destinations (possibly zero), with each popped bit mapped to its own fixed code. · OAI.Fifths.SM.drainBody
drainLoop def: Consume an isolated unary field, including its delimiter. · OAI.MaxCutGames.Foundations.Complexity.MachineHorner.drainLoop
drainLoop def: Consume an isolated unary field, including its delimiter. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.drainLoop
drainPhase def: The caller only supplies a local code equality; the physical drain and its entire runtime are obtained from the checked drain machine. · OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.drainPhase
drainPhase def: The caller only supplies a local code equality; the physical drain and its entire runtime are obtained from the checked drain machine. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.drainPhase
Draw structure: The actual draw before forgetting the hidden projection and private map. · OAI.MaxCutGames.Decoder.AdviceExperiment.Draw
Draw structure: The actual draw before forgetting the hidden projection and private map. · OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw
draw def: The physical port walk, starting and ending at the first/last ports. It has one middle edge per macro-edge, and two spokes between them. · OAI.TorsionFreeZeroDivisors.WeightedPortMoore.draw
drawAgreement def: A named pointwise observable makes the finite expectation permutations explicit without changing the actual sampled draw. · OAI.MaxCutGames.Decoder.ActualSeedSampling.drawAgreement
drawAgreement def: A named pointwise observable makes the finite expectation permutations explicit without changing the actual sampled draw. · OAI.UniqueGamesTheorem.Decoder.ActualSeedSampling.drawAgreement
Drawing structure: The literal topological drawing, with its coordinates identified with the complex plane. No polygonal or combinatorial planarity assumption is added. · OAI.PlanarL1.Topology.Drawing
DrawingPassages structure: Geometric cut data for the original drawing. Existence is proved below; this record asserts no crossing bound or drawing-normalization conclusion. · OAI.Paper170Geometry.DrawingPassages
drawProductEquiv def: Drawing an occurrence and a slot at each position is the same finite sample space as drawing the occurrence tuple and the slot tuple separately. · OAI.MaxCutGames.Soundness.PartnerFullSampling.drawProductEquiv
drawProductEquiv def: Drawing an occurrence and a slot at each position is the same finite sample space as drawing the occurrence tuple and the slot tuple separately. · OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.drawProductEquiv
drift def: The classical radial drift x·∇u. · OAI.StationaryNS.drift
driftConstant def: The constant in companion Lemma pilot-drift. · OAI.UniformKServer.PilotCompact.driftConstant
Drop def: Immediately follows a strict-to-weak threshold drop in the age-ordered list. · OAI.BoundedTreewidthL1.AnchorCache.Drop
drop def: Remove k initial levels. The additive depth form avoids subtraction casts. · OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.drop
dropPrefix def: Subtraction-indexed convenience wrapper for removing an initial prefix. · OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.dropPrefix
dsRate def: The scalar rate appearing in the alphabet-independent repetition estimate. · OAI.MaxCutGames.Repetition.dsRate
dsRate def: The scalar rate appearing in the alphabet-independent repetition estimate. · OAI.UniqueGamesTheorem.Repetition.dsRate
dssMatrix def: The oriented pair matrix is precisely the original edge-list interaction; parallel edges are summed, with no ghost and no change to the field. · OAI.BufferedIsing.dssMatrix
Dual abbrev: Its full real continuous dual. · OAI.DiamondDistortion.SegmentSystem.Dual
dual def: Literal rotation-system duality: faces and vertices exchange, while individual edge-side copies and their pairing are unchanged. · OAI.HyperbolicObstruction.PictureSwitch.PictureMap.dual
dualBaseChangeMap def: The canonical dual base-change map, without any false freeness assumption. · OAI.DualCartierRestriction.dualBaseChangeMap
DualCore abbrev: The polar core is identified with the full continuous dual using block reflexivity and density. · OAI.BoundedTreePotentials.Segments.DualCore
dualDetPhase def: The pullback of the dual determinant phase to primal coordinates. · OAI.AffineBernstein.dualDetPhase
dualEquiv def: Perfect duality for homogeneous symmetric powers in finite dimension. · OAI.Problem346.PairingConstruction.dualEquiv
dualFiniteFreeIso def: The dual of a finite free sheaf really is the same finite free sheaf. · OAI.CoherentDual.dualFiniteFreeIso
dualHead def: Coordinate truncation on the full dual, defined by the biorthogonal basis independently of the core isometry. · OAI.BoundedTreePotentials.Segments.dualHead
dualHeight def: Legendre tangent height pulled back by the actual gradient. No global Legendre transform or assumed dual regularity is needed for these identities. · OAI.AffineBernstein.dualHeight
dualIsometry def: Functorial conjugate Hilbert-space embedding. · OAI.NuclearUltrapower.dualIsometry
duality def: The Frobenius duality over the invariant ring is integral and perfect. · OAI.KLInvariance.ReflectionFrobenius.duality
dualLabelledMap def: The combinatorial dual in the dart convention. Choosing the inverse face orientation is unnecessary: this rotation gives the same planar oriented dual after reversing edge darts. · OAI.FKCRT.dualLabelledMap
dualMap def: The evaluation pairing of a symmetric power and the symmetric power of its dual. · OAI.Problem346.PairingConstruction.dualMap
dualOrientationEquiv def: Dualization is a bijection on finite-dimensional isomorphisms. This connects uniform primal orientations to uniform character-space orientations. · OAI.MaxCutGames.Gadget.Orientation.dualOrientationEquiv
dualOrientationEquiv def: Dualization is a bijection on finite-dimensional isomorphisms. This connects uniform primal orientations to uniform character-space orientations. · OAI.UniqueGamesTheorem.Gadget.Orientation.dualOrientationEquiv
dualPullbackRestrictIso def: Dual pullback restricted to an open of the target. · OAI.CoherentDual.dualPullbackRestrictIso
dualSchemeRestrictionIso def: In particular the genuine coherent dual restricts to the genuine dual of the restricted sheaf; no formal identification of section rings is used. · OAI.CoherentDual.dualSchemeRestrictionIso
dualToSupport def: Precomposition with a surjective stalk projection gives the integral single-support module. No field extension was used anywhere in this map. · OAI.KLInvariance.IntegralSupport.dualToSupport
dualUnitary def: The conjugate (contragredient) unitary on the strong dual. · OAI.NuclearUltrapower.dualUnitary
Due structure: Guarantees for one additive ray. · OAI.ExactDerandomization.Est.Line.Due
due def: index budget K=0 requests the all-bit bound · OAI.FourierLLogL.Dyadic.Procedure.Wire.due
Dummy def: The actual dummy positions on either raw axis. · OAI.Problem348.HostAnchorRigidity.Dummy
dummy abbrev: The precise number of always-accepting loop darts to add at each vertex. · OAI.MaxCutGames.Foundations.PCP.CloudPadding.dummy
dummy def: A sampled dummy position. · OAI.Problem348.HostSampledPath.dummy
dummy abbrev: The precise number of always-accepting loop darts to add at each vertex. · OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.dummy
dummyMachine def: The same fixed instructions, entered at the dummy-vertex port loop. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMachine
dummyMachine def: The same fixed instructions, entered at the dummy-vertex port loop. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyMachine
dummyRows def: For one vertex of an n-vertex degree-d graph, every dummy dart is its own reverse. The caller's initial index is the actual unary value d * v. · OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.dummyRows
dummyRows def: For one vertex of an n-vertex degree-d graph, every dummy dart is its own reverse. The caller's initial index is the actual unary value d * v. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.dummyRows
DunfordPettis1940Theorem321 def: Only the two kinetic measure spaces needed in the limit construction. · OAI.BoltzmannNonuniqueness.Published.DunfordPettis1940Theorem321
duplicate def: Duplicate the input word and quote the first copy to represent a pair. · OAI.ExactQuantumFactoring.BitStackProgram.Procedure.duplicate
duplicateReverse def: Two simultaneous reversed copies of a word, consuming the operand. · OAI.RationalHitting.StackLanguage.duplicateReverse
duration def: Unit-interval pulses have genuine open round gaps at both endpoints. · OAI.HarmonicCounterexample.FiniteControl.SmoothWord.duration
During structure: Parameters on which a loop body must be uniform. · OAI.PowerSaving.RAM.During
Dyad abbrev: An unreduced dyadic numerator difference and a power-of-two denominator. Computation never relies on Mathlib's noncomputable coding of ℚ. · OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad
Dyadic abbrev: The dyadic coefficient ring is exactly Z[1/2]. · OAI.NuclearUltrapower.Dyadic
dyadicBochnerEnvelope def: The actual positive mass envelope used in the cumulative comparison. · OAI.RegularPointCoordinates.dyadicBochnerEnvelope
dyadicBochnerMass def: The full positive Bochner measure on a fixed-root dyadic ball, with the dimensional scaling used by the heat decrement. · OAI.RegularPointCoordinates.dyadicBochnerMass
DyadicDistanceReplacements structure: These are actual solutions for the sources in S, not replacement existence or error estimates supplied as additional assumptions. · OAI.RegularPointCoordinates.DyadicDistanceReplacements
DyadicDistanceSources structure: Each source is the genuine positive Laplacian defect on four times its testing radius. The same scalar source value is used at all centers. · OAI.RegularPointCoordinates.DyadicDistanceSources
dyadicError def: The index starts at denominator four, so every encoded error is below one half. · OAI.MaxCutGames.Integration.DyadicErrors.dyadicError
dyadicError def: The index starts at denominator four, so every encoded error is below one half. · OAI.UniqueGamesTheorem.Integration.DyadicErrors.dyadicError
dyadicFalseIndex def: Follow the false child at every level of the actual coherent dyadic system. · OAI.Generator.Tracial.dyadicFalseIndex
DyadicGapPartition structure: A nonempty ordered partition of an actual interval by basic dyadic cells. · OAI.ThompsonNonamenability.DyadicGapPartition
dyadicGridKey def: Periodic cells used for a dyadic window with last index b. · OAI.Problem310.dyadicGridKey
dyadicHeatEnvelopeConstant def: A single constant for the shell convolution, exterior finite mass and scalar regularizer, independent of the dyadic index and vector. · OAI.RegularPointCoordinates.dyadicHeatEnvelopeConstant
dyadicHeatGram def: All dyadic heat metrics are the actual regularized heat Grams of one fixed coordinate span, cutoff and pole. · OAI.RegularPointCoordinates.dyadicHeatGram
dyadicHeatGramAt def: The cutoff remains fixed while the heat pole varies. · OAI.RegularPointCoordinates.dyadicHeatGramAt
DyadicIndex def: At depth n there are 2^n indices; a successor appends a binary branch. · OAI.Generator.Tracial.DyadicIndex
dyadicKey def: A finite-table address for the periodic dyadic grid. · OAI.Problem310.GridSeparation.dyadicKey
dyadicPositions def: Positions of the zero bits, numbered from the least significant end. · OAI.GammaFPP.dyadicPositions
dyadicRadialFit def: The bound only supplies local L2 membership. The numerical value is the actual least-squares residual for the canonical distance derivative. · OAI.RegularPointCoordinates.dyadicRadialFit
dyadicShell def: Disjoint dyadic balls, including the initial ball at index zero. · OAI.RegularPointCoordinates.dyadicShell
dyadicSpinProjection def: Ordered finite product, starting at the corner unit. · OAI.WeakPureInfiniteness.dyadicSpinProjection
dyadicSurvival def: The bits in x are the zero bits of the manuscript's uniform expansion. This is exactly 1-U^(t); zero is the cell whose rounded cost is infinity. · OAI.GammaFPP.BK.dyadicSurvival
dyadicWordAcceptRealizer def: The power of two is built from a prefix of the supplied word. Thus no binary integer supplied as a gap can cause an unbounded expansion. · OAI.ContingencyTables.DensePrograms.dyadicWordAcceptRealizer
dynkinFlowMap def: Right multiplication along the exponential line with velocity v, recorded jointly in its base point and time. · OAI.PolycyclicRecognition.dynkinFlowMap
dynkinProduct def: The binary multiplication polynomial, with fixed coefficients. · OAI.PolycyclicRecognition.dynkinProduct
dynkinRightTranslation def: The finite group laws give a homeomorphism, with inverse translation parameter -q. This identifies the inverse used by sampling densities. · OAI.PolycyclicRecognition.dynkinRightTranslation
dz def: Wirtinger derivative, defined from the real Frechet derivative. · OAI.Mahler.dz
D₀ def: D_0, computed by the same falling-factorial formula. · OAI.PixtonChow.ColorBudget.D₀
D₀ abbrev: The terminal binary cutoff exponent. · OAI.Problem337.RawDensityParameters.D₀