Glossary: L

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

L 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.L

L def

The two actual lower-bound sums on a conditional count distribution. · OAI.KServer.CompatibleBounds.L

L abbrev

The terminal expansion budget plus the backward descent budget. · OAI.Problem337.RawDensityParameters.L

L def

The source logarithmic girth, including its specified constant c=1/100. · OAI.TorsionFreeZeroDivisors.GirthAsymptotics.L

l def

The first new linear coordinate, denoted L in the manuscript. · OAI.StableCoordinate.Linearization.l

L1 abbrev

Minimum script length. Scripts always exist (delete x and insert y). · OAI.EditDistortion.L1

l1Append def

Direct sum of two finite real L1 vectors, with the sum norm (not the maximum norm on an ordinary product). · OAI.BoundedTreewidthL1.l1Append

L2 abbrev

Genuine complete complex Hilbert space for the quotient trace. · OAI.Generator.Tracial.L2

l2ClosureAlgebra def

The actual bounded algebra lying in the L² closure of S. · OAI.KadisonSimilarity.TracialCornerGeometry.l2ClosureAlgebra

l2DualEquiv def

Isometric dual description of arbitrary outer l2 sums. · OAI.BoundedTreePotentials.l2DualEquiv

l2Embedding def

An injection of coordinate sets induces an honest Hilbert isometry. · OAI.NuclearUltrapower.l2Embedding

l2Extension def

Extension by zero is an isometric linear inclusion of each stratum. · OAI.KadisonKastler.l2Extension

l2FactorAlgebra def

The concrete bounded algebra generated in L² by two prescribed factors. · OAI.KadisonSimilarity.TracialCornerGeometry.l2FactorAlgebra

l2FiniteAssembly def

Assemble a finite tuple of L² sections into one tuple-valued section. · OAI.KadisonSimilarity.l2FiniteAssembly

l2FiniteCoordinates def

The inverse takes the actual pointwise coordinate projections. · OAI.KadisonSimilarity.l2FiniteCoordinates

l2FiniteCopiesEquiv def

The exact unitary identification of finite L² sums. · OAI.KadisonSimilarity.l2FiniteCopiesEquiv

l2GeneratedAlgebra def

The bounded L²-generated algebra of an arbitrary star subalgebra, constructed by first taking its norm closure. · OAI.KadisonSimilarity.TracialCornerGeometry.l2GeneratedAlgebra

l2IsometryField def

Pointwise isometries give a genuine isometric inclusion of L² spaces. · OAI.KadisonKastler.l2IsometryField

l2MapIsometry def

Lift a Hilbert isometry pointwise to L². · OAI.KadisonSimilarity.l2MapIsometry

l2MeanSlope def

Averaging any L² cocycle gives a genuine height homomorphism. · OAI.PolycyclicRecognition.l2MeanSlope

l2Restriction def

The contractive linear restriction map to a measurable stratum. · OAI.KadisonKastler.l2Restriction

l2Single def

Coordinate lines in a Hilbert direct sum. · OAI.NuclearUltrapower.l2Single

l2StrataCoordinates def

The actual Hilbert-space coordinates associated with a measurable partition. · OAI.KadisonKastler.l2StrataCoordinates

l2ToL1 def

The canonical continuous inclusion L2 -> L1 on a probability space. · OAI.IndependentProducts.l2ToL1

Label abbrev

One initialization label and ten labels per fixed port. · OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.Label

Label abbrev

Two labels per coordinate, plus start, body, and exit labels. · OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Control.Label

Label abbrev

false denotes the negative half and true the positive half. · OAI.QuantitativeVanDerWaerden.AdaptiveMesh.Label

Label abbrev

One initialization label and ten labels per fixed port. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.Label

Label abbrev

Two labels per coordinate, plus start, body, and exit labels. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Control.Label

label def

Label noise law centered at zero relative to counting measure. · OAI.FourierLLogL.Dyadic.Thermal.label

label def

Genuine left reflection label; uniquely determined by the endpoints. · OAI.KLInvariance.BruhatGraph.label

label def

Actual permanent record labels in the finite source pool. · OAI.KServer.Chronological.label

label def

An index is coded by an actual ground set (eventually a ground ordinal). At coordinate j the name has precisely the positively assigned indices. · OAI.PartitionConsistency.ProductForcing.label

label def

In each nonzero row, its first k i factors use the common block. · OAI.Problem346.SecondTransfer.label

label def

Anchor mode and group, forgetting the irrelevant within-group offset. · OAI.Problem348.Construction.SelectedAnchors.label

label def

The original ordinal of a retained entry. · OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.label

label def

The actual legal word containing the origin, read as its unique selected level label. This is a function of the symbolic configuration, not added data. · OAI.SmoothObstruction.WordHierarchy.label

label def

The binary strict label carried by this actual oriental. · OAI.Thomason.Construction.SieveSimplex.label

label def

The reversed label sends the original value one to zero. · OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.label

label def

The cone is canonically a strict category over the walking arrow. · OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.label

label def

State label carried at a cell. · OAI.TwoWayComplementation.ChainNode.label

labelAtSlot def

Recover the optional label for a slot without choosing any distinguished label at an empty scale. · OAI.LipschitzHilbert.SourceSlopeLabels.labelAtSlot

labelBool def

Boolean indicator of one color of a labeling. · OAI.MaxCutGames.Fourier.MatrixEnergy.labelBool

labelBool def

Boolean indicator of one color of a labeling. · OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.labelBool

labelClass def

The actual canonical class of a label, supported by any diagram supporting E and containing that label's index. · OAI.PartitionConsistency.ProductForcing.labelClass

labelCongruence def

Each lattice element defines the equivalence relation of edges below its color. · OAI.FiniteCongruence.labelCongruence

labelCost def

The literal label/bin exponent, in the stage bound. · OAI.TorsionFreeZeroDivisors.StageEntropy.labelCost

labelCount def

Program-constant output alphabet size for degree d and walk length n+1. · OAI.MaxCutGames.Foundations.PCP.PoweringTables.labelCount

labelCount def

Program-constant output alphabet size for degree d and walk length n+1. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.labelCount

LabelDistribution def

This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content. · OAI.KServer.LabelDistribution

LabelDistribution def

The finite probability simplex of the available server labels. · OAI.KServer.LabelDistribution

labeledAcceptedThrough def

Accepted labels after t arrivals in the arbitrary-label model. · OAI.MatroidProphet.Labeling.labeledAcceptedThrough

labeledFreshMatch def

Full ancestry selector for a genuinely fresh path as the next color. · OAI.DilutedSpinGlass.PrescribedTree.labeledFreshMatch

LabeledHiddenRule structure

A hidden rule on arbitrary finite labels has the same online information restriction as the canonical Fin n hidden rule. · OAI.MatroidProphet.Labeling.LabeledHiddenRule

LabeledHistory abbrev

The available prefix, with arbitrary original labels. · OAI.MatroidProphet.Relabeling.LabeledHistory

labeledHistory def

The signed ordered history sum, retaining every actual old position and new branch. The terminal observable may inspect all assigned color positions. This is only an explicit finite expansion, not an assumed identity. · OAI.DilutedSpinGlass.PrescribedTree.labeledHistory

labeledHistory def

The actual observed history for an arbitrary labeled arrival order. · OAI.MatroidProphet.Labeling.labeledHistory

labeledHistory def

The history supplied by a genuine arrival stream on the original labels. · OAI.MatroidProphet.Relabeling.labeledHistory

labeledOldMatch def

Full ancestry selector for using an old unused path as the next color. · OAI.DilutedSpinGlass.PrescribedTree.labeledOldMatch

LabeledOnlineRule structure

A rule on arbitrary finite labels has exactly the same information restriction as OnlineRule: seed, initial samples, and the observed prefix. · OAI.MatroidProphet.Labeling.LabeledOnlineRule

LabeledOrder abbrev

A labeled arrival order uses arrival times Fin |E| and actual labels E. It is a bijection, so every label arrives exactly once. · OAI.MatroidProphet.Labeling.LabeledOrder

LabeledOrder abbrev

An arrival order on α lists every label exactly once. · OAI.MatroidProphet.Relabeling.LabeledOrder

labeledPairedCoordinates def

Every sample and online coordinate, indexed by original label and copy. · OAI.MatroidProphet.Relabeling.labeledPairedCoordinates

labeledUniformArrivalLaw def

The original-label arrival law is literally uniform over all enumerations. · OAI.MatroidProphet.Relabeling.labeledUniformArrivalLaw

labeledWord def

A fixed padding assignment and a tuple-class support define the symbolic word. · OAI.TwoPointCorrelations.CrudeWordCode.labeledWord

labelEquiv abbrev

Coordinate zero is the least significant bit. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.labelEquiv

labelEquiv def

Pull target raw labels back to old port coordinates; this is a bijection. · OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.labelEquiv

labelEquiv abbrev

Coordinate zero is the least significant bit. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.labelEquiv

labelEquiv def

Pull target raw labels back to old port coordinates; this is a bijection. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.labelEquiv

labelFiber def

Indices before k at which the word has label l. · OAI.QuantitativeVanDerWaerden.labelFiber

labelFiber def

The full subcategory on objects labelled by a fixed value. · OAI.Thomason.Construction.StrictOmegaCategory.labelFiber

labelFiber def

A letter fibre is exactly its empirical carrier set on this side. · OAI.TorsionFreeZeroDivisors.TypedGraphs.labelFiber

labelFiberEmbedding def

A probe profile supplies a genuine exact-fiber label, rather than merely an element of the ambient label range. · OAI.PartitionConsistency.LocalDiagramSystem.labelFiberEmbedding

labelFiberFunctor def

Fiber formation is functorial on the actual slice category. · OAI.Thomason.Construction.StrictOmegaCategory.labelFiberFunctor

labelFiberInclusion def

The inclusion of a label fiber in its ambient strict category. · OAI.Thomason.Construction.StrictOmegaCategory.labelFiberInclusion

labelFiberMap def

Every functor over the ordered label restricts to every fiber. · OAI.Thomason.Construction.StrictOmegaCategory.labelFiberMap

labelFiberSet def

The common ground subset of label indices underlying a component. · OAI.PartitionConsistency.LocalDiagramSystem.labelFiberSet

labelFiberToVertices def

Forget only the definitional description of fibre membership. · OAI.Thomason.Construction.SimplexComplex.labelFiberToVertices

labelFiberVerticesIso def

The label fibre is isomorphic to the actual full subcategory on its vertices. · OAI.Thomason.Construction.SimplexComplex.labelFiberVerticesIso

Labeling structure

Complete cell identities and vertex correspondences; compatibility includes labelled directions rather than merely equal group elements. · OAI.ArtinCAT0.TriangleMesh.Labeling

labelingCoeff def

Fourier coefficient array for a family of labelings, including color as part of the component index. · OAI.MaxCutGames.Fourier.MatrixEnergy.labelingCoeff

labelingCoeff def

Fourier coefficient array for a family of labelings, including color as part of the component index. · OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.labelingCoeff

labelLaw def

One coordinate receives label zero with the residual mass, and each of the L row labels with mass p. This does not assert independence of the rows. · OAI.TalagrandDiscreteConvexity.labelLaw

Labelled structure

Numerical Context State. · OAI.FourierLLogL.Compress.Labelled

labelledCoupling def

The actual augmented one-coordinate law, including its mixture label. · OAI.FiniteFactor.CouplingParameters.labelledCoupling

labelledFold def

Interpretation of leaf decorations by coordinate-local binary tensor. Decorations are indexed by literal bricks, not by an arbitrary ordering. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.labelledFold

labelledLeaves def

Reading the set of leaf addresses from a shape and numeric edge labels. Repeated or unordered coordinates are allowed; the true encoding is a particular subset of this unrestricted label domain. · OAI.TraceReconstruction.OccupiedParityTree.labelledLeaves

labelledPermutation def

The coordinate permutation underlying a group-labelled shift. Labels act on the left so that the operator commutes with every right translation. · OAI.KervaireMatrix.labelledPermutation

labelledShift def

A corner-labelled permutation on the actual arbitrary-group Hilbert space. · OAI.KervaireMatrix.labelledShift

labelledSimplexCocone def

This presentation lives in the finite-dimensional slice itself. · OAI.Thomason.Construction.FiniteReflectionInput.labelledSimplexCocone

labelledSimplexCocone def

The corresponding colimit cocone in the actual slice category. · OAI.Thomason.Construction.NormalizedSimplexIdentities.labelledSimplexCocone

labelledSimplexCocone_isColimit def

Forgetting labels recovers the original simplex colimit, so the lifted cocone is itself a colimit. · OAI.Thomason.Construction.NormalizedSimplexIdentities.labelledSimplexCocone_isColimit

labelledSimplexDiagram def

The simplex diagram with a fixed finite-dimensional binary label. · OAI.Thomason.Construction.FiniteReflectionInput.labelledSimplexDiagram

labelledSimplexDiagram def

Lift the oriental presentation along a fixed actual binary label. · OAI.Thomason.Construction.NormalizedSimplexIdentities.labelledSimplexDiagram

labelList def

The exact observed finite word-label list on the normalized boundary. · OAI.SmoothObstruction.WordHierarchy.labelList

labelMap def

The color synthesis operator. · OAI.SeparableQuotient.ActualSpace.labelMap

labelMass def

Six labels: zero is diagonal; the five successors retain both widths and the tag. · OAI.FiniteFactor.CouplingParameters.labelMass

labelMeasure def

Lebesgue times a fair sign; its total mass is infinite, as in the source. · OAI.PlanarL1.Threshold.labelMeasure

labelMoment def

The exact one-label branching spin moment at a real message or nested probability message. The last transition consists of independent q-spins. · OAI.DilutedSpinGlass.labelMoment

labelOutside def

The set of labels outside a specified small set. Every entry remains a literal Cohen label, and its support is the specified small set. · OAI.PartitionConsistency.ProductForcing.labelOutside

LabelPairingExpansion def

The restriction of a pairing expansion to an orthonormal alphabet. This is the concrete finite-expansion data used by the test, not an invariant classification hypothesis. · OAI.KadisonSimilarity.LabelPairingExpansion

labelPairVectors def

Difference first, coordinate direction second, so the generic maximal pair theorem applies without reordering the joint independent family. · OAI.TwoPointCorrelations.labelPairVectors

labelPolytope def

The superlevel set of every member of a finite affine family. · OAI.Problem326.Affine.labelPolytope

LabelQuotient abbrev

A genuine finitely presented intermediate quotient. The still-missing relations cannot be discarded: this quotient is not identified with the finite-table group. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.LabelQuotient

labelRelations def

The two universal label families. Other finite-table relations are not included here: in particular this is not asserted to be the evaluation kernel. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.labelRelations

labelRow def

Row j contains exactly the coordinates labeled by its successor label. · OAI.TalagrandDiscreteConvexity.labelRow

Labels structure

The four labels contributed by the four paths at a single vertex. · OAI.Problem335.Pairings.Labels

Labels def

All literal label assignments to this particular ordered shape. · OAI.TraceReconstruction.OccupiedParityTree.Labels

labels def

Coefficient inverses for the signed incidence operator. · OAI.KervaireMixing.labels

labels def

The partition labels are the actual symmetric coefficient contractions. · OAI.MetricEntropyDuality.FieldGraphSeparation.labels

labels abbrev

The literal contraction partition maps on forms of positive degree. · OAI.MetricEntropyDuality.FiniteFieldRows.labels

labels def

The binary labels of all simplices form a natural transformation. · OAI.Thomason.Construction.CosieveSimplex.labels

labels def

The binary labels of all simplices form a natural transformation. · OAI.Thomason.Construction.SieveSimplex.labels

labels def

Generator occurrences, with multiplicity and order retained. · OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression.labels

labels def

Projection to the actual labels of a fixed forced subtree. The shape selection is independent of these labels and of all random orientations. · OAI.TraceReconstruction.OccupiedParityTree.Forced.labels

labels def

The source allowed-label set, not a relaxed transition relation. · OAI.UniformKServer.EffectiveLP.labels

labelSamples def

Independent coordinate labels; the row membership events may be dependent. · OAI.TalagrandDiscreteConvexity.labelSamples

labelsEquiv def

Exact bijective partition of all actual edge coordinates into the forced binary coordinates and the genuine extra coordinates. · OAI.TraceReconstruction.OccupiedParityTree.Forced.labelsEquiv

labelSet def

The invariant set of all canonical generic labels. · OAI.PartitionConsistency.ProductForcing.labelSet

LabelsInjective def

No literal label is recorded at two different positions. · OAI.QuantitativeVanDerWaerden.RecordedSupport.LabelsInjective

labelSystem def

Label ranges form the literal system underlying the label availability ideals. Restriction is simply inclusion, not a choice of representatives. · OAI.PartitionConsistency.LocalDiagramSystem.labelSystem

labelTable def

Materialize a padded label in the common address order. · OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.labelTable

labelTable def

Materialize a padded label in the common address order. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.labelTable

labelTransport def

Coordinate transport for literal label fibers. · OAI.PartitionConsistency.LocalDiagramSystem.labelTransport

labelValidNet def

Every returned denominator, in EVERY mode, undergoes the full arithmetic check. No primality or order oracle appears in the network. · OAI.ExactQuantumFactoring.OrderTrial.labelValidNet

labelVertex def

The vertex associated to a literal available label at an extension of q. · OAI.PartitionConsistency.LocalDiagramSystem.labelVertex

LaceyLiInput def

Lacey--Li, published result 1.10 / equation (1.11), specialized to finite families in squared weak-type form (also arXiv:math/0601213v2, Theorem 1.4). C is the weak L² operator constant before squaring. · OAI.LipschitzHilbert.LaceyLiInput

ladderType def

Offspring and right-child index seen at a genuine weak ascending record. · OAI.FKCRT.TreeCoding.ladderType

lagBack def

The literal dyadic predecessor schedule of W1, padded by absent equations up to K slots. Groups restart this schedule at zero. · OAI.SmoothObstruction.WordLaw.lagBack

Lagrangian abbrev

Lagrangians are self-orthogonal subspaces, equivalently isotropic subspaces of half the ambient dimension. · OAI.SidorenkoCounterexample.Lagrangian

lagrangianConstant def

A field-independent fixed-dimension upper normalization constant. · OAI.SidorenkoCounterexample.lagrangianConstant

lambdaAbsorptionSiteEquiv def

Interleave the original and extra lambda families, leaving mu sites in their original order. · OAI.KadisonKastler.lambdaAbsorptionSiteEquiv

lambdaExit def

The same gate is used for plus and minus exits; the opposite payload space differs, but the exact plain target tag is always retained. · OAI.PureTypeSystem.ObservationValues.lambdaExit

lambdaTable def

A raw lambda table. Its body is selected by a continuing first frame; its exit operation is selected by the unique terminal frame. Gates and invalid-frame defaults can be included in these two functions. · OAI.PureTypeSystem.FreeObservations.lambdaTable

Lamp structure

Camera anchored at a jumping post. · OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp

laneMate def

All stay candidates are allowed locally; a nontransition candidate will be attached to a fresh leaf. This leaves the external degree unchanged. · OAI.OneWayLiveness.CellNetwork.laneMate

