Glossary: H

Definitions in this project whose names start with H. 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

H def: Shannon entropy of an observable on the finite law P. · OAI.FourierLLogL.Law.H
H def: H preserves this actual finite-dimensional family. · OAI.LittleFinitistic.FiniteSelectionFamily.H
H abbrev: Continuous functions are put into the actual spherical L² space. · OAI.PettyProjection.Spherical.H
H def: The scalar test function in the manuscript. · OAI.PositiveEinsteinFour.MomentObstruction.H
h def: The manuscript h, with zero components away from degree minus one. · OAI.ExternalTensor.Section4.h
h def: The source hypersurface relation, extended by the independent variable w. · OAI.StableCoordinate.Linearization.h
H1 def: H¹(D), with its weak gradient. · OAI.Bernoulli.H1
H10 def: H¹₀(D) is H¹-closure of C∞ compactly supported functions. Both L² errors tend to zero. This does not restrict competitors to smooth ones. · OAI.Bernoulli.H10
H10 structure: The real continuous representative of H¹₀ on a bounded interval. · OAI.SharpLiebThirring.H10
h1Equiv def: The Hilbert version is exactly the H¹ jet closure, not an extra regularity hypothesis or a replacement by a smaller test space. · OAI.Elasticity.h1Equiv
h1GraphError def: Squared error in the actual value-and-gradient graph. · OAI.ContinuumCoulomb.h1GraphError
H1Loc def: Ballwise H¹_loc, on an open set (balls have compact closure inside D). · OAI.Bernoulli.H1Loc
HaagerupBound def: The norm bound on the bilinear map viewed on the Haagerup product, in its concrete finite row-column formulation. · OAI.KadisonKastler.HaagerupBound
HaagerupCyclicVectorRealization def: The standard-form vector-realization property of a cyclic representation. It is the consequence of Haagerup (1975), Lemma 2.10(1), pp. 278–279, applied to the commutant on the cyclic subspace of a separating vector. · OAI.KadisonSimilarity.HaagerupCyclicVectorRealization
HaagerupForCyclicInput def: The applicability of the published standard-form theorem to a cyclic representation (Haagerup 1975, Lemma 2.10(1)). · OAI.KadisonSimilarity.HaagerupForCyclicInput
haarArc def: The centered closed arc of angular radius a. · OAI.KadisonKastler.haarArc
haarArcCutoff def: The same cutoffs in the complex continuous functional calculus. · OAI.KadisonKastler.haarArcCutoff
haarArcCutoffReal def: Continuous real cutoffs, equal to one on the arc. · OAI.KadisonKastler.haarArcCutoffReal
haarArcIndicator def: The real indicator of the centered arc. · OAI.KadisonKastler.haarArcIndicator
HaarArcProjection structure: The actual projection obtained from the continuous arc cutoffs. · OAI.KadisonKastler.HaarArcProjection
haarArcRadius def: A positive sequence of radii tending to zero. · OAI.KadisonKastler.haarArcRadius
haarCircleIntegral def: Integration of continuous functions against probability Haar measure. · OAI.KadisonKastler.haarCircleIntegral
haarCirclePolynomial def: The actual normalized Fourier polynomial on the quotient circle. · OAI.KadisonKastler.haarCirclePolynomial
HaarConcentrationInput def: Haar concentration for arbitrary Frobenius-Lipschitz observables on SO(N). The constants are uniform in dimension, observable, and Lipschitz constant. · OAI.InvariantIsing.HaarConcentrationInput
haarCornerCoefficient def: The coefficient a⁻¹ᐟ², embedded in the complex scalars. · OAI.KadisonSimilarity.haarCornerCoefficient
haarCornerLetter def: Positive Haar powers, normalized in the ambient tracial Hilbert norm. · OAI.KadisonSimilarity.haarCornerLetter
HaarCornerMoments def: Haar moments for the corner trace τ(·)/a; the zero moment is supplied by τ q = a in the following lemmas. · OAI.KadisonSimilarity.HaarCornerMoments
haarCornerPower def: Integer powers are taken in the unital corner, whose identity is q. · OAI.KadisonSimilarity.haarCornerPower
haarCosineCoefficient def: This real scalar equals 1 / sqrt 2. The equivalent form is convenient for proving normalization without dividing by a square root. · OAI.KadisonSimilarity.haarCosineCoefficient
haarCosineVector def: The (n+1)-st normalized cosine of the algebraic Haar unitary. · OAI.KadisonSimilarity.haarCosineVector
HaarEndpointIndependence def: Popa's precise mixed word, with the initial and final letters optional. The r + 1 nonzero Haar powers are interleaved with the r letters in l. · OAI.KadisonKastler.HaarEndpointIndependence
HaarEndpoints def: Full endpoint formula; the internal factors alone must be centered. · OAI.Generator.Tracial.HaarEndpoints
haarFiberSlice def: The group measure cut out by a measurable subset of the compact section. · OAI.PolycyclicRecognition.haarFiberSlice
haarGeometricSum def: The sum of the first N positive powers on the circle. · OAI.KadisonKastler.haarGeometricSum
HaarLaurentApproximable def: Approximation in the tracial two-norm by finite Laurent polynomials. · OAI.KadisonKastler.HaarLaurentApproximable
haarLaurentSpan def: Finite Laurent polynomials in a unitary. · OAI.KadisonKastler.haarLaurentSpan
haarLaurentTraceClosure def: The tracial closure of Laurent polynomials, restricted to bounded elements of the ambient C*-algebra, is an actual star subalgebra. · OAI.KadisonKastler.haarLaurentTraceClosure
haarMatrixCoordinate def: Coordinate evaluation in the Frobenius matrix space. · OAI.InvariantIsing.haarMatrixCoordinate
haarPolynomial def: The normalized polynomial used in the Haar tail estimate. · OAI.KadisonKastler.haarPolynomial
haarPolynomialLaplacian def: Ordered coordinate planes; its carré du champ is the sum of the ordered squares. · OAI.InvariantIsing.haarPolynomialLaplacian
haarRepeatedWordInclusion def: Unit vacuum endpoint and unit centered Haar letters give isometric columns at every word degree. · OAI.KadisonSimilarity.TracialCornerGeometry.haarRepeatedWordInclusion
haarSectionMeasure def: Average the coupling over a fixed finite Haar region to define its section measure. · OAI.PolycyclicRecognition.haarSectionMeasure
haarTailEnergy def: The normalized angular integral outside the symmetric arc of radius a. · OAI.KadisonKastler.haarTailEnergy
haarTwirl def: The Haar average is an actual bounded operator, with its weak integral constructed through Hilbert-space duality. · OAI.KadisonSimilarity.haarTwirl
hadamardPrefix def: Hadamards on increasing physical wires; no multi-qubit gate abbreviation. · OAI.ExactQuantumFactoring.hadamardPrefix
half def: Prefix-localize an entire diagram, including its bijection and labels. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.half
halfComplementEquiv def: Complementation permutes the subsets having exactly half the ambient size. · OAI.LowSpaceSubsetSum.halfComplementEquiv
halfCornerGeometry def: This is the ordinary normalized corner geometry before restriction to the algebra generated by its two free factors. · OAI.KadisonSimilarity.TracialCornerGeometry.halfCornerGeometry
halfFilledPartition def: An exact partition of the full fixed-particle basis, including all spin spectators in the charge-defect complement. · OAI.ContinuumCoulomb.HubbardGlobal.halfFilledPartition
halfOrderResidue def: The actual representative used by bounded modular gcd arithmetic. · OAI.ExactQuantumFactoring.halfOrderResidue
halfPower def: The repeated-squaring exponent is wired most-significant bit first. · OAI.ExactQuantumFactoring.BitArithmetic.halfPower
halfPowerBits def: The exponent word may be the entire completion-guess width. In particular an arbitrary rare-branch guess is NOT silently truncated to n bits. · OAI.ExactQuantumFactoring.BitArithmetic.halfPowerBits
halfspaceBody def: A finite intersection of closed halfspaces. · OAI.ProjectionCounterexample.halfspaceBody
halfSpectralProjection def: The actual half-threshold spectral projection. · OAI.KadisonSimilarity.halfSpectralProjection
halfSpectralProjectionElement def: The spectral projection as an element of the von Neumann algebra. · OAI.KadisonSimilarity.halfSpectralProjectionElement
halfStep def: Traversing one black turn and then the following white turn of a face. · OAI.KaplanskyCounterexample.Planar.Balanced.halfStep
halfTable def: small table-coordinate space J. · OAI.HadwigerCounterexample.halfTable
halfTableKeyAssignment def: Independent actual half-tables extend to the explicit padded key space. Only the canonically selected right anchor is read at each clause context. · OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.halfTableKeyAssignment
halfTableKeyAssignment def: Independent actual half-tables extend to the explicit padded key space. Only the canonically selected right anchor is read at each clause context. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.halfTableKeyAssignment
HalfTraceProjectionData structure: Minimal half-projection data, before constructing the reflection. The existence of this data is supplied by projection completion in the intended finite factor; the next constructor derives it from an actual complement. · OAI.KadisonSimilarity.HalfTraceProjectionData
halfTraceProjectionDataOfOrthogonal def: Completing a small corner by an orthogonal complement of the missing trace produces a half-trace projection containing the original corner. · OAI.KadisonSimilarity.halfTraceProjectionDataOfOrthogonal
halfTripleDifferenceAt def: The actual half squared three-copy contraction difference. Unlike covariance energy this retains the positive conditional-mean contribution. · OAI.DilutedSpinGlass.KernelTower.halfTripleDifferenceAt
halos def: choose dyadic root canonical always · OAI.PowerSaving.RAM.Bench.halos
halt def: `Instruction.halt k q` sets the next state to `none` and leaves every stack unchanged. · OAI.CurrentKS.Instruction.halt
Halted def: The halt test includes the implicit blank at the first unrepresented cell. · OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Halted
HaltsBy 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.HaltsBy
haltSector def: The first readout-rewind configuration, before any tape cell is moved. · OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.haltSector
haltTapes def: The tape component of the actual halted configuration: only output remains. · OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.haltTapes
haltTapes def: The tape component of the actual halted configuration: only output remains. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.haltTapes
halvePairs def: Literal paired coefficients on the quotient of a cyclic group of even order. Integer divisibility is proved separately before this is used. · OAI.CirculantHadamard.halvePairs
HamiltonianPath structure: An explicit smooth lift of a Hamiltonian isotopy, with inverse and generator. The Hamiltonian equation uses i_X omega = dH. · OAI.ArnoldCounterexample.HamiltonianPath
handles def: A handle is precisely an edge whose endpoints are already in one component but which merges two distinct face cycles when glued. · OAI.TorsionFreeZeroDivisors.ComponentEuler.handles
hardyCompressionAlgHom def: The compression used for Hardy evaluation. The first identity preserves the positive-frequency space on the kernel vectors, and the second expresses invariance of the evaluation kernel inside that space. · OAI.KadisonKastler.hardyCompressionAlgHom
hardyEvaluationAt def: Point evaluation constructed from the invariant Cauchy-kernel quotient. · OAI.KadisonKastler.hardyEvaluationAt
hardyKernelInclusion def: The isometric copy of the coefficient Hilbert space carried by a unit kernel. · OAI.KadisonKastler.hardyKernelInclusion
harmonic def: The finite harmonic potential, by its exact rational recurrence. · OAI.MaxCutGames.Gadget.Harmonic.harmonic
harmonic def: The finite harmonic potential, by its exact rational recurrence. · OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic
harmonicAffineResidualNorm def: The averaged affine residual, with its radius dependence exposed. · OAI.RegularPointCoordinates.harmonicAffineResidualNorm
harmonicAngularLie def: Exactly the trace-free squared angular-field Lie algebra on genuine harmonic polynomials. No irreducibility or controllability assumption is used. · OAI.HarmonicCounterexample.Control.harmonicAngularLie
harmonicBochnerSource def: The exact local measure Laplacian of the harmonic energy density. · OAI.RegularPointCoordinates.harmonicBochnerSource
HarmonicCompactnessSequence structure: The local bounds and measured approximations appearing in the published harmonic-compactness input, bundled for subsequence restriction. · OAI.RegularPointCoordinates.HarmonicCompactnessSequence
harmonicField def: The genuine harmonic restriction of an orthogonal angular field. · OAI.HarmonicCounterexample.ComplexAngular.harmonicField
HarmonicGrowth def: Membership in the actual space H_k, with the bound required at every point. · OAI.HarmonicCounterexample.HarmonicGrowth
harmonicHeatError def: The operator cutoff error is built from the actual scalar product-rule sources. It is not an additional analytic input. · OAI.RegularPointCoordinates.harmonicHeatError
harmonicKernelEquiv def: The kernel uses the actual polynomial Laplacian, not an abstract dimension count. · OAI.HarmonicCounterexample.Angular.harmonicKernelEquiv
harmonicRealAngularLie def: The genuine REAL generated algebra on the real-Cartesian form of the complex harmonic space; only real control times and linear combinations occur. · OAI.HarmonicCounterexample.Control.harmonicRealAngularLie
harmonicRepresentative def: A chosen true polynomial representative of a harmonic L² vector. · OAI.PettyProjection.Spherical.harmonicRepresentative
harmonicSL abbrev: The actual complex harmonic degree l+2, coordinatized only after its Laplacian kernel and dimension have been proved. · OAI.HarmonicCounterexample.Control.harmonicSL
harmonicSpace def: The actual degree-l complex harmonic polynomial space in independent complex coordinates. It is not postulated as an irreducible representation. · OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace
harmonicSpace def: The genuine homogeneous harmonic subspaces of spherical L². · OAI.PettyProjection.Spherical.harmonicSpace
harmonicTargetNorm def: The averaged norm, with its radius dependence exposed for rescaling. · OAI.RegularPointCoordinates.harmonicTargetNorm
harmonicTupleGenerator def: Shared weighted angular generators as ACTUAL endomorphisms, not just coordinate matrices. Positive source weights are allowed in particular. · OAI.HarmonicCounterexample.Control.harmonicTupleGenerator
Has abbrev: "Ready", i.e. can be computed in constant work, not free. · OAI.PowerSaving.RAM.Has
HasActionEnvelope def: Action-envelope hypotheses. · OAI.FiniteAlgebraicEnvelopes.HasActionEnvelope
HasAnalyticOrderAtLeast def: Genuine convergent analytic Taylor vanishing of order at least m. · OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast
HasAngularSpectralSystem def: The four real equations with angular eigenvalue η = ℓ(ℓ+10). · OAI.DefocusingNLS.HasAngularSpectralSystem
HasApproximateMidpoints def: The length-space consequence needed for properness and minimizing segments. · OAI.PolycyclicRecognition.HasApproximateMidpoints
HasBalancedSeparators def: Balanced vertex separators of size at most the square-root bound. · OAI.HyperbolicObstruction.PlanarRecursion.HasBalancedSeparators
HasBorelProductPartition def: The finite partition used by the graph regularization, with its actual cardinality. · OAI.Falconer.HasBorelProductPartition
HasBoundary def: All four literal cuts, with the prescribed boundary spin at each wire. · OAI.CriticalHoneycomb.Transfer.RasterGrid.HasBoundary
HasBoundedAmplitude def: Essential boundedness of the L² datum; only a finite amplitude is used. · OAI.RegularPointCoordinates.HasBoundedAmplitude
HasBoundedResolventAt def: Standard bounded-resolvent condition for a partially defined operator: R is a bounded everywhere-defined inverse of A-e on its full domain. The graph equivalence includes both inverse identities and domain membership. · OAI.SharpLiebThirring.OperatorProof.HasBoundedResolventAt
HasC1CurveChart def: A regular C¹ parametrization of the curve near a point, with a continuous inverse. · OAI.GammaFPP.HasC1CurveChart
HasCapacities def: Per-level cardinality capacities, starting with index zero at the root. · OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.HasCapacities
HasCentralFaithfulNormalState def: A normal state detecting all nonzero central subprojections of p. · OAI.BoundedHochschild.KadisonRingrose.HasCentralFaithfulNormalState
HasClassifyingSpace def: Ordinary classifying CW spaces, with no bound on the cardinality of their cells. · OAI.EilenbergGanea.HasClassifyingSpace
HasClassifyingSpace def: Ordinary K(G,1) of dimension at most n. The cell and space types have no finiteness or countability restriction. The contractible surjective covering is the usual universal-cover characterization of a classifying space. · OAI.EilenbergGanea.HasClassifyingSpace
HasConditionalJoins def: A conditional join exists exactly for pairs possessing a common upper bound. In the divisibility order this says that the intersection of two principal right cones, when nonempty, is a principal right cone. · OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins
HasConeJoins def: Conditional joins expressed as exact intersections of right cones. · OAI.PartitionConsistency.MergerAlgebra.RightFreeAction.HasConeJoins
HasConfigurationBounds def: This hypothesis runs over a countable list of compact configuration spaces. · OAI.CircleDomainRigidity.HasConfigurationBounds
HasConfigurationBounds def: This hypothesis runs over a countable list of compact configuration spaces. · OAI.CircleDomainRigidity.MarkedHit.HasConfigurationBounds
HasCycle def: An injectively labelled cycle, including its closing edge. · OAI.CycleClique.Construction.HasCycle
HasCyclicRayRealizations def: Even ray realizations of each cyclic subgroup's Frobenius characters. · OAI.DukePrimeDegree.HasCyclicRayRealizations
HasDecidableWordProblem def: Algorithmic decidability, not merely classical DecidablePred. · OAI.FiniteAlgebraicEnvelopes.HasDecidableWordProblem
HasDefectAtMost def: The block has a defect group whose order is at most M. · OAI.Donovan.HasDefectAtMost
HasDefectIsomorphic def: The block has a defect group isomorphic to the given group P. · OAI.Donovan.HasDefectIsomorphic
HasDegenerateFixedPoint def: Eigenvalue 1 in the derivative on the quotient tangent, not an ambient spurious vertical eigenvector. v is nonzero and horizontal. · OAI.ArnoldCounterexample.HasDegenerateFixedPoint
HasDiscreteLinearLowerBound def: A finite constant bounds inverse small-ball mass along integer scales. · OAI.DukePrimeDegree.HasDiscreteLinearLowerBound
HasDistortion def: The standing all-pairs distortion hypothesis, with its positive arbitrary scale. · OAI.DiamondDistortion.Diamond.HasDistortion
HasExactlyThreeAtoms def: The formalization proves one-third Hölder stability of Brenier maps from the uniform measure on a compact convex body with nonempty interior in $\mathbb R^d$, for every $d\ge2$. For targets supported in one fixed nonempty compact set, the … · OAI.Problem358.HasExactlyThreeAtoms
HasFactorization def: Real PSD factors of order r, without equivariance or rank-one restrictions. · OAI.PerfectMatchingPSD.HasFactorization
HasFiniteContourGenerator def: The exact invariant projection, decaying kernel, and finite generator data. · OAI.DefocusingNLS.HasFiniteContourGenerator
HasFiniteFolnerSets def: Finite Følner witnesses, in the symmetric-difference convention used by the actual finite-average translation estimate. · OAI.PolycyclicRecognition.HasFiniteFolnerSets
HasFiniteIntegralCohomologicalDimension def: Finite integral cohomological dimension is finite projective dimension of the trivial integral representation. · OAI.PolycyclicRecognition.HasFiniteIntegralCohomologicalDimension
HasFiniteLargeContinuumBound def: A uniform finite bound on the number of pairwise disjoint subcontinua having any fixed positive minimum diameter. · OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound
HasFiniteMergers def: Precisely the finite-overlap realization property in thm:monoid, item 2. Existence of a monoid having this property is still a separate obligation. · OAI.PartitionConsistency.DiagramForcing.HasFiniteMergers
HasFinitePresentation def: A finite presentation in the category of associative unital R-algebras. The finite generating set is not required to commute. A ring congruence is closed under multiplication on either side; these are two-sided equations. · OAI.LittleFinitistic.GroupAlgebraPresentation.HasFinitePresentation
HasFiniteProjectiveResolution def: A finite projective resolution, with all terms finite over the group ring. · OAI.PolycyclicRecognition.HasFiniteProjectiveResolution
HasFiniteQuadraticPresentation def: A finite noncommutative presentation whose zero relations have degree ≤ 2. · OAI.LittleFinitistic.QuadraticPresentation.HasFiniteQuadraticPresentation
HasFiniteRowBound def: A finite-row bound, expressed in the C*-algebra without an auxiliary operator-space structure. · OAI.BoundedHochschild.KadisonRingrose.HasFiniteRowBound
HasFiniteTwoDimensionalClassifyingSpace def: A connected finite Hausdorff 2-dimensional CW K(G,1). · OAI.TorsionFreeZeroDivisors.HasFiniteTwoDimensionalClassifyingSpace
HasGapReduction def: Polynomial-time gap reduction for the specific objective above. · OAI.UniformSparsestCut.HasGapReduction
HasGaussianHeatBounds def: The pair of Gaussian bounds, with the measure at the kernel's second argument and the exact 4 ± ε denominators. · OAI.RegularPointCoordinates.HasGaussianHeatBounds
HasGaussianHeatDifferenceBounds def: The localized Gaussian gradient estimate, integrated along a short path, in the only finite-difference form used by the application. · OAI.RegularPointCoordinates.HasGaussianHeatDifferenceBounds
HasGenerator def: The generator domain encoded by the exact orbit integral identity. This formulation makes weak closedness an immediate linear-test fact. · OAI.TriangularBilliards.Analysis.HilbertFlow.HasGenerator
HasGlobalPlateau def: The source global plateau identity is required pointwise for bits, not just in distribution and not after conditioning on successful layout. · OAI.TraceReconstruction.HasGlobalPlateau
HasGradient def: Directional, coordinate-free distributional gradient. · OAI.SignedDisk.WeakSobolev.HasGradient
HasGradient def: Directional, coordinate-free distributional gradient. · OAI.WeakSobolev.HasGradient
HasGraphWitness def: The graph size is unbounded, but each individual witness is finite and nonempty. · OAI.FiniteCongruence.HasGraphWitness
HasHamiltonianCycle def: A single spanning cycle, not a possibly disconnected spanning 2-factor. · OAI.Barnette.HasHamiltonianCycle
HasHitNormBound def: The finite nonnegative dual tests for the square norm of the hit vector. · OAI.CircleDomainRigidity.HasHitNormBound
HasHitNormBound def: The square norm is tested only on the marked compact space. · OAI.CircleDomainRigidity.MarkedHit.HasHitNormBound
HasIndependent def: An independent set of exactly n vertices. · OAI.CycleClique.Construction.HasIndependent
HasInternalIsometryRows def: Existence of finite families of orthogonal isometries. For a properly infinite algebra this is supplied by its projection classification. · OAI.KadisonSimilarity.HasInternalIsometryRows
HasInverseMajorantRecurrence def: The positive-order recurrence after removing the exponential jet base. · OAI.RegularPointCoordinates.HasInverseMajorantRecurrence
HasKazhdanGap def: Exact standing Kazhdan-gap convention in the tensor-norm formulation. · OAI.NuclearUltrapower.HasKazhdanGap
HasKernelRing def: A construction interface; every field is discharged below from the source algebra. · OAI.FiniteAlgebraicEnvelopes.HasKernelRing
HasL1Embedding def: A map to genuine finite-dimensional real ℓ₁, not just a cut pseudometric. · OAI.BoundedTreewidthL1.HasL1Embedding
HasLowerSectionModulus def: Prescribed lower modulus of tangent sections; this is the same section condition as rigidity.tex, with the frozen tangentSection definition. · OAI.AffineBernstein.HasLowerSectionModulus
HasMargins def: The row and column equations in both papers. · OAI.ContingencyTables.HasMargins
HasMarkedDivisorDensity def: Divisors at every multiplicative scale, in the form used by grouping. · OAI.Problem337.HasMarkedDivisorDensity
HasMatrixVelocity def: Entrywise velocity at the identity; the parameter approaches zero through positive real values, exactly as in the rescaling argument. · OAI.DukePrimeDegree.HasMatrixVelocity
HasModelWith def: A smooth positive-volume model with a specified Euclidean or half-space manifold model. All model dimensions will be quantified below. · OAI.SmoothObstruction.HasModelWith
HasNoFiniteDimensionalSubrep def: The absence of nonzero finite-dimensional subrepresentations, without separability. · OAI.NuclearUltrapower.HasNoFiniteDimensionalSubrep
HasNoMinimalProjection def: No nonzero projection is minimal, excluding matrix factors. · OAI.FiniteFactor.HasNoMinimalProjection
HasNonexpansiveFixedPointProperty def: Every nonexpansive selfmap of every nonempty closed bounded convex set has a fixed point, in the norm already carried by X. · OAI.ReflexiveFixedPoints.HasNonexpansiveFixedPointProperty
HasNoNontrivialTorsion def: Group-theoretic torsion freeness. This only excludes nonidentity finite-order elements; it does not impose the unique-root property on a noncommutative group. · OAI.PolycyclicRecognition.HasNoNontrivialTorsion
HasNormalGNS def: Normality of the native representation of the chosen positive trace. · OAI.KadisonSimilarity.HasNormalGNS
HasNormalizedAffineImprovement def: The normalized harmonic estimate in the original affine coordinate span. · OAI.RegularPointCoordinates.HasNormalizedAffineImprovement
HasOldGates def: Only elements with an old right multiple need a gate. For mergers all such elements are already old, so the second alternative is unused. · OAI.PartitionConsistency.DiagramOrder.HasOldGates
HasOldSplit def: The output records the exact source prefix criterion together with all U intersection images, rather than only relative-position dimensions. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.HasOldSplit
HasOperatorValues def: Pointwise algebra membership of the canonical representative. · OAI.KadisonKastler.HasOperatorValues
HasOrdinaryNoise def: Complete finite ordinary-noise sampler; its law is the displayed product of a fresh uniform xi, a finite location law, and independent uniform amplitudes. · OAI.BoundedTreewidthL1.LaunchNoise.HasOrdinaryNoise
HasPartition def: The brick occurs as one member of an actual finite partition. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.HasPartition
HasPointAt def: Every individual mask jet in the expansion is evaluated at the same point. · OAI.Falconer.MaskJetExpansion.HasPointAt
HasPolynomialBound def: An explicit polynomial upper bound on the positive half-line. · OAI.ClosedSurfaceR4.RealModes.HasPolynomialBound
HasPolynomialFormula def: The external parameter changes coefficients, but not the degree bound. · OAI.PolycyclicRecognition.HasPolynomialFormula
HasPolynomialImplementation def: A deterministic finite-stack-machine implementation, with a polynomial bound on bit-level running time in the explicitly encoded input length. · OAI.Superstring.HasPolynomialImplementation
HasPolynomialSlowFamily def: Uniform profiles for the nearby smooth maps at one finite stage. · OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.HasPolynomialSlowFamily
HasPortTails def: The flat graph's stored tails agree with its fixed regular-port ordering. · OAI.MaxCutGames.Foundations.PCP.PortTables.HasPortTails
HasPortTails def: The flat graph's stored tails agree with its fixed regular-port ordering. · OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.HasPortTails
HasQuantitativeMarkedPrefix def: The precise portion of the marked greedy-prefix output used by the final construction. The marker is not included in p; it is inserted afterwards. · OAI.Problem337.HasQuantitativeMarkedPrefix
HasRadialEnergyDecay def: The first two outgoing symbol estimates needed when Re λ ≥ 4. · OAI.DefocusingNLS.HasRadialEnergyDecay
HasRadialOutgoingExpansion def: A finite but sufficiently accurate outgoing expansion, including the velocity. · OAI.DefocusingNLS.HasRadialOutgoingExpansion
HasRadialSpectralSystem def: The four real equations for a radial complexified spectral mode. · OAI.DefocusingNLS.HasRadialSpectralSystem
HasRationalDivisorSum def: A rational number is a sum of at most B positive rational summands, whose natural numerators divide the fixed common supply K. · OAI.Problem337.HasRationalDivisorSum
HasRationalDivisorSupply def: A supply expresses every small integer as a short sum of rational divisors. · OAI.Problem337.HasRationalDivisorSupply
HasRawFDerivAt def: A coefficientwise derivative records actual HasFDerivAt proofs for all tuples. It adds no differentiability or exterior-calculus assumptions. · OAI.Mahler.HasRawFDerivAt
HasRelativeDefectFilling def: The filling changes the frame only on a compact subset of the prescribed open set; every point of that open set becomes regular. · OAI.ClosedSurfaceR4.FiniteOrderSmoothing.HasRelativeDefectFilling
HasRep def: A coordinate of the quotient letter exists when the letter belongs to that prescribed copy. Each such representative is unique. · OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.HasRep
HasResampledWitnesses def: The marked labels and attachment positions may depend on the numerical sample. · OAI.TwoPointCorrelations.HasResampledWitnesses
HasScalarCenter def: A concrete factor has scalar center. · OAI.FiniteFactor.HasScalarCenter
HasSeparablePredual def: A separable Banach space whose dual is conjugate-linearly isometric to M. · OAI.FiniteFactor.HasSeparablePredual
HasSeparablePredual def: Separable Banach predual, matching the existential predual convention of mathlib's WStarAlgebra. This is not norm separability of S. · OAI.Generator.HasSeparablePredual
HasSeparablePredual def: A same-universe separable Banach predual, with the conjugate-linear dual convention. This imposes no separability on the Hilbert representation or the operator norm topology. · OAI.RelativeGeneration.HasSeparablePredual
HasSeparableQuotient def: A bounded linear surjection onto an infinite-dimensional separable Banach space. · OAI.SeparableQuotient.HasSeparableQuotient
HasShiftLE def: A map's degree shift is bounded above by m. This does not require lower bounds and therefore applies to the source's integer gradings. · OAI.StableCoordinate.LeadingComponent.HasShiftLE
HasShort def: An actual vertex of a layer whose symbol length is at most the allowance. · OAI.Superstring.Hierarchical.Layer.HasShort
hasSign def: Leaf positions have both sign names; other positions have their own sign. · OAI.Problem348.ModeIncidence.hasSign
HasSmoothPositiveVolumeModel def: Closed manifolds of all dimensions (including zero), and smooth manifolds with boundary of every positive finite dimension. Nonorientable manifolds are included: no orientability hypothesis occurs. · OAI.SmoothObstruction.HasSmoothPositiveVolumeModel
HasSobolevFlowNeighborhood def: Existence for nearby data and times, together with joint continuity of the maximal flow. · OAI.DefocusingNLS.HasSobolevFlowNeighborhood
HasSobolevInteractionContinuation def: A right continuation is a classical solution across the endpoint agreeing on a left neighborhood. · OAI.DefocusingNLS.HasSobolevInteractionContinuation
HasSpatialAmplitude def: The given amplitude is fixed as a function of the base point, throughout the whole open jet domain used for nearby immersions. · OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.HasSpatialAmplitude
HasSpread def: Per-level spread conditions, starting with index zero at the root. · OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.HasSpread
HasSubexponentialLowerBound def: A lower bound of the form exp (-o(r)), expressed without a choice of error function. · OAI.PolycyclicRecognition.HasSubexponentialLowerBound
HasSubexponentialUpperBound def: An upper bound of the form exp (o(r)). · OAI.PolycyclicRecognition.HasSubexponentialUpperBound
HasSubmersiveWordSubsequence def: A convergent subsequence and a fixed word with full-rank limiting endpoint map. This packages only the explicit finite-dimensional data. · OAI.PolycyclicRecognition.HasSubmersiveWordSubsequence
HasSupply def: The remaining arithmetic existence interface at a fixed scale. It includes the actual common denominator, normalized residue lists, and terminal residue supply. The localization loss may vary with the scale. · OAI.Problem337.GeometricDensity.HasSupply
HasTimeConstantFor def: The passage-time limit predicate on the product probability space with marginal ν. · OAI.GammaFPP.HasTimeConstantFor
HasTubeDecay def: Uniform exponential tube bounds on each compact set. The constants are finite but may depend on the compact set. · OAI.DukePrimeDegree.HasTubeDecay
HasType def: A global judgment is witnessed in a finite prefix of the tower. · OAI.PureTypeSystem.ContextTower.HasType
HasUnboundedNodalRatio def: The eigensequence belongs to one fixed metric and has finite nodal measure. · OAI.YauCounterexamples.HasUnboundedNodalRatio
HasUniqueIrreducibleRepresentation def: Naimark's problem asks whether a $C^*$-algebra whose nonzero irreducible representations are all unitarily equivalent must be an algebra of compact operators. The formalization gives a counterexample in ZFC: a unital infinite-dimensional … · OAI.NaimarkZFC.HasUniqueIrreducibleRepresentation
HasUnitLifts def: Every target unit admits a unit lift (unitality included in the homomorphism). · OAI.OneWayLiveness.HasUnitLifts
HasVanishingRectangleBarriers def: A sequence of actual rectangle barriers, each crossing almost every horizontal line over (a,b], whose squared horizontal derivative energies tend to zero. The supporting horizontal interval is fixed for the sequence. · OAI.CircleDomainRigidity.HasVanishingRectangleBarriers
HasWeakGradient def: Distributional first derivatives represented by a vector-valued function. · OAI.CenteredDiskEndpoint.HasWeakGradient
HasWeakGradient def: Distributional first derivatives represented by a vector-valued function. · OAI.SignedDisk.CenteredDiskEndpoint.HasWeakGradient
HasWestNorth def: The parametrization has exactly the actual spin assignments with the west/north walls fixed; no geometric configurations are dropped. · OAI.CriticalHoneycomb.Transfer.RasterGrid.HasWestNorth
HasWidth def: All present keys have the specified length. Empty subtrees are allowed. · OAI.LowSpaceSubsetSum.BinaryTrie.HasWidth
HasWitness def: An actual normal witness of a feasible profile, with a declared inhabitant. All the sorting judgments, rather than one selected sort, are retained. · OAI.PureTypeSystem.HasWitness
HasWitnesses def: Tarski–Vaught condition for a subdomain, stated for the formula basis. · OAI.PartitionConsistency.CountableModel.HasWitnesses
hat def: Actual Euclidean-plane product hats at a positive physical scale. · OAI.DyadicHats.hat
hat def: Actual Euclidean-plane product hats at a positive physical scale. · OAI.SignedDisk.DyadicHats.hat
hat def: The consecutive ramp differences form an exact finite partition on a grid. · OAI.SquareRootDegree.SmoothSelector.hat
HatcherDoubleEulerInput def: Hatcher, Chapter 2, Exercise 22, specialized to the actual two-sheeted cover of closed smooth four-manifolds. The finite-CW comparison and Hatcher 3.26(c) identify the Euler characteristic with Topology.eulerFour. · OAI.PositiveEinsteinFour.HatcherDoubleEulerInput
HatcherOrientationCoverInput def: Hatcher, Proposition 3.25 and Theorem 3.26(c), together with smooth metric pullback: either an orientation exists, or its connected two-sheeted cover has the displayed actual geometric data. · OAI.PositiveEinsteinFour.HatcherOrientationCoverInput
HatcherProjectiveBettiInput def: The degree-zero through degree-four consequence of Hatcher 3.19 for a manifold identified with CP², using the ordinary isometry/homeomorphism and singular-homology invariance. No curvature classification is assumed. · OAI.PositiveEinsteinFour.HatcherProjectiveBettiInput
hBox def: hBox assumes real u in the designated range · OAI.GeneralMahler.SCal.hBox
hCoef def: rational/geometric remainder · OAI.GeneralMahler.SCal.hCoef
Hcond def: Conditional entropy H(X|W). · OAI.FourierLLogL.Law.Hcond
hden def: scaled derivatives · OAI.GeneralMahler.SCal.hden
Head inductive: Finite internal-head alphabet, with a single fresh handoff/start state. · OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Head
Head inductive: Distinct phases make every scan's designated reading side unambiguous. · OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Head
Head inductive: The complete head alphabet; internal control excludes raw, quota and cleanup. · OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Head
Head inductive: The validator states I,J,J',N,V and its fresh machine handoff. · OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Head
head def: Evaluate head of a row (L4 sum over columns), a convenient alternative to suprema that still bounds them. · OAI.ExactDerandomization.Est.Axis.head
head? def: Reading a singleton view touches one stored array entry. · OAI.EditApproximation.InputView.head?
headArray def: The array representing an arbitrary completed vector's finite head. · OAI.DiamondDistortion.SegmentSystem.headArray
headBlock def: The actual bounded prefix. · OAI.Problem358.FinitePrefix.headBlock
headed def: A headed sector written literally. Cells left of the head are supplied in nearest-first zipper order. · OAI.FiniteAlgebraicEnvelopes.Compiler.Path.headed
headerCommands def: Headers use only the preserved n and m tapes; all relation registers may still have their initial values. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands
headerCommands def: Headers use only the preserved n and m tapes; all relation registers may still have their initial values. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.headerCommands
headerFrame def: Explicit tape frame used during the header phase; all unlisted work tapes are empty. The archive is separate from the unread input. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerFrame
headerFrame def: Explicit tape frame used during the header phase; all unlisted work tapes are empty. The archive is separate from the unread input. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerFrame
headerInTime def: An actual entry-to-guard trace, valid for any unread row suffix and every finite ambient buffer. No execution premise is supplied by the caller. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerInTime
headerInTime def: A genuine finite TM2 execution certificate for the header phase. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.headerInTime
headerInTime def: Header preparation already has the common trailing-bit register layout. · OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.headerInTime
headerInTime def: No header execution is assumed: the checked template is instantiated at the concrete driver labels and transported through the finite state layout. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.headerInTime
headerInTime def: An actual entry-to-guard trace, valid for any unread row suffix and every finite ambient buffer. No execution premise is supplied by the caller. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerInTime
headerInTime def: A genuine finite TM2 execution certificate for the header phase. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.headerInTime
headerInTime def: Header preparation already has the common trailing-bit register layout. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.headerInTime
headerInTime def: No header execution is assumed: the checked template is instantiated at the concrete driver labels and transported through the finite state layout. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.headerInTime
headerPlacement def: Header writers use the common work tapes but emit on the final output. The relation producer continues to use commonPlacement rowOutput. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement
headerPlacement def: Only the header phase directs shared output role 10 to the external output. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement
headerPlacement def: The existing word placement, with its result directed to row-output 10. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement
headerPlacement def: Header writers use the common work tapes but emit on the final output. The relation producer continues to use commonPlacement rowOutput. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerPlacement
headerPlacement def: Only the header phase directs shared output role 10 to the external output. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.headerPlacement
headerPlacement def: The existing word placement, with its result directed to row-output 10. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement
headerPlan def: Output variable count and output clause count, in the checked CNF codec. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan
headerPlan def: Output variable count and output clause count, in the checked CNF codec. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan
headerProgram def: Each true bit from the first input field contributes one counter bit, one vertex-header bit, and B dart-header bits. No numeric register is used. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.headerProgram
headerProgram def: Each true bit from the first input field contributes one counter bit, one vertex-header bit, and B dart-header bits. No numeric register is used. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.headerProgram
headerResultTapes def: Exact row-guard handoff: the original table is protected in archive, the output header is accumulated in reverse, and the row index is unary zero. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes
headerResultTapes def: Exact row-guard handoff: the original table is protected in archive, the output header is accumulated in reverse, and the row index is unary zero. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes
headersInTime def: The exact header trace packaged in the machine execution-time interface. · OAI.MaxCutGames.Explicit.MachineClone100Headers.headersInTime
headersInTime def: The exact runtime machine starts on the complete ordinary target game codec and reaches the seed phase with its untouched row table and three unary headers. · OAI.MaxCutGames.Explicit.MachineProductHeadersRead.headersInTime
headersInTime def: The input headers are consumed literally; all unread constraint bits retain their original order and no tape contains an implicit runtime number. · OAI.MaxCutGames.Explicit.MachineSubdivisionHeaders.headersInTime
headersInTime def: The input headers are consumed literally; all unread constraint bits retain their original order and no tape contains an implicit runtime number. · OAI.MaxCutGames.Explicit.MachineUniformHeaders.headersInTime
headersInTime def: The exact header trace packaged in the machine execution-time interface. · OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.headersInTime
headersInTime def: The exact runtime machine starts on the complete ordinary target game codec and reaches the seed phase with its untouched row table and three unary headers. · OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.headersInTime
headersInTime def: The input headers are consumed literally; all unread constraint bits retain their original order and no tape contains an implicit runtime number. · OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.headersInTime
headersInTime def: The input headers are consumed literally; all unread constraint bits retain their original order and no tape contains an implicit runtime number. · OAI.UniqueGamesTheorem.Explicit.MachineUniformHeaders.headersInTime
headerStatement def: The native checked header statement is embedded and its inert extra register removed. All four native header tapes keep their identities. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerStatement
headerStatement def: The native checked header statement is embedded and its inert extra register removed. All four native header tapes keep their identities. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerStatement
headerTimePolynomial def: A fixed polynomial in the complete encoded input length. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerTimePolynomial
headerTimePolynomial def: A fixed polynomial in the complete encoded input length. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerTimePolynomial
headIdentity def: An identity vertex is retained even for an empty walk, so the resulting band always has two exposed main ports and loses no branch occurrence. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.headIdentity
headJ def: Completion of restriction to an ancestral head. · OAI.ForestSpace.headJ
Headline def: The exact two-model unconditional headline; neither intrinsic estimate is a hypothesis. · OAI.DiamondDistortion.Headline
headPhaseInTime def: The head-access call is part of this concrete program, with its actual finite labels and framed tape effects. Its data are read from the table. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headPhaseInTime
headPhaseInTime def: The head-access call is part of this concrete program, with its actual finite labels and framed tape effects. Its data are read from the table. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headPhaseInTime
headPrimal def: Finite head projection on the completed primal, defined even for nonancestral sets. · OAI.DiamondDistortion.SegmentSystem.headPrimal
Heads structure: An actual family of allowed finite-rank coordinate heads. Approximation is by a vector fixed by a head; no uniform bound on projection norms is imposed. · OAI.DiamondDistortion.Midpoint.Heads
headsCode def: `headsCode k s` recursively packs the empty/false/true status of each of the `k` stack heads into a natural number. · OAI.CurrentKS.headsCode
headWord def: Copy the next complete word, including its delimiter. Empty input and unterminated words fail explicitly. · OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.headWord
headWord def: Copy the next complete word, including its delimiter. Empty input and unterminated words fail explicitly. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.headWord
Heard def: Artificial terminal configurations get only replies already covered by the W induction. · OAI.ExactDerandomization.Chime.Dome.Heard
heat def: The heat density for one-dimensional standard Brownian motion. · OAI.FKCRT.SimpleWalk.heat
heatAt def: The same positive heat Gram used in the neighborhood construction. · OAI.RegularPointCoordinates.RegularBilinearData.heatAt
heatCappedOverlap def: The overlap of two density rows after clipping at a finite height. · OAI.RegularPointCoordinates.NoncollapsedRCD.heatCappedOverlap
heatConvolution def: The symmetric form of heat convolution, convenient for differentiating the kernel. · OAI.ForcedComputation.PlaneHeat.heatConvolution
heatCutoff def: The cutoff is one on the working interval and supplies a global square-root bound. · OAI.ForcedComputation.PlaneScalarMild.heatCutoff
HeathBrownFiniteDivisor def: The finite-divisor inequality following the exact identity on HB p.14. Since Nr, Nd ≥ 1, its factors (Nr)^(-1/2) and (Nd)^(-1/2) are discarded, and complementary divisors are reindexed. This weaker fixed-level version suffices solely … · OAI.CubicFirstMoment.HeathBrownFiniteDivisor
HeathBrownGaussPartialSums def: HB2000 Lemma 1, angular index zero and epsilon 1/12. · OAI.CubicFirstMoment.HeathBrownGaussPartialSums
HeathBrownZBound def: HB §3 (19), at large height only. The parameter e is retained literally; the application below uses just e = 1/10. · OAI.CubicFirstMoment.HeathBrownZBound
HeathBrownZFactorization def: Equation (14), after division by its absolutely convergent Euler factor. The reciprocal is the literal primary Möbius series above. · OAI.CubicFirstMoment.HeathBrownZFactorization
heatJointDensity def: A jointly measurable version of the actual heat densities. · OAI.RegularPointCoordinates.NoncollapsedRCD.heatJointDensity
heatKernel def: The globally square-root-bounded heat kernel, unchanged on the working interval. · OAI.ForcedComputation.PlaneScalarMild.heatKernel
heatKernelRow def: The actual L2 kernel row. The value at nonpositive times is unused. · OAI.RegularPointCoordinates.heatKernelRow
heatKernelRowLp def: A positive-time kernel row as an actual L² function. · OAI.RegularPointCoordinates.heatKernelRowLp
heatKernelSobolev def: Positive-time kernel rows belong to the actual Cheeger Sobolev space. · OAI.RegularPointCoordinates.heatKernelSobolev
heatL1Density def: The density as an element of the actual L¹ space. · OAI.RegularPointCoordinates.NoncollapsedRCD.heatL1Density
heatMarkovKernel def: The canonical heat family is an actual measurable Markov kernel. · OAI.RegularPointCoordinates.NoncollapsedRCD.heatMarkovKernel
heatMoment def: Average of exp(-c) on the sum-difference of 2T independent letters. · OAI.FourierLLogL.Compress.heatMoment
heatOperator def: The Gaussian heat operator on bounded spatial jets of order k. · OAI.ForcedComputation.PlaneHeat.heatOperator
heatOverlapKernel def: Increasing continuous capped overlaps define an extended-real kernel. Pointwise finiteness is kept separate from this construction. · OAI.RegularPointCoordinates.NoncollapsedRCD.heatOverlapKernel
heatPairMeasure def: The reference measure paired with its Markov transition. · OAI.RegularPointCoordinates.NoncollapsedRCD.heatPairMeasure
heatRadonDensity def: The Radon--Nikodym density of the constructed heat measure. · OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity
heatRadonMeasure def: The canonical Radon heat measure at a fixed positive time and center. · OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure
heatSourcePath def: The artificial positive-time cutoff disappears on the finite integration interval. · OAI.ForcedComputation.PlaneScalarMild.heatSourcePath
heatSourceValue def: Scalar value of the source integral, with the same constant time continuation. · OAI.ForcedComputation.PlaneScalarMild.heatSourceValue
heatSquarePairing def: The pairing whose endpoints give the heat variance. · OAI.RegularPointCoordinates.heatSquarePairing
heavyMass def: The high-atom mass of a finite law at threshold exp(-a log L). · OAI.SmoothObstruction.FiniteEntropy.heavyMass
heavySet def: The points whose weight is strictly above the cutoff. · OAI.TalagrandThreshold.Selector.heavySet
heckeDualTailIntegrand def: The integrand of the omitted part of the functional-equation series on the line Re s = 1/2-m. · OAI.CubicFirstMoment.heckeDualTailIntegrand
heckeExponentialError def: The conductor-dependent error in the published prime number theorem. · OAI.CubicFirstMoment.heckeExponentialError
HeckeFunctionalEquation def: The precisely normalized functional-equation input, supplied for an actual primitive character and its contragredient, away from the gamma poles. The regular-point restriction is necessary because mathlib totalizes Gamma at its poles; the … · OAI.CubicFirstMoment.HeckeFunctionalEquation
heckeSymmetryFactor def: D includes the fixed field factor in the completed L-function. · OAI.CubicFirstMoment.heckeSymmetryFactor
height def: Every standard generator has integral height one. · OAI.EilenbergGanea.height
height def: The logarithmic diagonal is a homomorphism to an additive real vector space. · OAI.PolycyclicRecognition.PositiveTriangular.height
height def: Height on an affine plane, measured along a fixed transverse direction. · OAI.Problem358.TransverseSurface.height
height def: A global height on all dimensions of the pasted-globe basis. · OAI.Thomason.Construction.PastingGlobeBasis.height
height def: The actual finite strong height, on all tensor degrees at once. · OAI.Thomason.Construction.PastingGlobeCylinderBasis.height
height def: Threefold spacing keeps the endpoint offsets inside their original slot. · OAI.Thomason.Construction.RightCylinderBasis.height
height def: The three successive intervals are placed consecutively in the height order. · OAI.Thomason.Construction.TripleGlobeBasis.height
heightCharacter def: Each character descends to the height quotient. · OAI.PolycyclicRecognition.heightCharacter
heightCode def: Actual normalized preorder height path, including both endpoint cells. · OAI.FKCRT.TreeCoding.heightCode
heightConePreimage def: Pull a cone of height functionals back to the actual Cartan weights. · OAI.PolycyclicRecognition.CartanWordModel.heightConePreimage
HeightCost structure: Exact height and cost hypotheses from equation (mono-margin). For the strict comparisons used in that equation, the set of costs is nonempty and bounded; the real conditional supremum is therefore the ordinary one. · OAI.PartitionConsistency.DiagramOrder.HeightCost
heightCost def: Limit-stage extension of the exact real height/cost margin, using unchanged old suprema at every transition of the tower. · OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.heightCost
heightCost def: Extending height and cost data on the actual probe normal forms. · OAI.PartitionConsistency.ProbeAlgebra.Word.heightCost
heightDualAction def: Precomposition of continuous covectors by a height automorphism. · OAI.PolycyclicRecognition.heightDualAction
HeightIntervals structure: Numerical intervals for the first-letter blocks. These inequalities are constructed from the old margin below, rather than supplied for the extension. · OAI.PartitionConsistency.ProbeAlgebra.HeightIntervals
heightIntervals def: Intervals for all the new letters of this actual probe extension. · OAI.PartitionConsistency.ProbeAlgebra.Path.heightIntervals
heightKernel def: The common kernel, including the empty family of characters. · OAI.PolycyclicRecognition.heightKernel
heightKernel def: The common kernel of the diagonal characters. Empty families give ⊤. · OAI.PolycyclicRecognition.heightKernel
heightProjection def: Second continuous coordinate of the actual joint coding. · OAI.FKCRT.TreeCoding.heightProjection
heightProjection def: The quotient map defining infinitesimal height. · OAI.PolycyclicRecognition.heightProjection
HeightQuasiAction structure: Height-coordinate data for a quasi-action. All geometric estimates are recorded explicitly, and no exact action law for F is assumed. · OAI.PolycyclicRecognition.HeightQuasiAction
heightRay def: The Cartan one-parameter ray representing the height t • w. · OAI.PolycyclicRecognition.CartanFactorModel.heightRay
heightSemisimpleAction def: The chosen Cartan section disappears from the eigenvalues: they are the canonical height weights. · OAI.PolycyclicRecognition.heightSemisimpleAction
heightSequence def: Extend the last covariance height constantly. · OAI.InvariantIsing.heightSequence
heightShield def: Literal trapezoidal height branch, constant outside the closed band. · OAI.PlanarL1.Clipping.heightShield
HeightSpace abbrev: The canonical linear height quotient. · OAI.PolycyclicRecognition.HeightSpace
HeightSpace abbrev: The canonical linear height space. · OAI.PolycyclicRecognition.HeightSpace
HeightTree structure: A rooted incidence tree with a nondecreasing metric height. Unlike the shortest-path tree, added terminal branches are permitted to have zero length. Termination follows the incidence tree, not strict metric height. · OAI.PlanarL1.HeightTree
heisenberg def: The spin-1/2 isotropic Heisenberg matrix in the computational basis. · OAI.ContinuumCoulomb.heisenberg
held def: Relative reference with genuine wholesale resets. Resetting discards, rather than spends, the unused scalar variation credit. · OAI.KServer.CoarseSide.held
held def: Reference reset policy run on every input step. · OAI.KServer.RankTracking.held
held def: A single relative-held reference, used for the parent and for one side epoch. · OAI.UniformKServer.AllocationSchedule.held
HellingerTracePair structure: Actual paired finite observations with a common complete-trace decoder and a squared Hellinger bound. This auxiliary structure is constructed from the source score oracle and closed under literal template substitution. · OAI.TraceReconstruction.HellingerTracePair
hemisphereCone def: Radial coordinates on the open upper half-ball. The i-th domain coordinate is radius; all remaining coordinates parametrize the hemisphere. · OAI.MahlerStokes.hemisphereCone
hemisphereGraph def: Upper hemisphere graph, in the precise coordinate order used by Stokes. · OAI.MahlerStokes.hemisphereGraph
hemisphereGraphDerivative def: Derivative of the hemisphere graph. · OAI.MahlerStokes.hemisphereGraphDerivative
hemisphereParam def: The upper hemisphere parametrization into the actual Euclidean unit sphere. · OAI.MahlerStokes.hemisphereParam
hemisphereParameterArea def: Actual Euclidean hemisphere area in graph coordinates. · OAI.MahlerStokes.hemisphereParameterArea
Herd inductive: Valid terminal program coherence/cost trace · OAI.ExactDerandomization.Sub.Quill.Herd
hermitianColumn def: The real and imaginary parts of the reshaped columns. · OAI.MUB6.Weiner.hermitianColumn
hermitianHomCore def: The Hom-tuple core is constructed from ordinary Hermitian bundles. The charts, orthonormalizations, transition matrices, and cocycle proofs are derived here; no unitary core is an input. · OAI.Kaplansky.hermitianHomCore
hessian def: Coordinate Hessian. On the open domain it depends only on the restriction of u. The order of the two differentiations is immaterial under the smoothness hypothesis. · OAI.AffineBernstein.hessian
hessianBlock def: Both derivative directions in the covariant Hessian of curvature. · OAI.PositiveEinsteinFour.Geometry.hessianBlock
hessianCovectorMatrix def: The complex-coordinate coefficient matrix, in split real/imaginary order. · OAI.Mahler.hessianCovectorMatrix
hessianForm def: The invariant scalar expression obtained after the Hessian integration by parts. · OAI.PositiveEinsteinFour.HessianAlgebra.hessianForm
hessianGram def: The matrix-weighted Gram form of three actual Hessian arrays. · OAI.PositiveEinsteinFour.HighestHessian.hessianGram
hessianNormSq def: Entry-first order is a permutation of the usual Frobenius sum. · OAI.PositiveEinsteinFour.TraceHessian.hessianNormSq
hessianPair def: Coordinate two-form associated with a complex Hessian. This is the standard (i/2) sum H_ij dz_i wedge dbar(z_j), represented by covectors. · OAI.Mahler.hessianPair
hessianPairing def: Frobenius pairing on all four tensor slots. · OAI.PositiveEinsteinFour.TraceHessian.hessianPairing
hessianQuadraticContribution def: The complete plus-block quadratic contribution before axial reduction. The opposite cubic invariant is kept as τ. · OAI.PositiveEinsteinFour.hessianQuadraticContribution
hessianRemainder def: The concrete trace-free remainder of the covariant Weyl Hessian. · OAI.PositiveEinsteinFour.HighestHessian.hessianRemainder
hessianTensorForm def: The first-derivative Hessian form expressed directly using concrete matrix contractions and the actual inverse-energy-metric operator. · OAI.PositiveEinsteinFour.Bianchi.hessianTensorForm
HexagonalBoundaryWalks structure: Geometric data still to be constructed from the six sides of the hexagon. These are own-paper obligations, not a published-input interface. · OAI.CoarseAssembly.HexagonalBoundaryWalks
hexDistSq def: The squared distances, by cyclic separation, not planar hexagon angles. · OAI.HyperbolicObstruction.hexDistSq
hgtL def: two projection maps for finite linear combinations · OAI.GeneralMahler.hgtL
HiaiNormalStandardEmbeddingInput def: The precise local standard-form embedding consequence of Hiai Corollary 5.14 / Remark 5.15 and countable cyclic decomposition. At the published application τ is the faithful normal trace of a finite von Neumann algebra and σ is a … · OAI.KadisonSimilarity.HiaiNormalStandardEmbeddingInput
hidden def: The genuine hidden configuration, frozen when the finite input ends. · OAI.KServer.FiniteExperiment.hidden
hiddenBinomialCap def: Numerical cap forced by at least half the mean number of hidden pairs. · OAI.TraceReconstruction.hiddenBinomialCap
HiddenCollectionConditions def: This is the source hidden-count predicate, before any conditioning on fit. · OAI.TraceReconstruction.HiddenCollectionConditions
HiddenRule structure: The observation mask is a measurable function of the seed alone. · OAI.MatroidProphet.General.HiddenRule
hiddenSignedL2Bound def: The half-mean hidden-count event yields the correct L², not supremum, exponent J^{-s-1/2} in the initial Prouhet cancellation. · OAI.TraceReconstruction.hiddenSignedL2Bound
hiddenWorstScore def: The order minimum is taken separately for each complete seed. · OAI.MatroidProphet.hiddenWorstScore
Hierarchy def: Nested probability laws: H_0=R and H_{j+1}=P(H_j), with weak topologies. · OAI.DilutedSpinGlass.Hierarchy
high def: The spectral projection [M ≥ r], explicitly expanded in its product eigenbasis. · OAI.QAC.Count.high
highAngularComparison def: The comparison polynomial in Appendix cert:high-angular. · OAI.DefocusingNLS.highAngularComparison
highAngularPolynomial def: The rational lower bound in equation free:high-polynomial. · OAI.DefocusingNLS.highAngularPolynomial
highCoefficientBasisFromCoefficients def: A source basis constructed from checked coefficient data transports to the literal Pi-power image; no independent basis hypothesis is needed. · OAI.Nagata.Workers.W10.highCoefficientBasisFromCoefficients
highCoefficientEquiv def: The high-branch image is linearly equivalent to its genuine source sections. This applies equally when d-3j=0; no positive-degree assumption hides the tip. · OAI.Nagata.Workers.W10.highCoefficientEquiv
highCoefficientMap def: The high-branch map is actual multiplication by the marked product power. · OAI.Nagata.Workers.W10.highCoefficientMap
highCount def: Number of generator occurrences strictly above the chosen level. · OAI.Thomason.Construction.StrictOmegaCategory.ExpressionDegree.highCount
higher def: Strict rounded-weight priority, including the fixed label tie-breaking rule. · OAI.MatroidProphet.CandidateSpecification.higher
higherFactor def: Normalized multiplier of the positive-power kernel on degree 2*j. · OAI.PettyProjection.Spherical.higherFactor
higherKernel def: Positive-hemisphere power kernel, including the constant zeroth power. · OAI.PettyProjection.Spherical.higherKernel
highestLinearMap def: The explicit twenty-one-coordinate map, regarded as a linear map into the Euclidean space of all four-slot tensors. · OAI.PositiveEinsteinFour.HighestHessian.highestLinearMap
highestProjection def: The actual orthogonal projection onto the symmetry/trace/Bianchi subspace. · OAI.PositiveEinsteinFour.HighestHessian.highestProjection
highExclusiveCell def: Conditional cell probability retaining only high exclusive products. · OAI.JointDickman.highExclusiveCell
HighGeneratorString inductive: An r-string with exactly one generator of degree greater than r in each factor. Its length is retained for the normalization induction. · OAI.Thomason.Construction.StrictOmegaCategory.HighGeneratorString
HighProductBound def: The product estimate required after opening one large middle factor. · OAI.Problem335.HighProductBound
highResidueExceptions def: The Fourier exception set for the deterministic high levels. · OAI.Problem337.highResidueExceptions
highRowEquiv def: Translate the high part of each row to the smaller staircase. · OAI.Saxl.highRowEquiv
highStepEquiv def: Expose the last fresh layer, retaining the two independent lower fresh halves. This is a bijection of the original fair coin spaces. · OAI.CubeShuffle.highStepEquiv
highTestEval def: The associated evaluation is an actual algebra homomorphism. · OAI.StableCoordinate.Obstruction.highTestEval
highTestPoint def: A specific point where the top auxiliary part and both of its factors are one. · OAI.StableCoordinate.Obstruction.highTestPoint
Hilbert abbrev: The Hilbert space l²(G)^n, with the product coordinates flattened. · OAI.GroupRingDeterminant.Hilbert
Hilbert abbrev: Square-summable functions on the discrete group. · OAI.TorsionFreeBass.Regular.Hilbert
hilbertArrayFlatten def: Flatten two finite Hilbert sums in the same order as block matrices. · OAI.KadisonSimilarity.hilbertArrayFlatten
hilbertBasisFullCorner def: Concrete full countable matrix units on the original Hilbert space. · OAI.KadisonKastler.hilbertBasisFullCorner
hilbertBasisInitialSpace def: The initial rank-one corner of a natural-number Hilbert basis. · OAI.KadisonKastler.hilbertBasisInitialSpace
HilbertBlocks structure: Orthogonal outer blocks whose finite unions have their actual norm equivalent to coordinate ℓ². Constants may depend on the finite union, not globally. · OAI.DiamondDistortion.CoordinateCompletion.Data.HilbertBlocks
hilbertCompression def: Compression by a bounded operator between two different Hilbert spaces. · OAI.KadisonKastler.hilbertCompression
hilbertCompressionCP def: Compression is completely positive at every finite matrix size. · OAI.KadisonKastler.hilbertCompressionCP
HilbertCopies abbrev: The Hilbert direct sum of n copies of H. · OAI.KadisonSimilarity.HilbertCopies
hilbertDiagonal def: A uniformly bounded diagonal family acts on the Hilbert direct sum. · OAI.NuclearUltrapower.hilbertDiagonal
hilbertDualRepresentation def: Precomposition reverses multiplication, so the conjugate Hilbert space carries an actual star representation of the opposite operator algebra. · OAI.WeakPureInfiniteness.hilbertDualRepresentation
hilbertFourfoldFlatten def: The Hilbert-space change of coordinates for the four-by-four dilation. · OAI.KadisonSimilarity.hilbertFourfoldFlatten
hilbertLevels def: The actual first k+1 levels of the Hilbert sum. · OAI.Kaplansky.hilbertLevels
hilbertMatrix def: The action of an operator-valued matrix on a finite Hilbert direct sum. · OAI.KadisonKastler.hilbertMatrix
hilbertMatrixHom def: The usual matrix action is a star representation. · OAI.KadisonKastler.hilbertMatrixHom
hilbertOrbitHull def: The closed convex hull of the actual orbit. · OAI.PolycyclicRecognition.hilbertOrbitHull
hilbertPlanarSchwartz def: Lift a planar Schwartz function to the Hilbert norm on the same coordinates. · OAI.LipschitzHilbert.hilbertPlanarSchwartz
HilbertSchmidt abbrev: Hilbert--Schmidt vectors, with the actual tensor Hilbert norm. · OAI.NuclearUltrapower.HilbertSchmidt
hilbertSchmidtSq def: Ordinary squared Hilbert--Schmidt norm on a possibly rectangular map. · OAI.RowColumn.hilbertSchmidtSq
hilbertSignSum def: The Hilbert-space sum of independent signs. · OAI.KadisonKastler.hilbertSignSum
hilbertSpace def: This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content. · OAI.CubeShuffle.Specht.hilbertSpace
HilbertTensor def: The Hilbert completion of the algebraic tensor product. · OAI.KadisonSimilarity.HilbertTensor
hilbertTensorInsert def: Insert the first tensor coordinate in a completed Hilbert tensor product. · OAI.KadisonSimilarity.hilbertTensorInsert
hilbertTensorLift def: The lift of an operator leaving the first tensor coordinate unchanged. · OAI.KadisonSimilarity.hilbertTensorLift
hilbertTensorRightInsert def: Insert a fixed second tensor vector, leaving the multiplicity variable free. · OAI.KadisonSimilarity.hilbertTensorRightInsert
hilbertTripleFlatten def: Three nested finite Hilbert sums, in the same order as triple block matrices. · OAI.KadisonSimilarity.hilbertTripleFlatten
HilbertUltraproduct abbrev: The Hilbert ultraproduct, implemented as the Hausdorff completion of bounded families for the ultralimit seminorm. This is equivalent to the standard norm-null quotient, but gives completeness without a separate lifting argument. · OAI.NuclearUltrapower.HilbertUltraproduct
hill def: The integer in the Harary–Hill formula. · OAI.Paper170.hill
hills def: Natural envelopes using a ceiling for real powers. · OAI.PowerSaving.hills
Hint abbrev: Step source determinable from destination and bounded side information. · OAI.ExactDerandomization.Base.R.Hint
hist def: Observation mass relative to s.norm. · OAI.FourierLLogL.Dyadic.Procedure.hist
hist def: law of accepted keys as an unnormalized histogram · OAI.HadwigerCounterexample.Volley.hist
Histogram abbrev: Histogram space is an actual finite set of attained occupancies. · OAI.CoordinateSweeps.OrdinaryTensor.Histogram
histogramWeight def: Type weight on the finite, attained histogram space. · OAI.CoordinateSweeps.OrdinaryTensor.histogramWeight
Histories structure: The auxiliary fields are the actual finite recorded histories, with a lower bound on every previously used scale. Empty fresh histories obey any bound. · OAI.PlanarL1.Columns.Model.BState.Histories
History abbrev: An ordered history, stored with the most recent outcome first. · OAI.ExactQuantumFactoring.RecordedHistory.History
History structure: The literal finite list of increments already recorded for an identifier. Regions are recorded at creation time, as required by . · OAI.PlanarL1.Columns.Model.Ambient.History
history def: The literal rational history is exactly the real history, including all unsuccessful histories. · OAI.ContingencyTables.CompanionRationalUpdates.history
history def: Histories include the independent partition tape from time zero. Coding a finite observation by a natural number is injective, not a loss of information. · OAI.KServer.FiniteExperiment.history
HistoryCover structure: The available original positions and the already assigned colors cover all current leaves. Previously fresh leaves are assigned, never made available. · OAI.DilutedSpinGlass.PrescribedTree.HistoryCover
historyField def: Every signed increment from the recorded lifetime is retained. Regions are those at their creation times and are not re-tapered after subsequent changes. · OAI.PlanarL1.Columns.Model.Ambient.historyField
historyFrequencyProduct def: The product includes every internal frequency and every leaf frequency, with multiplicity, exactly as in the residue-precision argument. · OAI.Ostmann.historyFrequencyProduct
HistoryGeometry structure: Primitive radial coefficients and fixed angular operators. All fields are scalar/asymptotic or pointwise geometric facts; no transmission/reset/growth conclusion is part of this data. · OAI.HarmonicCounterexample.LinearODE.HistoryGeometry
historyMass def: The absolute history sum with a terminal test. The old-leaf multiplier is exactly the number of eligible leaves (each contributes coefficient one). Fresh histories keep the genuine grow operation and coefficient at every step. · OAI.DilutedSpinGlass.PrescribedTree.historyMass
historyParent def: Earlier parent labels, read without changing their order. · OAI.ReflexiveFixedPoints.CandidateContext.historyParent
historyPoint def: Earlier candidate outputs at the fixed anchor. · OAI.ReflexiveFixedPoints.CandidateContext.historyPoint
historyResidueData def: Coefficients may use the total product and the exposed split prefix. They cannot inspect a future split coordinate. Invalid unit coefficients are rejected by the exact toData test. · OAI.Ostmann.historyResidueData
historyResidueSplit def: The root frequency and its divisibility are supplied by the actual history, rather than by a hypothesis on an arbitrary arithmetic record. · OAI.Ostmann.historyResidueSplit
historyRun def: The history track retains every recorded instruction. · OAI.ForcedComputation.Recorder.historyRun
HistoryState structure: A state type in which every possible state already has a legal complete history. · OAI.ReflexiveFixedPoints.HistoryState
hit def: Every target must first be tested by the time limit, and its first test must have declared it bad. Removing it prevents multiple visits from ever being counted as distinct successes in this estimate. · OAI.AdaptiveReveals.Scheme.hit
hit def: Specification only: equality of the original natural values, unless an earlier step has already detected overflow. · OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.hit
hit def: Specification only: equality of the original natural values, unless an earlier step has already detected overflow. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.hit
hitCylinder def: Words required to hit the distinguished set at each specified coordinate. · OAI.Problem337.RandomProducts.hitCylinder
HitFusionData structure: The data generated by the proved finite splitting construction. · OAI.CircleDomainRigidity.HitFusionData
HitFusionData structure: The data generated by the proved finite splitting construction. · OAI.CircleDomainRigidity.MarkedHit.HitFusionData
hitIndex def: A coordinate meets at most one original path piece. · OAI.SeparableQuotient.Norming.FinitePath.hitIndex
hitsOther def: The observable that a cluster contains another listed vertex. · OAI.HyperedgeComparison.hitsOther
HitTestSmall def: A candidate family is small when one countable set and one finite atomless test measure rule out every member. This is the manuscript's small-set ideal. · OAI.CircleDomainRigidity.HitTestSmall
HitTestSmall def: A candidate family is small when one countable set and one finite atomless test measure rule out every member. This is the manuscript's small-set ideal. · OAI.CircleDomainRigidity.MarkedHit.HitTestSmall
hitType def: Signed first-survivor event. Unlike the totalized first type, this is raw-prefix measurable. · OAI.FKCRT.Inventory.hitType
hitWords def: Words having at least k coordinates in the distinguished set. · OAI.Problem337.RandomProducts.hitWords
hodgeFirstTensor def: Hodge star in the first alternating pair of a covariant four-tensor. · OAI.PositiveEinsteinFour.Geometry.hodgeFirstTensor
hodgeStarFour def: Hodge star on two-forms in the positively oriented standard basis. The input is represented by a skew matrix; the formula also defines a linear map on arbitrary matrices. · OAI.PositiveEinsteinFour.Geometry.hodgeStarFour
Holds structure: Supply over all seats and a common work horizon. Carry lip & reservoir budget abstract. · OAI.ExactDerandomization.Reed.Board.Holds
Holds def: Geometric meaning, including the grade identifications, not just ranks or underlying flag subspaces. It is meaningful over full integer rings as well. · OAI.IntegralCharacterVarieties.FlagCircuit.Data.Holds
Holds def: Regularization of the indexed least-value relation. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.Holds
hole def: Witnesses v,w are in the cut-profile space. The gradients agree over that whole space. · OAI.HadwigerCounterexample.hole
HoleApprox structure: Data actually constructed by the small-hole lemma. · OAI.EuclideanFiveColor.HoleApprox
holePolynomial def: The interpolation choice is constrained by the exact degree cutoff. · OAI.KaplanskyCounterexample.PolynomialPairing.holePolynomial
Holes structure: Full disjoint paths, including every boundary of the ordered sweep. · OAI.CoordinateSweeps.Grid.Holes
Holes structure: Prescribed disjoint trajectories; disjointness is required at every boundary. · OAI.CoordinateSweeps.Grid.Holes
HolomorphicComparison def: The exact chart transition for End(O(-1)² ⊕ O). The two spatial coefficients are expressed in h₁(1,z),h₂(1,z) and h₁(w,1),h₂(w,1). · OAI.ElasticityRigidity.HolomorphicComparison
holonomyCharge def: Total signed crossing count. · OAI.CoarseAssembly.holonomyCharge
holonomyEndpoint def: Successively apply left Cayley moves and right integral holonomies. · OAI.CoarseAssembly.holonomyEndpoint
holonomyLocal def: Actual based-loop holonomy is flat; this is derived from square homotopy in I², rather than supplied as a geometric assumption. · OAI.EilenbergGanea.PathTransport.holonomyLocal
holonomyWord def: Product of the left moves, in the order in which they act. · OAI.CoarseAssembly.holonomyWord
Hom structure: Maps of construction stages retain right factors, disjointness, and exact old suprema. Such maps make continuous unions legitimate stages. · OAI.PartitionConsistency.MonoidConstruction.Hom
Hom structure: A chain map preserving the augmentation and positive submonoids. · OAI.Thomason.Construction.DirectedComplex.Hom
Hom structure: A strict functor preserves both boundaries and every defined composition. · OAI.Thomason.Construction.StrictOmegaCategory.Hom
hom def: Extend a group represented in a nonunital corner to units of the ambient ring. · OAI.FiniteAlgebraicEnvelopes.Unitize.hom
homAction def: The action of a commuting group on the multiplicity space. · OAI.CoordinateSweeps.CommutingRestriction.homAction
homCokernelIso def: Dualizing a genuine presentation gives the actual kernel. This is the kernel description used to prove coherence of the model dual, not a postulated exactness property of an abstract replacement dual. · OAI.CoherentDual.homCokernelIso
homeomorph def: The resulting homeomorphism retains the original coordinate values. · OAI.RegularPointCoordinates.OpenCoordinateData.homeomorph
homeomorph def: The homeomorphism uses the actual realization, with its original topology. · OAI.Thomason.Construction.HornBarycentric.homeomorph
homeomorph def: The affine barycentric map, as a homeomorphism of actual spaces. · OAI.Thomason.Construction.SubdivisionBarycentric.homeomorph
homeomorph def: A homeomorphism is induced by point-separating coordinates and actual continuous lifts on each characteristic disk, in both directions. · OAI.WeakRealization.homeomorph
homeomorphOfSimplyConnectedCovering def: A covering of a simply connected space from a connected space has a continuous global inverse. · OAI.PolycyclicRecognition.homeomorphOfSimplyConnectedCovering
homeomorphOrbitSetoid def: The orbit relation is used only to say that the section meets each orbit. Its finite-neighbor relation controls the measure of the section. · OAI.DukePrimeDegree.homeomorphOrbitSetoid
homEquiv def: Universal property among sheaves of modules. · OAI.ActualCotangent.homEquiv
homEquiv def: The actual hom-set correspondence for the right interval chain tensor. · OAI.Thomason.Construction.DirectedComplex.RightPath.homEquiv
homEquiv def: Positive maps from the globe complex are exactly bounded cells in Steiner's actual strict realization. · OAI.Thomason.Construction.DirectedGlobeComplex.homEquiv
homEquiv def: The actual lambda-nu hom-set equivalence. · OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.homEquiv
homEquiv def: The globe represents bounded cells in the actual strict category. · OAI.Thomason.Construction.StrictOmegaCategory.Globe.homEquiv
homEquiv def: The literal Hom bijection for the extended cylinder. · OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.homEquiv
homEquiv def: Currying and uncurrying are inverse on actual continuous maps. · OAI.Thomason.Construction.TopologicalInterval.homEquiv
homEquiv def: The ordinary compact-open exponential law, specialized to the parameter spaces used in finite realization approximations. · OAI.Thomason.Construction.TopologicalProduct.homEquiv
homFreeIso def: The genuine internal Hom out of a free sheaf is the product of the target sheaf, with no presentation/exactness assumed. · OAI.CoherentDual.homFreeIso
homIsometry def: The actual L² isometry of a trace-preserving ambient homomorphism. · OAI.KadisonSimilarity.TracialCornerGeometry.homIsometry
Homogeneous def: Laurent homogeneity for the source convention deg T = -1. · OAI.StableCoordinate.ModificationPieces.Homogeneous
homogeneous def: Degree-n polynomials inside the coefficient section algebra. · OAI.ReesProj.homogeneous
homogeneous def: Degree-n polynomials inside the coefficient section algebra. · OAI.SectionCompletion.homogeneous
homogeneous def: A homogeneous element of the Rees algebra. · OAI.StableCoordinate.FilteredRees.homogeneous
homogeneousBasis def: The monomial basis transported through the proved coefficient equivalence. · OAI.Nagata.W02.homogeneousBasis
homogeneousChartEquiv def: A literal basic affine Proj chart, identified by all normalized coefficients. · OAI.SectionCompletion.homogeneousChartEquiv
homogeneousCochainEquiv def: The concrete coordinate isomorphism underlying the group-ring cohomology comparison. No equivariance of the coarse map is needed. · OAI.PolycyclicRecognition.homogeneousCochainEquiv
homogeneousCoefficientEquiv def: Proved identification with the actual supported coefficient submodule. · OAI.Nagata.W02.homogeneousCoefficientEquiv
homogeneousCoordinates def: A genuine coefficient linear equivalence for the full space of degree-d homogeneous ternary forms. · OAI.Nagata.W27.homogeneousCoordinates
homogeneousCoords def: Actual coefficient coordinates on homogeneous polynomials. · OAI.HarmonicCounterexample.Control.homogeneousCoords
homogeneousDatum def: The homogeneous datum V(130z/(r²+z²)) of sa:homogeneous-datum, written in Cartesian coordinates. Its value at the origin is fixed to zero; that value has no bearing on its distributional interpretation. · OAI.StationaryNS.homogeneousDatum
homogeneousDim def: Dimension of homogeneous degree t polynomials in r variables, for a positive number of variables. · OAI.Problem335.homogeneousDim
homogeneousEvaluation def: Simultaneous evaluation of actual homogeneous forms at chosen coordinates. · OAI.Nagata.Workers.W24.homogeneousEvaluation
homogeneousFieldMap def: An actual finite-dimensional representation, in the actual monomial basis. · OAI.HarmonicCounterexample.Control.homogeneousFieldMap
homogeneousFreeFourier def: Fourier action of e^((-a+ib)s)e^(i(1-e^-s)Δ)v. · OAI.DefocusingNLS.homogeneousFreeFourier
homogeneousFunctionsEquivAntidiag def: The weak-composition function representation and the finite antidiagonal representation used by power-series coefficient extraction are equivalent. · OAI.Problem335.homogeneousFunctionsEquivAntidiag
homogeneousFunctionsFintype abbrev: An explicit finite enumeration for a weak-composition function type. This is not installed globally, so consumers may choose their preferred enumeration. · OAI.Problem335.homogeneousFunctionsFintype
homogeneousLaplacian def: Restricted polynomial Laplacian, between the correct degree spaces. · OAI.HarmonicCounterexample.Angular.homogeneousLaplacian
homogeneousLinearizedPotential def: The Schrödinger linearization is a bounded real operator on the actual Y space. · OAI.DefocusingNLS.homogeneousLinearizedPotential
homogeneousLineEquation def: The actual homogeneous linear equation Y-i²Z+iU. · OAI.Nagata.Workers.W24.homogeneousLineEquation
homogeneousLineGraph def: Binary homogeneous graph Y=i² Z-i U; binary coordinates are U,Z. · OAI.Nagata.Workers.W24.homogeneousLineGraph
homogeneousLineRestriction def: Binary restrictions are ordinary ring evaluations in the Y variable. · OAI.Nagata.Workers.W24.homogeneousLineRestriction
homogeneousLineSubstitution def: Explicit homogeneous coordinate substitution (U,Y,Z)=(U,i²Z-iU,Z). · OAI.Nagata.Workers.W24.homogeneousLineSubstitution
homogeneousLineUnion def: Homogeneous equation of the reduced union of k lines. · OAI.Nagata.Workers.W24.homogeneousLineUnion
homogeneousLocalization def: The Fourier representative of the actual physical localization. · OAI.DefocusingNLS.homogeneousLocalization
HomogeneousMonomial abbrev: All global ternary monomials of degree exactly d; these columns are independent of the affine charts chosen at the marked points. · OAI.Nagata.W27.HomogeneousMonomial
homogeneousNonlinearRemainder def: The actual odd-power nonlinearity with its constant and linear parts removed. · OAI.DefocusingNLS.homogeneousNonlinearRemainder
HomogeneousOnConstants def: The precise homogeneous-on-constants condition needed for Laurent descent. · OAI.StableCoordinate.LaurentDescent.HomogeneousOnConstants
homogeneousPathFlux def: The flux along the one-form deformation. · OAI.Mahler.homogeneousPathFlux
HomogeneousPlaneFamily def: Genuine one-parameter families of homogeneous plane forms. · OAI.Nagata.Workers.W17.HomogeneousPlaneFamily
homogeneousPolarDerivative def: Every Cartesian derivative from the homogeneous completion has an exact sphere/radius L² representative with the same norm. · OAI.DefocusingNLS.homogeneousPolarDerivative
homogeneousPowerRankOne def: Actual polynomial evaluation rank-one operator. · OAI.HarmonicCounterexample.Control.homogeneousPowerRankOne
homogeneousPrimitive def: The transgression primitive in every complex dimension k+2. · OAI.Mahler.homogeneousPrimitive
homogeneousProduct def: The degree-k part of an ordered product of 1 + x. · OAI.PolycyclicRecognition.homogeneousProduct
HomogeneousProductRankBound def: The product-rank statement is kept explicit as the one algebraic input. · OAI.Problem335.HomogeneousProductRankBound
homogeneousRadialAngularDerivative def: The contraction is formed after completing each Cartesian derivative. Its angular coefficients are r^11-weighted L² functions. · OAI.DefocusingNLS.homogeneousRadialAngularDerivative
homogeneousRadialTest def: The finite contracted test remains bounded on the full completion. · OAI.DefocusingNLS.homogeneousRadialTest
homogeneousRadialTestComponent def: Each separated angular/radial test acts boundedly on an ordered derivative. · OAI.DefocusingNLS.homogeneousRadialTestComponent
homogeneousRepresentationCochain def: The reconstructed values give an actual morphism of group representations. · OAI.PolycyclicRecognition.homogeneousRepresentationCochain
homogeneousRepresentationCochainEquiv def: Controlled scalar cochains are exactly the equivariant cochains with coefficients in the left regular group ring. · OAI.PolycyclicRecognition.homogeneousRepresentationCochainEquiv
HomogeneousRestrictionBound def: Every homogeneous output restriction of codimension at most r has the stated actual normalized squared norm. The dimension inequality avoids truncated subtraction in the restriction-composition step. · OAI.MaxCutGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound
HomogeneousRestrictionBound def: Every homogeneous output restriction of codimension at most r has the stated actual normalized squared norm. The dimension inequality avoids truncated subtraction in the restriction-composition step. · OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.HomogeneousRestrictionBound
homogeneousSection def: A homogeneous polynomial gives a section of the corresponding actual associated bundle; its local expression is computed from representatives. · OAI.Nagata.W16.AssociatedBundle.homogeneousSection
homogeneousSphereFlux def: The actual homogeneous endpoint, with no flux-constancy premise. · OAI.Mahler.homogeneousSphereFlux
HomogeneousState structure: Occupation coefficients with fixed particle number in every homogeneous degree. · OAI.Laughlin.Planar.HomogeneousState
homogeneousSupport def: The one-homogeneous extension of the literal spherical support function. · OAI.AffineBernstein.homogeneousSupport
homogeneousTwoPrimitive def: The transgression primitive in complex dimension two. · OAI.Mahler.homogeneousTwoPrimitive
homogeneousYConvolution def: The actual continuous-frequency convolution extends to every vector of Y. · OAI.DefocusingNLS.homogeneousYConvolution
homologyEquiv def: Actual vertex homology, identified with the actual subspace of module homology. · OAI.LittleFinitistic.LeftVertexHomology.homologyEquiv
homologyIso def: Actual homology of a selected chain tensor, with its chosen target identification. · OAI.LittleFinitistic.SelectedChainHomology.homologyIso
homologyOneEquiv def: Actual homotopy equivalences induce integral cubical H1 isomorphisms. · OAI.EilenbergGanea.CubicalSingular.homologyOneEquiv
Homotopic def: Finite chains suffice, so no smooth concatenation theorem is assumed. · OAI.KervaireUnitaryHomotopy.Homotopic
homotopy def: The horn contracts to its cone vertex through two simplicial homotopies. · OAI.Thomason.Construction.HornContraction.homotopy
homotopy def: A pair of compatible endpoint equations gives an actual continuous homotopy. · OAI.Thomason.Construction.RealizationPrism.homotopy
homotopy def: Realization turns every simplicial homotopy into an actual continuous homotopy. · OAI.Thomason.Construction.RealizedCylinder.homotopy
homotopyCategoryToFundamentalGroupoid def: A simplicial edge is sent to its actual linear path class. The triangle relation holds by the explicit barycentric relative homotopy. · OAI.Thomason.Construction.RealizationPrism.homotopyCategoryToFundamentalGroupoid
homotopyCategoryToFundamentalGroupoid_naturality def: The comparison with the actual fundamental groupoid is natural in simplicial maps, with the canonical endpoint identifications. · OAI.Thomason.Construction.RealizationPrism.homotopyCategoryToFundamentalGroupoid_naturality
homotopyCoproductIsColimit def: The actual coproduct survives the homotopy quotient. Both existence and uniqueness are proved; the latter assembles the component homotopies. · OAI.DerivedBar.homotopyCoproductIsColimit
homotopyCube def: Regard the homotopy parameter as the first coordinate of one larger cube. · OAI.Thomason.Construction.RealizedCube.homotopyCube
homotopyEquiv def: Coverings preserve the genuine higher homotopy sets/groups. · OAI.HyperbolicObstruction.HigherCovering.homotopyEquiv
homotopyEvaluation def: Termwise tensor evaluation on actual complexes, descended through chain homotopies. · OAI.LittleFinitistic.BalancedTensor.homotopyEvaluation
homotopyFiberEquiv def: For every continuous map into the realized cube, its actual homotopy fibre projects by a homotopy equivalence to its source. · OAI.Thomason.Construction.RealizedCube.homotopyFiberEquiv
homotopyFiberFromPath def: A family of points over the start of a path maps to its terminal homotopy fibre by attaching that same path to every point. · OAI.Thomason.Construction.homotopyFiberFromPath
homotopyFiberFromPathHomotopy def: Homotopic chosen paths produce homotopic maps from a fixed point fibre into the actual terminal homotopy fibre. · OAI.Thomason.Construction.homotopyFiberFromPathHomotopy
homotopyFiberLiftedPath def: An actual lift of a base path gives an explicit homotopy in its terminal homotopy fibre. The path coordinate is its remaining tail, so the statement retains the whole family, not just its path components or weak status. · OAI.Thomason.Construction.homotopyFiberLiftedPath
homotopyFiberMap def: The actual map on continuous homotopy fibres induced by a cubical base change retains both point and path coordinates. · OAI.Thomason.Construction.RealizedCube.homotopyFiberMap
homotopyFiberPath def: The path coordinate of an actual homotopy-fibre point, with both endpoints recorded in its type. · OAI.Thomason.Construction.homotopyFiberPath
homotopyFiberPathEquiv def: The explicit homotopy equivalence between homotopy fibres associated to a base path; its inverse appends the reversed path. · OAI.Thomason.Construction.homotopyFiberPathEquiv
homotopyFiberPathTransport def: Transport in the base appends the specified path and leaves the point in the total space fixed. · OAI.Thomason.Construction.homotopyFiberPathTransport
homotopyFiberPathTransportAssoc def: Associating the appended paths is a homotopy on the whole homotopy fibre, including the varying point and starting endpoint. · OAI.Thomason.Construction.homotopyFiberPathTransportAssoc
homotopyFiberPathTransportCancel def: A path followed by its reverse cancels on the full actual homotopy fibre. This is stronger than equality on components. · OAI.Thomason.Construction.homotopyFiberPathTransportCancel
homotopyFiberPathTransportHomotopy def: A homotopy of base paths induces a homotopy of the actual transport maps. All point coordinates remain fixed. · OAI.Thomason.Construction.homotopyFiberPathTransportHomotopy
homotopyFiberPathTransportUnit def: Appending the constant path is homotopic to the identity, continuously in every total-space point and every homotopy-fibre path. · OAI.Thomason.Construction.homotopyFiberPathTransportUnit
homotopyFiberReparametrize def: Reparametrizing a homotopy-fibre path preserves its point coordinate. · OAI.Thomason.Construction.homotopyFiberReparametrize
homotopyFiberReparametrizeHomotopy def: The reparametrization homotopy is continuous even as the starting point of the path varies over the total space. · OAI.Thomason.Construction.homotopyFiberReparametrizeHomotopy
homotopyGroupFunctor def: The actual homotopy group quotient, functorially in based spaces. · OAI.Thomason.Construction.PointedHomotopyGroups.homotopyGroupFunctor
homotopyIso def: The chosen representative's actual tensor is the source evaluation object. · OAI.LittleFinitistic.SelectedTensorComparison.homotopyIso
homotopyMap def: The actual induced map on the cube-relative homotopy quotient. · OAI.HyperbolicObstruction.HigherCovering.homotopyMap
homotopyOfPath def: Conversely: no quotient or merely formal track is used here. · OAI.TorsionFreeZeroDivisors.LoopTracks.homotopyOfPath
homotopyPath def: A path homotopy is a continuous path in the compact-open path space. · OAI.Thomason.Construction.PathSpace.homotopyPath
homotopyRelOfStationary def: The realized homotopy is relative to the entire image of the specified simplicial map; no embedding hypothesis is needed. · OAI.Thomason.Construction.RealizedCylinder.homotopyRelOfStationary
homotopyToIntegerDerived abbrev: Extension of the nonnegative homotopy category followed by the genuine integer derived localization. · OAI.DerivedBar.homotopyToIntegerDerived
homotopyVertexIso def: Evaluation of each concrete degree-zero vertex object is the stalk complex Y. · OAI.LittleFinitistic.QuadraticEncoding.homotopyVertexIso
homOverIso def: Internal Hom commutes with actual restriction to the slice site. · OAI.CoherentDual.homOverIso
homPresheaf def: The linear internal Hom presheaf, with its natural module structure. · OAI.CoherentDual.homPresheaf
homReindexPresheafIso def: Internal linear Hom is preserved by coefficient isomorphisms and a reindexing functor that is an equivalence on every slice. · OAI.CoherentDual.homReindexPresheafIso
homSchemeRestrictionIso def: The actual internal linear Hom commutes with restriction to an open subscheme, including the non-definitional coefficient-ring isomorphism. · OAI.CoherentDual.homSchemeRestrictionIso
homSheaf def: The actual sheaf of modules of local linear maps. · OAI.CoherentDual.homSheaf
homSheafCovFunctor abbrev: Covariant functoriality in the target of the actual internal Hom. · OAI.CoherentDual.homSheafCovFunctor
homSheafEvaluationIso def: Evaluation of internal Hom is the actual representable functor on the slice site. In particular no local presentation or exactness is postulated. · OAI.CoherentDual.homSheafEvaluationIso
homSheafFunctor def: Contravariant internal Hom into a fixed sheaf. · OAI.CoherentDual.homSheafFunctor
homSheafSectionsEquiv def: Sections of homSheaf are the actual morphisms of the restricted sheaves. · OAI.CoherentDual.homSheafSectionsEquiv
honestBits def: The same global proof in the construction's explicit radix numbering. · OAI.MaxCutGames.Foundations.Hastad.SourceHonest.honestBits
honestBits def: The same global proof in the construction's explicit radix numbering. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.honestBits
honestGlobal def: A single assignment to the globally tagged padded tables. It is defined from the input assignment alone, before any incidence or test is sampled. · OAI.MaxCutGames.Foundations.Hastad.SourceHonest.honestGlobal
honestGlobal def: A single assignment to the globally tagged padded tables. It is defined from the input assignment alone, before any incidence or test is sampled. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.honestGlobal
honestPoint def: The free-coordinate local assignment always has homogeneous coordinate one. · OAI.MaxCutGames.Reduction.ActualCompleteness.honestPoint
honestPoint def: The free-coordinate local assignment always has homogeneous coordinate one. · OAI.UniqueGamesTheorem.Reduction.ActualCompleteness.honestPoint
honestValidJ def: Satisfiability supplies one consistent valid right coordinate in every clause tuple, including tuples with repeated clauses or variable names. · OAI.MaxCutGames.Foundations.Hastad.SourceHonest.honestValidJ
honestValidJ def: Satisfiability supplies one consistent valid right coordinate in every clause tuple, including tuples with repeated clauses or variable names. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.honestValidJ
hookEmbedding def: Explicit signed-slot realization of every (h,h)-hook Specht module. The target, action, and intertwiner are concrete; no LR/Schur-Weyl occurrence axiom is used. This supplies the first necessary step of weighted.tex:88–93. · OAI.RowColumn.HookModel.hookEmbedding
hopfMultiplicity def: The exact source Hopf multiplicity, obtained as the bihomogeneous kernel minus its Laplacian target, not an asymptotic density. · OAI.HarmonicCounterexample.Certificate.hopfMultiplicity
hopfUnit def: Unit Hopf vector for the indicated orthogonal complex structure. · OAI.HarmonicCounterexample.Cartesian.hopfUnit
horizon def: A common clock for all witnesses of permitted length for one input. · OAI.MaxCutGames.Foundations.Complexity.CookLevin.NPVerifier.horizon
horizon def: The exact source horizon H. · OAI.UniformKServer.horizon
horizon def: A common clock for all witnesses of permitted length for one input. · OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.NPVerifier.horizon
Horizontal def: Horizontal lifts of the real tangent of Q3 at [z]. · OAI.ArnoldCounterexample.Horizontal
Horizontal structure: A horizontal differential on signed columns, with its actual square and mixed relation. · OAI.LittleFinitistic.FiniteColumnComplex.Horizontal
Horizontal def: A form annihilates a vector in every slot. · OAI.Mahler.Horizontal
horizontal def: The horizontal face in a literal outer block; there is no face at length zero. · OAI.DerivedBar.RecursiveTotal.horizontal
horizontal def: Horizontal tensor maps reindex the unchanged left factor along the total degree. · OAI.LittleFinitistic.ComplexTensor.horizontal
horizontalFactor def: The source normalization keeps the angular volume unchanged by q. · OAI.HarmonicCounterexample.Berger.horizontalFactor
horizontalJacobian def: The actual first derivative of the horizontal component, in graph coordinates. · OAI.AffineBernstein.horizontalJacobian
horizontalMode def: The anchor mode for one of the horizontal propagation steps. · OAI.Problem348.Construction.SampledSelection.horizontalMode
horizontalOuter def: The horizontal pair of vertical composites. · OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.horizontalOuter
HorizontalParameters abbrev: Real spectral part, shift, coupling, and the two normalized initial coordinates. · OAI.DefocusingNLS.HorizontalParameters
horizontalPotential def: Polynomial Hamiltonians for the elementary shears. The coefficients are rational whenever the instruction and parking point are rational. · OAI.ForcedComputation.PlanarHamiltonian.horizontalPotential
HorizontalStrip def: A horizontal strip removes at most one cell in each column. · OAI.Saxl.HorizontalStrip
horn def: The geometric horn is the union of all faces except the opposite face. · OAI.Thomason.Construction.HornBarycentric.horn
hornClampToId def: The clamp is below the identity, with no change of an omitted vertex. · OAI.Thomason.Construction.hornClampToId
hornClampToVertex def: The same clamp is below the constant distinguished vertex. · OAI.Thomason.Construction.hornClampToVertex
horner def: Horner value processes the actual physical data bits from low wire to high wire, matching the reversed input convention of the triangular transform. · OAI.ExactQuantumFactoring.BitArithmetic.horner
hornerBox def: Backward Horner recurrence; after n steps this is evaluation of the suffix. · OAI.SepticProfile.FixedInterval.hornerBox
hornerInEncodedPolynomialTime def: Actual subroutine time bounded in the concrete lengths of its operand fields. The destination suffix and unrelated tapes are preserved without scans. · OAI.MaxCutGames.Foundations.Complexity.MachineHorner.hornerInEncodedPolynomialTime
hornerInEncodedPolynomialTime def: Actual subroutine time bounded in the concrete lengths of its operand fields. The destination suffix and unrelated tapes are preserved without scans. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.hornerInEncodedPolynomialTime
hornOneIso def: A one-dimensional horn is its sole vertex. · OAI.Thomason.Construction.hornOneIso
hornVertex def: The distinguished vertex belongs to its horn in every positive dimension. · OAI.Thomason.Construction.hornVertex
HostBounds def: Integer certificates for one candidate host. This does not assert existence. · OAI.Problem348.SequenceAssembly.HostBounds
HostedGroup structure: One child group's single recorded host window, in host coordinates. This includes the actual recipient and full-window agreement, not just a common substring or an assumed possibility of connecting it. · OAI.Superstring.Hierarchical.HostedGroup
hostMatrix def: The canonical host viewed through independent row/column enumerations. · OAI.Problem348.Construction.hostMatrix
HS def: Hereditary symmetry follows the subname relation, not membership of the interpreted sets. · OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.HS
hsConjugation def: Conjugation is unitary for the Hilbert--Schmidt norm. · OAI.NuclearUltrapower.hsConjugation
hsInner def: The algebraic Hilbert--Schmidt scalar product, irrespective of the operator norm on the carrier. A core is used to avoid changing any source norm. · OAI.RowColumn.HilbertSchmidt.hsInner
hsNormSq def: The Hilbert--Schmidt norm squared for the counting inner product. This explicit entry sum does not use any norm instance on matrices. · OAI.LeanBlast.GotsmanLinial.hsNormSq
hsOperator def: Faithful operator realization of the Hilbert--Schmidt completion. · OAI.NuclearUltrapower.hsOperator
hsRepresentation def: The conjugation representation on all Hilbert--Schmidt operators. · OAI.NuclearUltrapower.hsRepresentation
hsSquared def: The squared Hilbert--Schmidt norm, without changing the ambient matrix norm. · OAI.SharpLiebThirring.MatrixProof.hsSquared
Hstar def: Highest weighted part of the source hypersurface equation. · OAI.StableCoordinate.Obstruction.Hstar
hubbardFermionBottom def: The actual fermionic spectral bottom on all nonzero half-filled states, in the canonical occupation norm. · OAI.ContinuumCoulomb.HubbardGlobal.hubbardFermionBottom
hull def: Close under dependencies as well as factors and actual conditional joins. This is a submonoid of the terminal monoid, not a substitute monoid. · OAI.PartitionConsistency.ConservativeMonoids.CellTower.hull
hull def: The countable union of the finite stages, not closure under arbitrary external functions. · OAI.PartitionConsistency.CountableModel.hull
hurewiczOne def: Integral degree-one Hurewicz for actual paths, with no cellular hypothesis: finite singular 1-cycles equal the abelianized topological fundamental group. · OAI.EilenbergGanea.CubicalSingular.hurewiczOne
HuxleyAdditiveLargeSieve def: Exact Q²+Z input, with neither a conductor power loss nor an invented multiplicative-character estimate hidden in the hypothesis. · OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve
huxleyPhase def: Gao–Zhao's additive character e_K(nh/q), with sqrt(D_K)=traceLambda. · OAI.CubicFirstMoment.huxleyPhase
Hybrid def: The actual hybrid selector from Appendix A.1, for genuine linear maps. · OAI.MaxCutGames.Appendix.LinearIdentities.Hybrid
Hybrid def: The actual hybrid selector from Appendix A.1, for genuine linear maps. · OAI.UniqueGamesTheorem.Appendix.LinearIdentities.Hybrid
hybridFiberEquiv def: The exact coordinate parametrization after imposing the genuine hybrid selector. The two remaining conditions are ordinary injectivity and surjectivity of displayed linear maps. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.hybridFiberEquiv
hybridFiberEquiv def: The exact coordinate parametrization after imposing the genuine hybrid selector. The two remaining conditions are ordinary injectivity and surjectivity of displayed linear maps. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.hybridFiberEquiv
hyperbola def: Positive lattice points below the multiplicative hyperbola a*b ≤ N. · OAI.Problem337.Vaughan.hyperbola
HyperbolicAt def: In dimension two these two distinct nonzero eigenvalues are all the eigenvalues. · OAI.RuledApproximation.HyperbolicAt
hyperbolicCost def: The explicit scalar cost of a hyperbolic Type I sum. · OAI.Problem337.RealTypeI.hyperbolicCost
hyperbolicIsometries def: The full isometry group, including orientation-reversing isometries. · OAI.CannonRelease.hyperbolicIsometries
HyperbolicThree def: The upper-half-space model of hyperbolic three-space. · OAI.CannonRelease.HyperbolicThree
Hypergraph abbrev: Full labelled hyperedges; allowing empty hyperedges causes no change to clusters. · OAI.HyperedgeComparison.Hypergraph
hyperplane def: The field hyperplane perpendicular to the generator of the line. · OAI.MaxCutGames.Quadratic.hyperplane
hyperplane def: The field hyperplane perpendicular to the generator of the line. · OAI.UniqueGamesTheorem.Quadratic.hyperplane
hyperplaneEvaluationEquiv def: Evaluation at any nonzero vector is a genuine coordinate on the dual of its one-dimensional line. · OAI.Kaplansky.hyperplaneEvaluationEquiv
hyperplaneEvaluationHomeomorph def: Evaluation at a nonvanishing continuous line vector trivializes the actual pullback hyperplane bundle, with its ordinary bundle topology. · OAI.Kaplansky.hyperplaneEvaluationHomeomorph
hyperplaneExtend def: Extend a frequency by specifying its value on the new coordinate. · OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend
hyperplaneExtend def: Extend a frequency by specifying its value on the new coordinate. · OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend
hyperplaneExtensionEquiv def: Exact parametrization of a restriction fiber, including dependent extensions. · OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtensionEquiv
hyperplaneExtensionEquiv def: Exact parametrization of a restriction fiber, including dependent extensions. · OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtensionEquiv
hyperplaneFunctionalSection def: Restrict an ambient linear functional to each actual tautological line, viewed as a section of its dual, the hyperplane bundle. · OAI.Kaplansky.hyperplaneFunctionalSection
hyperplaneIdeal def: The coordinate hyperplane's defining ideal. · OAI.StableCoordinate.GeometricInterpretation.hyperplaneIdeal
hyperplaneMeasure def: Intrinsic measure of a hyperplane, with a fixed canonical basepoint. · OAI.Problem358.IntrinsicSurface.hyperplaneMeasure
hyperplaneNoiseShift def: Translation by the polar term permutes the vertical hyperplane. · OAI.MaxCutGames.Quadratic.hyperplaneNoiseShift
hyperplaneNoiseShift def: Translation by the polar term permutes the vertical hyperplane. · OAI.UniqueGamesTheorem.Quadratic.hyperplaneNoiseShift
hyperplaneProductStage def: Exactly K_i copies of each actual pulled-back hyperplane line. · OAI.Kaplansky.hyperplaneProductStage
hyperplaneProjection def: Restrict the actual orthogonal projection to the source tangent hyperplane. · OAI.ProjectionCounterexample.hyperplaneProjection
Hyperplanes abbrev: Hyperplanes, expressed without truncated dimension subtraction. · OAI.MaxCutGames.Inverse.MatrixChart.Hyperplanes
Hyperplanes abbrev: Hyperplanes, expressed without truncated dimension subtraction. · OAI.UniqueGamesTheorem.Inverse.MatrixChart.Hyperplanes
hyperplanesEquivDualLines def: Dual annihilation bijects hyperplanes with lines in the dual space. · OAI.MaxCutGames.Inverse.MatrixChart.hyperplanesEquivDualLines
hyperplanesEquivDualLines def: Dual annihilation bijects hyperplanes with lines in the dual space. · OAI.UniqueGamesTheorem.Inverse.MatrixChart.hyperplanesEquivDualLines
hypersurfaceIsoOfAlgEquiv def: In particular every algebra equivalence of a hypersurface coordinate ring with a polynomial algebra gives the required affine-space isomorphism. · OAI.StableCoordinate.AffineGeometry.hypersurfaceIsoOfAlgEquiv
Hypotheses def: Type-(A) action hypotheses. · OAI.FiniteAlgebraicEnvelopes.TypeAAction.Hypotheses