Language abbrev

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.Language

language def

Existential finite-run acceptance, allowing a run of length zero. · OAI.TwoWayComplementation.TwoNFA.language

language def

`language input` holds exactly when the entire bit list decodes to some formula and that formula has a satisfying Boolean assignment. · OAI.UniqueGamesTheorem.BinaryLanguage.language

laplaceAmplitude def

The amplitude operator for d²/dt²-1 on exp(-t) times a polynomial. · OAI.ElasticityBoundarySymbol.laplaceAmplitude

laplaceBeltrami def

Trace of the covariant Hessian, i.e. the Laplace-Beltrami operator. · OAI.HarmonicCounterexample.laplaceBeltrami

laplaceBeltrami def

The local coordinate formula det(g)^(-1/2) d_i(det(g)^(1/2) g^{ij} d_j u). The chart at the evaluation point is used, so all derivatives are taken in its open target. · OAI.YauCounterexamples.laplaceBeltrami

laplaceKernel def

The integrable two-sided exponential, with complex values. · OAI.KadisonKastler.laplaceKernel

laplaceProfile def

Scalar comparison used in the actual bridge renewal transform. · OAI.CriticalHoneycomb.RenewalInput.laplaceProfile

laplacian def

sum of squared unitary displacements. · OAI.NuclearUltrapower.laplacian

laplacianCoordinateForm def

Evaluation of the finitely many L² source coordinates defines a pointwise linear form without choosing representatives for each direction. · OAI.RegularPointCoordinates.laplacianCoordinateForm

largeCoefficient def

Explicit coefficients for converting the uniform large-prime class estimate into the form required by eventually_divisor_moment_absorption. · OAI.Problem337.DivisorMomentAbsorption.largeCoefficient

largeIndexEquiv def

Increasing list order gives a fixed, computed indexing of every large row. The same construction is used for columns. · OAI.ContingencyTables.SmallGraphProfiles.largeIndexEquiv

largeIntersectionTail def

The finite binomial upper tail used by the resampling argument. · OAI.LeanBlast.SecondKahnKalai.largeIntersectionTail

largePrimeSet def

Allowed large primes up to the real endpoint N. · OAI.JointDickman.largePrimeSet

largeStarts def

Candidate starts of suffixes whose head sum reaches the gate threshold. · OAI.ForestSpace.largeStarts

largeWeightFamily def

The generators whose weights pay directly for their cost. · OAI.TalagrandDiscreteConvexity.largeWeightFamily

lastCutChildTransport def

Child transport from the old positive end to the last vertex of the cut band. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastCutChildTransport

LastCutColumnHasGrade def

A positive endpoint column has the grade of its original child coordinate. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastCutColumnHasGrade

LastCutColumnsCompatible def

Compatibility of column coordinates at the positive endpoint of the cut band. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastCutColumnsCompatible

LastCutNewFrameCompatible def

The new positive frame has the terminal coordinates of the identified band. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastCutNewFrameCompatible

LastCutOldFrameCompatible def

The old positive frame retains its named seam coordinates after the cut. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastCutOldFrameCompatible

LastCutRowsCompatible def

Compatibility of row coordinates at the positive endpoint of the cut band. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastCutRowsCompatible

lastDigit def

Write at most one bit before the uncopied high bits. · OAI.Fifths.Bin.lastDigit

lastEndpointFirst def

Put the last endpoint first, leaving the interior list in its original order. · OAI.CoarseAssembly.Analytic.lastEndpointFirst

LastShortCanonicalNewFrameCoordinates def

The unmarked endpoint frame has terminal band coordinates. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortCanonicalNewFrameCoordinates

LastShortChildCoordinates def

The ordered child inverse of the positive short seam retains its named coordinates. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortChildCoordinates

LastShortColumnsAligned def

The terminal band port and the old positive port use the same seam columns. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortColumnsAligned

LastShortGrade def

The positive short seam retains the grades of the original child coordinates. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortGrade

LastShortLeftWordCoordinates def

Coordinates of the positive short seam's complete left word. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortLeftWordCoordinates

LastShortNewFrameCoordinates def

The new endpoint frame has the terminal coordinates of the identified band. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortNewFrameCoordinates

LastShortOldFrameCoordinates def

The old endpoint frame retains its named child coordinates. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortOldFrameCoordinates

LastShortParentCoordinates def

The parent transport of the positive short seam is the chosen cut matrix. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortParentCoordinates

LastShortRightWordCoordinates def

Coordinates of the positive short seam's complete right word. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortRightWordCoordinates

LastShortRowsAligned def

The terminal band port and the old positive port use the same seam rows. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortRowsAligned

lastVertex def

The last-vertex map Sd K ⟶ K, defined for every simplicial set. · OAI.Thomason.Construction.lastVertex

lastVertexExhaustionMap def

The last-vertex map restricted to each actual subdivision image stage. · OAI.Thomason.Construction.lastVertexExhaustionMap

lastVertexStandardSection def

Last vertex is split surjective on every standard simplex. · OAI.Thomason.Construction.lastVertexStandardSection

late def

The later part is the old deformation, with its original time parameter. · OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.late

lateEval def

Explicit finite evaluation of populations born strictly below this root. The complete prefix is retained, including the part before birth. · OAI.IntrinsicMarks.lateEval

lateEval def

Explicit finite evaluation of populations born strictly below this root. The complete prefix is retained, including the part before birth. · OAI.SignedDisk.IntrinsicMarks.lateEval

lattice def

The normalized graph in the same geometric source type. Its thresholds are inherited only to satisfy the record; all coefficient and matrix normalization theorems continue to use the literal family definition. · OAI.ContinuumCoulomb.SourceNormalizedSpectrum.lattice

lattice def

The old pair relation with the scalar action on its second factor twisted. Alpha-annihilation of the old edge is what makes this an R-submodule. · OAI.KLInvariance.ReflectionPairTranslation.lattice

LatticeCover structure

Actual discrete full-rank lattice coverings; no assumed density theorem. · OAI.CoveringOrder.LatticeCover

latticeEnergy def

The full nonzero-lattice energy, allowing a divergent series. · OAI.AtomicTriangular.latticeEnergy

latticeInSaturation def

The original lattice inside its maximal-order span. · OAI.DukePrimeDegree.latticeInSaturation

LatticeMachineHaltingUndecidable def

Ragged finite tables, stopping at the first absent instruction. · OAI.ForcedComputation.LatticeMachineHaltingUndecidable

latticeMajorant def

The geometric majorant for weights at the integers around a chosen center. · OAI.Problem335.latticeMajorant

LatticeModel def

Exact affine lattice template. The uniform bound retains finitely many centers. · OAI.RuledApproximation.LatticeModel

latticeOrbitStabilizer def

Integral elements whose conjugates lie in the given actual orbit group. These are precisely its lattice stabilizer in matrix coordinates. · OAI.DukePrimeDegree.latticeOrbitStabilizer

latticePoint def

An invertible row basis determines a covolume-one lattice. · OAI.DukePrimeDegree.latticePoint

LatticeSpace abbrev

The unimodular lattice space, with its quotient topology. · OAI.DukePrimeDegree.LatticeSpace

latticeStabilizerMatrix def

The rational matrices of the actual integral orbit stabilizer. · OAI.DukePrimeDegree.latticeStabilizerMatrix

latticeVector def

An integer lattice vector in the Euclidean cover. · OAI.CubicTorus.latticeVector

launch def

Length-uniform placement of the completed runtime-modulus list sampler. · OAI.ExactQuantumFactoring.PhysicalListSlots.launch

launchBatch def

Launch all new active keys at one interface, reserving a pair immediately before proceeding to the next key. Retained keys are supplied in C. · OAI.BoundedTreewidthL1.ParticleBatch.launchBatch

launchWork abbrev

Runtime-modulus launch of the entire raw split. The circuit description contains n only, never the input integer, its prime factors, or true orders. · OAI.ExactQuantumFactoring.FixedSplit.launchWork

laurent def

A finite Laurent polynomial in the actual twist Koopman operator. · OAI.ThreeTorus.ColoredState.laurent

laurentCoefficientMap def

Actual Laurent-coefficient extraction at radius one is a linear map on the existing analytic automorphic-section space. · OAI.Nagata.W09.laurentCoefficientMap

laurentExponent def

The exact exponent, before distributing the factor n inside the quotient. · OAI.Nagata.W08.laurentExponent

laurentProductCoefficient def

Coefficient of z^r in the two Laurent polynomials supported on [-K,K]. The finite indices enumerate each Laurent exponent exactly once as i-K. · OAI.FiniteFactor.laurentProductCoefficient

Law abbrev

A finite real lottery; list entries need not have distinct outcomes. · OAI.CliqueFreeIndependence.Lottery.Law

Law structure

Explicit rational finite probability law. The weighted test below is a finite rational graph construction, not an oracle distribution. · OAI.OptimalMaxCut.LongCode.Law

law def

The finite integer weights sum to |A|*Q; all truncations are exact because the ordinary law is pointwise dominated by the uniform law. · OAI.ContingencyTables.IntegerResidualCorrection.law

law def

Independent retention with parameter p ∈ [0,1] of each labelled bond. · OAI.CriticalPercolation.BondGraph.law

law def

The push-forward of the uniform law on all independent fair coin tapes. · OAI.CubeShuffle.law

law def

The manuscript's original, unnormalized-on-retained-pairs law. All zero-mass cells contribute zero; no conditional renormalization is used. · OAI.SmoothObstruction.PairLaw.law

law def

Literal normalized Lebesgue restriction. It is proved to be a probability measure below under the finite-volume model hypotheses. · OAI.TriangularSurface.FiniteModel.law

LawCutoffs structure

The two actual smooth cutoffs used by the manuscript's quantile construction. · OAI.ThreeTorus.LawCutoffs

lawOfCoefficients def

Every block decomposition is a finite probability law, with its unused mass placed on the zero atom. · OAI.DiamondDistortion.SegmentSystem.lawOfCoefficients

layer abbrev

The jth supported quotient of the ideal-image filtration. · OAI.ActualCartier.layer

layer def

A rectangular vector layer still charges every scalar gate separately. · OAI.ExactFourier.LinearDAG.layer

layer def

The half-open radial layer of the source. Its connected components, not components of the ambient graph, are the cell column sets. · OAI.PlanarL1.Columns.Model.Point.layer

layer def

The ordered-layer construction for a specified primitive-text group. · OAI.Superstring.Hierarchical.Threading.layer

LayerAdapted def

A function of the revealed layers only. · OAI.CubeShuffle.LayerAdapted

layerBlocks def

The consecutive blocks of the matrix-layer index list. · OAI.Problem335.layerBlocks

LayerCertificate structure

Exactly the information needed from one recursively constructed type family. The zero type is the constant baseline; positive types have normalized offset -1. No continuity of offsets or tolerances is assumed. · OAI.Problem326.Affine.LayerCertificate

LayerCollection structure

Finite ordered primitive-text groups supplied by the fixed base decomposition. All fields describe actual layers, never connecting walks. · OAI.Superstring.Hierarchical.LayerCollection

layerCover def

An ambient ideal power of the original lattice surjects onto each corresponding layer of its quotient. · OAI.ActualCartier.layerCover

layerDepth def

The unique depth of the layer assigned to a column. · OAI.PlanarL1.Columns.Model.Point.RadialTree.layerDepth

Layered inductive

Exact-width mixed rounds. Monomial rounds are counted, not silently free scalar multiplications. Disjoint parallel blocks share a round. · OAI.ExactFourier.Layered

LayeredTrail structure

The child-seam graph of a half-band: internal seams have distinct ends and strictly increasing layer. This will be constructed from the literal whole- port gallery below, not requested as a lower-diagram hypothesis. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail

LayerId abbrev

Stable IDs for every sorted primitive layer of the exact base threading. · OAI.Superstring.Hierarchical.Threading.LayerId

layerLabels def

The four edge coordinates in a layer of endpoint-fixed paths. · OAI.Problem335.MomentPairing.layerLabels

layerLabels def

The four layer coordinates of endpoint-fixed paths. · OAI.Problem335.Pairings.layerLabels

layerNodeCount def

Nodes at physical descent exactly j. · OAI.EditApproximation.DependencyExpansion.layerNodeCount

LayerOK structure

Properties proved later in the scalar estimates and used in abstract layer lemmas · OAI.GeneralMahler.Profile.LayerOK

layerProjection def

Restrict a finitely supported coordinate vector to one matrix layer. · OAI.Problem335.Pairings.layerProjection

layerQuotient def

The quotient morphism on the Cartier divisor. · OAI.ActualCartier.layerQuotient

Layers abbrev

Amplification axes. First come all m groups whose f-bit digit is indexed by one of α. These are followed by r spectator axes. · OAI.PowerSaving.Binary.Layers

layers def

Successive quotients selected by images of the ideal action. · OAI.CartierImageFiltration.layers

layerSequence def

Canonical image/cokernel sequence of the ideal action. · OAI.CartierImageFiltration.layerSequence

layerShift def

A signed coordinate in every layer, as used by the mixed IMM operator. · OAI.Problem335.Pairings.layerShift

layerUnion def

The union of all types, numbered from zero through d - 1. · OAI.Problem326.Affine.layerUnion

layerVariableEquiv def

Layer-restricted IMM variables are a product of selected layers and matrix entries. · OAI.Problem335.LowerParameters.layerVariableEquiv

layerWeight def

Normal pairings retain their coordinate-coincidence factor. Diagonal pairings retain the assigned constant even after their inequality is dropped. · OAI.Problem335.MomentPairing.layerWeight

Layout abbrev

Gather's table/query/scan/scratch and coordinate tapes; then radix, two Horner accumulators, counter, scratch, isolated field output, global output. · OAI.MaxCutGames.Explicit.MachineProductField.Layout

Layout structure

The combinatorial output of a planar tree contour construction. No metric realization or metric estimates are part of this data. · OAI.PlanarL1.HeightTree.Layout

Layout abbrev

Gather's table/query/scan/scratch and coordinate tapes; then radix, two Horner accumulators, counter, scratch, isolated field output, global output. · OAI.UniqueGamesTheorem.Explicit.MachineProductField.Layout

layoutTime def

Rokhlin's multiple-mixing problem asks whether ordinary mixing of one invertible probability-preserving transformation implies mixing of every finite order. The formalization proves this implication. For each $k\ge3$ and every $k$ … · OAI.Rokhlin.layoutTime

lazyChoice def

A causal minimum-matching choice. Repeated actual and virtual positions are retained: only the permutation of occurrence labels is used. · OAI.KServer.lazyChoice

lazyFallback def

A null-history fallback that satisfies strong laziness at every history. · OAI.KServer.HiddenMachine.lazyFallback

lazyMachine def

Source's matching simulation, with the entire virtual private state kept. There is no illegal conditioning of a marginal coupling on realized ancestors. · OAI.KServer.HiddenMachine.lazyMachine

LazyPath inductive

Endpoints of complete strongly lazy paths, with no cap imposed in the relation. · OAI.UniformKServer.LazyPath

lazyPorts def

False/stay ports occupy rows 0,...,d-1; true/move ports occupy rows d,...,2*d-1, before the vertex offset is added. · OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts

lazyPorts def

False/stay ports occupy rows 0,...,d-1; true/move ports occupy rows d,...,2*d-1, before the vertex offset is added. · OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazyPorts

LazyStep def

The source's strongly lazy rule: a hit changes nothing; a miss chooses exactly one label and counts one positive move. · OAI.UniformKServer.LazyStep

LazyTrace def

Pathwise strong laziness, imposed only on the trace actually selected. · OAI.KServer.Episode.LazyTrace

lblP def

m-letter block of joint letter-and-context pairs, iid. · OAI.FourierLLogL.Compress.lblP

lcs def

The length of a longest arbitrary common subsequence. · OAI.TreeEdit.lcs

lead def

act on lead coordinates with parameter other pair fixed. aff=true includes translations · OAI.ExactDerandomization.Analysis.Affine.lead

leading def

The leading old coefficient of the normal form. · OAI.PartitionConsistency.MergerAlgebra.Word.leading

leadingBarSequence def

The actual sequence of two-sided X bars, ending in one leading free D bar. · OAI.DerivedBar.leadingBarSequence

leadingBase def

Raise the first block length. · OAI.DerivedBar.Multibar.leadingBase

leadingModuleCoordinates def

The degreewise tensor-block isomorphism for the actual recursive leading total. · OAI.DerivedBar.RecursiveTotal.leadingModuleCoordinates

leadingParameterMap def

The leading parameter map in equation nl:leading-expansion. · OAI.DefocusingNLS.leadingParameterMap

leadingPattern def

Leading internal D slots; the exterior D coefficient is kept separate. · OAI.DerivedBar.RecursiveTotal.leadingPattern

leadingSummandIso def

The source tensor D ⊗ D^i₀ ⊗ X ⊗ ... ⊗ D^iᵣ ⊗ Z^q, with every field scalar action and every exterior D action checked. · OAI.DerivedBar.RecursiveTotal.leadingSummandIso

leadingTotalEmbedding def

The exterior D bar is assembled on its actual finite totalization diagonal. · OAI.DerivedBar.ParityBridge.leadingTotalEmbedding

Leaf def

A leaf label is a vertex, not its sampled spin value. · OAI.DilutedSpinGlass.PrescribedTree.Leaf

Leaf abbrev

A terminal path. This is definitionally a list with the required length. · OAI.Problem310.FiniteTableModel.Leaf

Leaf abbrev

The finite leaf set, represented by ordered paths of exactly k edges. · OAI.TreeEdit.BinaryLower.FiniteTree.Leaf

leaf def

The actual identity leaf, with every symbol vector used once as noise. · OAI.MaxCutGames.Gadget.ActualGadget.leaf

leaf def

The actual identity leaf, with every symbol vector used once as noise. · OAI.UniqueGamesTheorem.Gadget.ActualGadget.leaf

leafBackgroundSize def

The two leaves split each child's background with at most half an item of error, because the remainder is assigned to the second leaf. · OAI.LowSpaceSubsetSum.leafBackgroundSize

LeafBound def

Every supplied emitter leaf obeys its local time allowance. There is no whole-loop runtime premise at any internal node. · OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.LeafBound

LeafBound def

Every supplied emitter leaf obeys its local time allowance. There is no whole-loop runtime premise at any internal node. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.LeafBound

leafCoefficientSet def

The scalars actually occurring at a leaf. · OAI.Problem335.leafCoefficientSet

leafColModes def

The two possible modes for a shared leaf column. · OAI.Problem348.ModeIncidence.leafColModes

leafCoordinate def

Insertion into one factor of the manuscript's product of cyclic groups. · OAI.TreeEdit.BinaryLower.FiniteVectors.leafCoordinate

leafCount def

Counts use the original branching structure, independent of assignments. · OAI.Ostmann.BranchingWordHistory.leafCount

leafDecoder def

Decode an actual leaf path. The fallback only totalizes this function on paths of the wrong length; the root construction never evaluates that branch. · OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder

leafEquiv def

The list-path and function-path presentations of the same leaf set. · OAI.TreeEdit.BinaryLower.FiniteTree.leafEquiv

leafExtension def

Adding finitely many new leaves to one vertex; no geometric or metric conclusion is included in this graph definition. · OAI.PlanarL1.Topology.leafExtension

leafM def

synchronization for a reel at every axis · OAI.PowerSaving.Grove.leafM

leafModuli def

The terminal integer moduli, with the same pivot divisions and child order as the full recursive coefficient. · OAI.Ostmann.MovingSlotData.leafModuli

leafParent def

Parent and private index give an injective description of leaf-coded vertices. · OAI.WLIdentification.leafParent

leafPins def

The entire e-field, in all branches, is pinned in the leaf count. · OAI.HyperbolicObstruction.StarModel.leafPins

leafPolynomials def

Polynomial extension in one free top coordinate. Its coefficients may contain reciprocals of the fixed frequency and compensation products. · OAI.Ostmann.MovingSlotData.leafPolynomials

leafProduct def

Every descendant leaf receives the same one-site terminal observable, with its own sampled path. · OAI.DilutedSpinGlass.PrescribedTree.leafProduct

leafRank def

Terminal logical rank along the actual recursively sampled path. The final uniform symbol is ignored by this rank function. · OAI.MaxCutGames.Gadget.Descent.leafRank

leafRank def

Terminal logical rank along the actual recursively sampled path. The final uniform symbol is ignored by this rank function. · OAI.UniqueGamesTheorem.Gadget.Descent.leafRank

leafRowModes def

The four possible modes for a shared leaf row. · OAI.Problem348.ModeIncidence.leafRowModes

leafSum def

Sum of the terminal marks, retaining multiplicity of equal sampled paths. · OAI.DilutedSpinGlass.PrescribedTree.leafSum

leafSum def

Unweighted finite sum over every possible terminal continuation. · OAI.SignedRuns.leafSum

leafValue def

The actual groupoid interpretation of a whole permutation of leaves. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue

leafValues def

A total extension of the specified distinct leaf values. The filler only occupies other field names and plays no part in the pinned statistic. · OAI.HyperbolicObstruction.StarModel.leafValues

leafWeight def

A distribution over entire leaf-test tables, not random bits added to the cube. · OAI.SquareRootDegree.FiniteRounding.leafWeight

Learner structure

A finite-state one-pass procedure. The Boolean true means stop. All indices are prescribed ordinary sample indices, not stored real registers. · OAI.SubsphereRegression.Learner

least def

First successful bounded index. All searches are expanded into finite counter loops, so the certificate does not postulate a search operation. · OAI.OptimalMaxCut.CounterMachine.Expr.least

leastBound def

The first distinguishing bound in the fixed ordinal ordering. The proof of existence is an input only to this definition, not to its application to countable germs in distinguished_bound. · OAI.PartitionConsistency.TailSelector.TailData.leastBound

leastCode def

The least code is chosen in a single fixed wellordering of the set of all chain codes, not a fresh ordering at each filter. · OAI.PartitionConsistency.ProductForcing.ChainCode.leastCode

leastCodeOrderIso def

The order-isomorphism form of least-code-covariance. · OAI.PartitionConsistency.ProductForcing.ChainCode.leastCodeOrderIso

leastDistortion def

The infimum over injective maps to real absolutely summable sequences. · OAI.EditDistortion.leastDistortion

leastDivisorIn def

A distinguished component can be tested by polynomially many pairwise comparisons, without constructing the least prime factor of an unknown N. · OAI.ExactQuantumFactoring.leastDivisorIn

LeastValue def

The index is the least possible index of this value. Negative equality with every earlier entry is forced, not merely unforced at this condition. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.LeastValue

Leaves abbrev

Leaf indices stay in the small universe, even for large colour sets. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Leaves

leBody def

Binder i:P_X for le(i,x). · OAI.PureTypeSystem.Labelled.RelationalCode.leBody

Ledger abbrev

records of x indexed by opposite pin plan signs · OAI.HadwigerCounterexample.Ledger

ledger def

Marked points pay the unfinished part of the current block; completed blocks pay their endpoint as well. This potential prevents a charge per raw request, even when an epoch is arbitrarily long. · OAI.UniformKServer.Fallback.ledger

Left inductive

The reversed left side tested from I: workspace, C, then anchors. · OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Left

Left abbrev

Original vertices and the middle vertices q_e. · OAI.MaxCutGames.Explicit.Subdivision.Left

Left abbrev

Original vertices and the middle vertices q_e. · OAI.UniqueGamesTheorem.Explicit.Subdivision.Left

left def

Run a procedure on the first component, keeping the second component literally on a disjoint stack. Parsing and re-quoting are explicitly charged. · OAI.ExactQuantumFactoring.BitStackProgram.Procedure.left

left def

Left multiplication on a bimodule, regarded as a right-linear map. · OAI.ExternalTensor.Section4.ArrowVertex.left

left def

L(a) δ_x = δ_(ax) including infinite and uncountable groups. · OAI.KervaireRegular.left

left def

Normalized Hecke multiplication: H_s² = 1 + a H_s. · OAI.KLInvariance.Hecke.left

left def

Unnormalized equal-parameter Hecke multiplication, T_s²=q+(q−1)T_s. · OAI.KLInvariance.HeckeQ.left

left def

Surjective projection to the untwisted (lower) stalk. · OAI.KLInvariance.ReflectionPairTranslation.left

left def

The left endpoint of a literal interval in [0,1). · OAI.QuantitativeVanDerWaerden.UniformMesh.left

left def

Forget the disjoint summand tag from a walk in the left component. · OAI.Release075.SumWalk.left

left def

The left globe supplies the chosen representatives of shared faces. · OAI.Thomason.Construction.PastingGlobeBasis.left

leftAction def

Bounded left multiplication extended to the actual Hilbert completion. · OAI.Generator.Tracial.leftAction

leftAction def

Left composition lifts a bounded coefficient to the Banach space of operators. · OAI.HarmonicCounterexample.LinearODE.leftAction

leftAction def

The left coefficient action is induced from the first balanced-tensor factor. · OAI.LittleFinitistic.BalancedTensor.leftAction

leftAction def

The left B tensor C action takes values in actual right-B-linear maps. · OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.leftAction

leftAppend def

Append a fixed path on the left. · OAI.Thomason.Construction.PathSpace.leftAppend

leftAppendEquiv def

Concatenating a fixed path on the left is a homotopy equivalence. · OAI.Thomason.Construction.PathSpace.leftAppendEquiv

leftAxis def

Every unit axis reflection has an explicit left-quaternion lift. · OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.leftAxis

leftBaseInTime def

Left query-block base from the preserved variable tuple rank and a zero offset field. · OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.leftBaseInTime

leftBaseInTime def

Left query-block base from the preserved variable tuple rank and a zero offset field. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.leftBaseInTime

leftBracket def

The outer pair of the left-associated composite. · OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.leftBracket

LeftBranch def

Parametrization of the left copy of C(a,h). · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch

leftCancellation def

Cancelling a path and its reverse on the left, uniformly in the remaining path. · OAI.Thomason.Construction.PathSpace.leftCancellation

leftCoefficient def

Exact rescaling used in coefficient-sequences; neither sequence is required to belong to ℓ². · OAI.FiniteFactor.leftCoefficient

leftContactStripSite def

Left-path internal sites and its central endpoint satisfy the common length-17 strip bounds. · OAI.ContinuumCoulomb.leftContactStripSite

LeftDivOrder def

The underlying monoid, equipped with the left-divisibility order below. · OAI.PartitionConsistency.DiagramOrder.LeftDivOrder

leftEntry def

The matrix unit in the first tensor factor, with identity on the second. · OAI.Generator.Bell.leftEntry

leftGivenRight def

The fallback exists even when the question types were not supplied with Nonempty instances: it is a marginal of the game's actual probability law. · OAI.MaxCutGames.Repetition.leftGivenRight

leftGivenRight def

The fallback exists even when the question types were not supplied with Nonempty instances: it is a marginal of the game's actual probability law. · OAI.UniqueGamesTheorem.Repetition.leftGivenRight

leftIdeal def

The actual principal left ideal B e, the image of right multiplication by e. · OAI.ExternalTensor.leftIdeal

leftIndex def

Index of a coordinate in the prefix. · OAI.Problem358.FinitePrefix.leftIndex

leftInv def

Inverse normalized Hecke generator, available without inverting any scalar. · OAI.KLInvariance.Hecke.leftInv

leftInvariantDistance def

The bounded supremum over all left translations of a given metric. · OAI.PolycyclicRecognition.leftInvariantDistance

leftInvariantMetric def

The left-invariant metric with exactly the original topology. · OAI.PolycyclicRecognition.leftInvariantMetric

LeftLabel abbrev

The valid left labels and projection maps give the concrete Label Cover presentation. Their alphabet depends on the clause, with at most 8 bit triples. · OAI.MaxCutGames.Foundations.PCP.LeftLabel

LeftLabel abbrev

The valid left labels and projection maps give the concrete Label Cover presentation. Their alphabet depends on the clause, with at most 8 bit triples. · OAI.UniqueGamesTheorem.Foundations.PCP.LeftLabel

leftLayer def

The layer immediately left of an internal vertex. · OAI.Problem335.BalancedSchedule.leftLayer

leftMap def

The actual left-factor map on the bar's balanced quotient. · OAI.DerivedBar.BimoduleTensor.leftMap

leftMap def

The first rational-function copy, in the independent left variables. · OAI.EuclideanRamsey.IndependentTensor.leftMap

leftMap def

The first local map fixes the common input basis. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftMap

leftMap def

The remaining part of the left surjection is its literal restriction. · OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftMap

leftMap def

The remaining part of the left surjection is its literal restriction. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftMap

leftMulPreTrace def

Bounded left multiplication with the L² norm, proved from positivity. · OAI.TraceConeClassification.ExtendedTrace.leftMulPreTrace

leftMultilinear def

Descend the right-hand family of the normalized permanent. · OAI.Problem346.PairingConstruction.leftMultilinear

leftMultiply def

An element of e'Ae acts by left multiplication on the right projectives. · OAI.LittleFinitistic.IdempotentTensor.leftMultiply

leftOccupancyDeviation def

Occupancy deviation at the left site. · OAI.ContinuumCoulomb.leftOccupancyDeviation

leftOuterSlice def

The negative outer cell of the sharpness map, with all ties assigned centrally. · OAI.Problem358.SharpSlice.leftOuterSlice

leftRangeEquiv def

The first factor, regarded as its actual coordinate subspace. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.leftRangeEquiv

leftRangeEquiv def

The first factor, regarded as its actual coordinate subspace. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.leftRangeEquiv

leftRegular def

Left regular operators U_g commute with the right regular operators. · OAI.Dixmier.leftRegular

leftRegular def

The actual left regular translation λ(g)η(x)=η(g⁻¹x). · OAI.Generator.FreeConvolution.leftRegular

leftRegular def

The left regular representation by bounded operators. · OAI.TorsionFreeBass.Regular.leftRegular

leftRegular abbrev

The left regular operator, constructed on every square-summable vector. · OAI.UltrapowerBridge.leftRegular

leftSpace def

The vertex part eN, without assuming e is central. · OAI.LittleFinitistic.IdempotentTensor.leftSpace

leftSpectralCut def

The high left spectral cut of an element of the normal algebra. · OAI.KadisonSimilarity.leftSpectralCut

leftSphere def

The two sphere factors, in self-dual / anti-self-dual plane coordinates. · OAI.ArnoldCounterexample.Factors.leftSphere

LeftTensor def

A tensor retaining the left action of the middle bimodule. · OAI.LittleFinitistic.LeftTensor

leftTensor def

The left retained branch, still in the common ambient coordinate spaces. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor

leftTensorFunctor def

The finite signed total is functorial in the genuine bimodule complex too. · OAI.LittleFinitistic.BimoduleTotal.leftTensorFunctor

leftTensorNat def

An augmentation of bimodule complexes induces this concrete natural transformation. · OAI.LittleFinitistic.BimoduleTotal.leftTensorNat

leftTensorVector def

Insert a fixed vector in the first tensor leg. · OAI.KadisonKastler.leftTensorVector

leftTermMap def

The actual tensor map induced by a bimodule-complex morphism in each bidegree. · OAI.LittleFinitistic.BimoduleTotal.leftTermMap

leftTotalFunctor def

Fixed-input finite tensor total as an actual functor on bimodule complexes. · OAI.LittleFinitistic.BimoduleTotal.leftTotalFunctor

leftTotalMap def

Tensoring an actual bimodule chain map gives an actual B-linear total chain map. · OAI.LittleFinitistic.BimoduleTotal.leftTotalMap

leftTranslate def

Left translation on the actual ambient cube chains. · OAI.EilenbergGanea.LevelBasis.leftTranslate

leftTranslate def

A left translate, expressed as a measurable preimage. · OAI.PolycyclicRecognition.leftTranslate

leftTranslationHom def

Left translations form a unitary representation, with the ample coefficient space unchanged. · OAI.CoarseAssembly.leftTranslationHom

leftUnitHomotopy def

The left unit law follows by reversing the continuous right unit homotopy. · OAI.Thomason.Construction.PathSpace.leftUnitHomotopy

leftUnitIso def

Tensoring the structure sheaf is canonically the identity, not a postulated operation on formal Chern data. · OAI.ActualSheafTensor.leftUnitIso

leftY def

Embed the left second-leg interval. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftY

leftZ def

Embed the left third-leg interval. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftZ

leg abbrev

The continuous map from an original topological simplex to realization. · OAI.Thomason.Construction.RealizationPrism.leg

leg def

Each original diagram object maps by an actual strict functor. · OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.leg

Legal def

Legality is relative to the exact immutable preceding prefix. · OAI.ReflexiveFixedPoints.CandidateContext.Legal

Legal def

Every level boundary carries a legal word; the sign convention records the index of the origin inside its word, exactly as in source section 6. · OAI.SmoothObstruction.PhaseDynamics.Legal

LegalAt def

A legal phase-marked bilateral sequence, with no restriction at window endpoints; adjacent words are allowed to be identical. · OAI.SmoothObstruction.RecognitionWindow.LegalAt

LegalFinitePath def

A finite path with its original finite-stage children. · OAI.SeparableQuotient.ActualSpace.LegalFinitePath

legalTranslate def

Only local nonemptiness is used here; no simultaneous solution is presumed. · OAI.WLIdentification.AffineBlocks.legalTranslate

legLambda def

The genuine fixed diagonal scalar coefficient. · OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.legLambda

LegPermutation abbrev

A permutation of the three tensor legs. · OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation

legU def

ACTUAL complete-leg columns with the physical schedule. · OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.legU

length def

`x.length` is exactly the length of `x.encode`, including the representation tag and all framing bits. · OAI.AlgorithmicThinTrees.Input.length

length def

Count each actual symbol, returning a unary length. · OAI.ExactQuantumFactoring.BitStackProgram.Procedure.length

length def

Number of new letters, used to distinguish old from genuinely new words. · OAI.PartitionConsistency.MergerAlgebra.Word.length

length def

Source length: sum of the lengths of vertical segments, with switches free. · OAI.PlanarL1.Columns.Model.Path.length

length def

Length of an incoming window whose parent has height h + 1. The value at height zero is unused and is set equal to the threshold. · OAI.Problem310.WindowRecursion.length

lengthAt def

The length function consumed by the canonical numeric placement API. · OAI.Problem310.WindowMetadata.lengthAt

lengthAt def

Extract a window length from a finite preorder list, using zero outside the list. · OAI.Problem310.WindowPlacement.lengthAt

lengthBall def

Balls for a left-invariant length function. · OAI.PolycyclicRecognition.lengthBall

lengthDifferenceConstant def

Explicit fixed-order smoothing constant; no asymptotic hypothesis is hidden. · OAI.TraceReconstruction.lengthDifferenceConstant

lengths def

Actual window lengths, in the finite tree preorder. · OAI.Problem310.WindowConstruction.lengths

lengths def

Window lengths in precisely the canonical tree-edge preorder. · OAI.Problem310.WindowMetadata.lengths

lengthTwo def

Includes a length-two residue class as the 0-to-2 component. · OAI.LittleFinitistic.QuadraticEncoding.lengthTwo

Lens structure

analyzing scalar path with a chosen signed component · OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens

LensProperty def

The exact separated approximate-midpoint estimate proved for the target space. · OAI.ForestSpace.Diamond.LensProperty

LepingleInput def

Lépingle's unweighted scalar L² bound for 3-variation. The constant is uniform in the probability space, the filtration, and the finite horizon. · OAI.LipschitzHilbert.LepingleInput

Letter abbrev

p even basis symbols followed by p odd ones, exactly E⊕O in05. · OAI.CoordinateSweeps.SignedTensor.Letter

Letter inductive

There are no vertex-identity letters. zero is the absorbing letter. · OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter

Letter abbrev

The fixed six-letter alphabet in the algebra construction, in the order u,v,u⁻¹,v⁻¹,e₀,e₁. · OAI.FiniteAlgebraicEnvelopes.PartialAffine.Letter

letter def

The letter at a specified finite stage. Distinct stage elements need not have distinct images. · OAI.PartitionConsistency.ProbeAlgebra.Path.letter

letterAct def

Prepending a letter performs its only possible front reduction. · OAI.PartitionConsistency.ProbeAlgebra.Word.letterAct

LetterCycles₂ def

The exact algebraic cycle space whose sphere producer is needed. · OAI.HyperbolicObstruction.ConeSkeleton.LetterCycles₂

letterError def

A fixed integer loss shared by all comparison sides. · OAI.TorsionFreeZeroDivisors.GridAsymptotics.letterError

letterFloor def

The supremum of the heights of all old divisors of a new letter. · OAI.PartitionConsistency.ProbeAlgebra.Path.letterFloor

letterGrade def

Additive grade on literal words. The head and boundary letters each have grade one, while all cell-tag data is ignored by a supplied base grade. · OAI.FiniteAlgebraicEnvelopes.Compiler.Path.letterGrade

letterGroupCover def

A fully constructed cover target for the actual letter quotient. Its relation equations are theorems, not assumptions of the chain conclusion. · OAI.HyperbolicObstruction.ConeSkeleton.letterGroupCover

letterIdeal def

The old first-letter divisors are a bounded ideal of the old monoid. · OAI.PartitionConsistency.ProbeAlgebra.Path.letterIdeal

Letters abbrev

The direct-limit letters [x,i] of the probe normal forms. · OAI.PartitionConsistency.ProbeAlgebra.Path.Letters

letters def

Finite coding of a normal form; only the existing coefficient and finitely many quotient letters are needed. · OAI.PartitionConsistency.MergerAlgebra.Word.letters

lettersMap def

Map the actual, potentially non-injective direct limits. · OAI.PartitionConsistency.ProbeAlgebra.Path.lettersMap

letterVoltage def

The actual original marked presentation supplies the deck labels, via fixed fan routes; the larger auxiliary polygon bouquet group is not used. · OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage

level def

A level is a list, not a set: multiplicities of occurrences are retained. · OAI.ExactQuantumFactoring.AuxiliaryTree.level

level def

The least geometric level covering a requested size. Nat.clog is the ordinary finite ceiling logarithm algorithm. · OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.level

level def

A geometric scale, kept in logarithmic coordinates. · OAI.Problem337.ResidueLevels.level

level def

The least geometric level covering a requested size. Nat.clog is the ordinary finite ceiling logarithm algorithm. · OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.level

levelBoundary def

The connecting boundary on a crossing square is the difference of its two height-zero vertices. · OAI.CubicalChains.LevelExact.levelBoundary

levelCoordinates def

Replace the k-th coordinate by the potential itself. · OAI.MahlerStokes.levelCoordinates

levelCount def

Number of vertices at a given distance below the root. · OAI.TraceReconstruction.OccupiedParityTree.levelCount

levelExtension def

Assemble the retained positive children, in their original parent order. · OAI.ReflexiveFixedPoints.CandidateContext.levelExtension

levelLoopInTime def

Every body is the already constructed actual resize run. There is no whole-loop, body-trace, or computational-correctness premise. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.levelLoopInTime

levelLoopInTime def

Every body is the already constructed actual resize run. There is no whole-loop, body-trace, or computational-correctness premise. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.levelLoopInTime

levelMinimum def

The minimum of all actual budgets at positive depth k+1. · OAI.ReflexiveFixedPoints.OrderedTree.levelMinimum

levelPrefix def

The literal immutable history preceding a candidate in the full level. · OAI.ReflexiveFixedPoints.CandidateContext.levelPrefix

levelPrefixInclusion def

The prefix indices are the corresponding initial candidate ordinals. · OAI.ReflexiveFixedPoints.CandidateContext.levelPrefixInclusion

levelRecord def

Decode the actual concatenated ordinal into its originally chosen record. · OAI.ReflexiveFixedPoints.CandidateContext.levelRecord

levels def

Remaining number of bits in nats · OAI.FourierLLogL.Dyadic.Procedure.levels

levels def

Only the radial layers meeting a column occur. No infinite layer family or arbitrary cut-off is added to the finite random step. · OAI.PlanarL1.Columns.Model.BandTrees.levels

levelSet def

The strict superlevel set at the lower endpoint of a positive layer. · OAI.ThompsonNonamenability.FiniteLevelChain.levelSet

levelsLE def

Every internal composition level is at most the given bound. · OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression.levelsLE

levelStates def

Successive parents share the complete chronological candidate history. · OAI.ReflexiveFixedPoints.CandidateContext.levelStates

levelValue def

The original mixture at one ball radius. · OAI.MetricEntropyDuality.CompressionLevels.levelValue

Liaison structure

A reserved opaque motion; synaptic grab may also return "no". (motion called only at address clock=0; enclosing data operations strip their shot clock while keeping bounded record). · OAI.ExactDerandomization.Arena.Pier.Liaison

LiDualityInput def

Li, Corollary 4.48, integral Poincaré duality transfer with both finite cohomological dimension hypotheses retained. · OAI.PolycyclicRecognition.LiDualityInput

lieAlgebraOfBilinear def

The bracket is compatible with the original real vector-space structure. · OAI.PolycyclicRecognition.lieAlgebraOfBilinear

LieMinimizingMetricInput def

Precisely the metric specialization of the cited published results; there is no height, quasi-isometry, or recognition assertion in this input. · OAI.PolycyclicRecognition.LieMinimizingMetricInput

LieModularExponentialInput def

The scalar specialization of Knapp's modular and exponential identities, for the intrinsic exponential characterized in this project. · OAI.PolycyclicRecognition.LieModularExponentialInput

liePiEval def

Coordinate projections of the genuine direct-product Lie algebra. · OAI.HarmonicCounterexample.Control.liePiEval

lieQuotientAutomorphism def

An automorphism preserving an ideal in both directions induces an actual Lie equivalence on the quotient. · OAI.PolycyclicRecognition.lieQuotientAutomorphism

LieRiemannianMetricInput def

Only the tangent-space global coordinates used by the application are retained from the general Riemannian local length comparison. · OAI.PolycyclicRecognition.LieRiemannianMetricInput

lieRingOfBilinear def

A bilinear bracket satisfying alternation and Jacobi gives the ordinary Lie ring structure on the existing additive group. · OAI.PolycyclicRecognition.lieRingOfBilinear

LiFinitenessInput def

Li, Corollary 4.47, specialized to integral coefficients and finitely generated groups. The choice of left coarse structure is changed to Li's right coarse structure by inversion. · OAI.PolycyclicRecognition.LiFinitenessInput

Lift structure

A linear lift of a logical character subspace to the actual stage input. · OAI.MaxCutGames.Gadget.Lift

Lift structure

The actual group-coordinate lift of every boundary occurrence. Rotation and paired sides share the prescribed endpoint in the Cayley one-skeleton. · OAI.TorsionFreeZeroDivisors.PictureChains.Lift

Lift structure

A linear lift of a logical character subspace to the actual stage input. · OAI.UniqueGamesTheorem.Gadget.Lift

lift def

Lift of a polar profile; values at the origin use the usual total operations. · OAI.Bernoulli.Axisymmetric.lift

lift def

A smooth cylindrical cap, expressed using the squared transverse radius so that the symmetry axis is included without a singular-coordinate convention. · OAI.Bernoulli.Cylindrical.lift

lift def

Inverse stereographic projection, regarded as an ambient R4-valued map. · OAI.ClosedSurfaceR4.SphericalStart.lift

lift def

The universal property of the Grothendieck group. In particular a Chern character must be invariant under isomorphism and additive on short exact sequences before this construction can be used. · OAI.CoherentK0.lift

lift abbrev

Character displacement away from low frequencies. · OAI.ExactDerandomization.Analysis.Square.lift

lift def

A degree-one substitution into a genuinely graded target is graded. · OAI.GradedPolynomialMap.lift

lift def

The universal mapping property, with all attaching equations explicit. · OAI.GroupRingTopology.Attachment.lift

lift def

Universal property for k-bilinear maps satisfying the actual A-balancing equation. · OAI.LittleFinitistic.BalancedTensor.lift

lift def

The block matrix [I+FH,FZ;H,Z]. · OAI.MaxCutGames.Appendix.CompressionCount.lift

lift def

The block matrix [F Z, F H; Z, H]. · OAI.MaxCutGames.Appendix.DerivativeInduction.lift

lift def

The lifted finite set in the whole map space. · OAI.MaxCutGames.Inverse.KMSBasisComparison.lift

lift def

The constructive preimage used in Lemma 6.1: choose the free bit to be zero. · OAI.MaxCutGames.Soundness.PartnerProjection.lift

lift def

Only the Cohen coordinate is examined. No diagram-generic or ambient fully generic filter occurs in this predicate. · OAI.PartitionConsistency.ProductForcing.CohenSelection.lift

lift def

Apply the same spatial isometry to each particle. · OAI.Problem356.IsometryTransport.lift

lift def

The Fourier lift as a finite Hahn series. · OAI.RationalHitting.QuantumLift.lift

lift def

The three-parameter polynomial lift, before specialization. · OAI.RationalHitting.ThreeLift.lift

lift def

Matching opposite face labels at a shared lifted edge forces matching group coordinates on the other two edges. Thus reduction cannot hide a downstairs dipole. · OAI.Release075.TriangleFilling.Dipole.lift

lift def

Matching opposite face labels at a shared lifted edge forces matching group coordinates on the other two edges. Thus reduction cannot hide a downstairs dipole. · OAI.Release075.TriangleSphere.Dipole.lift

lift def

The universal homomorphism out of the determinant quotient. · OAI.StableCoordinate.DeterminantRing.lift

lift def

Extend to the actual p-localization and transport to the Laurent model. · OAI.StableCoordinate.LaurentDerivationTransport.lift

lift def

The degreewise universal property, retaining every composition relation. · OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.lift

lift def

The strict functor determined by a chosen n-dimensional cell. · OAI.Thomason.Construction.StrictOmegaCategory.Globe.lift

lift def

An original cone gives bounded families because each input cell has one dimension bound preserved by all the projection functors. · OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.lift

lift def

The block matrix [I+FH,FZ;H,Z]. · OAI.UniqueGamesTheorem.Appendix.CompressionCount.lift

lift def

The block matrix [F Z, F H; Z, H]. · OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.lift

lift def

The lifted finite set in the whole map space. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.lift

lift def

The constructive preimage used in Lemma 6.1: choose the free bit to be zero. · OAI.UniqueGamesTheorem.Soundness.PartnerProjection.lift

liftAffine def

The genuine projective point [U:Y:1]. · OAI.Nagata.W06.LineArrangement.liftAffine

liftBilinear def

Extend a bilinear form in both arguments. · OAI.ActualExterior.liftBilinear

liftClosedPath def

Give arbitrary continuous paths a measurable closed-half-plane version. On every actual chordal trace this is precisely the original path. · OAI.SLEExactGauge.liftClosedPath

liftConstant def

Quantitative lift constant for a perturbed quotient map. · OAI.SeparableQuotient.liftConstant

liftDensity def

The indicator's density in the full linear-map space. · OAI.MaxCutGames.Inverse.KMSBasisComparison.liftDensity

liftDensity def

The indicator's density in the full linear-map space. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftDensity

liftDivergence def

The actual Bianchi divergence of an inner-gradient slice of the lift. · OAI.PositiveEinsteinFour.TraceHessian.liftDivergence

liftDropPath def

Lift a retained path through the fixed choices on the removed prefix. · OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.liftDropPath

liftDualEquiv def

Lift a perfect-duality chart through a symmetric power using the canonical duality chart for that symmetric power. · OAI.Problem346.PlethysmDual.liftDualEquiv

liftedAdditiveAction def

The actual additive action on the determinant ring lifting a given action on the quadric ring. Its group law is a theorem of normalized-frame uniqueness. · OAI.StableCoordinate.Obstruction.liftedAdditiveAction

liftedBarycentric def

The barycentric cone in the universe-lifted simplex used by realization. · OAI.Thomason.Construction.ConePrism.liftedBarycentric

liftedBoundary def

All individual lifted polygons, expressed in genuine signed lift edges. · OAI.HyperbolicObstruction.VoltageWords.liftedBoundary

LiftedCellularChain abbrev

Integral chains with independent coordinates for every deck translate of an elementary top triangle, fan triangle, square, or six-cell. No topological realization or equation on these chains is part of the definition. · OAI.HyperbolicObstruction.ConeSkeleton.LiftedCellularChain

liftedCoefficients def

The constant coefficient is the first coordinate of the homogeneous lift. · OAI.QuantitativeVanDerWaerden.Arrangement.liftedCoefficients

liftedComparison abbrev

The larger comparison written with a fixed association of its target. · OAI.Thomason.Construction.CobaseChangeCellularClosure.liftedComparison

liftedEndHom def

Canonical transport of every endomorphism of Y to its universe lift. · OAI.LittleFinitistic.QuadraticEncoding.liftedEndHom

liftedEndpoints def

Precisely the lifted lattice endpoints lying in a closed target interval. · OAI.QuantitativeVanDerWaerden.UniformMesh.liftedEndpoints

LiftedFace def

A genuine lift of a triangular face: all three corners are glued at the same group coordinates, not merely at the same original vertex colors. · OAI.Release075.BlockPresentation.LiftedFace

liftedIndicator def

Real Boolean indicator, in the orientation used by the matrix Fourier transform. · OAI.MaxCutGames.Inverse.KMSBasisComparison.liftedIndicator

liftedIndicator def

Real Boolean indicator, in the orientation used by the matrix Fourier transform. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftedIndicator

liftedKernelEquiv def

Closed lifting gives the actual kernel, including all (possibly infinitely many) lifted cells and without a cellular-homology assumption. · OAI.EilenbergGanea.CWPresentation.liftedKernelEquiv

liftedLineEquiv def

A line with a unit first coefficient has one zero lift for each lift of the second coordinate, over any fixed solution in the quotient. · OAI.Ostmann.liftedLineEquiv

liftedMap def

The real inverse chart is obtained by projecting to the ordinary base chart. It is not chosen by an abstract set-theoretic inverse. · OAI.EilenbergGanea.CWCover.liftedMap

liftedMapFun def

Extend the genuine lifted characteristic disk outside its domain only so that it can be used in Mathlib's ordinary PartialEquiv CW convention. · OAI.EilenbergGanea.CWCover.liftedMapFun

LiftedMatching structure

Actual boundary occurrences are graph darts; only their labels are inverse matched. In particular, this does not silently require equal graph lifts. · OAI.TorsionFreeZeroDivisors.WordBlocks.LiftedMatching

liftedRangeEquiv def

The dependent extensions are enumerated exactly once by the small space. · OAI.MaxCutGames.Inverse.KMSAnalytic.liftedRangeEquiv

liftedRangeEquiv def

The dependent extensions are enumerated exactly once by the small space. · OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.liftedRangeEquiv

liftedStandardPrism def

The standard prism expressed in the exact topological-simplex convention used by the realization colimit (including its universe lift). · OAI.Thomason.Construction.PrismBarycentric.liftedStandardPrism

liftedTraceLie def

A matrix acts on the genuine subspace with trace-free restriction in L. The witness is an operator, not the desired controllability conclusion. · OAI.HarmonicCounterexample.Control.liftedTraceLie

liftEmbedding def

Injective ordinal maps act on faces by taking their actual vertex image. · OAI.Thomason.Construction.SubdivisionBarycentric.liftEmbedding

liftEvalBody def

The genuine logical-element binder in i@lift_m(y). · OAI.PureTypeSystem.Labelled.RelationalCode.liftEvalBody

LiftExpansionPrinciple def

The precise analytic obligation at the ordered-basis lift. Its constants are fixed before the tuple length, which is fixed before the ambient size. · OAI.MaxCutGames.Inverse.KMSBasisComparison.LiftExpansionPrinciple

LiftExpansionPrinciple def

The precise analytic obligation at the ordered-basis lift. Its constants are fixed before the tuple length, which is fixed before the ambient size. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.LiftExpansionPrinciple

liftField def

The autonomous lift of a right-translation field to the time cylinder. · OAI.KervaireUnitaryHaarCurrent.liftField

liftFullSimplex def

Lift a simplex all of whose cells belong to a full subcategory. · OAI.Thomason.Construction.NormalizedSimplexIdentities.liftFullSimplex

liftGrid def

Cell averages from the real model. · OAI.FourierLLogL.Dyadic.liftGrid

liftGroup def

Cubical singular lifting descends through actual relative homotopies. · OAI.Thomason.Construction.RealizedCube.liftGroup

liftHom def

Universal evaluation of merger words for an equivariant interpretation of the quotient of copies. · OAI.PartitionConsistency.MergerAlgebra.Word.liftHom

liftHom def

No extra relations were introduced by using irreducibles: any model of the displayed reductions and old-action relation admits this homomorphism. · OAI.PartitionConsistency.ProbeAlgebra.Word.liftHom

liftHom def

The actual normalized polynomial-family homomorphism on the determinant ring. The independent u coordinate is lifted through the same base action. · OAI.StableCoordinate.NormalizedDeterminantLift.liftHom

liftHomotopy def

The full homotopy lifts with both endpoints and all boundary values prescribed; this is stronger than lifting an unbased path. · OAI.Thomason.Construction.CubicalLifting.liftHomotopy

liftKernel def

a can contain the entire past. Only read a is used for the next random transition; put a retains every coordinate needed afterward. · OAI.ContingencyTables.RealKernelApproximation.liftKernel

liftLinear def

The localized linear-map universal property, linear in its input. · OAI.ActualExterior.liftLinear

liftLinear def

A zero-preserving XOR-additive map becomes a genuine binary linear map. · OAI.MaxCutGames.Integration.BinaryLinear.liftLinear

liftLinear def

A zero-preserving XOR-additive map becomes a genuine binary linear map. · OAI.UniqueGamesTheorem.Integration.BinaryLinear.liftLinear

liftLoop def

A positive-dimensional based loop lifts with every boundary value fixed. · OAI.Thomason.Construction.CubicalLifting.liftLoop

liftLoop def

Every based topological cube has a based lift through singular realization. · OAI.Thomason.Construction.RealizedCube.liftLoop

liftLoopHomotopy def

The cubical lift preserves a homotopy relative to the entire boundary. · OAI.Thomason.Construction.RealizedCube.liftLoopHomotopy

liftM def

Apply frame maps to the two factors of every tensor. · OAI.HadwigerCounterexample.liftM

liftMap def

The realized cubical lift of a continuous map. · OAI.Thomason.Construction.RealizedCube.liftMap

liftOperatorTensor def

Tensorial inclusion of finite-rank operators along a Hilbert-space isometry. · OAI.NuclearUltrapower.liftOperatorTensor

liftOrNone def

The partial lift of a simplex point, defined precisely when its carrier is in A. · OAI.Thomason.Construction.RealizationPrism.liftOrNone

liftPair def

Integer real and imaginary parts interpreted in any coefficient ring. The linear identities do not require an equation such as i^2 = -1. · OAI.CirculantHadamard.BinaryCoefficients.liftPair

liftPerm def

Lift a local classical reversible gate to the actual wires; this is not an additional circuit instruction, just its classical semantics. · OAI.ExactQuantumFactoring.Instruction.liftPerm

liftRange def

The range quotient restricted to the lifted event itself. · OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRange

liftRange def

The range quotient restricted to the lifted event itself. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRange

liftRen def

Under a binder, a renaming leaves the newly bound variable bound. · OAI.PartitionConsistency.Formula.liftRen

liftResidueRepresentative def

An arbitrary representative at the original modulus. Its reduction is independent of this lift whenever the remaining precision suffices. · OAI.Ostmann.liftResidueRepresentative

liftRetention def

Start uniformly in the lifted set, then run the unconditioned update. · OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRetention

liftRetention def

Start uniformly in the lifted set, then run the unconditioned update. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRetention

liftRotationCharacter def

Compose the rotation character with a group-valued weight map. · OAI.PolycyclicRecognition.ComplexTriangularAdjoint.liftRotationCharacter

liftRow def

Lift a finite set of second coordinates to one fixed first coordinate. · OAI.Nagata.FiniteExponents.liftRow

liftSimplexToSubposet def

Every simplex whose vertices lie in A lifts to the nerve of A. · OAI.Thomason.Construction.liftSimplexToSubposet

liftSlicePairing def

Pairing of one outer-derivative slice of the lift with an actual Bianchi matrix of four-vectors. · OAI.PositiveEinsteinFour.TraceHessian.liftSlicePairing

liftToLabelFiber def

Factor a strict functor whose entire image has a fixed label through the full fibre. · OAI.Thomason.Construction.StrictOmegaCategory.liftToLabelFiber

lightPositions def

Lightness is measured in the full word, before restriction to light positions. · OAI.QuantitativeVanDerWaerden.OuterWordTests.lightPositions

limitActivity def

All limiting activity points as the positive parameter tends to zero. · OAI.Problem326.AffineApproximation.limitActivity

limitJ abbrev

A threshold usable for incoming normalization. · OAI.ExactDerandomization.Hie.limitJ

limitMap def

The limit map defined by the convergent correction series. · OAI.ClosedSurfaceR4.ExactCorrection.limitMap

limK def

largest norm limit as point · OAI.GeneralMahler.Cert.IV.limK

Line def

Line d f v: f fits a low-degree polynomial with coefficient v at d. · OAI.Fifths.Modulus.Line

line def

The field line generated by v. · OAI.MaxCutGames.Quadratic.line

line def

Each exponent has the one-dimensional coefficient line of its ordered quantum monomial. Lexicographic leading terms do not require a domain matrix coefficient ring. · OAI.RationalHitting.QuantumSeries.line

line def

The field line generated by v. · OAI.UniqueGamesTheorem.Quadratic.line

linear def

The ambient average is complex linear. · OAI.KadisonKastler.FiniteInnerAverage.linear

linearAtlasPhase def

The fixed geometric phase expressed as a smooth function on the surface. · OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.linearAtlasPhase

linearAutTuple def

Evaluate a linear automorphism on a fixed basis. · OAI.SidorenkoCounterexample.linearAutTuple

linearBallProfile def

An ambient linear label observed through a surjective height map. · OAI.PolycyclicRecognition.linearBallProfile

LinearBlock def

A separate type is used for the infimal-cost norm. It is not silently identified with the original Hilbert norm. · OAI.BoundedTreePotentials.LinearBlock

linearBlockCost def

L_n, not Q_n: the two costs are added, not squared. · OAI.BoundedTreePotentials.linearBlockCost

linearBlockHilbertEquiv def

Completeness is transported by equivalence of norms, with exactly the finite-height comparison constant sqrt(n+1). · OAI.BoundedTreePotentials.linearBlockHilbertEquiv

LinearBounds def

Sylvester's strict inequalities and the denominator/linear-size comparisons. · OAI.DefocusingNLS.ProfileCertificate.LinearBounds

linearChange def

Actual substitution of a linear coordinate motion in a polynomial. · OAI.HarmonicCounterexample.Control.linearChange

linearChartAlgMap def

The actual ring map on an affine chart, including its scalar structure. · OAI.SectionCompletion.linearChartAlgMap

linearCoboundary def

The Hochschild coboundary of a linear cochain. · OAI.KadisonKastler.linearCoboundary

linearCoeff def

Real coefficient on the actual space of binary linear maps. · OAI.MaxCutGames.Fourier.MatrixFourier.linearCoeff

linearCoeff def

Real coefficient on the actual space of binary linear maps. · OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linearCoeff

linearCoefficient def

Explicit matrix coefficients of the projection operator. · OAI.MaxCutGames.Repetition.ProjectionKernel.linearCoefficient

linearCoefficient def

Explicit matrix coefficients of the projection operator. · OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.linearCoefficient

linearCoordinate def

The jth coordinate linear polynomial of an actual linear map. · OAI.Nagata.W01.linearCoordinate

linearCost def

Linear Hilbert-plus-path cost, with the Hilbert residual eliminated. This is exactly inf_{x=h+B μ} (‖h‖+‖μ‖), not the quadratic cost. · OAI.BoundedTreePotentials.linearCost

linearCostSeminorm def

Seminorm supplied to Hahn--Banach in exact linear-cost duality. · OAI.BoundedTreePotentials.linearCostSeminorm

linearData def

Exact path-cost completions on the original finite-height components. · OAI.DiamondDistortion.PathModel.linearData

linearDescendRange def

Restrict a linear map to the range of an injection and invert there. · OAI.KadisonKastler.linearDescendRange

linearEquiv def

A vector-space isomorphism respecting the finite generating actions is a B-module isomorphism with exactly the original forward and inverse functions. · OAI.LittleFinitistic.EncodingLinearity.linearEquiv

linearField def

The actual infinitesimal linear coordinate motion, specified on generators. · OAI.HarmonicCounterexample.Control.linearField

linearFullData def

The original underlying ℓ² space endowed with its literal infimal path cost. · OAI.DiamondDistortion.PathModel.linearFullData

linearFunctionalCharacter def

A binary linear functional determines a complex additive character. · OAI.MaxCutGames.Fourier.MatrixCharacters.linearFunctionalCharacter

linearFunctionalCharacter def

A binary linear functional determines a complex additive character. · OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearFunctionalCharacter

linearGradedMap def

The genuine degree-one Noether-normalization map, now with its grading. · OAI.SectionCompletion.linearGradedMap

linearHom def

The exact homomorphism of linear height parts. · OAI.PolycyclicRecognition.HeightQuasiAction.linearHom

linearImageKaroubiIso def

A functor takes a concrete linear idempotent's formal image to the actual image module. · OAI.LittleFinitistic.QuadraticEncoding.linearImageKaroubiIso

linearIsometry def

Coordinate reflection as an isometric linear equivalence in the sup norm. · OAI.SharpLiebThirring.CubeFlags.Signs.linearIsometry

linearIsometrySphereHomeomorph def

Restriction of a real linear isometry equivalence to actual unit spheres. · OAI.Kaplansky.linearIsometrySphereHomeomorph

linearJoin def

Binary associativity reduces two right combs to one right comb. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.linearJoin

linearLayer def

Measurable-window restriction to P_i \ P_{i-1}. · OAI.BoundedTreePotentials.CostHeads.linearLayer

linearLocalHom def

Local morphisms that are linear for every local ring of sections. · OAI.CoherentDual.linearLocalHom

linearLocalSubfunctor def

Linearity is preserved by restricting local natural transformations. · OAI.CoherentDual.linearLocalSubfunctor

linearMap def

The original k-linear map, upgraded without changing its values. · OAI.LittleFinitistic.EncodingLinearity.linearMap

linearMap def

The cell Laplacian as an operator on Euclidean coordinate space. · OAI.Problem358.CellLaplacian.linearMap

linearMap def

A face contribution to the mass derivative, with its scalar and vector moments made explicit. The input is the site and intercept variation (v,r). · OAI.Problem358.FaceDerivative.linearMap

linearMatrixTrace def

The normalized two-by-two matrix extension of a linear functional. · OAI.KadisonSimilarity.linearMatrixTrace

LinearMetricChains structure

Explicit chains with bounded steps and a linear bound on their length. · OAI.PolycyclicRecognition.LinearMetricChains

LinearMetricChains structure

Chains joining any two points with bounded step size and a linear bound on the number of steps, including their vertices and endpoint identities. · OAI.PolycyclicRecognition.LinearMetricChains

linearMetricChains_of_minimizing_paths def

Sampling the chosen minimizing paths gives the concrete chain witnesses needed by the canonical-height and proper-homomorphism metric bridges. · OAI.PolycyclicRecognition.linearMetricChains_of_minimizing_paths

linearMotion def

The affine-linear homogeneous-coordinate motion a + s V. · OAI.Nagata.Workers.W14.linearMotion

linearNoiseEigenvalue def

Weighted probability that the dual map annihilates the sampled noise vector. · OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseEigenvalue

linearNoiseEigenvalue def

Weighted probability that the dual map annihilates the sampled noise vector. · OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseEigenvalue

linearOuterCoordinate def

Canonical coordinates in every finite-height component, including the last level (not only the shallower nodes used in the obstruction trees). · OAI.BoundedTreePotentials.linearOuterCoordinate

LinearPhaseNeighborhood structure

Compactly controlled geometry for one fixed linear phase. · OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.LinearPhaseNeighborhood

linearProjectiveMap def

The actual projective morphism associated to a finite degree-one normalization. Finiteness is used to PROVE the radical irrelevant containment. · OAI.SectionCompletion.linearProjectiveMap

linearRankOn def

The actual rank of a Fourier index restricted to the alphabet subspace. · OAI.MaxCutGames.Fourier.MatrixEnergy.linearRankOn

linearRankOn def

The actual rank of a Fourier index restricted to the alphabet subspace. · OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linearRankOn

linearRayleigh def

The supremum of variance divided by the rate-one Dirichlet form over nonzero linear spin observables. · OAI.CriticalSK.linearRayleigh

linearScore def

A score affine in the matching vector; the constant permits centering without changing the duality calculation. · OAI.MatchingEntropy.linearScore

linearSection def

Choose a linear section of the map onto its image. · OAI.MaxCutGames.Appendix.CompressionCount.linearSection

linearSection def

The actual degree-one Rees element associated to t ∈ I. · OAI.ReesProj.linearSection

linearSection def

The homogeneous degree-one section with coefficient c. · OAI.SectionCompletion.linearSection

linearSection def

Choose a linear section of the map onto its image. · OAI.UniqueGamesTheorem.Appendix.CompressionCount.linearSection

linearSliceEquiv def

Exact finite sample-space equivalence between the matrix representation and the linear-map representation of a nonempty affine slice. · OAI.MaxCutGames.Inverse.Shortcode.Slice.linearSliceEquiv

linearSliceEquiv def

Exact finite sample-space equivalence between the matrix representation and the linear-map representation of a nonempty affine slice. · OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.linearSliceEquiv

linearSubstitution def

Literal substitution of the three coordinate linear forms. · OAI.Nagata.W01.linearSubstitution

linearSum def

Five fixed terms, of which only the constant and linear ones are nonzero. · OAI.ExactQuantumFactoring.OrderTrial.linearSum

linearSupportSymmetryGroup def

The algebraic finite group of possible segment-support symmetries. · OAI.PolycyclicRecognition.linearSupportSymmetryGroup

linearTraceCharacter def

The trace character on actual linear maps, with no choice of basis. · OAI.MaxCutGames.Fourier.MatrixCharacters.linearTraceCharacter

linearTraceCharacter def

The trace character on actual linear maps, with no choice of basis. · OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTraceCharacter

linearTracePair def

The basis-independent trace pairing in the statement of Lemma 2.1. · OAI.MaxCutGames.Fourier.MatrixCharacters.linearTracePair

linearTracePair def

The basis-independent trace pairing in the statement of Lemma 2.1. · OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTracePair

LineCellMajorant structure

The finite prediction data on one actual line mesh. · OAI.LipschitzHilbert.LineCellMajorant

lineCharacter def

The actual character on the algebraic parameter line, forgetting only its discrete-domain continuity proof. · OAI.PlaneFiveColor.Spectral.lineCharacter

LineCoreIsUnitary def

The ordinary isometry condition on the given line-bundle transitions. · OAI.Kaplansky.LineCoreIsUnitary

lineCount def

Holes using a particular stage-line, counted before that stage. · OAI.CoordinateSweeps.Grid.Holes.lineCount

lineCount def

At the origin all three singleton lines contribute. · OAI.MaxCutGames.Decoder.SparseLaw.lineCount

lineCount def

At the origin all three singleton lines contribute. · OAI.UniqueGamesTheorem.Decoder.SparseLaw.lineCount

lineEquation def

The affine equation of component i. · OAI.Nagata.W04.ReducibleSquare.lineEquation

lineFirst def

The explicit first derivative along a line, used to avoid assuming an ODE or a second derivative in the Euclidean Laplacian computation. · OAI.Bernoulli.Axisymmetric.lineFirst

lineFrameEquiv def

Coordinates relative to an actual nowhere-zero line section. · OAI.Kaplansky.lineFrameEquiv

lineFrameHomeomorph def

A nonzero continuous frame gives a homeomorphism for the original line-core topology, with complex-linear fibers. · OAI.Kaplansky.lineFrameHomeomorph

lineGenerator def

A chosen nonzero generator, only used with generator-independent data. · OAI.MaxCutGames.Quadratic.lineGenerator

lineGenerator def

A chosen nonzero generator, only used with generator-independent data. · OAI.UniqueGamesTheorem.Quadratic.lineGenerator

lineGridRound def

Rounding a line coordinate to a grid of mesh δ. · OAI.Falconer.lineGridRound

lineGroup def

Permutations preserving each fibre of a given line map. · OAI.RowColumn.lineGroup

lineHom def

The dual restriction to the line aF. · OAI.PlaneFiveColor.Spectral.lineHom

LineIsolated def

A line-isolated additional trajectory, relative to all other additional paths AND the prescribed holes. Stage indices are never conflated. · OAI.CoordinateSweeps.Grid.Holes.LineIsolated

lineLaw def

The line law L_m(z)=(1-z)U_m+zB_m, with m=2^d. · OAI.CoordinateSweeps.lineLaw

lineMarkCoordinateMotion def

Actual coordinate polynomials of the explicit vertical affine motions. · OAI.Nagata.Workers.W14.lineMarkCoordinateMotion

lineMarkVelocity def

Explicit vertical velocity realizing the requested normal displacement. · OAI.Nagata.Workers.W14.lineMarkVelocity

lineMarkYDerivative def

The certified Y derivative of the actual reduced line-union equation. · OAI.Nagata.Workers.W14.lineMarkYDerivative

lineNormalPolynomial def

Actual normal polynomial restricted to component i, with coefficients in its affine coordinate ring K[U]. The outer polynomial variable is the fiber. · OAI.Nagata.W03.LowDegree.lineNormalPolynomial

LinePartition structure

A partition by full lines, represented without arbitrary labels or duplicates. · OAI.KaplanskyCounterexample.FiniteGeometry.LinePartition

linePoints def

A direction vector parametrizes every point of its full line. · OAI.KaplanskyCounterexample.FiniteGeometry.linePoints

lineRestriction def

Restriction to the full parametrized affine line. · OAI.KaplanskyCounterexample.PolynomialPairing.lineRestriction

lineRestriction def

The actual polynomial restriction homomorphism from plane forms to component i. · OAI.Nagata.W04.ReducibleSquare.lineRestriction

lineRestriction def

Actual polynomial restriction to an affine line. · OAI.Nagata.Workers.W24.lineRestriction

Lines abbrev

One-dimensional vector subspaces. · OAI.MaxCutGames.Inverse.MatrixChart.Lines

Lines abbrev

One-dimensional vector subspaces. · OAI.UniqueGamesTheorem.Inverse.MatrixChart.Lines

lineSectionTrivialization def

Slice-site line trivializations induce section-module trivializations on Cartier charts. · OAI.ActualCartier.lineSectionTrivialization

lineShares def

Sharing means using the same decorated line at the same stage. · OAI.CoordinateSweeps.Grid.lineShares

LineStage structure

A finite list of actual projective-product line bundles. · OAI.Kaplansky.LineStage

lineStageDiskCollapse def

Radial collapse of the entire unit sphere bundle to the point at infinity. · OAI.Kaplansky.lineStageDiskCollapse

lineStageDiskInterior def

An actual vector has a canonical interior preimage under radial collapse. · OAI.Kaplansky.lineStageDiskInterior

LineStageThomQuotient abbrev

The disk/sphere quotient, with its quotient topology. The exact relation is given by lineStageDiskCollapse_eq_iff. · OAI.Kaplansky.LineStageThomQuotient

lineStageThomQuotientHomeomorph def

The actual disk/sphere Thom quotient is homeomorphic to the one-point total space used in the singular homology construction. This assertion is for positive fiber rank; no characteristic class is assumed. · OAI.Kaplansky.lineStageThomQuotientHomeomorph

lineStageTrivialTotalHomeomorph def

A sum consisting entirely of trivial projective-product lines has a global chart, for the existing bundle topology. · OAI.Kaplansky.lineStageTrivialTotalHomeomorph

lineSubstitution def

Homogeneous coordinates on Y=i²-iU in the affine parameter U. · OAI.Nagata.W04.ReducibleSquare.lineSubstitution

lineSumBaseSet def

The simultaneous finite cover for the direct sum of actual line cores. · OAI.Kaplansky.lineSumBaseSet

lineSumChartPullbackHomeomorph def

Pulling the actual sum into full chart coordinates gives exactly the restriction of its original total space, with its inherited topology. · OAI.Kaplansky.lineSumChartPullbackHomeomorph

lineSumPullbackStep def

Pull continuous normalized maps from a projective subproduct to the full product. Continuity uses the actual line-sum pullback topology. · OAI.Kaplansky.lineSumPullbackStep

lineSumReindexUnitary def

Reindexing an orthogonal line sum is unitary on fibers and continuous in both directions on the actual total space. · OAI.Kaplansky.lineSumReindexUnitary

lineSumRelabelUnitary def

Relabeling justified by an exact slot bijection preserves topology and metric, as well as the fiber linear structure. · OAI.Kaplansky.lineSumRelabelUnitary

lineSumTransition def

Componentwise transition on the finite Hilbert direct sum. · OAI.Kaplansky.lineSumTransition

lineTestPolynomials def

The distinguished row supplies the coefficient tests; its minors with all other rows supply the rank tests. · OAI.Ostmann.lineTestPolynomials

LineTrivialization structure

Local trivializations of a rank-one locally free module sheaf. · OAI.ActualSheafTensor.LineTrivialization

lineUnaryRemoval def

Values of every line factor and every unary factor after zero, one, and two removals give exactly this two-removal matrix. · OAI.ContingencyTables.lineUnaryRemoval

lineUnionEquation def

Equation of the entire reduced line union in the actual affine plane ring. · OAI.Nagata.Workers.W24.lineUnionEquation

lineValue def

The actual affine line equation evaluated at a point. · OAI.Nagata.W06.LineArrangement.lineValue

lineValue def

Six homogeneous forms in the affine rational trivialization. · OAI.SourceSymmetry.lineValue

lineVector def

Indicator of one line-coordinate group. · OAI.ContingencyTables.lineVector

link def

Every ordered pair of pieces has a displayed equivalence witness. · OAI.Generator.Tracial.EquivalentPartition.link

LinkDirection abbrev

Signed edge directions in the nine-letter triangular presentation. Indices 0..8 are positive; indices 9..17 are negative. · OAI.ArtinCAT0.LinkDirection

LinkedProbeChains structure

All three logarithmic chains in the original neighboring-sheet coordinates. The first starts at the allowed suffix, the second at its neighbor, and the third starts at the second's actual last vertex. Their coefficients retain their … · OAI.PolycyclicRecognition.CartanWordModel.LinkedProbeChains

LinkedRootProbeFrames structure

Retain the logarithmic chains together with the group equalities used by the measured comparison. The sampling domain stays an abstract parameter so that its coordinate construction is not repeated in every projection. · OAI.PolycyclicRecognition.CartanWordModel.LinkedRootProbeFrames

LinkedSource abbrev

The linked frames on this exact source cell. · OAI.PolycyclicRecognition.CartanWordModel.PolarTiledSamplerData.LinkedSource

linkEnds def

Endpoints of nonbacktracking walks with a prescribed first oriented edge. · OAI.ArtinCAT0.linkEnds

linkNeighbors def

The three theta graphs, glued at a±, b±, c±, with cell identities retained. · OAI.ArtinCAT0.linkNeighbors

Links def

At every sufficiently late chain vertex a code entry equals the given name at w, and that vertex actually is a successor of w. · OAI.PartitionConsistency.ProductForcing.ChainCode.Links

Links structure

A finite directed presentation of substring links. Both directions of an actual interval-isometry link may be included; extra constraints only reduce the set of feasible strings. · OAI.TorsionFreeZeroDivisors.StageLabels.Links

linW def

densities of β integrals at a fixed x,z · OAI.GeneralMahler.ProjField.linW

liouville def

The standard Liouville function, viewed as complex valued. Its value at zero is zero, as in mathlib; only positive arguments occur in the main statements. · OAI.TwoPointCorrelations.liouville

LiouvilleLogSaving def

Theorem 1.1 (thm:q-affine) of the manuscript, through all real cutoffs, with a single exponent independent of the four affine coefficients. · OAI.TwoPointCorrelations.LiouvilleLogSaving

lipschitzConstant def

A finite positive constant valid for all pairs in the ambient Hilbert space. · OAI.ThompsonNonamenability.Analytic.CorrectionData.lipschitzConstant

LipschitzPairBounds def

Uniform Lipschitz, lower-distance, and two-sided quasi-inverse bounds. The source manuscript uses the same constant in these four bounds. · OAI.PolycyclicRecognition.LipschitzPairBounds

list def

The list with all parameters fixed by the unary inputs. · OAI.RationalHitting.Generator.list

listBitDraw def

Read a binary index; every index beyond the list gives a hold. · OAI.ContingencyTables.FairBits.listBitDraw

listCode def

Reusable dense records. Individual word lengths need not be fixed. · OAI.RationalHitting.StackLanguage.listCode

listDeletionExpectation def

Exact complete-trace expectation, recursively on the actual binary word. · OAI.TraceReconstruction.listDeletionExpectation

listDifference def

Preserve the second list's length, including malformed inputs. · OAI.ContingencyTables.ProfilePrograms.listDifference

listed def

Interpolation in a listed cube, independent of any topological model. · OAI.EilenbergGanea.CubeInterpolation.listed

listedAtom def

A fixed representation for each name, chosen from geometry before noises. Off the list the harmless zero branch makes this a total function. · OAI.PlanarL1.Columns.Model.Point.RadialTree.listedAtom

listedCost def

The single path-expansion budget of a listed group, with its real-valued density contribution. · OAI.MatroidProphet.AccountingContracts.listedCost

listedStepCounts def

Completion counts are cached once per state; only the short proposal word is enumerated to form this finite transition matrix. · OAI.ContingencyTables.SmallGraphProfiles.listedStepCounts

listedTrialCounts def

Each final table count sums over the reached profile and its fresh terminal completion; failed outer trials retain their exact numerator. · OAI.ContingencyTables.SmallGraphProfiles.listedTrialCounts

listedWalkCounts def

The complete adaptive walk is an integer matrix power. · OAI.ContingencyTables.SmallGraphProfiles.listedWalkCounts

listens def

Read the whole channel frames of a unit. · OAI.HadwigerCounterexample.listens

listEquiv def

An explicit complete list supplies both directions of a finite encoding. The forward direction searches the list; its inverse performs list indexing. · OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv

listEquiv def

An explicit complete list supplies both directions of a finite encoding. The forward direction searches the list; its inverse performs list indexing. · OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.listEquiv

listInput def

Actual quoted-list conversion for a complete source field, with no postulated record-decoding primitive. · OAI.ContinuumCoulomb.PrefixListPrograms.listInput

listMaskNet def

Compute ceil-log activation bits by bounded comparisons. The constant 2^i fits n bits, and the circuit is polynomial on invalid inputs too. · OAI.ExactQuantumFactoring.listMaskNet

listSelector def

A concrete complete address list supplies a computational selector. Its length depends on the degree and radius, not on the ambient vertex count. · OAI.MaxCutGames.Foundations.PCP.PoweringLabels.listSelector

listSelector def

A concrete complete address list supplies a computational selector. Its length depends on the degree and radius, not on the ambient vertex count. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.listSelector

listSplitRow def

The list version of the already proved dimension-recursive row split. · OAI.ContingencyTables.GreedyFeasibleTable.listSplitRow

listTraceLaw def

The genuine complete-trace law embedded in a specified finite trace space. The extra elements have mass zero, not a cemetery mass. · OAI.TraceReconstruction.listTraceLaw

listTraceOverlap def

Ordinary overlap of complete traces, including unequal input lengths. · OAI.TraceReconstruction.listTraceOverlap

Literal structure

A `Literal` pairs an arbitrary natural-number variable name with a Boolean sign. · OAI.UniqueGamesTheorem.BinaryFormula.Literal

literal def

Only a change of representation. The cell order and both literal boundary flags are retained exactly. · OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.literal

literalAt def

Fixed clause/slot indexing for the machine's finite emission plan. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.literalAt

literalAt def

Fixed clause/slot indexing for the machine's finite emission plan. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.literalAt

literalAttachmentCapacity def

Integer Euclidean division by positive2 is the literal integer floor. Unlike Nat subtraction, this expression retains negative h-d before clamping. · OAI.ArithmeticTensorSquares.Capacity.literalAttachmentCapacity

literalBlockStartNorm def

The infimum over precisely all countable segment representations on the specified component. The original recursive M_{n+1}, not a replacement, is used in the set of costs. · OAI.BoundedTreePotentials.Segments.literalBlockStartNorm

literalCircleConfig def

The rational parametrization of nine points in the Euclidean plane. · OAI.EuclideanRamsey.NineStatement.literalCircleConfig

literalComponent def

Literal configurations, rather than an oracle for connectivity, returned by exhaustive search on the fixed finite base skeleton. · OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.literalComponent

literalFullLabel def

The actual two-system full label of a cyclic point. · OAI.QuantitativeVanDerWaerden.literalFullLabel

literalInTime def

Polynomial resource bound attached to the proved literal execution. · OAI.MaxCutGames.BinaryLiteralMachine.literalInTime

literalInTime def

Polynomial resource bound attached to the proved literal execution. · OAI.UniqueGamesTheorem.BinaryLiteralMachine.literalInTime

literalPaddingBinMass def

rho_j as a sum over actual numerical squarefree divisors. · OAI.TwoPointCorrelations.literalPaddingBinMass

literalPlan def

Seven real commands for the two unary fields of a literal. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan

literalPlan def

Seven real commands for the two unary fields of a literal. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.literalPlan

literalPolynomialBasis def

A genuine basis on the literal polynomial-section space, conditional exactly on the source Laurent-coordinate injectivity and theta coefficient identities. Every index is an actual column in the manuscript's three-branch exponent set. · OAI.Nagata.Workers.W10.literalPolynomialBasis

literalProgressionHeavy def

Heavy positions are defined by their literal full-label multiplicity in the entire progression, rather than within an individual block. · OAI.QuantitativeVanDerWaerden.literalProgressionHeavy

literalR def

Rational enclosures for every entry of the finite atomic jet map. · OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.literalR

literalSignature def

The color and box are fixed functions of the full label, while the band is the literal integer value. No signature-dependent coding is used. · OAI.QuantitativeVanDerWaerden.literalSignature

literalStartNorm def

Exactly the original infimal forest representation formula, including all finite-cost countable arrays and the original signed coordinate output. · OAI.BoundedTreePotentials.Segments.literalStartNorm

littleFinitisticDimension def

The little finitistic dimension: the supremum of the actual projective dimensions of finitely generated modules whose projective dimension is finite. The value of the zero module follows mathlib's -∞ convention. · OAI.LittleFinitistic.littleFinitisticDimension

LittleGrothendieckInput def

Subnormalized states also cover the zero algebra. Only their values on positive squares and their mass bound are used in the application. · OAI.KadisonSimilarity.LittleGrothendieckInput

littlewoodValue def

The Littlewood polynomial of length N, evaluated at z. · OAI.AsymptoticallyMinimalLittlewood.littlewoodValue

littlewoodValue def

The consecutive-degree polynomial of a real coefficient family. · OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.littlewoodValue

live def

Nonemptiness is the existence of a path through the word's ordered product. · OAI.OneWayLiveness.BRel.live

liveCells def

All simultaneously allowed representation structures, with one retained left dictionary, one task arena and the scalar prefix continuation stack. · OAI.LowSpaceSubsetSum.RepresentationSetup.liveCells

lo abbrev

Surface p(x,y). · OAI.ExactDerandomization.Aurora.Folk.lo

load def

Total event weight at a random variable. · OAI.KaplanskyCounterexample.FiniteLocalLemma.load

loaded def

Work stacks empty. Argument j on its right stack. · OAI.Fifths.TM.loaded

loadedFields def

The executable field order is slot-major within each tuple position. · OAI.MaxCutGames.Integration.AddressTupleCleanup.loadedFields

loadedFields def

The executable field order is slot-major within each tuple position. · OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.loadedFields

loadedPrepareInTime def

Exactly the loaded context signature is computed by the concrete finite program. Scratch is reset and all loaded fields and caller tapes are preserved. · OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.loadedPrepareInTime

loadedPrepareInTime def

Exactly the loaded context signature is computed by the concrete finite program. Scratch is reset and all loaded fields and caller tapes are preserved. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.loadedPrepareInTime

loadTuplePolynomialInTime def

The same concrete run with a univariate polynomial in the combined size. · OAI.MaxCutGames.Reduction.MachineSourceTuple.loadTuplePolynomialInTime

loadTuplePolynomialInTime def

The same concrete run with a univariate polynomial in the combined size. · OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.loadTuplePolynomialInTime

loadUnaryInTime def

Actual odometer digits have empty suffixes. The resulting complete loader runs in a polynomial whose coefficients depend only on the fixed repetition u. · OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.loadUnaryInTime

loadUnaryInTime def

Actual odometer digits have empty suffixes. The resulting complete loader runs in a polynomial whose coefficients depend only on the fixed repetition k. · OAI.MaxCutGames.Reduction.MachineSourceTuple.loadUnaryInTime

loadUnaryInTime def

Actual odometer digits have empty suffixes. The resulting complete loader runs in a polynomial whose coefficients depend only on the fixed repetition u. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.loadUnaryInTime

loadUnaryInTime def

Actual odometer digits have empty suffixes. The resulting complete loader runs in a polynomial whose coefficients depend only on the fixed repetition k. · OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.loadUnaryInTime

Local abbrev

Localization of the actual cyclotomic order at the chosen prime ideal. · OAI.CirculantHadamard.CyclotomicLocalBase.Local

localAffineMomentFamily def

Target, constant and coordinates with the same normalized local L² scale. · OAI.RegularPointCoordinates.localAffineMomentFamily

LocalAlmostSplittingInput def

The precise product-map consequence used from Huang--Huang Theorem 2.9(2) and its first-order criterion, including the residual product factor. · OAI.RegularPointCoordinates.LocalAlmostSplittingInput

localAnalysis def

The coefficient map in an ambient chart. · OAI.Kaplansky.ContinuousOrthonormalStageFrame.localAnalysis

localAnchorAverage def

Local unsigned anchor averaged against its actual known/hidden flags. · OAI.TraceReconstruction.localAnchorAverage

localAngle def

Local real lift based at a vertex of the supporting simplex. · OAI.CoarseAssembly.Rips.IntegralCocycle.localAngle

localAtomic def

Atomic forcing at a fixed ground diagram, retaining the Cohen coordinate as the forcing parameter. Its laws follow from actual product forcing. · OAI.PartitionConsistency.ProductForcing.localAtomic

localAvailability def

The availability ideal of a specified local name with respect to any directed filter. No dense-set meeting assumptions are required for this purely algebraic ideal assertion. · OAI.PartitionConsistency.ProductForcing.localAvailability

LocalAverageSupport def

All averaging samples eventually lie in each relative neighborhood of this particular boundary point. This is an almost-everywhere support condition, so it also applies after choosing Borel representatives. · OAI.CircleDomainRigidity.LocalAverageSupport

localBitProposal def

Binary lookup in the polynomial-length local list. · OAI.ContingencyTables.SmallGraphProfiles.localBitProposal

LocalCertificate structure

The output required at a fixed minimum before neighborhood extension. decay_gt and offsets are essential data for the subsequent gluing step. · OAI.Problem326.Affine.LocalCertificate

localCertificate_one def

The fixed-minimum singleton construction in species dimension one. · OAI.Problem326.Affine.localCertificate_one

localCertificate_upper def

The fixed-minimum singleton construction at the upper corner. · OAI.Problem326.Affine.localCertificate_upper

localChartDenominatorUnit def

The invertible denominator for the substitution from chart c into the local ring of chart b. Its invertibility has just been proved. · OAI.Nagata.ProjectiveGeometry.localChartDenominatorUnit

localChartDomain def

The actual chart domain restricted to a bundle trivializing open set. · OAI.Kaplansky.localChartDomain

localCode def

A genuine block code on any finite alphabet injected into the displayed support. No choice of an enumeration at the parameter is used. · OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.localCode

localComplementBundleHomeomorph def

The local ordinary kernel bundle realizes the exact orthogonal complement, not an independently assigned topology on the same fibers. · OAI.Kaplansky.ContinuousOrthonormalStageFrame.localComplementBundleHomeomorph

localComplementKernelHomeomorph def

A homeomorphism to the genuine kernel incidence set over an ambient chart. Both spaces retain their ambient subspace topologies. · OAI.Kaplansky.ContinuousOrthonormalStageFrame.localComplementKernelHomeomorph

localComponent def

A normalized multiplicative component with one of two local choices at each prime in P. · OAI.TwoPointCorrelations.localComponent

localConstant def

Exact constant displayed in (6.10), with no dependence on the metric size. · OAI.KServer.Pilot.localConstant

LocalConstantLaplacianBochnerInput def

local Bochner calculus, restricted to the n+2 directions used in the Poisson comparison. The volume in the trace correction is restricted to the interior ball and hence is finite. · OAI.RegularPointCoordinates.LocalConstantLaplacianBochnerInput

localContinuationWithWork def

Numerical tail of the actual local refinement query, after its finite wide, group and online lists have been prepared from gathered data. · OAI.EditApproximation.BinaryFraction.localContinuationWithWork

localCoordinatePullback def

Transport through a smooth local inverse, including the coefficient dependence on all positional order-two jets. · OAI.ClosedSurfaceR4.JetPolynomial.Expression.localCoordinatePullback

localCoulombKernel def

Local part of the singular kernel; the omitted tail is bounded by one. · OAI.Problem356.localCoulombKernel

LocalDescent structure

Descending neighbors at one vertex lie in one strict-sublevel component; a tied edge carries that component to the other vertex. · OAI.HarmonicArtin.ParabolicIntersections.LocalDescent

LocalDirichletSobolevInput def

A fixed superquadratic exponent and normalized zero-boundary Sobolev constant for small balls with a definite exterior annulus. · OAI.RegularPointCoordinates.LocalDirichletSobolevInput

LocalDistanceConverges def

The local distance-function topology used in geometry.tex:70–101. Sets are separately required to be nonempty and closed when those properties enter. · OAI.AffineBernstein.LocalDistanceConverges

LocalEllipticEquation def

Local distributional equation with scalar Laplacian principal part. The coefficients need only be globally smooth: cutoff multiplication, not a hidden boundedness or temperedness condition, defines every coefficient product. · OAI.ElasticityRegularity.LocalEllipticEquation

LocalEnd abbrev

Local endpoint occurrences at permitted vertices. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalEnd

LocalEq def

Equality of actual distributions tested strictly within the open domain. · OAI.ElasticityDistribution.LocalEq

localEventFactor def

The number of local verifier events for an alphabet with q symbols. · OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.localEventFactor

localEventFactor def

The number of local verifier events for an alphabet with q symbols. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.localEventFactor

localExtraProbability def

Exact one-line probability after the hole assignments are prescribed. · OAI.CoordinateSweeps.Grid.Holes.localExtraProbability

localFactor def

A per-layer factor in the normalized four-path moment bound. True is the diagonal type; A = alpha⁻¹, B = beta, x = n⁻¹. · OAI.Problem335.WordLocalProduct.localFactor

localFactor def

The normalized cubic prime-frequency contribution to the ternary singular series. · OAI.Problem337.ThreePrimeLocalFactor.localFactor

LocalFailure def

A local failure is the complement of the actual local success event. · OAI.LeanBlast.SecondKahnKalai.LocalFailure

LocalFamily def

All local disjoint families. This type is finite even when the tree branches countably, because each member is a family of subsets of the fixed head K. · OAI.DiamondDistortion.SegmentSystem.LocalFamily

LocalFamilyData structure

All data needed from one fixed-minimum construction after its localization radius has been shrunk to retain a stronger offset decay exponent. · OAI.Problem326.Affine.LocalFamilyData

LocalFlatSplittingInput def

Only this Euclidean-flat coordinate consequence of the product theorem is used in the chart construction. It is also proved directly from the noncollapsed measured-coordinate input in FlatSplittingApproximation. · OAI.RegularPointCoordinates.LocalFlatSplittingInput

LocalFreeCornerPublishedInputs structure

Published local ingredients, specialized to the chosen small corner and test symmetry. The applicability to the actual finite normal free product is kept explicit in the finite-factor assembly. · OAI.KadisonSimilarity.TracialCornerGeometry.LocalFreeCornerPublishedInputs

LocalFunctionLift def

A local smooth extension of the pullback of h to the unit isotropic cone. · OAI.ArnoldCounterexample.LocalFunctionLift

LocalGenerator abbrev

Generators belonging to a prescribed local point group. · OAI.KaplanskyCounterexample.GluedGroup.LocalGenerator

localGeometricMass def

Exact independent geometric expectation of the local table at a common mean. · OAI.Problem335.LocalMoments.localGeometricMass

LocalGoodCutoffInput def

Exact existence consequence at bounded rescaled curvature. · OAI.RegularPointCoordinates.LocalGoodCutoffInput

LocalHarmonicBochnerInput def

Local calculus on interior balls with eightfold room for regularity. · OAI.RegularPointCoordinates.LocalHarmonicBochnerInput

LocalHarmonicEnergy structure

The bounded representative and local measure equation furnished by local harmonic test calculus on an interior ball. · OAI.RegularPointCoordinates.LocalHarmonicEnergy

LocalHarmonicL2GradientInput def

The normalized L² interior gradient bound for harmonic functions. This is a analytic input, not an affine approximation premise. · OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput

LocalHarmonicL2MeanValueInput def

The fixed-ratio, harmonic L²-to-L∞ specialization of Jiang Lemma 4.1. · OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput

LocalHarmonicMomentCompactnessInput def

Only the normalized moments of one harmonic function and the finite coordinate family are retained from the published local compactness theorem. All target functions are genuine Sobolev functions of the original space. · OAI.RegularPointCoordinates.LocalHarmonicMomentCompactnessInput

localHessianAction def

The three-term gradient formula for Hess f(grad v, grad u), when the three local gradient pairings have Sobolev representatives. · OAI.RegularPointCoordinates.localHessianAction

LocalHessianPairing structure

A local Hessian pairing with one fixed gradient. All functions in the Koszul formula are genuine Sobolev functions. The regular test core is dense in the zero-boundary Sobolev space. · OAI.RegularPointCoordinates.LocalHessianPairing

localHomEquiv def

Local linear transformations are exactly ordinary module morphisms on the slice site. This identifies the just-constructed sheaf with genuine internal Hom. · OAI.CoherentDual.localHomEquiv

localHomogeneousCoordinates def

The homogeneous coordinate functions in the genuine local ring of chart b; the distinguished coordinate is one. · OAI.Nagata.ProjectiveGeometry.localHomogeneousCoordinates

LocalInitialSplittingInput def

Huang--Huang Theorem 2.9(1), specialized to the Euclidean target. The enlarged measured ball leaves room for a compact Sobolev extension of the local harmonic map without changing it on the output ball. · OAI.RegularPointCoordinates.LocalInitialSplittingInput

localizationAtComapMap def

The actual map from the localization at a contracted prime ideal. · OAI.CirculantHadamard.localizationAtComapMap

localizationComplexEquiv def

The same explicit equivalence also preserves the original complex scalars. · OAI.AbhyankarSathaye.CommutingDerivations.localizationComplexEquiv

localizationEquiv def

Actual equivalence over the Laurent coefficient ring. · OAI.AbhyankarSathaye.CommutingDerivations.localizationEquiv

localizationMargin def

The extra none index is the driver margin, so empty point families are allowed without an artificial height condition. · OAI.SLEExactGauge.Multipoint.localizationMargin

localizationRingEquiv def

Actual localized ring equivalence, with explicit maps and both composites. · OAI.AbhyankarSathaye.CommutingDerivations.localizationRingEquiv

localizationSeed def

An actual lift of prefix localization to the presentation seed. It respects both Γ factors as homomorphisms; only the free factor uses chosen preimages. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.localizationSeed

LocalizationStatement def

Full uniform localization theorem, including s = 0 and arbitrary t > s. · OAI.QAC.LocalizationStatement

localizationTwoMap def

Exterior vectors transform by the localization of their entries. · OAI.ActualExterior.localizationTwoMap

localize def

Every brick contains a canonical isomorphic copy of the entire twisted group. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localize

localize def

Insert a whole finite table into one member of a finite partition. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.localize

localize def

Extend a derivation to a localization whose denominators it annihilates. · OAI.StableCoordinate.LocalizationLND.localize

localizeAway def

The common special case of localization at one invariant element. · OAI.StableCoordinate.LocalizationLND.localizeAway

localizedFourierPolynomial def

The localized physical Fourier polynomial, before zero extension is needed. · OAI.DefocusingNLS.localizedFourierPolynomial

localizedMatrixChart def

Universal split coefficients over the principal open D(det[F,J]det(GJ)). The only equation required on the base matrices is GF=0. · OAI.IntegralCharacterVarieties.ExactSequenceChart.localizedMatrixChart

localizedSchwartzPolynomial def

The actual finite cutoff polynomial, bundled in the Schwartz space. · OAI.DefocusingNLS.localizedSchwartzPolynomial

localizeFun def

On fractions with invariant denominators the extension differentiates only the numerator. · OAI.StableCoordinate.LocalizationLND.localizeFun

localizePerm def

Conjugate a cube permutation into a brick, extending by identity. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localizePerm

localizeTo def

Extend to any algebra satisfying the localization universal property. · OAI.StableCoordinate.LocalizationLND.localizeTo

localKernelFamily def

A continuous surjective family on every ambient chart, constructed from an arbitrary continuous orthonormal frame. · OAI.Kaplansky.ContinuousOrthonormalStageFrame.localKernelFamily

LocalL1Converges def

Local L¹ convergence is stated with the extended L¹ seminorm, so that an undefined Bochner integral cannot make a nonintegrable error appear to have zero norm. · OAI.BoltzmannNonuniqueness.Published.LocalL1Converges

localL2Restriction def

Restriction to a smaller measurable region as a continuous linear map. · OAI.RegularPointCoordinates.localL2Restriction

localLeaf def

The leaf reached from a local child, with its ambient-depth proof retained. · OAI.Problem310.FiniteLocalPredicate.localLeaf

LocalList structure

A local finite atom expansion, including its proved one-coordinate tests. This is proof data for an actual named field, not a substitute for a chart. · OAI.PlanarL1.Interpolation.LocalList

localList def

The canonical evaluation list range, formed as a genuine HS name with support D_r; its domain has been enumerated by a ground ordinal. · OAI.PartitionConsistency.ProductForcing.localList

localListOrdinal def

A ground ordinal enumerating the entire normalized local-name set. · OAI.PartitionConsistency.ProductForcing.localListOrdinal

LocallyCompact def

The usual local-compactness condition, with the actual multiplication operators. · OAI.CoarseAssembly.DiscreteRoe.LocallyCompact

LocallyFinite def

Local finiteness counts bonds, not just distinct neighbors. · OAI.CriticalPercolation.BondGraph.LocallyFinite

LocallyInjective def

A locally injective graph homomorphism preserves internal reduction. · OAI.Release075.LocallyInjective

LocallyNilpotent def

Literal pointwise local nilpotence; there is no uniform exponent requirement. · OAI.AbhyankarSathaye.CommutingDerivations.LocallyNilpotent

LocallyNilpotent def

Local nilpotence, allowing the bound zero for the zero element. · OAI.ComplexCancellation.LND.LocallyNilpotent

locallyNilpotentEquivAdditiveCoaction def

The full characteristic-zero correspondence between locally nilpotent algebra derivations and algebraic additive polynomial coactions. · OAI.StableCoordinate.locallyNilpotentEquivAdditiveCoaction

LocallyRepresented def

Local quotient values actually represented by a member of the specified family at a stronger diagram. This is a subcollection of the unrestricted local quotient, not a replacement definition for eligible E-classes. · OAI.PartitionConsistency.ProductForcing.LocallyRepresented

LocalMachine structure

A finite-control presentation of the very same local multitape model. packed below changes ONLY the names of states, with zero simulation cost. · OAI.ParityWL.Complexity.LocalMachine

localMap def

Local atoms as linear images of Euclidean blocks. · OAI.DiamondDistortion.SegmentSystem.localMap

LocalMeanPoincareInput def

Only approximation by one constant on an interior ball is retained from the Sobolev--Poincare inequality. This applies to arbitrary Sobolev functions, with no harmonic or Euler equation assumed. · OAI.RegularPointCoordinates.LocalMeanPoincareInput

LocalMeasuredCoordinateInput def

Quantitative Euclidean specialization of noncollapsed measured convergence. The input is metric approximation on a larger ball; the output adds normalized test-integral control on the smaller ball. · OAI.RegularPointCoordinates.LocalMeasuredCoordinateInput

LocalMildSolution structure

The local solution properties established before the entropy and continuation steps. · OAI.BoltzmannNonuniqueness.LocalMildSolution

LocalMinimizer def

Full ballwise local comparison. Competitor and gradient are arbitrary Sobolev representatives on the ball, with zero-trace difference. · OAI.Bernoulli.LocalMinimizer

localMiss def

The concrete center atom together with all child-window trial misses. · OAI.Problem310.ConcreteWindowAtom.localMiss

LocalMultiplicity def

The source's local label multiplicity, using half-open intervals to assign boundary labels unambiguously. · OAI.LipschitzHilbert.SourceSlopeLabels.LocalMultiplicity

LocalName def

The ground collection X(r): all normalized subset names supported literally by the diagram range. It is a set, rather than an unrestricted class of HS names. · OAI.PartitionConsistency.ProductForcing.LocalName

localNeighborList def

Passing candidates are decoded with the arithmetic feasibility test. · OAI.ContingencyTables.SmallGraphProfiles.localNeighborList

localNoiseFailure def

The actual honest noise test on a fixed valid homogeneous point. · OAI.MaxCutGames.Reduction.ActualCompleteness.localNoiseFailure

localNoiseFailure def

The actual honest noise test on a fixed valid homogeneous point. · OAI.UniqueGamesTheorem.Reduction.ActualCompleteness.localNoiseFailure

localNormalize def

Canonical normalization into X(r), for any supported name at any rank. · OAI.PartitionConsistency.ProductForcing.localNormalize

localOrderAtLeast def

Multiplicity in the actual local ring uses its maximal ideal. · OAI.Nagata.AffineMultiplicity.localOrderAtLeast

LocalPoissonGradientInput def

The constant-Laplacian, bounded-value specialization of Jiang2014, Theorem3.1, with one constant uniform at bounded rescaled curvature. · OAI.RegularPointCoordinates.LocalPoissonGradientInput

LocalPoissonGradientProductInput def

The gradient-product rule and shifted Hessian bound, using the same canonical local energy measure as the same local Poisson span. Locality allows any Sobolev representative of its gradient pairing. · OAI.RegularPointCoordinates.LocalPoissonGradientProductInput

LocalPoissonHarmonicCompactnessInput def

A bounded-Laplacian radial sequence and an arbitrary bounded harmonic sequence have joint local limits. All assumptions are analytic bounds; the projected Euler equation is deliberately absent. · OAI.RegularPointCoordinates.LocalPoissonHarmonicCompactnessInput

LocalPoissonHessianActionInput def

The local Hessian action specialization needed for the two-center commutator, using the same full Bochner measure at every radius. · OAI.RegularPointCoordinates.LocalPoissonHessianActionInput

LocalPoissonHessianInput def

Local second-order calculus for n harmonic coordinates and two constant-Laplacian replacements. The same full Bochner measure occurs in the energy equation, the positivity assertion and the Hessian bound. · OAI.RegularPointCoordinates.LocalPoissonHessianInput

localPolynomial def

The complete local second-trace polynomial. The all-equal case belongs to normal pairing. · OAI.Problem335.LocalMoments.localPolynomial

localPolynomialExpansion def

All branches of the local four-path table have total factorial order at most two. The normal branch includes coincident coordinates and their first-order corrections. · OAI.Problem335.LocalMoments.localPolynomialExpansion

localPolynomialNat def

Natural-valued version of the exact local table. · OAI.Problem335.LocalMoments.localPolynomialNat

localPrism def

The local strict prism takes values in the oriental of the finite image chain. · OAI.Thomason.Construction.RelativePrismData.localPrism

localProductNat def

The natural polynomial for a finite set of layers. · OAI.Problem335.LocalMoments.localProductNat

LocalProductSwaps structure

The two finite-site properties sufficient for the product-state argument. No centralizer irreducibility or core-type conclusion is a field here. · OAI.KadisonKastler.LocalProductSwaps

localQ def

The actual local Boolean test, using the canonical tables and subtree router. · OAI.Problem310.WindowExceptionalTransfer.localQ

LocalQuotient abbrev

The finite self-similar closure of any given finite family of actual table relations. Completeness of a particular family still has to be proved. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.LocalQuotient

LocalQuotient def

All local normalized subsets modulo local forced equality. The local E-class sets used subsequently are subcollections of this actual quotient. · OAI.PartitionConsistency.ProductForcing.LocalQuotient

LocalQuotientGain def

The unit-sphere finite-codimensional version of the local midpoint input. · OAI.DiamondDistortion.Midpoint.LocalQuotientGain

localRadialDerivative def

A locally bounded gradient defines a genuine linear derivative on Sobolev functions with values in the common local L2 space. · OAI.RegularPointCoordinates.localRadialDerivative

LocalRanks structure

Ranks are attached to local occurrences. Their only identification is the corner pairing from the source vertex table. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks

LocalRecord abbrev

The actual triple (b,x,t⁻¹d) in the local-quotient proof. · OAI.PartitionConsistency.ProductForcing.LocalRecord

localRefinementInitialQuery def

First gather the finite parent initial data that select all later representative and cell lists. Child mass/initial data are gathered by a separate layer, independently of the current-index reads. · OAI.EditApproximation.localRefinementInitialQuery

localRepairCandidates def

Candidates are generated by ordered cell pairs, without enumerating positive defect states. A later feasibility test removes unused pairs. · OAI.ContingencyTables.SmallGraphProfiles.localRepairCandidates

localRightInverse def

Right inverse on the open neighborhood where A R is invertible. · OAI.Kaplansky.SmoothKernel.localRightInverse

localRule def

A completely fixed radius-one alphabet table. The arbitrary multihead cases are settled by center, then left, then right priority. · OAI.WLIdentification.Machine.localRule

localScalar def

The actual fixed local covering-space expression in logarithmic coordinates. · OAI.Nagata.W20.localScalar

localSection def

A concrete polynomial parametrization transverse to the complex scaling. For horizontal v it stays on the quadric and its first derivative at zero is v. This makes the horizontal tangent identification independent of any assumed atlas. · OAI.ArnoldCounterexample.Quadric.localSection

localSelectorAddress def

The actual finite-model selector coordinate read at one child-window trial. · OAI.Problem310.WindowTrialAddresses.localSelectorAddress

localSetoid def

The local equality relation is witnessed by a Cohen condition in F. · OAI.PartitionConsistency.ProductForcing.localSetoid

localShiftExtra def

Literal adjacent-gap allocation of the units used by a displacement. Value zero means translate left, one leave fixed, two translate right. · OAI.TraceReconstruction.localShiftExtra

localSlope def

Asymptotic Lipschitz slope; zero at an isolated point. · OAI.WeakHessian.localSlope

LocalSobolev def

Local Bessel-potential regularity, using actual compact smooth multipliers. · OAI.ElasticityRegularity.LocalSobolev

localSpan def

The span of the spaces on the edges incident to a given vertex. · OAI.SidorenkoCounterexample.localSpan

LocalStep inductive

Exactly the seven rows of the manuscript's guarded local table. · OAI.ForcedComputation.Recorder.LocalStep

localStep def

The one actual cloud-table lookup used by this internal row. · OAI.MaxCutGames.Foundations.PCP.PreprocessingInternalRows.localStep

localStep def

The one actual cloud-table lookup used by this internal row. · OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.localStep

LocalSuccess def

The denominator is large enough and the retained fragment fits in the halved integral capacity. · OAI.LeanBlast.SecondKahnKalai.LocalSuccess

LocalSupportingCharts structure

A local exact supporting certificate, with the stationary branches retained as analytic local diffeomorphisms and both domains shrunk to metric balls. · OAI.Problem356.LocalGeometry.LocalSupportingCharts

localSwaps def

The actual finite swap is assembled from the two matrix systems. Triple product moments put it in the centralizer of the full algebra. · OAI.KadisonKastler.ProductMatrixStages.localSwaps

localTail def

The local union-bound sum, allowing any fixed nonnegative dimension coefficient in the pattern count. · OAI.QuantitativeVanDerWaerden.Parameters.localTail

LocalTestFamily structure

A countable determining family with explicit support control. Density is in the uniform norm within each compact exhaustion set. · OAI.SLEExactGauge.LocalTestFamily

localTestFamily def

A chosen countable family can be used for all times and all random outcomes of a measure-valued construction. · OAI.SLEExactGauge.localTestFamily

LocalTracialCutInput def

The remaining local consequence of the finite-algebra trace theorem. · OAI.BoundedHochschild.KadisonRingrose.LocalTracialCutInput

LocalTransformationInput def

A precisely cited conditional input. It retains both the flatness and no-extra-factor hypotheses of Theorem 4.1. Only its first two conclusions are requested here; interscale growth is not assumed as part of this input. · OAI.RegularPointCoordinates.LocalTransformationInput

localTransportAmplitude def

Transport of a compactly supported amplitude through a local homeomorphism, with a prescribed Jacobian square-root factor. · OAI.Problem356.localTransportAmplitude

LocalTypeCertificate def

A supporting certificate on an ordered component product, with the one-way contact localization needed for excluding deterministic optimizers. · OAI.Problem356.GoodTypePermutation.LocalTypeCertificate

localUnitToFraction def

The actual map from local units to the fraction field of B u. · OAI.CirculantHadamard.BinaryProductTransport.localUnitToFraction

LocalUpper def

Upper rule with its complement identity built into the definition. · OAI.InfiniteMatroidCounterexample.LocalUpper

localVanishing abbrev

The original vanishing subspace viewed inside the chosen large summand. · OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.localVanishing

localVanishing abbrev

The original vanishing subspace viewed inside the chosen large summand. · OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.localVanishing

localVectorSphereHomologyIso def

Relative homology at the origin, in degrees at least two, is identified with the preceding integral sphere homology. No sphere group calculation is assumed. · OAI.Kaplansky.localVectorSphereHomologyIso

LocalVolumeRigidityInput def

The map formulation of De Philippis--Gigli Theorem 1.6. The universal error absorbs the usual factor between GH distance and approximation maps. · OAI.RegularPointCoordinates.LocalVolumeRigidityInput

LocalWitness structure

A local representation by the covariant family, with its literal stronger diagram and supported Cohen condition. · OAI.PartitionConsistency.ProductForcing.LocalWitness

locations def

Finite control locations, computed structurally, despite unbounded loop iteration counts. · OAI.RationalHitting.StackLanguage.locations

lockedNat opaque

An opaque value with a checked equality prevents the kernel's closed-numeral evaluator from expanding the astronomical powers. Its body is proved once for an arbitrary natural number; no axiom or trusted evaluator is introduced. Only size … · OAI.MaxCutGames.Foundations.PCP.RoundSize.lockedNat

lockedNat opaque

An opaque value with a checked equality prevents the kernel's closed-numeral evaluator from expanding the astronomical powers. Its body is proved once for an arbitrary natural number; no axiom or trusted evaluator is introduced. Only size … · OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.lockedNat

log def

Epoch prefix history stores n+1 controllers beginning at visit-number t. · OAI.Fifths.Tour.log

logApprox def

Rational bisection is not required: an exhaustive finite search of strict certified brackets terminates for every positive input. · OAI.ForcedComputation.logApprox

logarithmic def

Exponent bounding all denominator-cleared matrix entries by a power of 2. · OAI.RationalHitting.PolynomialBounds.logarithmic

logarithmicBox def

Closed logarithmic boxes agree exactly with the source definition. · OAI.AffineBernstein.logarithmicBox

logarithmicCutoff def

Closed boxes in the literal logarithmic base coordinates. A fixed-width smooth box cutoff; its derivatives have no dependence on L apart from coordinate translations. · OAI.AffineBernstein.logarithmicCutoff

logarithmicPoints def

Actual covering lifts of the moving logarithmic centers, on fibre value one. · OAI.Nagata.CoefficientSpaces.logarithmicPoints

logarithmicUnitCell def

Closed unit cells in the actual logarithmic base coordinates. · OAI.AffineBernstein.logarithmicUnitCell

logClock def

The logarithmic slowdown traverses infinitely many periods. · OAI.ForcedComputation.logClock

logCompactAnnulus def

A fixed closed annulus containing the unit sphere in its interior. · OAI.SymmetricMahler.logCompactAnnulus

LogConcaveOn def

Log-concavity is needed only on the common ambient box. · OAI.ContingencyTables.PublishedInputs.LogConcaveOn

logCutoffPolynomialFactor def

The center appears in the lower endpoint and its reciprocal Lipschitz constant. These cancel in the total variation budget. · OAI.Ostmann.logCutoffPolynomialFactor

logDenominatorWeight def

Parameters are the normalized scale logarithm and inverse logarithm of the outer length. Both range over a compact rectangle. · OAI.CubicFirstMoment.logDenominatorWeight

logDilate def

A bounded logarithmic dilation preserves the given uniform smooth weight bounds. Its support and all derivatives are derived explicitly. · OAI.CubicFirstMoment.UniformLogWeights.logDilate

logEnergyDerivative def

The derivative of logarithmic energy as an actual bounded linear functional. · OAI.LipschitzHilbert.logEnergyDerivative

logEntropyPrimitive def

A finite-spectrum primitive, continuous even at a zero eigenvalue. · OAI.GAD.logEntropyPrimitive

logFactorClock def

The source clock in logarithmic capacity-two coordinates. · OAI.SLEExactGauge.Multipoint.logFactorClock

Logged structure

A bounded deterministic computation and the chronological requests it actually made. Failure retains its prefix and does not query later work. · OAI.ExactQuantumFactoring.Logged

logHessianDet def

The logarithm is taken only on the positive Hessian determinant at points where the estimates are asserted. Outside the domain this is just a total function. · OAI.AffineBernstein.logHessianDet

logicalCharacters def

Turn the fixed generic vector subspace into its actual logical characters. · OAI.MaxCutGames.Gadget.BaseDetection.logicalCharacters

logicalCharacters def

Turn the fixed generic vector subspace into its actual logical characters. · OAI.UniqueGamesTheorem.Gadget.BaseDetection.logicalCharacters

logicalShift def

The logical alphabet is realized as actual linear shifts of the quotient. · OAI.MaxCutGames.Gadget.Quotient.logicalShift

logicalShift def

The logical alphabet is realized as actual linear shifts of the quotient. · OAI.UniqueGamesTheorem.Gadget.Quotient.logicalShift

LogicCode structure

Raw code for the already constructed logical operations. This separates syntax naturality from the dependent typing certificate of a logic setup. · PureTypeSystem.Labelled.LogicCode

LogicSetup structure

Actual finite ambient context data for the source's classical logical calculus. All fields are constructed below from fixed graph paths and terms. · OAI.PureTypeSystem.Labelled.LogicSetup

logMean def

Logarithmic form of the conditional power means T_0 using independent message labels. The current eta's are held fixed; only their descendants are integrated. Physical disorder is a fixed argument of g throughout. · OAI.DilutedSpinGlass.logMean

logMean def

Logarithmic conditional power mean, for an arbitrary Borel probability law. · OAI.DilutedSpinGlass.MeasureMean.logMean

logMoment def

The logarithm of a zero moment is minus infinity. · OAI.CoordinateSweeps.logMoment

logMoment def

Natural logarithm with the manuscript's log zero = minus infinity. · OAI.CoordinateSweeps.logMoment

logNets def

The rows are at their true retained locations. This construction has no quantum conditioning and does not evaluate a factorization operation. · OAI.ExactQuantumFactoring.NodeMachine.logNets

logPartition def

Log partition with the uniform probability prior on a finite state space. · OAI.InvariantIsing.logPartition

logPullback def

Extension by zero of a compact test in logarithmic coordinates; a negative coordinate must not be silently sent through Real.log. · OAI.AffineBernstein.logPullback

logSlope def

Half the logarithmic derivative of the volume-normalized Berger anisotropy. · OAI.HarmonicCounterexample.Pulses.logSlope

LogSpace 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.LogSpace

logTotientPrimes def

The only factor data used are supplied parent factors and already verified p−1 rows. This representation is a mathematical list interface; its Boolean implementation is a separate obligation, not hidden in this definition. · OAI.ExactQuantumFactoring.PhysicalTree.logTotientPrimes

logTubeMeasure def

The actual logarithmic pushforward of a tube density, restricted to its positive base domain. Only the nonnegative part outside that domain is discarded. · OAI.AffineBernstein.logTubeMeasure

logWeight def

A finite realized row in the full countable-type model. · OAI.DilutedSpinGlass.HeterogeneousMarks.logWeight

logWeight def

Minus the Hamiltonian, with all index choices including repetitions. · OAI.DilutedSpinGlass.logWeight

longCombination def

Its combined long mean. Individual means need not vanish. · OAI.JointDickman.PublishedInputs.longCombination

longitudinal def

Low-jet longitudinal vector, including the velocity loop. · OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.longitudinal

longitudinalCoordinate def

The source longitudinal coordinate is the real part of the inverse ribbon chart, translated by the current front coordinate. · OAI.SLEExactGauge.RibbonCoordinates.longitudinalCoordinate

longPart def

The complementary part, supported on integers strictly above U. · OAI.Problem337.Vaughan.longPart

longScaleError def

The long-scale error in the published complex estimate. · OAI.JointDickman.PublishedInputs.longScaleError

look def

Read with fixed out of bounds default. · OAI.PowerSaving.Tape.look

lookback def

The source's lookback constant, independent of diameter and tree depth. · OAI.PlanarL1.Columns.Model.Point.RadialTree.lookback

Lookup abbrev

Enumerated candidates together with a feasible fallback. · OAI.ContingencyTables.ExactMatrixTrial.Lookup

Lookup inductive

A declaration's type viewed in the full newest-first context. · OAI.PureTypeSystem.Lookup

lookup def

One indexed read after computing a bounded mask's local code. · OAI.LowSpaceSubsetSum.StoredSeparatorQueries.lookup

lookup def

A finite association table; every stage is materialized before the next. · OAI.Superstring.Computable.lookup

lookupEncoded def

The index is on a separate tape and must decode to exactly one word. · OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded

lookupEncoded def

The index is on a separate tape and must decode to exactly one word. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.lookupEncoded

lookupFields def

Data lookup runs on the retained flat rows, not on a factorization oracle. · OAI.ExactQuantumFactoring.PhysicalTree.lookupFields

lookupInTime def

A proved linear transition budget in the lengths of the encoded table and index, including invalid indices. The witness is the actual trace above. · OAI.MaxCutGames.Foundations.Complexity.MachineLookup.lookupInTime

lookupInTime def

Lookup at a valid numbered clause, starting with its ordinary unary index. The output fields are those of F.clauses[i], with the rest of the work copy and the original formula retained exactly as stated by the frame lemmas. · OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.lookupInTime

lookupInTime def

A proved linear transition budget in the lengths of the encoded table and index, including invalid indices. The witness is the actual trace above. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.lookupInTime

lookupInTime def

Lookup at a valid numbered clause, starting with its ordinary unary index. The output fields are those of F.clauses[i], with the rest of the work copy and the original formula retained exactly as stated by the frame lemmas. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.lookupInTime

lookupPhaseInTime def

A linear bound in the original encoded table length for the same actual phase. This includes the copy, restore, lookup, and residual cleanup. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseInTime

lookupPhaseInTime def

A linear bound in the original encoded table length for the same actual phase. This includes the copy, restore, lookup, and residual cleanup. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupPhaseInTime

lookupResultTapes def

The exact cleaned tape state produced by either lookup. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes

lookupResultTapes def

The exact cleaned tape state produced by either lookup. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupResultTapes

lookupSteps def

The number of nodes examined by a membership lookup. · OAI.LowSpaceSubsetSum.BinaryTrie.lookupSteps

lookupTailInTime def

The exact row-selection trace packaged with its linear transition budget. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.lookupTailInTime

lookupTailInTime def

The exact row-selection trace packaged with its linear transition budget. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.lookupTailInTime

lookupWithSplitInTime def

A polynomial bound on the actual complete copy/skip/read execution. · OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.lookupWithSplitInTime

lookupWithSplitInTime def

A polynomial bound on the actual complete copy/skip/read execution. · OAI.MaxCutGames.Reduction.SourceEquationLookup.lookupWithSplitInTime

lookupWithSplitInTime def

A polynomial bound on the actual complete copy/skip/read execution. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.lookupWithSplitInTime

lookupWithSplitInTime def

A polynomial bound on the actual complete copy/skip/read execution. · OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.lookupWithSplitInTime

lookupWordNet def

Fixed-capacity, first-match read-only lookup. Every iteration is an explicit Boolean network; malformed/missing labels use the zero word. · OAI.ExactQuantumFactoring.lookupWordNet

Loop structure

The actual geometric hypotheses on the second-jet neighborhood. The first and second derivatives are fixed coordinate projections of that jet. · OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop

Loop structure

A closed walk with its base vertex retained as explicit data. · OAI.Superstring.Hierarchical.Loop

loop def

The only comparison performed by the program is on two Option Bool heads. In particular, no statement is given a whole-list equality oracle. · OAI.MaxCutGames.Foundations.Complexity.MachineCompare.loop

loop def

A fixed finite statement; arithmetic is performed by the physical unary tapes. · OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.loop

loop def

The only comparison performed by the program is on two Option Bool heads. In particular, no statement is given a whole-list equality oracle. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.loop

loop def

A fixed finite statement; arithmetic is performed by the physical unary tapes. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.loop

loopBase def

The accumulator is indexed by the remaining number of outer iterations. · OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.loopBase

loopBase def

The accumulator is indexed by the remaining number of outer iterations. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.loopBase

loopBudget def

Running time after the parser: actual body budgets, two transfers per body result, one guard per iteration, and the final transfer and empty guard. · OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.loopBudget

loopBudget def

Running time after the parser: actual body budgets, two transfers per body result, one guard per iteration, and the final transfer and empty guard. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.loopBudget

loopClosure def

Closure of alternating returns at a boundary. · OAI.TwoWayComplementation.Diagram.loopClosure

loopDimensionShift def

Dimension shift on the actual homotopy-group quotients. · OAI.Thomason.Construction.HomotopyMaps.loopDimensionShift

loopHomeomorphEquiv def

A homeomorphism gives an actual equivalence on based generalized loops. · OAI.Thomason.Construction.HomotopyMaps.loopHomeomorphEquiv

loopInTime def

The complete record loop consumes exactly the specified occurrence list. The final zero guard retains the counter delimiter for the final cleanup stage. Arbitrary suffixes and already emitted prefixes are preserved explicitly. · OAI.MaxCutGames.Explicit.MachineClone100Loop.loopInTime

loopInTime def

Every list occurrence is read once, emits exactly its four rows, and advances the three private numeric names. The loop includes its final zero-counter test. · OAI.MaxCutGames.Explicit.MachineSubdivisionLoop.loopInTime

loopInTime def

Induction follows the actual unary row counter and the actual unconsumed input suffix. Every iteration invokes the checked row program. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.loopInTime

loopInTime def

An actual timed execution witness with the exact composed step count. · OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.loopInTime

loopInTime def

The complete record loop consumes exactly the specified occurrence list. The final zero guard retains the counter delimiter for the final cleanup stage. Arbitrary suffixes and already emitted prefixes are preserved explicitly. · OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.loopInTime

loopInTime def

Every list occurrence is read once, emits exactly its four rows, and advances the three private numeric names. The loop includes its final zero-counter test. · OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoop.loopInTime

loopInTime def

Induction follows the actual unary row counter and the actual unconsumed input suffix. Every iteration invokes the checked row program. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.loopInTime

loopInTime def

An actual timed execution witness with the exact composed step count. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.loopInTime

loopInTime_linear def

A linear bound derived from the actual composed execution. · OAI.MaxCutGames.Explicit.MachineClone100Loop.loopInTime_linear

loopInTime_linear def

A linear bound derived from the actual composed execution. · OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.loopInTime_linear

loopLabels def

Labels of all closed walks, exactly as in the cone presentation. · OAI.TorsionFreeZeroDivisors.GraphPresentation.loopLabels

loopMap def

Postcomposition of actual cube-relative loops. · OAI.HyperbolicObstruction.HigherCovering.loopMap

loopPolynomial def

The source's map marginal, with its common factor sqrt(q) removed. · OAI.FKCRT.loopPolynomial

LoopResult structure

Concrete final configuration and full remaining-loop execution. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Loop.LoopResult

LoopResult structure

Concrete final configuration and full remaining-loop execution. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Loop.LoopResult

loopTapes def

These are the only four stacks changed by the complete loop. · OAI.MaxCutGames.BinaryRenameLoop.loopTapes

loopTapes def

Complete initial loop state. Every auxiliary tape not listed here is empty. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.loopTapes

loopTapes def

These are the only four stacks changed by the complete loop. · OAI.UniqueGamesTheorem.BinaryRenameLoop.loopTapes

loopTapes def

Complete initial loop state. Every auxiliary tape not listed here is empty. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.loopTapes

looseCost def

The source uniform block-propagation and chain-tail error, before taking limits. All blocks and both sides are counted only once. · OAI.TorsionFreeZeroDivisors.StageEntropy.looseCost

loss def

Scale loss when the second jet is controlled. · OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss

loss def

Exact first-moment loss, deliberately kept separate from asymptotic parameter estimates. · OAI.Problem335.FirstMoment.loss

lossBound def

The exponential lower bound for 2 ≤ h. · OAI.TwoWayComplementation.lossBound

lossIndices def

The actual finite event of a child map having a nonzero kernel. · OAI.MaxCutGames.Quadratic.lossIndices

lossIndices def

The actual finite event of a child map having a nonzero kernel. · OAI.UniqueGamesTheorem.Quadratic.lossIndices

Lot structure

fixed syntactic play, prices ignored until the enclosing layer is ready. · OAI.ExactDerandomization.Relay.Lot

Lower abbrev

Each lower gate is an enumerated path for one block entry. · OAI.Problem335.BlockData.Lower

lower def

The caller supplies a cached number of binary-search steps. · OAI.LowSpaceSubsetSum.StoredSeparatorQueries.lower

lower def

Extend the universal n-cell to an m-dimensional identity cell. · OAI.Thomason.Construction.StrictOmegaCategory.Globe.lower

lowerAt def

The actual lower restriction, with its source explicitly identified. · OAI.KLInvariance.MomentGraph.GradedSheaf.lowerAt

LowerBasis def

The half-closed interval used by the lower-limit rule. · OAI.InfiniteMatroidCounterexample.LowerBasis

lowerBidiagonal def

A unit lower bidiagonal matrix, with arbitrary noncommuting blocks. · OAI.PositiveEinsteinFour.Jacobi.lowerBidiagonal

lowerBlock def

The pure non-axial block in the quadratic part of the plus Weyl estimate. · OAI.PositiveEinsteinFour.lowerBlock

lowerBlock def

Lower diagonal block of the regularized Hessian. · OAI.Problem356.LocalHessian.lowerBlock

lowerConstant def

Chebyshev's classical elementary lower constant, approximately 0.92129. · OAI.Problem337.ChebyshevLowerSharp.lowerConstant

lowerEndpoint def

Relative endpoints are chosen by measurable rational exits. On the only components whose weight is positive they are the genuine finite endpoints. · OAI.HenonLaneEmden.LineComponents.lowerEndpoint

lowerFace def

The face omitting the lower occurrence of the cut vertex. · OAI.Thomason.Construction.PrismBarycentric.lowerFace

lowerFiberMass def

Source mass before the cut that is identified with the cut vertex. · OAI.Thomason.Construction.PrismBarycentric.lowerFiberMass

lowerFinset def

A concrete finite lower ideal of the genuine Bruhat order. · OAI.KLInvariance.lowerFinset

LowerHit def

Coordinate form of membership in the first intercept cylinder. · OAI.TriangularCovering.LowerHit

lowerMap def

The lower clamping endomorphism of the horn. · OAI.Thomason.Construction.HornContraction.lowerMap

lowerMonomial def

The lower-gate monomial belonging to an enumerated block path. · OAI.Problem335.BlockData.lowerMonomial

lowerOfCoords def

Exact linear coordinates on the entire lower-triangular coefficient space; no nonvanishing or invertibility restriction is imposed. · OAI.SharpLiebThirring.PathTopology.lowerOfCoords

lowerProductForm def

The lower-arity form used in the stabilization induction. · OAI.Problem346.lowerProductForm

lowerRows def

The lower end of an interval is given by a spanning list of graph vectors. · OAI.MaxCutGames.Inverse.MatrixChart.lowerRows

lowerRows def

The lower end of an interval is given by a spanning list of graph vectors. · OAI.UniqueGamesTheorem.Inverse.MatrixChart.lowerRows

lowerSimple def

The smaller of x and s*x in Bruhat order. · OAI.KLInvariance.lowerSimple

lowerSobolevGenerator def

The free Schrödinger generator, with the loss of two Sobolev derivatives. · OAI.DefocusingNLS.lowerSobolevGenerator

lowerSobolevInclusion def

The continuous inclusion from H^k into H^(k-2), in weighted coordinates. · OAI.DefocusingNLS.lowerSobolevInclusion

lowerUnit def

Complete a table of strict lower triangular entries with unit diagonal. · OAI.MUB6.Certificate.lowerUnit

lowerValue def

Value of a lower product gate before relabelling the gate types. · OAI.Problem335.IndexedDepth5Circuit.lowerValue

lowExclusiveKernel def

Equal cell atom weights give the manuscript's m⁻² kernel. · OAI.JointDickman.lowExclusiveKernel

lowExclusiveMass def

The common mass is integrated after multiplying the two independent exclusive cell probabilities; only the second exclusive is restricted. · OAI.JointDickman.lowExclusiveMass

lowHistory def

Actual pieces, original weights, and original metadata below a threshold. This is deliberately not the compressed history, nor a cropped code. · OAI.SeparableQuotient.Norming.FinitePath.lowHistory

lowJetCoordinateChange def

Transport a positional low jet at T x to the positional low jet at x. The old positional components are unnecessary; the value and ordered jets are evaluated by the chain rule. · OAI.ClosedSurfaceR4.JetPolynomial.lowJetCoordinateChange

lowJetPosition def

The position slots of an actual low jet. · OAI.ClosedSurfaceR4.JetPolynomial.lowJetPosition

lowJetScalarProduct def

Multiplication preserves the position slots and transforms the value, first derivatives, and ordered second derivatives by the product rule. · OAI.ClosedSurfaceR4.JetPolynomial.lowJetScalarProduct

lowPart def

The strict lower half of a polynomial, used in the KL recursion. · OAI.KLInvariance.CanonicalP.lowPart

lowPosition def

The position stored in a positional two-jet. · OAI.ClosedSurfaceR4.JetPolynomial.lowPosition

LowProductBound def

The product estimate required when every positive formal degree is small. · OAI.Problem335.LowProductBound

lowProjection def

Low coordinate projection and its complementary support subspace. · OAI.RationalHitting.LaurentReduction.lowProjection

lowUnionExclusiveMass def

The discarded mass is the genuine union event, so overlap is counted once. · OAI.JointDickman.lowUnionExclusiveMass

lowWalshSets def

Nonempty coordinate sets through order t. · OAI.TwoPointCorrelations.lowWalshSets

LPFunction structure

Regularity actually used by the density LP proof. Gaussian-bounded Fourier pairs are put into this class below; no separation of a competitor is assumed. · OAI.TriangularUniversal.LPFunction

lpGaugeEquiv def

A genuine Hilbert-space unitary, with inverse given by the opposite gauge. · OAI.BoundedRecovery.RealSpectralCalculus.lpGaugeEquiv

lpUnitary def

A coordinate permutation with unitary entries on a Hilbert direct sum. · OAI.NuclearUltrapower.lpUnitary

LT def

The physical stress-divergence, using the conjugated coordinate derivative. · OAI.ElasticityAugmented.LT

LT def

The wellordering of the glued classes induced by their least codes. · OAI.PartitionConsistency.ProductForcing.ChainCode.LT