Glossary: A

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

A def

Half the logarithmic ratio; it is artanh on (-1,1). · OAI.Bernoulli.DeSilvaJerison.A

A abbrev

The manuscript's one fixed square-zero algebra. No projective-dimension conclusion is asserted here. · OAI.LittleFinitistic.SelectedOrdinaryAlgebra.A

A def

Exponent bounding one regular extension factor. · OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.A

a def

Source constants a=1/100, c0=e0=a/100. · OAI.CoordinateSweeps.a

a def

A fixed support interval containing degree zero, chosen before any test module. · OAI.LittleFinitistic.SelectedOrdinaryAlgebra.a

a0 def

The three augmented rational parametrization entries. · OAI.EuclideanRamsey.NineField.a0

A4Survives def

The full index and selectors of a right-hand summand of (A.4). · OAI.MaxCutGames.Appendix.LinearIdentities.A4Survives

A4Survives def

The full index and selectors of a right-hand summand of (A.4). · OAI.UniqueGamesTheorem.Appendix.LinearIdentities.A4Survives

A5PairSurvives def

The precise right-hand pair selector of (A.5). · OAI.MaxCutGames.Appendix.LinearIdentities.A5PairSurvives

A5PairSurvives def

The precise right-hand pair selector of (A.5). · OAI.UniqueGamesTheorem.Appendix.LinearIdentities.A5PairSurvives

abelianDynkinCoefficients def

Only the degree-one coefficients are nonzero. · OAI.PolycyclicRecognition.abelianDynkinCoefficients

abelianizationCosimplicialIso def

The inverse presentation of normalized chains commutes with all simplex operators, including those which collapse a basis element to zero. · OAI.Thomason.Construction.SimplexAtomsInput.abelianizationCosimplicialIso

abelianizationGlobeIso def

Naturality is proved through the actual lambda-nu adjunction, whose unit followed by globe evaluation is the canonical globe isomorphism. · OAI.Thomason.Construction.DirectedGlobeComplex.abelianizationGlobeIso

abelianizationIso def

The positive chain presentation of a strict globe is exactly the explicit globe complex, not an additional comparison input. · OAI.Thomason.Construction.DirectedGlobeComplex.abelianizationIso

abelianizationIso def

The ordered finite complex is the actual abelianization of the pasted pair, with its specified two globe inclusions. · OAI.Thomason.Construction.PastingGlobeBasis.abelianizationIso

abelianizationIso def

The actual directed-complex isomorphism, with all positivity and augmentation information retained. · OAI.Thomason.Construction.SimplexAtomsInput.abelianizationIso

abelianizationToBasis def

Evaluating strict abelianization on the actual ordered chain model. · OAI.Thomason.Construction.PastingGlobeBasis.abelianizationToBasis

abelianizationToGlobe def

Evaluation from the additive strict-cell presentation to the explicit positive globe chains. · OAI.Thomason.Construction.DirectedGlobeComplex.abelianizationToGlobe

abelianLieModel def

The additive group, equipped with its actual tangent Lie algebra. · OAI.PolycyclicRecognition.abelianLieModel

abelianScalarInvariantMean def

An actual invariant scalar mean on every discrete abelian group. · OAI.KadisonKastler.abelianScalarInvariantMean

abKernelCycleEquiv def

The exact integral abelianized-kernel/Cayley-cycle comparison, with its literal Fox/path-chain coefficients. No graph realization is assumed. · OAI.EilenbergGanea.KernelCycles.abKernelCycleEquiv

Able def

The charge Z is additive work allowed (used in body proofs for calls). Unlike the budget W it does not get an implicit constant multiplier. · OAI.PowerSaving.RAM.Able

AboveAtomOrZero def

The upper table is zero or agrees with one higher-dimensional atom. · OAI.Thomason.Construction.SimplexComplex.AboveAtomOrZero

AboveIso structure

An isomorphism already constructed strictly above x, including the edge modules whose upper endpoints are above x. The latter are canonically supplied by the upper quotient rule in the local decomposition. · OAI.KLInvariance.MomentGraph.Sheaf.AboveIso

aboveMap def

A threshold request fixes its high prefix and first strictly-larger bit. · OAI.WLIdentification.BinaryAddress.aboveMap

abpContactSet def

A closed set large enough to contain every lower supporting point. · OAI.AffineBernstein.abpContactSet

absoluteConstant def

The absolute raw-envelope constant contains no frequency or carrier. · OAI.LipschitzHilbert.SourceLatticePacket.absoluteConstant

absoluteDiskAverage def

Absolute disk average, retaining possible infinite values. · OAI.CenteredDiskEndpoint.absoluteDiskAverage

absoluteDiskAverage def

Absolute disk average, retaining possible infinite values. · OAI.SignedDisk.CenteredDiskEndpoint.absoluteDiskAverage

absoluteMeasure def

A density measure built from the actual absolute values; a.e. changes of representative do not change any radius average. · OAI.DiskMaximalTools.absoluteMeasure

absoluteRate def

This coefficient contains only the fixed numerical parameters, never an instance size, aspect ratio, tree height, hidden law, or horizon. · OAI.UniformKServer.PartitionTree.absoluteRate

absoluteReference def

The held posterior used for the source's fixed-threshold core flags. · OAI.UniformKServer.RankTracking.absoluteReference

absolutize def

Convert the modular subtraction result to an absolute magnitude according to its genuinely computed borrow bit. · OAI.RationalHitting.StackLanguage.absolutize

Absorbs def

The absorbing equations, stated as finite-table membership, not as an additional computation oracle. · OAI.FiniteAlgebraicEnvelopes.Bootstrap.Absorbs

AbsorbsOInfinity def

Absorption of the Cuntz algebra, expressed by a star-algebra isomorphism. · OAI.WeakPureInfiniteness.AbsorbsOInfinity

AC def

Ordinary Choice for every set of nonempty sets. · OAI.PartitionConsistency.SetLanguage.AC

AC0Circuit inductive

Finite AC⁰ syntax in negation normal form. Sharing is not needed for the finite residue tests; literals can have either polarity. · OAI.TwoPointCorrelations.AC0Circuit

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

accepted def

Literal event specification for completed-data retrospective checking. The Boolean implementation of the arithmetic and the whole polynomial-time compiler are separate obligations, not consequences of this definition. · OAI.ExactQuantumFactoring.PhysicalTree.accepted

acceptedCount def

An occurrence index supplies Alice's full question and its equation. · OAI.MaxCutGames.Reduction.Incidence.acceptedCount

acceptedCount def

An occurrence index supplies Alice's full question and its equation. · OAI.UniqueGamesTheorem.Reduction.Incidence.acceptedCount

acceptedEquiv def

The table conversion preserves all chains, including zero upper chains. · OAI.Thomason.Construction.DirectedComplex.Cell.acceptedEquiv

acceptedSlots def

Invalid Alice answers lose in every slot. · OAI.MaxCutGames.Reduction.Incidence.acceptedSlots

acceptedSlots def

Invalid Alice answers lose in every slot. · OAI.UniqueGamesTheorem.Reduction.Incidence.acceptedSlots

accepts def

Explicit finite verifier. The occurrence and slot are randomness, never an additional argument supplied to Bob's strategy. · OAI.MaxCutGames.Foundations.PCP.accepts

accepts def

Lookup of the full stored binary predicate. · OAI.MaxCutGames.Foundations.PCP.PortTables.accepts

accepts def

A verifier using only the two displayed questions. The retained indices are verifier witnesses compatible with the displayed names, never player inputs. The output equality is the actual projection on all ambient coordinates. · OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.accepts

accepts def

Explicit finite verifier. The occurrence and slot are randomness, never an additional argument supplied to Bob's strategy. · OAI.UniqueGamesTheorem.Foundations.PCP.accepts

accepts def

Lookup of the full stored binary predicate. · OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.accepts

accepts def

A verifier using only the two displayed questions. The retained indices are verifier witnesses compatible with the displayed names, never player inputs. The output equality is the actual projection on all ambient coordinates. · OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.accepts

Access def

Ordinary capped access condition. Log is binary (Cost.Log n = log base two of (n+2)). Real constants. · OAI.Fifths.Single.Access

accessBody def

The outer access predicate, with the exact inner data callback fi. · OAI.PureTypeSystem.Labelled.DoubleCode.accessBody

accumulate def

Every draw is retained even when the reduction attempt fails. · OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.accumulate

accumulate def

This is exactly the accumulator update performed after each emitted row. · OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate

accumulate def

This is exactly the accumulator update performed after each emitted row. · OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.accumulate

accurateCall def

The relative-accuracy event describes the weight evaluator at each labelled state. · OAI.ContingencyTables.CompanionWeightOracle.accurateCall

accurateCall def

The relative-accuracy event for the rational labelled-weight estimate. · OAI.ContingencyTables.RootedWeightOracle.accurateCall

Achievable def

The liminf rate condition written as its eventual lower-bound characterization. There is no preshared entanglement, feedback, or restriction on encodings/decoding. · OAI.GAD.Achievable

act def

Read, carry out one stack/head transition, and return a label. · OAI.Fifths.SM.act

act def

Multiplication on the right by an old element acts only on the last new letter (or on the old coefficient, if no new letter is present). · OAI.PartitionConsistency.MergerAlgebra.Word.act

act def

Left multiplication commutes with the right transition maps. · OAI.PartitionConsistency.ProbeAlgebra.Path.act

actCLM def

The literal orthogonal action, bundled as a real continuous linear map. · OAI.ArnoldCounterexample.CriticalBound.actCLM

actCode def

Extend a permutation of the conditions by the identity on all other codes. · OAI.PartitionConsistency.SetForcingNames.ConditionAction.actCode

Action inductive

A nonraw literal sector, an unchanged singleton raw sector, or a genuine program call on an entire maximal raw run. · OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action

action abbrev

The ideal resolution in the coherent category. A Cartier hypothesis here is only local triviality of the closed ideal. · OAI.ActualCartier.action

action def

Independent permutations of the actual fibers, on the literal ambient set. · OAI.CoordinateSweeps.FiberBlocks.action

action def

Exact signed tensor representation of the symmetric group. · OAI.CoordinateSweeps.SignedTensor.action

action def

Multiplication/action on the first two positions of an augmented bar word. · OAI.DerivedBar.action

action def

The genuine enveloping algebra representation; the right action is encoded by Bᵐᵒᵖ. · OAI.ExternalTensor.action

action def

The actual Steinberg action, with its three defining relations verified. · OAI.FiniteAlgebraicEnvelopes.AffineAction.action

action def

A concrete action on the ordinary geometric root space over ℝ. Its faithfulness and the root-sign theorem are still required for the main proof. · OAI.KLInvariance.TitsSpace.action

action def

The original left B action on a genuine bimodule descends through balancing over B. · OAI.LittleFinitistic.BimoduleBalancedTensor.action

action def

The action on the formal summand, with restriction along alpha. · OAI.LittleFinitistic.FormalSummandAction.action

action def

Coordinate action induced by the genuine differential, not an assumed representation. · OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action

action def

The original vertex action is linear for the commuting right restriction. · OAI.LittleFinitistic.VertexFunctor.action

action def

The action is allowed to inspect only stack heads and the finite local variable. Its maps have finite domain and finite range. · OAI.UniformKServer.FlatTM2.action

action def

Extend the finite transition table by its stipulated frozen halts. · OAI.WLIdentification.Machine.action

ActionBound def

The local induction hypotheses used at a lambda. · OAI.PureTypeSystem.ObservationValues.ActionBound

ActionClaim def

The action inequality, with an extended-real supremum so boundedness is not implicit. · OAI.SharpLiebThirring.ActionClaim

actionCW def

A free permutation of cell orbits can be made strictly equivariant at the level of characteristic maps. This changes neither the space nor the cells. · OAI.GroupRingTopology.Cellular.actionCW

actionK def

Second component of H⁻¹ B. · OAI.PositiveEinsteinFour.HessianAlgebra.actionK

actionL def

Last component of H⁻¹ B. · OAI.PositiveEinsteinFour.HessianAlgebra.actionL

actionOfNormalizedExtension def

Construct the genuine additive action from a normalized extending family. The family is supplied by the separately proved determinant-frame construction; its group law is proved here, not taken as an assumption. · OAI.StableCoordinate.FrameLiftCoassoc.actionOfNormalizedExtension

actionP def

First component of H⁻¹ B, for H = diag(5/3,5,1). · OAI.PositiveEinsteinFour.HessianAlgebra.actionP

Active def

Only the fresh handoff and machine configurations participate in simulation; in particular there is no return to I,J,J',N,V. · OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Active

Active def

Only bins meeting the original good set require a reference. · OAI.SmoothObstruction.FiniteBins.Active

active def

Here l is the limit of the first excluded scale scale (N+1) / r. The retained colors have strictly larger scales. · OAI.BoltzmannNonuniqueness.GeometricBackground.active

active def

Trackers are not reinitialized; the active state alone is updated. · OAI.KServer.CoarseProcess.active

active def

Whether a switch has occurred since the most recent exceptional level. · OAI.LabelSwitches.active

active def

Active labels for any number of components. The selector support is common to the label, so the bound has no component-count factor. · OAI.LipschitzHilbert.SourceSlopeLabels.active

active def

The last activated stage at parameter p. · OAI.SeparableQuotient.CoherentClosures.active

active def

Whether a switch has occurred since the most recent exceptional level. · OAI.SignedDisk.LabelSwitches.active

ActiveBits structure

One coefficient bit at every active position; all other coefficients vanish. · OAI.MaxCutGames.Soundness.PartnerProjection.ActiveBits

ActiveBits structure

One coefficient bit at every active position; all other coefficients vanish. · OAI.UniqueGamesTheorem.Soundness.PartnerProjection.ActiveBits

activeBlockEquiv def

The active-block subtype counts exactly the full blocks of the active chains; no inactive full block is inserted into this stage. · OAI.TorsionFreeZeroDivisors.StageExpectation.activeBlockEquiv

activeCodes def

The set of active literal condition codes. · OAI.PartitionConsistency.SetForcingNames.AtomicForcing.activeCodes

activeCorrection def

The actual early--suffix formula after the scalar prefix conjugation. · OAI.ExactFourier.Boundary.activeCorrection

activeGraph def

A link is active in a band exactly when it has an allowed height there. · OAI.PlanarL1.Columns.Model.activeGraph

activeHead def

Empty heads are used exactly on zero components of the center. · OAI.BoundedTreePotentials.CostHeads.activeHead

activeLeaves def

The number of active leaves in the full m-ary tree of height h. A node is represented by its list of child indices, starting at the root. · OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.activeLeaves

activeMainFamily def

Changing a bound field changes no packet; the centered family uses the narrow modulation bound supplied by active labels. · OAI.LipschitzHilbert.SourceLabeledLattice.activeMainFamily

activeMass def

Actual source cell, not a giant-complement occurrence. · OAI.WeakPinned.SmallFiber.activeMass

activeNames def

Explicit list of occurring names, with duplicates removed. The list lengths depend only on occurrences; no interval of natural-number names is enumerated. · OAI.MaxCutGames.BinaryFormula.activeNames

activeNames def

Explicit list of occurring names, with duplicates removed. The list lengths depend only on occurrences; no interval of natural-number names is enumerated. · OAI.UniqueGamesTheorem.BinaryFormula.activeNames

activeOrientation def

Literal active chain orientations, with no padding by inactive chains. · OAI.TorsionFreeZeroDivisors.ChainActiveStages.activeOrientation

activePatches def

Only cutoffs whose closed support contains the point are active. · OAI.RegularPointCoordinates.activePatches

activePath def

Only paths ending in a nonzero terminal vector can carry particles. · OAI.IntrinsicMarks.activePath

activePath def

Only paths ending in a nonzero terminal vector can carry particles. · OAI.SignedDisk.IntrinsicMarks.activePath

ActivePrime def

A contiguous relation with a nonzero contribution from this label. · OAI.TwoPointCorrelations.ActivePrime

activeRadiusClock def

The radius clock measured from activation, in capacity-two time. The clock derivative is the square of the Poisson rate. · OAI.SLEExactGauge.Multipoint.activeRadiusClock

ActiveSet abbrev

The literal support of the uniform active-set sample. · OAI.MaxCutGames.Soundness.PartnerSampling.ActiveSet

ActiveSet abbrev

The literal support of the uniform active-set sample. · OAI.UniqueGamesTheorem.Soundness.PartnerSampling.ActiveSet

activeSet def

Active domain and literal held epoch mass, rather than a bound supplied to an allocation interface. · OAI.KServer.AllocationSchedule.activeSet

activeStart def

Reversed chronological histories. The active run's start is retained when its new label agrees, and is reset to the new time at a switch. · OAI.SignedDisk.SignedRuns.activeStart

activeStart def

Reversed chronological histories. The active run's start is retained when its new label agrees, and is reset to the new time at a switch. · OAI.SignedRuns.activeStart

Activity structure

One label of a nested-set system. Nesting and exact switching are the set invariants, not any embedding or separation assumption. · OAI.PlanarL1.Columns.Model.Activity

activityLimitSet def

Limiting points of activity as the positive parameter tends to zero, expressed using closed sets; no continuity of active is required. · OAI.Problem326.activityLimitSet

Actual def

This Borel set remembers the entire genuine orbit, and the actual cocycle value at every integer index, despite measurable trivializations. · OAI.SmoothObstruction.OrbitCocycle.Actual

actualAttachment def

The abstract single-stage attachment is obtained from the given ordinary CW complex itself, with no restriction on or enumeration of its cells. · OAI.EilenbergGanea.CWCollar.actualAttachment

actualBarResolutionIso def

The native bar functor's defining localization comparisons, with integer extension. · OAI.LittleFinitistic.BimoduleTotal.actualBarResolutionIso

actualBergerComparison def

The actual comparison used in the slow pulse: the scalar part is built from PB flow, not chosen as an unproved solution of a Riccati equation. · OAI.HarmonicCounterexample.LinearODE.actualBergerComparison

actualCanonicalPublishedOrientedData def

The complete flow preserves canonical base-volume times orthonormal-fiber probability under the measure-preservation hypothesis. · OAI.PositiveEinsteinFour.Geometry.actualCanonicalPublishedOrientedData

actualCellCover def

The actual regular covering target, constructed from ordinary group edge values satisfying the ORIGINAL cell equations. No lifted-chain conclusion is assumed. In particular it applies to quotient group values, not only to the bouquet … · OAI.HyperbolicObstruction.ConeSkeleton.actualCellCover

actualChildProducts def

Both actual child products, in the same preorder as the frequencies. · OAI.Ostmann.actualChildProducts

ActualColoredBlock structure

An actual finite block, centered using its ACTUAL input packet densities. The finite chain contains the anchor and every signal/refresh pair. · OAI.ThreeTorus.ActualColoredBlock

ActualColoredBlocks inductive

A finite trace of actual centered blocks. A is exactly the sum of their estimators. This data retains each anchor and each physical passage. · OAI.ThreeTorus.ActualColoredBlocks

ActualComparison structure

The sign records translation versus reflection, not a chosen graph label. · OAI.TorsionFreeZeroDivisors.PatternCoding.ActualComparison

actualCoordinateFunctions def

Literal covering-space coordinate functions; no representative choices enter. · OAI.Nagata.W06.TorusConfiguration.actualCoordinateFunctions

actualCoordinateSections def

The three actual holomorphic multiplier sections defining the genuine map. · OAI.Nagata.W06.TorusConfiguration.actualCoordinateSections

actualCost def

Exact number of transitions, including the final state-reset transition. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.actualCost

actualCost def

Exact number of transitions, including the final state-reset transition. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.actualCost

actualCoverOfEq def

Exact covering lifts after the source equality r=9+q. · OAI.Nagata.W06.TorusConfiguration.actualCoverOfEq

actualCubicBasis def

A chosen actual basis of D(3,γ), built from convergent theta sections. · OAI.Nagata.W07.actualCubicBasis

actualCubicExponentialMap def

Evaluate the actual cubic map in the genuine exponential parameter around a lift. · OAI.Nagata.W07.actualCubicExponentialMap

actualCubicMap def

The genuine projective map on the genuine multiplicative torus quotient. · OAI.Nagata.W07.actualCubicMap

actualCuntzDimensionState def

A chosen state on actual Cuntz classes. No analytic correspondence is claimed. · OAI.Kaplansky.actualCuntzDimensionState

actualDefectAmplificationEquiv def

Explicit matrix correspondence for every further amplification. · OAI.Kaplansky.actualDefectAmplificationEquiv

actualDihedralColumns def

The finite column of actual word inclusions. · OAI.KadisonSimilarity.actualDihedralColumns

actualDihedralInclusion def

Actual normalized word inclusion for the unit convention of the Fourier calculation. · OAI.KadisonSimilarity.actualDihedralInclusion

actualDisplacementOfEq def

The literal source displacement over each reindexed genuine torus point. This is an actual multiplier fibre, whose geometric normal identification is separate. · OAI.Nagata.W06.TorusConfiguration.actualDisplacementOfEq

actualDraw def

The real draw corresponding to a fixed mask and the independently sampled complement and hidden matrices. · OAI.MaxCutGames.Decoder.ActualAdviceUpper.actualDraw

actualDraw def

The real draw corresponding to a fixed mask and the independently sampled complement and hidden matrices. · OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.actualDraw

actualFirstOrder def

The actual first-order homomorphism associated with a nonzero element killed by the given residue map. Multiplicative K uses addition in K. · OAI.CirculantHadamard.actualFirstOrder

actualFullLabel def

The first-system labels together with the actual second-system boxes. · OAI.QuantitativeVanDerWaerden.CyclicColoring.actualFullLabel

actualGame def

The common weighted-game interface for the actual fixed-advice experiment. · OAI.MaxCutGames.Clean.StochasticBound.actualGame

actualGame def

The common weighted-game interface for the actual fixed-advice experiment. · OAI.UniqueGamesTheorem.Clean.StochasticBound.actualGame

ActualInterval structure

An actual comparison endpoint. Its path and integer position are retained. · OAI.TorsionFreeZeroDivisors.PatternCoding.ActualInterval

actualJetMap def

The actual manuscript jet map on the concrete polynomial section space. Its linearity follows from proved holomorphicity and differentiation rules. · OAI.Nagata.W20.actualJetMap

actualMarkedChart def

A genuine nonzero homogeneous coordinate is chosen at every actual marked point. · OAI.Nagata.W06.TorusConfiguration.actualMarkedChart

actualMarkedConfiguration def

Actual ordered distinct points with the cubic embedding premise discharged. · OAI.Nagata.W06.TorusConfiguration.actualMarkedConfiguration

actualMarkedConfigurationOfEq def

Exact r=9+q reindexing of the actual cubic configuration. · OAI.Nagata.W06.TorusConfiguration.actualMarkedConfigurationOfEq

actualMarkedPoint def

The actual cubic-map point, with multiplier exactly τ^η. · OAI.Nagata.W06.TorusConfiguration.actualMarkedPoint

actualMarkedVector def

Actual degree-three theta evaluation vector at each selected covering lift. · OAI.Nagata.W06.TorusConfiguration.actualMarkedVector

actualMatrixRestriction def

The actual finite rectangular matrix map into G, constructed from all its polynomial terms. This definition assumes no obstruction or lower bound. · OAI.Kaplansky.actualMatrixRestriction

actualOffspring def

The actual corner offspring distribution, not an abstract replacement. · OAI.FKCRT.Inventory.actualOffspring

actualParameter def

The actual coefficients are used only after the retained weights are known. · OAI.ReflexiveFixedPoints.CandidateLedger.actualParameter

actualPresence def

Actual lifetime: ages 0,...,K-1 certain, trials K,...,K²-1, compulsory retirement at K². · OAI.KServer.RosterLifetimes.actualPresence

actualProhibitedPrimeFamily def

The exclusion set need only contain prime divisors of the fixed shift. It may contain additional fixed primes, such as those dividing the modulus. · OAI.TwoPointCorrelations.actualProhibitedPrimeFamily

ActualProjectionConfiguration structure

Equal-Laplacian replacements and harmonic coordinates centered at the second point, with their source and normalization bounds. · OAI.RegularPointCoordinates.ActualProjectionConfiguration

ActualQuantileFamily def

The full conclusion of the actual quantile passage. This abbreviation contains geometry, exact Fourier coefficients, all moments, and both errors; its constructor below assumes no one of these output conclusions. · OAI.ThreeTorus.ActualQuantileFamily

actualRangeCalls def

The calls outside the families are the whole-input permutation, three block permutations, three size guesses, and three low-residue draws. · OAI.LowSpaceSubsetSum.RepresentationSetup.actualRangeCalls

actualRankSamplingStage def

Diagonalizing in the desired diagram size imposes no additional sampling hypothesis, and does not change the defining presentation. · OAI.HyperbolicObstruction.IncidenceTemplate.actualRankSamplingStage

actualRealCharacterZeroExpansion def

The Hadamard expansion fields of the real-zero input. · OAI.Ostmann.actualRealCharacterZeroExpansion

ActualRealLowHeightRegion def

The low-height clause of Montgomery--Vaughan 11.3/11.10, stated for the analytic multiplicity enumeration. · OAI.Ostmann.ActualRealLowHeightRegion

actualRow def

Read one row of the actual output, in the chosen global coordinates. · OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.actualRow

actualRow def

Read one row of the actual output, in the chosen global coordinates. · OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.actualRow

actualRowCost def

Source Equation (sample:eq-costs), with the critical integer cost displayed. · OAI.HyperbolicObstruction.IncidenceTemplate.actualRowCost

actualSplitProducts def

Prime products of the actual pair of splits. · OAI.JointDickman.actualSplitProducts

actualSuccess def

Actual success starts with genuinely sampled hidden and complement maps. The iid incidence law includes every slot choice, including unused choices at full positions. Policies receive only their respective visible table. · OAI.MaxCutGames.Decoder.AdviceLaw.actualSuccess

actualSuccess def

Actual success starts with genuinely sampled hidden and complement maps. The iid incidence law includes every slot choice, including unused choices at full positions. Policies receive only their respective visible table. · OAI.UniqueGamesTheorem.Decoder.AdviceLaw.actualSuccess

actualTestOperator def

Actual bounded blocks of the normalized bundle test, at all levels. · OAI.Kaplansky.actualTestOperator

actualThetaBasis def

The exact centered source vectors, retaining their local scalar normalization. · OAI.Nagata.Workers.W10.actualThetaBasis

actualTransverse def

The finite coefficient formula for the b-th transverse derivative at y=0. · OAI.Nagata.W20.actualTransverse

actualTransverseLinear def

A transverse expression is a linear function of the actual polynomial section, before any choice of basis. · OAI.Nagata.W20.actualTransverseLinear

ActualType def

Source actual types: a normal sorted expression, or a literal sort. · OAI.PureTypeSystem.Candidates.ActualType

actualWeights def

Weights are the literal selected-face multiplicities and maximum of actual apex count / same-top slot multiplicity. No contact capacity is a field. · OAI.HyperbolicObstruction.ConeSkeleton.actualWeights

actualWeights def

Weights are the literal selected-face multiplicities and maximum of actual apex count / same-top slot multiplicity. No contact capacity is a field. · OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actualWeights

ACwo def

Choice for every ordinal-indexed family of nonempty sets, including ordinals which may fail to be well founded from outside a model. · OAI.PartitionConsistency.SetLanguage.ACwo

AcylindricallyHyperbolic def

An isometric non-elementary acylindrical action on a geodesic Gromov-hyperbolic metric space. · OAI.HarmonicArtin.ParabolicIntersections.AcylindricallyHyperbolic

Adapted def

The cut at zero is the genuine inversion set of the upper vertex. · OAI.KLInvariance.TitsSpace.RatioOrder.Adapted

Adapted def

Functions known from the observed finite history label. · OAI.KServer.RankTracking.Adapted

adaptedBasis def

The explicit basis obtained by transporting the initial-corner basis. · OAI.Generator.MatrixUnitSystem.adaptedBasis

adaptedTensor def

All multiplication coefficients in the explicit adapted bases. Here a=d+1, b=e+1, and no first-leg change of coordinates occurs. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor

adaptive_parent_return def

Choose the proved finite parent return, retaining all its witnesses. · OAI.ReflexiveFixedPoints.adaptive_parent_return

adaptiveFailureCount def

Number of failed attempts along the actual adaptive state trajectory. · OAI.LeanBlast.SecondKahnKalai.adaptiveFailureCount

AdaptiveLinearWindows structure

Both window endpoints are chosen from the past history. Within a history A_t is contained in D_t, and D_t is contained in either next A_{t+1}. There is deliberately no support assertion. · OAI.BoundedTreePotentials.CostHeads.AdaptiveLinearWindows

AdaptiveParentReturn structure

A finite return to one parent. state and selected describe the entire legal sequence. retain extracts exactly its positive coefficients in the original order, without discarding any of the stored transitions. · OAI.ReflexiveFixedPoints.AdaptiveParentReturn

adaptivePartition def

The actual centered adaptive mesh, translated to the shared fundamental interval. This is a translation of cells, not an identification of labels. · OAI.QuantitativeVanDerWaerden.adaptivePartition

adaptivePivotCoefficients def

Choose any valid completion of the exposed prefix. The precision theorem below proves that the required reduced coefficients do not depend on it. · OAI.Ostmann.adaptivePivotCoefficients

adaptiveRun def

A deterministic adaptive update iterated over a finite sequence of draws. · OAI.LeanBlast.SecondKahnKalai.adaptiveRun

adaptiveSeedStep def

Only the coordinate belonging to the actual incoming table is consumed. All states within that coordinate retain their shared copy streams. · OAI.EditApproximation.adaptiveSeedStep

add def

The manuscript's two-vector cone addition (not an associative operation). · OAI.HyperbolicObstruction.ConeData.add

add def

Actual block addition, relabeled by the standard finite-sum equivalence. · OAI.Kaplansky.CuntzPositiveMatrix.add

add def

Addition preserves positivity of the factorial-basis coefficients. · OAI.Problem335.FactorialExpansion.add

add def

Destructive binary addition. The second operand and all scratch words are cleared; the first register holds the exact sum. · OAI.RationalHitting.StackLanguage.add

add def

Positive tables add without an artificial augmentation-one restriction. · OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable.add

add def

Pointwise addition of the actual extended weights, including infinite values. · OAI.TraceConeClassification.ExtendedTrace.add

addAux def

Introduce two vacant auxiliary wires at the input boundary. · OAI.CriticalHoneycomb.Transfer.PlanarNormalization.addAux

addChan def

Lift the derivative changes into one actual abstract cross Gram (on column channel arguments only). · OAI.HadwigerCounterexample.addChan

addColumn def

Append a scaled original input into each existing output accumulator. The two scalar operations per row are charged even for a zero scalar. · OAI.ExactFourier.LinearDAG.addColumn

addEdge def

The identity with one extra pair. · OAI.OneWayLiveness.BRel.addEdge

addEdge def

Adjoining one new edge. · OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge

addInTime def

A composable time witness whose stored transition count is exactly a + 1. · OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.addInTime

addInTime def

A composable time witness whose stored transition count is exactly a + 1. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAddAt.addInTime

additionalPoint def

The extra point on line zero. For the triangle it is (-5,0). · OAI.Nagata.W06.LineArrangement.additionalPoint

additionMatrix def

Actual row-conditioned addition matrix, with the required zero diagonal. · OAI.DistinctLifts.additionMatrix

AdditionProperty def

The paper's addition property: fix precisely k-2 elements and test only the remaining quadratic matrix. · OAI.ContingencyTables.BinaryContraction.AdditionProperty

additive def

The compatible derivation on the basis extends as an additive map to all opens, using the sheaf condition of the target. · OAI.AffineDerivation.additive

additive def

Compatible principal-open comparison, extended by sheaf gluing. · OAI.AffineExterior.additive

additiveCharacter def

The usual additive character e(αn) = exp(2πiαn). · OAI.TwoPointCorrelations.additiveCharacter

additiveFiberEquiv def

Translate an additive fiber to the zero fiber. · OAI.Ostmann.additiveFiberEquiv

additiveFourier def

The additive Fourier transform with probability normalization. · OAI.Ostmann.additiveFourier

addMod def

One extra carry bit before reduction avoids overflow even on noncanonical coefficient representatives; all arrays use exactly as many bits as specified. · OAI.ExactQuantumFactoring.BitArithmetic.addMod

addParameterHom def

Substitute the sum of the two independent action parameters. · OAI.StableCoordinate.FrameLift.addParameterHom

Address abbrev

A left half-table address or the one dummy address. · OAI.MaxCutGames.Foundations.Hastad.EmptyContext.Address

Address abbrev

Left and right stored tables have disjoint variable names. · OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.Address

Address abbrev

A left half-table address or the one dummy address. · OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.Address

Address abbrev

Left and right stored tables have disjoint variable names. · OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.Address

address def

Every earlier rejected selector and the selected selector are tested. · OAI.Problem310.FirstDefault.address

addressCount def

The number of words with length at most t, including the empty word. · OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.addressCount

addressCount def

The number of words with length at most t, including the empty word. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.addressCount

addressEquiv def

Arithmetic prefix sums give a rank for every bounded-length address. · OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.addressEquiv

addressEquiv def

Arithmetic prefix sums give a rank for every bounded-length address. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.addressEquiv

AddressIndex abbrev

A local label slot is an index into the explicit bounded address list. · OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.AddressIndex

AddressIndex abbrev

A local label slot is an index into the explicit bounded address list. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.AddressIndex

addressIndex def

Tape roles: tail, old reverse, relation, scratch, divided copy, quotient, new reverse, accumulated output, row buffer. · OAI.MaxCutGames.Foundations.Complexity.MachineLazyRows.addressIndex

addressIndex def

Tape roles: tail, old reverse, relation, scratch, divided copy, quotient, new reverse, accumulated output, row buffer. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.addressIndex

addSplit def

Output invariant for the single pass: a reversed low part is on out. · OAI.RationalHitting.StackLanguage.addSplit

addTerminalFields def

Actual addition of two (possibly mixed-sign) finite external fields. · OAI.BufferedIsing.addTerminalFields

addWord def

Grade-school addition, scanning the second operand one bit at a time. The first operand is shifted after adding the incoming low bit. · OAI.RationalHitting.StackLanguage.addWord

aDeriv def

The derivative profile of a, with its common values at the junctions. · OAI.ThompsonNonamenability.Analytic.aDeriv

Adj def

Adjacency across a full triangular edge. · OAI.CriticalHoneycomb.Adj

Adj def

Independent finite arithmetic facts; the source labels are Z/5Z, represented by Fin 5. · OAI.EuclideanFiveColor.FiveComb.Adj

Adj def

Adjacency in the graph dual to the band sides, with orientations retained. · OAI.KervaireFlow.Adj

Adj def

The six triangular-lattice steps, not square-lattice adjacency. · OAI.TriangularSurface.Lattice.Adj

adjacencyTableGraph def

Present H by a separately checked finite adjacency table. · OAI.CycleClique.Construction.adjacencyTableGraph

Adjacent def

A neighbor is distinct and meets the vertex in a hyperplane. The explicit distinctness also makes the definition harmless at dimension zero. · OAI.MaxCutGames.Inverse.KMS.Adjacent

Adjacent def

A neighbor is distinct and meets the vertex in a hyperplane. The explicit distinctness also makes the definition harmless at dimension zero. · OAI.UniqueGamesTheorem.Inverse.KMS.Adjacent

adjacent def

Literal child lists for one adjacent event; the decoration is exactly the allowed passage table, with its full two-block identified quotient. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep.adjacent

adjacent def

Adjacent layer positions in either order. · OAI.Problem335.BalancedSchedule.adjacent

adjacent def

Adjacent positions of the path, in either orientation. · OAI.Problem335.PathIsolatedWeight.adjacent

adjacentHypergeomTV def

Exact adjacent visible-count TV, expressed with complementary hidden counts. The shift by one is essential: the two totals are different. · OAI.TraceReconstruction.adjacentHypergeomTV

adjacentSwitches def

Number of interfaces at which a word changes its letter. · OAI.Problem335.Pairings.adjacentSwitches

adjoin def

Build the augmented hole family directly from disjoint geometry. · OAI.CoordinateSweeps.Grid.Holes.adjoin

adjointCharacterHom def

The actual adjoint diagonal integrates exactly the canonical height characters, using the already required representation and exponential chart. · OAI.PolycyclicRecognition.adjointCharacterHom

adjointEquiv def

The genuine adjoint equivalence of a transverse linear normalization. · OAI.AffineBernstein.adjointEquiv

adjointEquiv def

Invertibility of the transpose uses the transpose of the inverse. · OAI.PettyProjection.adjointEquiv

adjointExponentialLinear def

The algebraic endomorphism underlying the analytic exponential of ad x. The auxiliary finite-dimensional norm is not part of the output. · OAI.PolycyclicRecognition.adjointExponentialLinear

adjointGroupAutomorphism def

Integration of the complete adjoint action, including its residual part. · OAI.PolycyclicRecognition.CartanWordModel.adjointGroupAutomorphism

adjointOperator def

The adjoint operation, viewed as a real continuous linear map. · OAI.RegularPointCoordinates.adjointOperator

adjointRealizationHomotopy def

An arbitrary continuous homotopy on a realization has a simplicial adjoint, with its two specified adjoint endpoint maps. · OAI.Thomason.Construction.adjointRealizationHomotopy

adjointVector def

The coefficient vectors used in the adjoint bound. · OAI.SeparableQuotient.PrefixNormers.adjointVector

adjTransport def

The genuine Hermitian formal adjoint of dbar+a, written using conjugation and the transpose coefficient. No elliptic right inverse is assumed. · OAI.ElasticityPlanar.adjTransport

adjunction def

Transport of the global right interval adjunction preserves its actual functors. · OAI.Thomason.ConstructedInterval.adjunction

adjunction def

Lambda is left adjoint to the actual positive-table realization nu. · OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.adjunction

adjunction def

The actual global right interval internal-hom adjunction. · OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.adjunction

adjunction def

The explicit intelligent-truncation / inclusion adjunction. · OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.adjunction

adjunction def

The actual zero-fibre / terminal-cone adjunction. · OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.adjunction

adjunction def

The interval cylinder is left adjoint to compact-open paths. · OAI.Thomason.Construction.TopologicalInterval.adjunction

adjunction def

Product with a locally compact parameter is left adjoint to its compact-open mapping-space functor. · OAI.Thomason.Construction.TopologicalProduct.adjunction

Admissible structure

Exactly the standing hypotheses (model:integrability through positivity). norm on the finite function space is max_s |theta(s)|. · OAI.DilutedSpinGlass.Admissible

Admissible def

Strict ancestry and the genuine terminal grid horizon. · OAI.DilutedSpinGlass.ReducedTopology.Admissible

Admissible def

A chain of nonbottom elements satisfying the admissibility condition. · OAI.FiniteChain.Admissible

Admissible def

A label-decreasing self-map; collapsed edges are permitted. · OAI.FiniteCongruence.Admissible

Admissible def

Exact admissibility from Definition 2.3 of the manuscript. · OAI.HyperbolicObstruction.IncidenceTemplate.Admissible

Admissible def

Admissibility uses the long-side length restriction, with no restriction when K = 0. · OAI.LipschitzHilbert.Rectangle.Admissible

Admissible structure

Normalized twice continuously differentiable potentials with Hessian between the identity and twice the identity. · OAI.LogConcaveSampling.Admissible

Admissible abbrev

Maps satisfying the geometric complement conditions, before their compression is fixed. · OAI.MaxCutGames.Appendix.AntecedentCount.Admissible

Admissible structure

The explicit inequalities from the parameter lemma that are consumed by both circuit-rank and moment estimates. All are asserted for the same n. · OAI.Problem335.LowerParameters.Admissible

Admissible structure

Exact support, succession, weight and metadata conditions of a path. The Type-I construction contributes only additional restrictions, not needed below. · OAI.SeparableQuotient.PathCoding.RawPath.Admissible

Admissible def

An admissible cutoff includes all heavy points and meets the truncated weighted-excess test. · OAI.TalagrandThreshold.Selector.Admissible

Admissible structure

Actual states on a regular recursively extendible ray. Boundary initial states are allowed only with strict inward velocity. · OAI.TriangularBilliards.Admissible

Admissible abbrev

Maps satisfying the geometric complement conditions, before their compression is fixed. · OAI.UniqueGamesTheorem.Appendix.AntecedentCount.Admissible

Admissible def

A stronger sufficient family using globally completed cut stars. Its address restriction is imposed only by wrapping subcollections of size r. · OAI.WLIdentification.ComparisonSchemas.SpecialImages.Admissible

admissible def

Value zero means no displacement; a nonzero tuple entry i+1 means color i. · OAI.DoublingHilbert.admissible

admissible def

Zero belongs to the admissible control space as a genuinely absent pulse, not as the generally nonzero word at parameter zero. · OAI.HarmonicCounterexample.LinearODE.PhysicalWord.admissible

admissible def

Literal three errors entering the actual endpoint-minor theorem. · OAI.SmoothObstruction.EndpointBudget.admissible

admissible def

All allowed transpositions for the distinguished port, omitting prior edges and both radius-R endpoint balls. · OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.admissible

AdmissibleDensity def

Almost-everywhere measurable probability densities between fixed bounds. · OAI.WeakMTWTransport.AdmissibleDensity

AdmissibleExponent def

Positive slack, one uniform constant, and a correct program at every size. · OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.AdmissibleExponent

AdmissibleExponent def

Positive slack, one uniform constant, and a correct program at every size. · OAI.MatrixMultiplication.Arithmetic.AdmissibleExponent

AdmissibleField def

The smooth vector fields on the flat torus with pointwise length at most one, expressed as Z³-periodic fields on its Euclidean cover. The explicit ℕ∞ index is C^∞; top of WithTop ℕ∞ would instead mean analytic in this Mathlib. · OAI.CubicTorus.AdmissibleField

AdmissibleGlobal structure

Full global admissibility, including both separately renormalized collision terms, local mass, total momentum, and the every-time energy and entropy inequalities. · OAI.BoltzmannNonuniqueness.AdmissibleGlobal

AdmissibleLocal structure

Local admissibility retains endpoint terms for arbitrary tests. This permits pasting at T without assuming that a test vanishes at the joining time. · OAI.BoltzmannNonuniqueness.AdmissibleLocal

admissibleSets def

All admissible subsets are fixed before a pair of rows is chosen. · OAI.MetricEntropyDuality.FiniteFieldRows.admissibleSets

admissibleWordFamily def

Every word admitted by the source definition, with its leading coefficient. · OAI.Generator.Tracial.admissibleWordFamily

AdmitsBiLipschitzEmbedding def

Finite distortion includes an arbitrary positive change of scale. · OAI.DoublingHilbert.AdmitsBiLipschitzEmbedding

Admitted def

Literal admission; every ordinary seed is kept, and in an ordered chart this tests all points on the intrinsic narrow-band sphere. · OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.Admitted

Admitted abbrev

The small carrier before quotienting. · OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Admitted

admittingExponents def

Exponents giving a fixed Laurent monomial in a mixed rounded divisor. D i j is the coefficient of the i-th resolved summand along the j-th snc component. K j and n j are the relative-canonical and monomial exponents. · OAI.CartierSections.LocalMultiplier.admittingExponents

advance def

Propagation through halt is explicit, as in the supplied TM2 support. · OAI.OptimalMaxCut.CounterMachine.advance

advance def

Advance to the next finite frontier using only the completed choices. · OAI.ReflexiveFixedPoints.CandidateContext.advance

advance def

Exactly one primitive; the AST is not evaluated in a unit-cost StackCompiler.step. · OAI.UniformKServer.FlatTM2.advance

advance def

Little-endian carry without converting or enumerating the address space. · OAI.WLIdentification.BinaryAddress.advance

adviceMass def

The row-advice probability in actual matrix coordinates. In particular, dependent rows of A are sampled with their full multiplicity. · OAI.MaxCutGames.Decoder.ActualGoodRows.adviceMass

adviceMass def

Sample a uniform matrix, then an independent uniform row map. · OAI.MaxCutGames.Inverse.RowErasure.adviceMass

adviceMass def

The row-advice probability in actual matrix coordinates. In particular, dependent rows of A are sampled with their full multiplicity. · OAI.UniqueGamesTheorem.Decoder.ActualGoodRows.adviceMass

adviceMass def

Sample a uniform matrix, then an independent uniform row map. · OAI.UniqueGamesTheorem.Inverse.RowErasure.adviceMass

AECellPartition structure

The ordinary measurable, almost-everywhere partition properties of cells. · OAI.Problem358.StationaryMoment.AECellPartition

AF abbrev

The real algebraic field and the literal discrete quotient F/Z. · OAI.PlaneFiveColor.InvariantMean.AF

affine def

Translate and dilate the physical coordinates without changing the curve parameter. · OAI.SLEExactGauge.RibbonPassageScaling.affine

AffineActive def

Pairwise comparison formulation of activity in a finite affine family. · OAI.Problem326.AffineActive

affineAll def

Simultaneously replace every variable X i by a * X i + b. · OAI.StableCoordinate.affineAll

affineAreaDensity def

The density of affine area in the original graph coordinates. · OAI.AffineBernstein.affineAreaDensity

affineAverage def

The paper uses this with weights W r = conj (G r). · OAI.Ostmann.affineAverage

affineAvoidanceChart def

A finite chart chooses a nonzero signed real coordinate for each image. · OAI.Kaplansky.affineAvoidanceChart

affineAvoidanceSet def

The complement of finitely many affine zero sets, including dependent or zero affine maps. No general-position or nonempty assumption is made. · OAI.Kaplansky.affineAvoidanceSet

AffineBarrierData structure

Finite barrier data, after the network, rates, and initial point have been fixed. The remaining analytic step is trapping and global ODE continuation. · OAI.Problem326.BarrierConstruction.AffineBarrierData

affineBase def

The canonical point of the affine hyperplane with normal n and intercept a. · OAI.Problem358.TangentNormalCoordinates.affineBase

affineBaseMap def

The affine pullback uses the continuous map associated with the actual matrix, so its determinant and nonsingularity have their usual meanings. · OAI.AffineBernstein.affineBaseMap

affineChangedColumn def

The local constant is supplied by a genuine compact Sobolev cutoff. · OAI.RegularPointCoordinates.affineChangedColumn

affineChannel def

padding by a fixed suffix leaves joint law unchanged · OAI.ExactDerandomization.Analysis.affineChannel

affineChartCoordinateMotion def

The manuscript's affine-linear motions in the chosen local charts, expressed as actual coordinate polynomials in the parameter. · OAI.Nagata.Workers.W14.affineChartCoordinateMotion

affineCoefficient def

The coefficient normalization for the operator T* T. · OAI.Ostmann.affineCoefficient

affineCoefficientSum def

The unnormalized coefficients obtained by collecting ordered unit pairs. · OAI.Ostmann.affineCoefficientSum

affineCohEquiv def

Affine coherent sheaves are genuinely equivalent to finite modules. · OAI.CoherentGlobal.affineCohEquiv

affineCoordinate def

Scaling and translating a signed lattice coordinate uses genuine binary arithmetic and emits the signed-coordinate code. · OAI.ContinuumCoulomb.EncodingPrograms.affineCoordinate

affineCoordinateMap def

Constants and linear combinations of the given coordinates, restricted as actual L² functions on the testing set. · OAI.RegularPointCoordinates.affineCoordinateMap

affineCoordinateMotion def

A literal polynomial affine motion, valid for every parameter. · OAI.Nagata.Workers.W17.affineCoordinateMotion

affineCoordinates def

Coordinates of a uniform linear map, translated by a fixed linear map, are still exactly uniform. This also covers zero-dimensional free domains. · OAI.MaxCutGames.Inverse.KMSAffineRestriction.affineCoordinates

affineCoordinates def

Translation after the reflection straightens an affine hyperplane. · OAI.Problem358.HouseholderCoordinates.affineCoordinates

affineCoordinates def

Affine coordinates with arbitrary Euclidean vertex locations. · OAI.Thomason.Construction.SubdivisionBarycentric.affineCoordinates

affineCoordinates def

Coordinates of a uniform linear map, translated by a fixed linear map, are still exactly uniform. This also covers zero-dimensional free domains. · OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.affineCoordinates

AffineCorrectedElliott def

Corollary 1.3 (cor:affine), including coefficients sharing prime factors. · OAI.TwoPointCorrelations.AffineCorrectedElliott

AffineCoset def

A coset variable is its full point set, so no arbitrary representatives enter the random choices. · OAI.KaplanskyCounterexample.FiniteGeometry.AffineCoset

affineCounitIso def

The canonical affine quasi-coherent counit isomorphism. · OAI.CartierAffineLattice.affineCounitIso

AffineCoverData structure

An affine cover retaining its actual interval endpoints. · OAI.Paper170.AffineCoverData

affineDefining def

The genuine defining function for any affine coordinates of the graph. · OAI.AffineBernstein.affineDefining

AffineDensityBound def

All affine restrictions with at most r prescribed input/output dimensions have normalized squared density at most ε. The dimension sum avoids any truncated-subtraction ambiguity. · OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound

AffineDensityBound def

All affine restrictions with at most r prescribed input/output dimensions have normalized squared density at most ε. The dimension sum avoids any truncated-subtraction ambiguity. · OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound

affineDetBarrier def

Literal log-determinant barrier. On a negative section its logarithmic cutoff is exactly log (-u), because the real logarithm uses absolute value. · OAI.AffineBernstein.affineDetBarrier

affineDetPhase def

Continuous phase whose logarithm is the maximum-principle barrier on a negative section; the phase vanishes, rather than diverging, on its boundary. · OAI.AffineBernstein.affineDetPhase

affineDistance def

A physical affine coordinate, including a reflected tree coordinate. · OAI.ContingencyTables.EqualitySoftening.affineDistance

affineDualIso def

The affine sheaf dual is the associated sheaf of the actual module dual. Coherence, rather than a blanket Hom/localization assumption, supplies the counit isomorphism. · OAI.CoherentDual.affineDualIso

affineDualPullbackGammaIso def

Global sections of affine pullback of the sheaf dual are the tensor extension of the module dual, as modules over the target ring. · OAI.CoherentDual.affineDualPullbackGammaIso

affineDualPullbackIso def

A concrete affine restriction of the actual sheaf dual, with the actual scalar-extension module, rather than a substitute quotient object. · OAI.CoherentDual.affineDualPullbackIso

affineEIso def

The affine description of the precise double-dual model extension. · OAI.CoherentModelActual.affineEIso

affineEnvelope def

Envelope for twice the affine-signature count times the survival bound. · OAI.QuantitativeVanDerWaerden.Parameters.affineEnvelope

affineEpigraphFiber def

A genuine affine slice of the original epigraph, in arbitrary transverse coordinates. · OAI.AffineBernstein.affineEpigraphFiber

affineEpigraphLogMeasure def

The paper's sigma measure, pushed to logarithmic coordinates. This definition uses the actual affine epigraph support function, not an abstract model metric. · OAI.AffineBernstein.affineEpigraphLogMeasure

affineEpigraphPullback def

The literal inverse image of the original epigraph under affine coordinates. · OAI.AffineBernstein.affineEpigraphPullback

affineEPullbackGammaIso def

The actual section module of a restriction of the affine double-dual model extension, expressed as an honest scalar extension of the double dual. · OAI.CoherentModelActual.affineEPullbackGammaIso

affineFirstDualIso def

The first sheaf dual of the actual pullback is the associated module dual of the actual tensor extension, not an abstract reflexive object. · OAI.CoherentModelActual.affineFirstDualIso

AffineForm structure

A real affine form in e parameters. · OAI.QuantitativeVanDerWaerden.AffineForm

affineFourierMatrix def

The input frequency is ξ and the output frequency is η. · OAI.Ostmann.affineFourierMatrix

affineGraphConormal def

The inward conormal of the actual affine-image graph, pulled back to its original base. Its norm is NOT replaced by a vertical component. · OAI.AffineBernstein.affineGraphConormal

affineGraphPullback def

Change of base variables, positive vertical scaling, and arbitrary affine height correction. This includes the normalization of sections in rigidity. · OAI.AffineBernstein.affineGraphPullback

affineHomEquiv def

The affine comparison on Hom sets, using sheaf derivations. · OAI.ActualCotangent.affineHomEquiv

affineHomLinearEquiv def

The global sections of the actual affine internal Hom are precisely the module Hom, as modules, not merely as abstract sets. · OAI.CoherentDual.affineHomLinearEquiv

affineIdealUnitIso def

On an affine target, a section-module trivialization produces a sheaf trivialization by the proved coherent affine equivalence. · OAI.ActualCartier.affineIdealUnitIso

affineImageCapArea def

Affine area of the actual cap, in the original global graph chart. The determinant exponent is the one proved for the literal parametric density. · OAI.AffineBernstein.affineImageCapArea

affineImageLinearCapArea def

The affine-area cap for an arbitrary linear height, in the original literal graph chart. · OAI.AffineBernstein.affineImageLinearCapArea

affineIncidenceGraph def

Line vertices and point vertices are distinct, even when their types coincide. · OAI.TwoPointCorrelations.affineIncidenceGraph

affineInTime def

The affine template itself has an actual composable machine certificate. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.affineInTime

affineInTime def

The affine template itself has an actual composable machine certificate. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.affineInTime

affineIso def

The intrinsic cotangent sheaf of Spec R over k is the tilde sheaf of its Kähler module. · OAI.ActualCotangent.affineIso

affineIso def

The intrinsic exterior sheaf on an affine scheme is the tilde of its exterior module, constructed without local-rank or coherence assumptions. · OAI.AffineExterior.affineIso

affineJetEntry def

The coefficient of ξ^u η^v in (x+ξ)^a (y+η)^b, written as a polynomial in the coordinates of point i. This explicit expression is used without a claimed Taylor/multiplicity bridge. · OAI.Nagata.W27.affineJetEntry

affineKernel def

The exact Jacobian kernel for the affine-on-the-good-arc neutral jitter. · OAI.ThreeTorus.affineKernel

AffineLine structure

A full affine line, not a segment or a subset of one. · OAI.KaplanskyCounterexample.PolynomialPairing.AffineLine

affineLineGraph def

The actual affine graph polynomial of line i, using U=-x. · OAI.Nagata.Workers.W24.affineLineGraph

affineLineMap def

Standard affine parametrization, with the marked point at parameter zero. · OAI.Release075.affineLineMap

affineLineVector def

Explicit nonzero homogeneous coordinates [1 : z : 0]. · OAI.Nagata.ProjectiveGeometry.affineLineVector

affineLogTail def

Logarithmic comparison primitive on the upper half of the marked integral. · OAI.KServer.SimplexAnalytic.affineLogTail

affineMap def

Translated coordinates for a hyperplane through base. · OAI.Problem358.TangentNormalCoordinates.affineMap

affineMinimum def

The finite affine minimum used as a barrier. All minimizing labels are active; no tie-breaking convention is built into this definition. · OAI.Problem326.Barrier.affineMinimum

affineModule abbrev

The affine Kähler module, bundled before subsequent specialization. · OAI.ActualCotangent.affineModule

affineModule abbrev

The actual scalar-extension module on an affine model chart. · OAI.CoherentModelActual.affineModule

affineMomentFamily def

Target, constant and coordinate functions, in that order. · OAI.RegularPointCoordinates.affineMomentFamily

AffineNeighborRow structure

One affine supported pair together with its original sampling data. The fields record the actual maps, cells, root step and weak law; no neighbor-label conclusion is included. · OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow

affineParameters def

Slope and translation of the affine map underlying U_r^* U_s. The translation is written in ratio coordinates. · OAI.Ostmann.affineParameters

affineParametricVariationArea def

The literal arbitrary affine image of a parametrized graph variation. · OAI.AffineBernstein.affineParametricVariationArea

affinePath def

The canonical affine term includes the prescribed initial data and actual heat source. · OAI.ForcedComputation.PlaneScalarMild.CompatibleData.affinePath

affinePlaneVector def

The standard two-dimensional affine chart [1 : z₀ : z₁]. · OAI.Nagata.ProjectiveGeometry.affinePlaneVector

affineProfileClass def

Restrictions of the finitely many linear profiles, with arbitrary offsets. · OAI.PolycyclicRecognition.affineProfileClass

affineProgressions def

The designated affine family is the actual nonzero-step family whose centered representative vectors are affine in the sample index. · OAI.QuantitativeVanDerWaerden.CyclicColoring.affineProgressions

affineProjection def

The least-squares affine fit exists without assuming independence of its generators. Coefficient uniqueness can be added after normalization. · OAI.RegularPointCoordinates.affineProjection

affinePullbackGammaIso def

Affine pullback on a quasicoherent sheaf, on global sections. · OAI.CoherentGlobal.affinePullbackGammaIso

affinePunctureSectionsIso def

The precise puncture identification on the associated section modules. · OAI.CartierAffineLattice.affinePunctureSectionsIso

affineReflectionPath def

This path has an explicit affine formula and retains every commutator bound of the reflection. Its speed is at most π. · OAI.WeakPureInfiniteness.affineReflectionPath

affineResidual def

The residual is a bounded linear map, so all scalar directional fits can be assembled linearly before taking their matrix coefficients. · OAI.RegularPointCoordinates.affineResidual

affineResultTapes def

Exact final dependent tape family, with all other tape contents retained. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes

affineResultTapes def

Exact final dependent tape family, with all other tape contents retained. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineResultTapes

affineScalar def

Scalar action on a quasi-coherent affine sheaf via its canonical section-module presentation, rather than an unspecified endomorphism. · OAI.CartierAffineLattice.affineScalar

affineSchur def

The affine oblique Schur complement after diagonalizing the shared positive symmetric pencil. · OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.affineSchur

affineSincSchwartz def

The genuine affine sinc multiplier applied to a Schwartz packet. · OAI.LipschitzHilbert.affineSincSchwartz

AffineSlice def

The concrete affine slice around any one point satisfying its equations. · OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.AffineSlice

AffineSlice def

The concrete affine slice around any one point satisfying its equations. · OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.AffineSlice

affineSpaceIsoOfAlgEquiv def

A polynomial-ring algebra presentation gives affine space as a scheme, not just its underlying collection of rational points. · OAI.StableCoordinate.AffineGeometry.affineSpaceIsoOfAlgEquiv

affineSpaceOverIsoOfAlgEquiv def

Scheme-over-base version of polynomial-ring coordinates. · OAI.StableCoordinate.AffineGeometry.affineSpaceOverIsoOfAlgEquiv

affineSum def

The ordinary affine correlation, allowing nonunit coefficients. · OAI.TwoPointCorrelations.affineSum

affineSwap def

The genuine polynomial-ring equivalence exchanging the two affine variables. · OAI.Nagata.Workers.W17.affineSwap

affineTailPhase def

Extend a finite phase by keeping its final increment constant. · OAI.Problem337.affineTailPhase

affineTorusEquivalence def

The literal affine-Steinberg mapping torus is the previously constructed full action group. · OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.affineTorusEquivalence

affineValue def

Evaluation of an affine real coordinate by its original vertex values. · OAI.Thomason.Construction.SubdivisionBarycentric.affineValue

affineValueFamily def

The target, constant and coordinate values in the same order as the Hilbert family. · OAI.RegularPointCoordinates.affineValueFamily

affineWeight def

The classical determinant weight; in particular, this is not a generalized exponent. · OAI.AffineBernstein.affineWeight

affineZariski def

Affine Zariski topology: the topology generated by principal open sets on which a multivariate polynomial does not vanish. · OAI.Nagata.W27.affineZariski

affinity def

Hellinger affinity of finite probability weights. · OAI.LipschitzHilbert.affinity

after def

Post law after observing W=b. · OAI.FourierLLogL.Law.after

after def

Exact finite-input Bellman expectation of an arbitrary terminal observable. The private action history, not only the current configuration, is retained. · OAI.KServer.Amplification.after

afterBlock def

The actual root just after the entire descendant block switches. · OAI.ReflexiveFixedPoints.TreeEvaluation.afterBlock

afterField def

Stack state after one completed field, retaining an arbitrary old destination. · OAI.MaxCutGames.Foundations.Hastad.SourceMachine.afterField

afterField def

Stack state after one completed field, retaining an arbitrary old destination. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.afterField

afterInitializationInTime def

Consume the preserved header registers established by SourceLoopInit. The caller supplies the static placement and empty work registers. · OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.afterInitializationInTime

afterInitializationInTime def

Consume the preserved header registers established by SourceLoopInit. The caller supplies the static placement and empty work registers. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.afterInitializationInTime

afterPort def

The only data-changing index operation is a tape push, below. This function chooses a finite continuation among the fixed port-control labels. · OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.afterPort

afterPort def

The only data-changing index operation is a tape push, below. This function chooses a finite continuation among the fixed port-control labels. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.afterPort

afterRound def

Inclusion of the completed successor round into the final union. · OAI.PartitionConsistency.MonoidConstruction.Saturation.afterRound

age def

Number of later insertions in the fixed-radius neighbourhood of an entry. · OAI.KServer.Chronological.age

age def

Ages count subsequent chronological insertions, whether or not those entries have retired. Equal physical centers remain distinct records. · OAI.UniformKServer.ChronologicalRoster.age

agen def

Base-chart coordinate functions. · OAI.StableCoordinate.BundleCharts.agen

aggregate def

Sum of the oriented block inclusions on the child logical symbols. · OAI.MaxCutGames.Gadget.aggregate

aggregate def

A general finite rational law of ordered test endpoints becomes an ordinary symmetric rational graph by adding both orientations and deleting loops. · OAI.OptimalMaxCut.LongCode.aggregate

aggregate def

Sum of the oriented block inclusions on the child logical symbols. · OAI.UniqueGamesTheorem.Gadget.aggregate

Agree def

Equality of the first e sampled coordinates (root variables are held fixed). · OAI.DilutedSpinGlass.FinitePath.Agree

Agree def

The finite observation equivalence on unrestricted plus tables. · OAI.PureTypeSystem.FreeObservations.Agree

Agree def

Coefficient locality at the singular point. Although differentiating costs one coefficient, its multiplier has zero constant term, so the nth residual coefficient only depends on coefficients through n. · OAI.SepticProfile.Formal.Agree

Agree def

Agreement of the four data fields at a collision; the proof fields are proposition-valued and need no extra equality assumptions. · OAI.TriangularBilliards.FlightChain.Agree

AgreeBelow def

Two subsets of ℕ agree on the first m labels. · OAI.InfiniteMatroidCounterexample.AgreeBelow

agreementProbability def

Choose uniform coordinates in the two masks and check the projection. An empty support contributes zero. · OAI.MaxCutGames.Foundations.Hastad.agreementProbability

agreementProbability def

Choose uniform coordinates in the two masks and check the projection. An empty support contributes zero. · OAI.UniqueGamesTheorem.Foundations.Hastad.agreementProbability

AgreeOn def

Agreement on the half-open integer interval [a,b). · OAI.Superstring.Hierarchical.AgreeOn

agrees def

Offered replay from step t. Predicates need only check each block separately. · OAI.Fifths.Tour.agrees

AgreeThrough def

Equality of the already exposed outward layers. · OAI.CubeShuffle.AgreeThrough

aiming def

list for a cross edge · OAI.HadwigerCounterexample.aiming

aimingAt def

States whose straight starting line passes through p, in either direction. · OAI.TriangularBilliards.aimingAt

ainv def

Inverse of z+1 on the first chart. · OAI.StableCoordinate.BundleCharts.ainv

aksBranch def

The auxiliary modulus branch. The bounded small-divisor test is performed before the congruences. Evaluating every modulus is a polynomial unrolling of (the first qualifying modulus in) the manuscript's bounded search. · OAI.ExactQuantumFactoring.BitArithmetic.aksBranch

aksStaticBranch def

The condition is on the compile-time parameter s≤n^8, not on the possibly exponentially large input integer. Decidable primality here is a finite bounded search; its generation-cost proof is separate from circuit size. · OAI.ExactQuantumFactoring.BitArithmetic.aksStaticBranch

AlexanderWhitneyInput structure

Only the classical chain identity and its ordinal naturality are left as hypotheses. All objects and maps here have their explicit formulas. · OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput

Algebra abbrev

The ring of the block: the corner has identity b, rather than the identity of the ambient ring. · OAI.Donovan.BlockIdempotent.Algebra

Algebra abbrev

The actual block algebra KGb. · OAI.Donovan.FiniteGroupBlock.Algebra

Algebra structure

A finite list of total finite-arity operations. Arity zero is allowed. · OAI.FiniteCongruence.Algebra

Algebra abbrev

The ordinary complete C*-algebra underlying the concrete algebra. · OAI.KadisonKastler.Algebra

Algebra def

The universal completion is separated; Cuntz relations vanish in its norm. · OAI.NuclearUltrapower.CuntzUniversal.Algebra

algebra def

The strongly closed algebra in which the phase comparison is performed. · OAI.KervaireCentralizer.algebra

algebra def

The closed algebra M_D(M_A) represented on the arbitrary-group Hilbert space. · OAI.KervaireMatrix.algebra

algebraApply def

The same finite average, with its value retained inside the algebra. · OAI.KadisonKastler.FiniteInnerAverage.algebraApply

algebraBimoduleMean def

The algebra-valued mean satisfies the two module identities. · OAI.KadisonKastler.ScalarInvariantMean.algebraBimoduleMean

algebraCocycleRepresentative def

Replace the exceptional values of an ambient unitary family by one. · OAI.KadisonKastler.algebraCocycleRepresentative

algebraConstantField def

Constant fields with values in the specified von Neumann algebra. · OAI.KadisonKastler.algebraConstantField

AlgebraD abbrev

The actual ordinary algebra D of Section 5. · OAI.LittleFinitistic.OrdinarySimulation.AlgebraD

algebraDualInjection def

Canonical specialization into the dual over the target of a ring map. · OAI.CoherentDual.algebraDualInjection

algebraEquiv def

Algebraic identification; it transports no topology. · OAI.Tingley.UltraSequence.algebraEquiv

algebraGram def

The Gram matrix of a finite family in the algebra. · OAI.BoundedHochschild.KadisonRingrose.algebraGram

algebraGroupTangentLie def

The tangent span is a concrete Lie subalgebra of the ambient matrix algebra. · OAI.PolycyclicRecognition.algebraGroupTangentLie

algebraGroupTangentSpan def

The finite-dimensional linear span of the actual curve derivatives. · OAI.PolycyclicRecognition.algebraGroupTangentSpan

AlgebraGroupTangentVector def

A derivative at the identity of a curve contained in a given matrix group. · OAI.PolycyclicRecognition.AlgebraGroupTangentVector

algebraicTensorWordIsometry def

The tensor power of an actual Hilbert-space isometry. · OAI.KadisonSimilarity.algebraicTensorWordIsometry

algebraInclusion abbrev

The faithful inclusion of a concrete von Neumann algebra into its ambient bounded operators. · OAI.KadisonKastler.algebraInclusion

algebraMatrix def

Matrix form of an actual algebra element, with the unchanged physical coordinate basis on the signed tensor sector. · OAI.RowColumn.MatrixState.algebraMatrix

algebraMean def

The actual algebra-valued mean. · OAI.KadisonKastler.ScalarInvariantMean.algebraMean

algebraPresentation def

The source algebra B has precisely the literal compiler equations and a zero equation. · OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.algebraPresentation

AlgebraProjection def

Projections with their algebraic range-inclusion order. · OAI.Generator.Tracial.AlgebraProjection

algebraSequenceVector def

A bounded algebra sequence, viewed as a bounded family of GNS vectors. · OAI.KadisonSimilarity.algebraSequenceVector

algebraSequenceVectorLinear def

Algebra sequences act linearly on the bounded-vector subspace. · OAI.KadisonSimilarity.algebraSequenceVectorLinear

AlgebraSimilarityProperty def

The similarity property of one algebra, with an independent universe for Hilbert spaces. This is property (SP) in Ozawa's formulation. · OAI.KadisonSimilarity.AlgebraSimilarityProperty

algebraSpec def

The spectrum of a k-algebra, viewed as a scheme over Spec k. · OAI.StableCoordinate.AffineGeometry.algebraSpec

algebraSpecIso def

The stronger isomorphism in the category of schemes over Spec k. · OAI.StableCoordinate.AffineGeometry.algebraSpecIso

algebraTensorSlice def

Contract the first tensor coordinate against x. · OAI.KadisonSimilarity.algebraTensorSlice

algebraUltraweakTopology abbrev

The concrete algebra carries the induced ultraweak topology. · OAI.RelativeGeneration.algebraUltraweakTopology

algebraUnitaryOfMem def

A unitary with value in the algebra is a unitary of that algebra. · OAI.KadisonKastler.algebraUnitaryOfMem

algebraVectorMap def

Evaluating the represented algebra at its trace vector. · OAI.KadisonKastler.algebraVectorMap

algEquivOfAlgebraSpecIso def

In particular, every automorphism in the category of schemes over Spec k is accounted for by an algebra automorphism. · OAI.StableCoordinate.AffineGeometry.algEquivOfAlgebraSpecIso

algEquivOfSpecIso def

Every affine scheme isomorphism over the coefficient base induces an algebra isomorphism. Thus algebra automorphisms do not omit any ambient automorphisms. · OAI.StableCoordinate.AffineGeometry.algEquivOfSpecIso

AlgorithmicStrongThinTrees def

There exist one positive real constant `C`, one fixed finite stack machine `M`, and natural numbers `a` and `degree` with `a > 0` such that every valid input is solved within `a * (length + 1) ^ degree` steps. · OAI.AlgorithmicThinTrees.AlgorithmicStrongThinTrees

Aligned def

Tokens with a specified full-text alignment, not just a matching finite word. · OAI.Superstring.Hierarchical.Threading.Aligned

Aligned def

An alignment is only required to respect actual vertical readout names. No assertion is made that ambient labels inhabit every product factor. · OAI.WLIdentification.RingLayout.Aligned

aligned_of_return_fixed def

A fixed point of the genuine sphere return map gives the exact four chords. · OAI.Tingley.aligned_of_return_fixed

alignmentEvent def

Nonzero inputs aligned by a specified linear lift. · OAI.MaxCutGames.Quadratic.alignmentEvent

alignmentEvent def

Nonzero inputs aligned by a specified linear lift. · OAI.UniqueGamesTheorem.Quadratic.alignmentEvent

alignmentIndexEquiv def

Permutation of the stabilized relator indices into distinguished and ordinary blocks, in exactly the order of source (ordinary-diagonal). · OAI.EilenbergGanea.alignmentIndexEquiv

alignmentMatrix def

The |n| * |ι| alignment columns for a fixed parametrization and input set. The input set is represented by any map point : E → V; no injectivity is needed for the exact algebraic equivalence. · OAI.MaxCutGames.Quadratic.alignmentMatrix

alignmentMatrix def

The |n| * |ι| alignment columns for a fixed parametrization and input set. The input set is represented by any map point : E → V; no injectivity is needed for the exact algebraic equivalence. · OAI.UniqueGamesTheorem.Quadratic.alignmentMatrix

alignmentObstruction def

Clearing the rational dual's denominator and squaring gives this one polynomial obstruction to simultaneous alignment. Its degree is finite and depends only on the fixed set of inputs. · OAI.MaxCutGames.Quadratic.alignmentObstruction

alignmentObstruction def

Clearing the rational dual's denominator and squaring gives this one polynomial obstruction to simultaneous alignment. Its degree is finite and depends only on the fixed set of inputs. · OAI.UniqueGamesTheorem.Quadratic.alignmentObstruction

alignmentRightHandSide def

The cubic square-root right hand side of the alignment equation. · OAI.MaxCutGames.Quadratic.alignmentRightHandSide

alignmentRightHandSide def

The cubic square-root right hand side of the alignment equation. · OAI.UniqueGamesTheorem.Quadratic.alignmentRightHandSide

Alignments def

These are the literal alignments of the moved chain with contractions of its initial vertex. There is no replacement relation assumed here. · OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.Alignments

alignNormal def

A Householder reflection sends the chosen normal to a coordinate normal. · OAI.Problem358.HouseholderCoordinates.alignNormal

alive def

Certain initial ages are included even on zero-weight tape outcomes; this makes deterministic coverage a pathwise property, not just an almost-sure one. · OAI.KServer.ActualRoster.alive

all def

The route is selected by its original direct annotation, not by a later sorting profile of the domain. · OAI.PureTypeSystem.Labelled.LogicSetup.all

allAddresses def

The complete address list, including the unique empty word. · OAI.MaxCutGames.Foundations.PCP.PoweringAddresses.allAddresses

allAddresses def

The complete address list, including the unique empty word. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringAddresses.allAddresses

allCopyOverlap def

The all-copy operator-overlap sum, with each squared operator norm. · OAI.RowColumn.allCopyOverlap

allCounterexample def

A negated universal has a consistent fresh counterexample context. · OAI.PartitionConsistency.Completeness.Condition.allCounterexample

AllData inductive

A terminal contains data/data labels only. · OAI.PureTypeSystem.Labelled.Expr.AllData

allEvents def

All indexed events hold; the index set and events are kept literally. · OAI.MetricEntropyDuality.FiniteProductCounting.allEvents

allLink def

At O a larger complete bipartite graph suffices for the four-edge girth bound; at V and W we use precisely the shifted incidence links. · OAI.Release075.MarkedLineData.allLink

allLocalSystem def

The normalized names and the proved support descent instantiate the intersection calculus. Eligibility as an E-class is a later subcollection. · OAI.PartitionConsistency.ProductForcing.allLocalSystem

allocatedBackground def

The background coloring used by the finite program, in its fixed sorted order. · OAI.LowSpaceSubsetSum.RepresentationSetup.allocatedBackground

allocatedChildAssignment def

The four-child assignment used in the survival proof is obtained from the same computed eight-leaf assignment used for the resource counts. · OAI.LowSpaceSubsetSum.RepresentationSetup.allocatedChildAssignment

allocateLeft def

Signed arithmetic prevents truncation before the final division. · OAI.LowSpaceSubsetSum.allocateLeft

allocateSide def

A Boolean selects the two complementary allocations without changing the fixed remainder convention. · OAI.LowSpaceSubsetSum.allocateSide

allowance def

Full-tree analysis allowance; the executable never evaluates it. · OAI.LowSpaceSubsetSum.BudgetedPrefixController.allowance

allowance def

Proof-only allowance for one comparison or one complete tie group. · OAI.LowSpaceSubsetSum.BudgetedStreamStep.allowance

allowance def

Proof-only allowance for the operations performed by this tie group. · OAI.LowSpaceSubsetSum.BudgetedTieGroup.allowance

Allowed def

The side lengths are in [R, R²], where the single global scale is R = 2^r. · OAI.CoordinateSweeps.Grid.Allowed

Allowed def

Allowed grid, with R=2^r. This is precisely m_j ∈ [R,R²] in bit coordinates. · OAI.CoordinateSweeps.Grid.Allowed

Allowed def

Keep at most the specified two points, but retain every line and the subdivision vertex. Such an induced graph is a forest. · OAI.HyperbolicObstruction.MacroGraph.Allowed

Allowed def

A p-subgroup normalized by J. · OAI.PCoreCancellation.Allowed

Allowed def

Adjacencies are allowed only between a valuation class and a named bit coordinate used by that block. This records no right-hand-side information. · OAI.WLIdentification.AffineBlocks.Allowed

allowed def

l in I_d. · OAI.HadwigerCounterexample.allowed

allowed def

The exact nonzero choices, not an independent-equations approximation. · OAI.SmoothObstruction.SymplecticSampling.allowed

allowed def

Actual vertex carriers: all outgoing template ports must be available; pin imposes exactly the prescribed images, not extra random conditions. · OAI.TorsionFreeZeroDivisors.StageRealization.allowed

allows def

O-blocks disallowed at l are set to zero. · OAI.HadwigerCounterexample.allows

allPairsEq def

Simultaneous agreement of card κ independent label pairs. · OAI.Problem335.IndependentCoordinates.allPairsEq

allPatternYoungConstant def

A common coefficient for all active subsets of a fixed finite family. · OAI.SLEExactGauge.Multipoint.allPatternYoungConstant

AllQuotientMoments def

Every admissible mixed word in an indexed coefficient family vanishes. · OAI.KadisonSimilarity.AllQuotientMoments

allRefine abbrev

Simultaneously refine every brick by the same finite partition. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.allRefine

allRowsBits def

Product rows are emitted in ascending radix address, exactly the literal order of the output constraint list. · OAI.MaxCutGames.Explicit.ProductMachineSemantics.allRowsBits

allRowsBits def

Product rows are emitted in ascending radix address, exactly the literal order of the output constraint list. · OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.allRowsBits

AllScaleProfileData structure

Only the metric data used to form a normalized chart profile. · OAI.PolycyclicRecognition.AllScaleProfileData

allSmallFibre def

The output data consists only of the two stored small views. Existence of a completion supplies the erased proof that these are valid margins. · OAI.ContingencyTables.SmallGraphProfiles.allSmallFibre

allTapes def

A fixed finite list of all tape names is available without ambient search. · OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.allTapes

allTapes def

An explicit tape enumeration, fixed before the input is supplied. It uses constructor lists and increasing finite coefficient indices. · OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.allTapes

allTapes def

A fixed finite list of all tape names is available without ambient search. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.allTapes

allTapes def

An explicit tape enumeration, fixed before the input is supplied. It uses constructor lists and increasing finite coefficient indices. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.allTapes

allTupleUnion def

The union of an unrestricted ordered edge tuple. · OAI.TalagrandDiscreteConvexity.Covering.allTupleUnion

allTupleWeightSum def

The larger sum in which repeated edges are allowed. · OAI.TalagrandDiscreteConvexity.Covering.allTupleWeightSum

allWords def

All words of a specified length, ordered first by their head port. · OAI.MaxCutGames.Foundations.PCP.PoweringAddresses.allWords

allWords def

All words of a specified length, ordered first by their head port. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringAddresses.allWords

allZero def

Bounded fan-in conjunction, built incrementally, not an unbounded gate. · OAI.ExactQuantumFactoring.BooleanNetwork.allZero

AlmostInvariant def

Pointwise approximate invariance in a varying Hilbert family. · OAI.NuclearUltrapower.AlmostInvariant

along def

The closed ancestral interval [g,w]. · OAI.ForestSpace.along

along def

averages on segment · OAI.GeneralMahler.along

Alphabet structure

Finite work alphabet, including a literal code for every input letter and a distinct blank. The remaining symbols are rejected by output reading. · OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet

Alphabet structure

The letter action and exit map used in the terminating probe normal forms. These laws will be realized by the path direct limit above. · OAI.PartitionConsistency.ProbeAlgebra.Alphabet

Alphabet abbrev

0 is blank, 1 and 2 are the two literal binary digits, 3 is work space. Fixed finite tape alphabet and finite state space; no advice or oracle. · OAI.RationalHitting.Alphabet

Alphabet abbrev

Compact alphabet of uniformly bounded, uniformly invertible derivative matrices. The coercion remembers the actual matrix, not an extra axiom. · OAI.SmoothObstruction.CompactMatrix.Alphabet

alphabet def

The direct limit supplies all the alphabet laws for the probe extension. · OAI.PartitionConsistency.ProbeAlgebra.Path.alphabet

alphabetDistortion def

Distortion of the ordinary edit metric on the all-length capped domain. · OAI.TreeEdit.BinaryLower.alphabetDistortion

alphabetDistortionSup def

Supremum over finite alphabets of cardinality at least two, represented by canonical alphabets Fin K. Relabeling invariance identifies this with the source's supremum over all finite alphabets. · OAI.TreeEdit.BinaryLower.alphabetDistortionSup

alphabetEquiv def

The integer label is the packed, least-significant-bit-first coordinate word. · OAI.MaxCutGames.Reduction.Encoding.alphabetEquiv

alphabetEquiv def

The integer label is the packed, least-significant-bit-first coordinate word. · OAI.UniqueGamesTheorem.Reduction.Encoding.alphabetEquiv

AlphabetSimulation structure

A map of probe alphabets whose old divisibility tests are unchanged. All these laws will be proved for the path direct limits; no assumptions about joins between new words or their gates enter this definition. · OAI.PartitionConsistency.ProbeAlgebra.AlphabetSimulation

alphabetSub def

Coordinate subrepresentation using only letters with property A. · OAI.Saxl.alphabetSub

alphabetSup def

Supremum over finite alphabet cardinalities. · OAI.EditDistortion.alphabetSup

alphaGW def

The exact Goemans–Williamson ratio, as an infimum over -1 ≤ ρ < 1. · OAI.OptimalMaxCut.alphaGW

alphaPath def

The actual one-form alpha_t = m alpha_0 + t beta. · OAI.Mahler.alphaPath

alt def

The alternating expression starting with i, unlike Mathlib's alternatingWord, which specifies the final letter. · OAI.KLInvariance.Dihedral.alt

alternating def

Alternating word of length n, starting with s. · OAI.ArtinCAT0.alternating

AlternatingCenteredWord inductive

An alternating word of centered letters in two specified algebras. · OAI.KadisonSimilarity.AlternatingCenteredWord

AlternatingCreationCoordinates structure

The two elementary creation formulas for reduced words starting in the opposite free factor. The tensor maps are the usual isometric inclusions of reduced-word summands, and the specified letters have Hilbert norm one. · OAI.KadisonSimilarity.AlternatingCreationCoordinates

alternatingCycles def

Full alternating cycles, not their projection-side overcount. This is the cycle count needed for sparse low-level blocks. · OAI.CubeShuffle.PairRouting.alternatingCycles

alternatingHeight def

Weights are listed in strictly decreasing order. · OAI.Thomason.Construction.SimplexComplex.alternatingHeight

alternatingKernel def

The source's s-normalized alternating kernel, over all coordinate subsets. · OAI.CoordinateSweeps.Placement.alternatingKernel

AlternatingMachineHaltingUndecidable def

Flattened finite tables with a finite list of terminal states. · OAI.ForcedComputation.AlternatingMachineHaltingUndecidable

alternatingMomentsZero def

Vanishing of every nonempty alternating word from two specified sets. · OAI.Generator.alternatingMomentsZero

alternatingPerm def

Alternating traversal of the identity matching and the p-matching on two halves. A fixed point of p is precisely a parallel-edge alternating cycle. · OAI.CubeShuffle.CycleColoring.alternatingPerm

alternatingProduct def

The alternating product of the actual family indexed by subsets of t. · OAI.CirculantHadamard.alternatingProduct

alternatingProduct def

The finite alternating product, in its prescribed left-to-right order. · OAI.KadisonSimilarity.alternatingProduct

alternatingProduct def

Ordered alternating products, with the first list supplying fixed left letters and the second list supplying the variable right letters. · OAI.KadisonSimilarity.DihedralCornerWords.alternatingProduct

alternatingValue abbrev

The single fixed field element used for every prime-direction comparison. · OAI.CirculantHadamard.alternatingValue

altWord def

The genuine unnormalized signed block alternation. · OAI.Saxl.altWord

Amalgamates def

An ambient pseudometric on the disjoint union giving isometric embeddings. · OAI.FKCRT.Amalgamates

Ambient abbrev

The ambient homotopy category; no bounded-projective identification is asserted here. · OAI.LittleFinitistic.QuadraticEncoding.Ambient

Ambient structure

Full columns regarded in the unrestricted path pseudometric. Connectedness here is supplied by the connected graph realization, not an extra condition on the embedding theorem. · OAI.PlanarL1.Columns.Model.Ambient

Ambient abbrev

The complex affine four-space in its standard spectrum presentation. · OAI.StableCoordinate.GeometricInterpretation.Ambient

ambientAffineSpaceIso def

Standard identification of the ambient spectrum with affine four-space. · OAI.StableCoordinate.GeometricInterpretation.ambientAffineSpaceIso

ambientAlgebraFamily def

Pointwise inclusion of bounded algebra-valued families. · OAI.KadisonKastler.ambientAlgebraFamily

ambientAlgebraUnitary def

The unitary in the ambient operator algebra. · OAI.KadisonKastler.ambientAlgebraUnitary

ambientCornerColumns def

The finite range decomposition in the ambient Hilbert space. · OAI.KadisonSimilarity.TracialCornerGeometry.ambientCornerColumns

ambientGenerated def

The ambient function-space image of the generated actual selfmaps. · OAI.ReflexiveFixedPoints.ambientGenerated

ambientInverse def

Extend the inverse endpoint restriction back to an ambient linear map. It is a left inverse on the actual moving fast space, with uniform norm 2. · OAI.SmoothObstruction.CloseProjection.ambientInverse

ambientMap def

The ambient representative of an actual selfmap. · OAI.ReflexiveFixedPoints.ambientMap

ambientMeasure def

Ambient Liouville measure, before restriction and normalization. · OAI.TriangularBilliards.ambientMeasure

ambientNormalScalar def

Actual evaluation of an ambient normal polynomial on the chosen cubic coordinate functions and the normal fibre coordinate. · OAI.Nagata.CoefficientSpaces.ambientNormalScalar

ambientParameter def

The parameter inverted in the localization, F + 1. · OAI.AbhyankarSathaye.CommutingDerivations.ambientParameter

ambientPrimalEquiv def

Reindex primal matrices by changing the ambient domain. · OAI.MaxCutGames.Inverse.KMSAnalytic.ambientPrimalEquiv

ambientPrimalEquiv def

Reindex primal matrices by changing the ambient domain. · OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.ambientPrimalEquiv

AmbientQuotient abbrev

A quotient fixed before Y is chosen, for the ambient homotopy category. · OAI.LittleFinitistic.QuadraticEncoding.AmbientQuotient

ambientQuotientEvaluation def

Actual tensor evaluation on the ambient quotient, with the generator hypotheses proved. · OAI.LittleFinitistic.QuadraticEncoding.ambientQuotientEvaluation

ambientSignature def

Coercion keeps literal key identities and is injective on signature words. · OAI.QuantitativeVanDerWaerden.CyclicColoring.ambientSignature

AmbientStatement def

Compatible extensions in a finite group glue uniquely over their generated join, whose relative core retains the inner automorphisms. · OAI.FiniteLattice.CommonCore.AmbientStatement

ambientTailConvexHull def

The algebraic convex hull, before pointwise weak closure is taken. · OAI.ReflexiveFixedPoints.ambientTailConvexHull

ambientTailFamily def

Tail maps represented in the actual vector space of ambient-valued maps. · OAI.ReflexiveFixedPoints.ambientTailFamily

Amenable def

A positive normalized left-invariant complex mean. · OAI.Dixmier.Amenable

amount def

Total number of interior vertices outside the clique. · OAI.CycleClique.Construction.ExpandedPathSystem.amount

amount def

height parameter allowing very small mass static entries. · OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.amount

amountSequences def

Positive amount sequences with at most the indicated number of edges and total amount at most the budget. · OAI.CycleClique.Construction.amountSequences

amountSequenceSum def

Sum over amount sequences by their short branching recursion, rather than reducing a list whose length can approach the recursion-depth limit. · OAI.CycleClique.Construction.amountSequenceSum

ampleRipsFamilyBoundary def

The self-contained construction includes its support proofs. · OAI.CoarseAssembly.Rips.ampleRipsFamilyBoundary

amplificationPartition def

The diagonal partition indexed by a single finite label set. · OAI.KadisonKastler.amplificationPartition

amplificationPhaseUnitary def

The diagonal matrix phase is an actual unitary in the amplified algebra. · OAI.KadisonKastler.amplificationPhaseUnitary

amplificationProgram def

Five actual programs: prepare, mark good, unprepare, mark zero work, prepare. The two phase predicates share a clean flag and scratch area. · OAI.ExactQuantumFactoring.amplificationProgram

amplificationSupport def

A multiset of phase labels names the corresponding outer/inner support atoms. · OAI.KadisonKastler.amplificationSupport

amplifiedAlgebra def

The concrete amplification in the coordinates supplied by F. · OAI.KadisonKastler.FullMatrixCorner.amplifiedAlgebra

amplifiedCommutantSet def

The diagonal copy of the commutant, viewed just as a set of operators. · OAI.KadisonSimilarity.amplifiedCommutantSet

amplifiedScalarRepresentation def

The actual diagonal amplification of a star representation. · OAI.KadisonSimilarity.amplifiedScalarRepresentation

amplify def

The diagonal amplification of one operator. · OAI.KadisonSimilarity.amplify

amplitude def

The Fock coefficient of a layered path. · OAI.Problem335.LayeredFourPath.amplitude

AnalyticIterationData structure

Explicit analytic inputs for the finite iteration. The mass and principal comparisons come before construction of the coordinate maps; none of the fields below assumes a coordinate metric or a scalar error recurrence. · OAI.RegularPointCoordinates.AnalyticIterationData

analyticLaurentCoeff def

The actual kth Laurent coefficient obtained on the circle of radius r. · OAI.Nagata.W09.analyticLaurentCoeff

analyticNormalScale def

The actual rescaling of the normal coordinate. · OAI.Nagata.Workers.W28.analyticNormalScale

AnalyticStationaryCharts structure

Two separately invertible coordinates of one local stationary branch. · OAI.Problem356.LocalImplicit.AnalyticStationaryCharts

Ancestor abbrev

The exact reverse fiber after the earlier dimensions are fixed. · OAI.MaxCutGames.Appendix.A5ReverseIndex.Ancestor

Ancestor abbrev

The exact reverse fiber after the earlier dimensions are fixed. · OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.Ancestor

ancestor def

The last head ancestor of any vertex. · OAI.IndependentProducts.FiniteHead.ancestor

ancestor def

The ancestor map across any number of generations of the same grid. · OAI.LipschitzHilbert.FiniteLineGrid.ancestor

ancestor def

Ancestors are constructed by inclusion of actual superlevel components. · OAI.PlanarL1.Columns.Model.Point.RadialTree.ancestor

ancestorLE def

The ancestor at an earlier level, obtained by composing parent maps. · OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE

ancestorMap def

The actual maps on the fixed path to a parent. · OAI.ReflexiveFixedPoints.CandidateContext.ancestorMap

ancestorNodeIndex def

The prefix of length i is an earlier internal node. · OAI.Ostmann.ancestorNodeIndex

ancestors def

Prefix ancestors, including both the root and the coordinate itself. · OAI.DiamondDistortion.RecursiveModel.ancestors

Ancestral def

Downward closed sets are precisely ancestral heads. · OAI.DiamondDistortion.Ancestry.Ancestral

Ancestry class

An ancestral partial order: the predecessors of any vertex form a chain. · OAI.DiamondDistortion.Ancestry

anchor def

Empty comparison sides may be placed at the preimage of target boundary zero; this has no occurrences and satisfies the global range condition. · OAI.TorsionFreeZeroDivisors.AffineIntervals.anchor

anchor def

This value, rather than the identity, is the immediate path anchor. · OAI.WeakPureInfiniteness.BufferAbsorptionCorner.anchor

Anchor64Pinned def

The precise form of anchor rigidity needed for counting: every ordered anchor copy contains one representative of each group of one common mode. · OAI.Problem348.Construction.Anchor64Pinned

anchorAt def

A subset of old positions remains unused. Every used old position and all fresh colored positions are canceled. · OAI.DilutedSpinGlass.PrescribedTree.anchorAt

anchorCoefficient def

The literal ordered-history Taylor coefficient of the single anchor. Only the anchor is initially protected. · OAI.DilutedSpinGlass.PrescribedTree.anchorCoefficient

anchorDerivative def

The derivative of a canceled-anchor insertion, retaining the actual tree score and the correction from the canceled denominator. · OAI.DilutedSpinGlass.PrescribedTree.anchorDerivative

Anchored def

Each layer is between consecutive support heads, not separated by a new unrecorded head. This is imposed only for the inputs that require it. · OAI.DiamondDistortion.SignCube.Protocol.Anchored

AnchoredCandidateContext abbrev

An actual stage remembers that its anchor is the one selected initially. · OAI.ReflexiveFixedPoints.AnchoredCandidateContext

anchoredFamily def

The finite union over all rational step vectors and all possible anchor positions. The scalar families can depend on both, as in the actual re-anchored breakpoint construction. · OAI.QuantitativeVanDerWaerden.anchoredFamily

anchoredIncidences def

Literal (step vector, recorded word) incidences, retaining the step vector even when two different steps yield the same word. The two scalar systems have their actual different output types. · OAI.QuantitativeVanDerWaerden.anchoredIncidences

anchorEval def

Unused old positions are a finite family of genuine path projections. In a canceled-anchor application these are all old leaves except the anchor. Every already selected color is canceled. · OAI.DilutedSpinGlass.PrescribedTree.anchorEval

anchorFirst32 def

Inclusion of the dense 32-position prefix. · OAI.Problem348.anchorFirst32

anchorGroup def

The anchor-group label forgets only the coordinate within a group. · OAI.Problem348.Construction.anchorGroup

anchorIncoming def

The incoming anchor edge before normalization by the bulk parity. · OAI.Ostmann.anchorIncoming

anchorInsertion def

The actual anchor expectation in pert:palm-expression, with the prior kernels updated by the new insertion. G includes the numerator score mark. · OAI.DilutedSpinGlass.PrescribedTree.anchorInsertion

anchorIterate def

Ordered histories for all orders of the canceled-anchor expansion. The state records precisely which OLD positions remain eligible. · OAI.DilutedSpinGlass.PrescribedTree.anchorIterate

anchorLastCol def

The five bit-coordinate columns of the anchor. · OAI.Problem348.anchorLastCol

anchorPairAllowed def

The actual finite central domain, distinctness and close-label restriction. It is purely deterministic and is never added to the orientation posterior. · OAI.TraceReconstruction.anchorPairAllowed

AnchorPoint structure

This record states actual output properties. Its tail-set equality retains the concrete intersection definition used to construct it. · OAI.ReflexiveFixedPoints.AnchorPoint

Anchors inductive

Exact clean-anchor language; dirty tags are not accepted. · OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Anchors

anchorTailClosure def

The closure of the (n+1)st tail image, in the weak subtype topology. · OAI.ReflexiveFixedPoints.anchorTailClosure

anchorTailSet def

The literal tail-limit set, viewed in the original ambient space. · OAI.ReflexiveFixedPoints.anchorTailSet

anchorWord def

All five-bit words, in the order used by the replacement rectangle. · OAI.Problem348.anchorWord

ancillaValid def

The zero-ancilla computational subspace, without any condition on final garbage. · OAI.QAC.ancillaValid

andReject def

Six oracle queries, using three independent self-correction masks. · OAI.MaxCutGames.Foundations.PCP.AssignmentTester.andReject

andReject def

Six oracle queries, using three independent self-correction masks. · OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.andReject

andThen def

Structured sequential composition; one finite-control step starts the second routine once the first has returned. No external simulator is presumed. · OAI.ParityWL.Complexity.StackMachine.andThen

angle def

Interior angle at vertex i. · OAI.TriangularBilliards.Triangle.angle

AngleDiskCounts structure

The numerical incidence identities of a nonempty planar triangle disk, with boundary visits counted with multiplicity (including both sides of naked edges). All fields are finite counts or angle data. No group conclusion is assumed. · OAI.Release075.AngleDiskCounts

angleMeasure def

Angular Haar probability in additive angle coordinates, used to verify invariance of the explicit angular measure. · OAI.TriangularBilliards.angleMeasure

angular def

Simultaneously smooth infinite angular coefficient. No angular selector is used in its definition, so discontinuous labels cannot spoil regularity. · OAI.HarmonicCounterexample.AngularStream.angular

angular def

The exact Berger angular coefficient, with b=B_l Id and D=D_J². Here r=1/m, and the outer scalar a^{-2} is applied separately. · OAI.HarmonicCounterexample.PulseTaylor.angular

angularCharacter def

Angular characters with the sign convention of arcFourierIntegral. · OAI.KadisonSimilarity.angularCharacter

angularCircleAction def

The actual oriented tangent-circle representation on the double. · OAI.TriangularBilliards.angularCircleAction

angularCoefficientPolynomial def

Fixed-angle polynomial with arbitrary finite Eisenstein support. · OAI.CubicFirstMoment.angularCoefficientPolynomial

angularConductorFactor def

Upper bound for the degree-two analytic conductor: finite conductor at most 9 N(q₁q₂), field discriminant 3, and gamma shifts k,k+1. · OAI.CubicFirstMoment.angularConductorFactor

angularCorrectionChar def

The correction is literally a multiplicative residue character modulo 3. Thus its conductor divides 3. · OAI.CubicFirstMoment.angularCorrectionChar

angularDualTailIntegrand def

The integrand of the omitted part of the functional-equation series on the line Re s = 1/2-m. · OAI.CubicFirstMoment.angularDualTailIntegrand

AngularGammaQuotientStripBound def

The fixed-shift specialization of the uniform vertical Stirling formula, DLMF 5.11.9. · OAI.CubicFirstMoment.AngularGammaQuotientStripBound

AngularGrid structure

A single common translation is used at every angular level. · OAI.LipschitzHilbert.AngularGrid

angularHilbertFlow def

Rotation of the oriented tangent fiber, not a rotation of the physical velocity with the same sign on both copies. · OAI.TriangularBilliards.angularHilbertFlow

AngularKummerPrimeExplicitEstimate def

Precisely the raw fixed-angular prime Chebyshev estimate for the finite numerator character, including ramification and unit factors. No stopped-sequence, smooth-weight, or dispersion conclusion is assumed. · OAI.CubicFirstMoment.AngularKummerPrimeExplicitEstimate

angularLie def

The actual squared-complex-structure Lie algebra on homogeneous polynomials; the restriction to harmonic polynomials is taken later. · OAI.HarmonicCounterexample.Control.angularLie

angularMass def

A finite constant depending only on q, independent of the direction. · OAI.BoltzmannNonuniqueness.TransverseAverage.angularMass

angularMeasure def

Uniform angular probability, parameterized by [0,2π). · OAI.TriangularBilliards.angularMeasure

angularMellinPolynomial def

The convention used in the Dirichlet-polynomial mean-square estimates. · OAI.JointDickman.angularMellinPolynomial

angularMixedCubic def

The actual fixed-angular character on the primary generators used by this development. A nonzero angular index makes it nonprincipal. · OAI.CubicFirstMoment.angularMixedCubic

angularOperator def

The actual negative Berger Laplacian on the genuine harmonic-polynomial space. Here c is the horizontal metric coefficient and q the squared Hopf stretch (the manuscript q). · OAI.HarmonicCounterexample.Angular.angularOperator

angularPairingLinear def

The Frobenius pairing, packaged only to expand finite directional sums. · OAI.PositiveEinsteinFour.Angular.angularPairingLinear

angularPowerMoment def

Normalized angular moments of powers of the real coordinate. · OAI.KadisonSimilarity.angularPowerMoment

angularPrimeDifference def

The difference between the Gauss-sum moment and its elementary model. · OAI.CubicFirstMoment.angularPrimeDifference

angularPrimeModel def

The elementary prime model in the fixed angular mode ℓ. · OAI.CubicFirstMoment.angularPrimeModel

angularPrimeMoment def

The prime Gauss-sum moment in the fixed angular mode ℓ. · OAI.CubicFirstMoment.angularPrimeMoment

angularProjection def

These are actual Fourier projections of the double, not externally specified coefficient operators. · OAI.TriangularBilliards.angularProjection

angularResidueIdealChar def

Full primitive coefficients, before removing any Euler factor. · OAI.CubicFirstMoment.angularResidueIdealChar

angularSeparatedTreeEnergy def

The separated portion of the original coefficient family, as in Eq. (size) of the manuscript. · OAI.LipschitzHilbert.SourceLabeledLattice.angularSeparatedTreeEnergy

angularSourceFunction def

The right-hand side of the normal covariance equation. · OAI.ClosedSurfaceR4.JetPolynomial.angularSourceFunction

angularSpeed def

The angular-speed expression B as a real scalar function. · OAI.SymmetricMahler.angularSpeed

AngularUnitCompatible def

The correct unit condition for infinity type ell. For ell=0 it reduces to triviality on global units. · OAI.CubicFirstMoment.AngularUnitCompatible

angularUnitCorrection def

On elements prime to 3 this is precisely the unit correction theta_l(primaryNormalize x) / theta_l(x). It vanishes at the ramified prime; it is a finite character, not an additional archimedean phase. · OAI.CubicFirstMoment.angularUnitCorrection

angularWeightedPrimeSum def

The angular power-weighted sum before multiplying by cStar. · OAI.CubicFirstMoment.angularWeightedPrimeSum

Annihilates def

Vanishing on all finite tests in a specified coordinate region. · OAI.ForestSpace.Annihilates

annularConnector def

An explicit annular extension reduces arbitrary cyclic boundary endpoints to the already-proved cardinal-endpoint disk crossing obstruction. · OAI.PlanarL1.Topology.annularConnector

annulus def

The exact annulus charged at a heavy update. · OAI.KServer.HeavyCenters.annulus

annulusHomeomorph def

The actual overlap of the two CW collar open sets is the disjoint union of punctured open disks, even for an unrestricted cell index. · OAI.EilenbergGanea.CWCollar.Attachment.annulusHomeomorph

annulusUnits def

The annulus maps to actual nonzero complex points without a chosen surrogate. · OAI.Nagata.Workers.W05.annulusUnits

anodyneRealizationData def

A chosen actual stationary deformation for any anodyne extension. · OAI.Thomason.Construction.anodyneRealizationData

antecedentEquiv def

Exact antecedent bijection; neither direction assumes the desired count. · OAI.MaxCutGames.Appendix.DerivativeInduction.antecedentEquiv

antecedentEquiv def

Exact antecedent bijection; neither direction assumes the desired count. · OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.antecedentEquiv

AParallel inductive

A disjoint union of forward calls and untouched coordinates. · OAI.ExactFourier.AParallel

aParentPath def

A keeps its old surface orientation; time on it is opposite to U,Q. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.aParentPath

Apart def

A named member of σ which a condition forces not to belong to τ. This is a concrete witness to inequality, not a postulated decision law. · OAI.PartitionConsistency.SetForcingNames.AtomicForcing.Apart

ApexInstance abbrev

Actual source vertices over this fan, represented in the chosen fragment. · OAI.HyperbolicObstruction.ConeSkeleton.ApexInstance

ApexInstance abbrev

Actual source vertices over this fan, represented in the chosen fragment. · OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.ApexInstance

aPhys def

The actual normalized matrix coefficients, with the sign of the Carleman operator. · OAI.ElasticityPhysicalEstimate.aPhys

App def

Application is the forcing of the literal internal ordered-pair graph formula. It does not replace a set function by an external function. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.App

append def

Finite chart-table extension. Old identifiers are literally retained in the right summand; installing a fresh chart never refines the old regions. · OAI.PlanarL1.Columns.Model.BState.append

append def

Finite chart-table extension. Old identifiers are literally retained in the right summand; installing a fresh chart never refines the old regions. · OAI.PlanarL1.Columns.Model.OrdinaryState.append

append def

Concatenate switching words. Any redundant final/initial vertical detour at the common column is removed, so length can only decrease. · OAI.PlanarL1.Columns.Model.Path.append

append def

Append two finite coordinate blocks, with their usual sup norms. · OAI.Problem358.FinitePrefix.append

append def

Append one newly chosen record without changing any previous record. · OAI.ReflexiveFixedPoints.HistoryState.append

append def

Append a vertex above the final vertex of an ordered simplex. · OAI.Thomason.Construction.ConePrism.append

append def

Append one upper vertex to a monotone tuple. · OAI.Thomason.Construction.SimplexComplex.append

append def

Two arbitrary smooth packet lists in the SAME good arc and speed may be merged. The coefficient supports are not required to be disjoint. · OAI.ThreeTorus.PassagePackets.append

appendBasis def

Append the basis supplied by the completion theorem. · OAI.MUB6.Weiner.appendBasis

appendCoordinates def

Grouping changes coordinate indexing only, not the scalar operation. · OAI.ExactFourier.TensorAxis.appendCoordinates

appendHomotopy def

The path-space version of concatenating a fixed homotopy with a variable path. · OAI.Thomason.Construction.PathSpace.appendHomotopy

appendInTime def

The timed witness stores the exact three-loop transition count. · OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.appendInTime

appendInTime def

The timed witness stores the exact three-loop transition count. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.appendInTime

appendNonempty def

Literal concatenation by a genus-zero connected sum at exterior corners. · OAI.HyperbolicObstruction.WordPictures.WordPicture.appendNonempty

appendPair def

Serialize two already encoded fields by actual word concatenation. · OAI.ContinuumCoulomb.EncodingPrograms.appendPair

appendSpin def

Append the distinguished cavity spin in the last position. · OAI.DilutedSpinGlass.appendSpin

appendState def

A fresh controlled computation appends a register, retaining the old one. · OAI.ExactQuantumFactoring.RecordedHistory.appendState

appendSuffix def

Append an arbitrary suffix, staying within prefixes of the final word. · OAI.Superstring.Hierarchical.Path.appendSuffix

appendTwo def

Append two values to a function on a finite initial segment. · OAI.Problem348.appendTwo

appendTwoIncreasing def

The increasing map obtained by appending two positions after an anchor. · OAI.Problem348.appendTwoIncreasing

appendWord def

Concatenation of exact binary inputs, not an encoded surrogate. · OAI.TraceReconstruction.appendWord

apply def

`stay` returns the stack unchanged, `pop` takes its tail, and `push b` prepends `b`. · OAI.CurrentKS.StackAction.apply

apply def

Popping empty is allowed and does nothing. · OAI.Fifths.StOp.apply

apply def

Apply the projection operator to an arbitrary real assignment table. · OAI.MaxCutGames.Repetition.ProjectionKernel.apply

apply def

Literal finite maximum of overlapping secondary proposals, with the exact winning chart table and label variables. No sum over group movements is used. · OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.apply

apply def

The actual simultaneous layer and selected ordinary/ordered chart table. · OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.apply

apply def

Actual one-group secondary installation with old identifiers retained and fresh ordinary, ordered, and rebased height chart data supplied by their formulas. · OAI.PlanarL1.Columns.Model.BState.SecondaryStep.apply

apply def

Actual finite main update, with the chart table containing every ancestor formula and each shield's rebased label variables. · OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.apply

apply def

The exact single kept main-cell update, including the fresh shield label rebase and retention of every old identifier wherever the scalar clip is old. · OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.apply

apply def

The actual finite average, with the inverse convention of the Koopman action. · OAI.PolycyclicRecognition.FiniteOrbitAverage.apply

apply def

The intercept derivative of the cell masses, written in coordinates. · OAI.Problem358.CellLaplacian.apply

apply def

Apply the projection operator to an arbitrary real assignment table. · OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply

applyPath def

Apply a continuous family of linear maps pointwise to a path. · OAI.ForcedComputation.Flow.applyPath

applyPathL def

Pointwise application depends continuously and linearly on the family. · OAI.ForcedComputation.Flow.applyPathL

applySuper def

Apply a matrix on pairs of indices to an ordinary matrix. · OAI.MUB6.Weiner.applySuper

applyValue def

Exact application: plain next, free continue slice, or checked exit. · OAI.PureTypeSystem.ObservationValues.applyValue

applyWord def

Apply a word of operators, in the multiplication order used by noncommutative polynomials. A generator and its adjoint are separate letters of the alphabet. · OAI.Kaplansky.applyWord

appRelation def

The application relation of a particular graph name. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.appRelation

ApproachingContinuum structure

The approach data furnished by the manuscript interface proposition, with no assumption of angular strip conclusions. · OAI.EuclideanFiveColor.ApproachingContinuum

approx def

The directed weighted-cube averages. · OAI.PlaneFiveColor.InvariantMean.approx

ApproxAnswer def

The approximation algorithm must return a feasible cut, not just an estimated value. · OAI.UniformSparsestCut.ApproxAnswer

ApproximateCyclicColumns def

Every unit vector in a finite Hilbert sum is a limit of bounded cyclic columns applied to one unit vector. · OAI.KadisonSimilarity.ApproximateCyclicColumns

ApproximatelyInner def

Approximation by finite sums of inner compressions (KR02 Definition 7.1). · OAI.WeakPureInfiniteness.ApproximatelyInner

ApproximatelyInnerAlong def

Finite inner approximation relative to the specified inclusion. · OAI.WeakPureInfiniteness.ApproximatelyInnerAlong

ApproximatelyOneStepAlong def

One-coefficient approximation relative to the specified inclusion. · OAI.WeakPureInfiniteness.ApproximatelyOneStepAlong

ApproximatelyOneStepInner def

Point-norm approximation by a single inner compression. · OAI.WeakPureInfiniteness.ApproximatelyOneStepInner

approximateRepresentation def

Pointwise asymptotic multiplicativity suffices. There is no hidden intersection over all group relations, nor any dimension bound. · OAI.NuclearUltrapower.HilbertUltraproduct.approximateRepresentation

Approximates def

The full sequential approximation conclusion, with unrestricted approximating exponent vectors, as required by the dimensional induction. · OAI.Problem326.Affine.Approximates

ApproximatesAtMinimum def

The sequential condition required of a family at one fixed minimum level. · OAI.Problem326.Affine.ApproximatesAtMinimum

ApproximatesOnCube def

The full sequential conclusion of the affine approximation lemma. · OAI.Problem326.Affine.ApproximatesOnCube

ApproximatesOnSupport def

The lower-dimensional induction hypothesis, transported to one support. · OAI.Problem326.Affine.ApproximatesOnSupport

approximationEnvelope def

The standard three-term envelope for a reduced rational approximation. · OAI.Problem337.Vaughan.approximationEnvelope

approximationFactors def

Deterministic polynomial-time approximation factors for arbitrary specified clients and facilities. · OAI.MetricKMedian.approximationFactors

ApproximationNPHard def

NP-hardness of the factor-C search problem, under one-call polynomial-time oracle reductions. The postprocessor must work for every valid approximate answer, not just for a helpful choice of answer. · OAI.UniformSparsestCut.ApproximationNPHard

approximationRows def

Independent coordinate rows followed by a finite prefix of polar rows. · OAI.SymmetricMahler.approximationRows

aprox def

Exp series truncated. · OAI.FourierLLogL.Dyadic.Thermal.aprox

ArbitraryFieldCovarianceBound def

Arbitrary real background fields do not increase the spin covariance above the zero-field correlation. · OAI.BufferedIsing.ArbitraryFieldCovarianceBound

ArbitraryTailInput def

Exact arbitrary-displacement cancellation input (unlike a pure-tail assertion). · OAI.DiamondDistortion.PathApplications.ArbitraryTailInput

arc def

A closed major arc about a reduced rational, at Dirichlet scale N. · OAI.Problem337.MinorArc.arc

arcCoefficient def

A positive Fourier coefficient of the centered narrow-arc indicator. · OAI.KadisonSimilarity.arcCoefficient

arcFourierIntegral def

The normalized angular Fourier transform of the actual centered arc. · OAI.KadisonSimilarity.arcFourierIntegral

Arch structure

exponent with both it and the power of two available in polynomial resources. · OAI.PowerSaving.RAM.Bench.Arch

arcHankelMatrix def

The actual N × N Hankel block tested in the manuscript. · OAI.KadisonSimilarity.arcHankelMatrix

Arches inductive

Ordered stack matching, with unpaired positions allowed. The skipped positions will be endpoints of the other colour in the map tour. · OAI.FKCRT.MapCycles.Arches

archivePolynomial def

Full unary lengths of both physical archives, including all graph predicate entries, all delimiters, and all expander reverse addresses. · OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.archivePolynomial

archivePolynomial def

Full unary lengths of both physical archives, including all graph predicate entries, all delimiters, and all expander reverse addresses. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.archivePolynomial

arcPairs def

Adjacent path entries, using only indices below the stored path length. · OAI.ContingencyTables.FlowPathProgram.arcPairs

arcSign def

Signed open-arc membership. Boundary columns have sign zero. · OAI.PlanarL1.Columns.Model.Field.arcSign

arctanTest def

A bounded continuous arctangent test of a law. · OAI.MetricMeasureLimits.DiameterCenter.arctanTest

arcWidth def

The angular half-width used in the manuscript. · OAI.KadisonSimilarity.arcWidth

arcX def

Rational parametrization of a small arc around (1,0). · OAI.ClosedSurfaceR4.CollarVelocity.arcX

area def

Euclidean planar Lebesgue area, extended to ambient subsets. · OAI.TriangularCovering.area

areaDensity def

The limiting polynomial for the second-order area coefficient. · OAI.TriangularCovering.areaDensity

Arena structure

Normalized potentials. A can only move down in time. Across indices A moves up while the low and high potentials are margins of disjoint intervals that move down. · OAI.FourierLLogL.Compress.Arena

ArgSplit structure

Unlike the work splits, never push either marker. · OAI.Fifths.ArgSplit

ArgsStep inductive

Exactly one reduction step in one term of an argument list. · OAI.PureTypeSystem.ArgsStep

argumentFrame def

A function's normalized argument frame, formed at the exact stored product, not at an independently chosen derivation of that product. · OAI.PureTypeSystem.ObservationValues.ProductInstance.argumentFrame

ArithmeticBound abbrev

A uniform scalar-operation bound with arbitrary positive exponent slack. · OAI.MatrixMultiplication.AuxiliarySeparation.ArithmeticBound

ArithmeticEdge def

All predicates are bounded integer-coordinate tests. · OAI.ContingencyTables.SmallGraphProfiles.ArithmeticEdge

arithmeticMapInvocations def

Includes the map's base frame and every recursive traversal frame. · OAI.EditApproximation.arithmeticMapInvocations

arithmeticPairSplitTest def

none means a preceding unit or support test failed. It has zero weight and does not impose any condition on an unexposed split. · OAI.Ostmann.arithmeticPairSplitTest

ArithmeticRepair def

A directed repair is identified by its two defect cells. · OAI.ContingencyTables.SmallGraphProfiles.ArithmeticRepair

ArithmeticResidueSplit structure

The two coefficients contain the current giant and its nonbulk factors. They are allowed to fail the required unit tests. · OAI.Ostmann.ArithmeticResidueSplit

arithmeticScale def

The unfolding scale Q = [O_K M : M] √|disc K|. · OAI.DukePrimeDegree.arithmeticScale

ArithmeticSplitData structure

All entries are known before the child product is exposed. The units contain the current giants and the nonbulk constants. · OAI.Ostmann.ArithmeticSplitData

ArithmeticSupport def

This support is exactly the original node validity together with the sampled compensation division. It also specifies the actual child giants. · OAI.Ostmann.MovingSlotData.ArithmeticSupport

arithmeticTestFlag def

Use one fixed decision procedure in statements and proofs. · OAI.Ostmann.arithmeticTestFlag

arity abbrev

Number of internal nodes, so that the number of leaves is arity+1. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.arity

Array structure

Actual orbit-coordinate arrays with a uniform bound from the minimizing basepoints, before taking any product or limiting metric. · OAI.HyperbolicObstruction.OrbitLimit.Array

array def

The actual graph-valued orbit array, uniformly bounded using the fixed finite route to each vertex. · OAI.HyperbolicObstruction.MasterGraph.array

array def

A rational array, as an ℓᵖ vector. · OAI.SeparableQuotient.LpFinite.array

arrayCode def

A zero-filled rational array recorded by order positions, including zero values. · OAI.SeparableQuotient.PathCoding.arrayCode

arrayHessianTerm def

The part of one actual normalized Hessian Green integrand containing its invariant quadratic form, distinguished cubic trace and projected cost. · OAI.PositiveEinsteinFour.QuaternionFrame.arrayHessianTerm

arrayRead def

Indexed read. Register 4 is a unary index; register 0 is a serialized array and is restored byte-for-byte. Register 5 receives the exact binary word. · OAI.RationalHitting.StackLanguage.arrayRead

arrayThreading def

The actual polynomially computed greedy matching, used as a mathematical threading. Only its finite inverse proof is noncomputable; the forward table is code. · OAI.Superstring.Computable.arrayThreading

arrayWrite def

Indexed overwrite with no fixed cell width or numerical oracle. · OAI.RationalHitting.StackLanguage.arrayWrite

ArrivalOrder abbrev

A physical arrival order visits every label once, indexed by arrival time. · OAI.MatroidProphet.LabeledTransport.ArrivalOrder

Arrow structure

A contraction with its uniquely determined monoid index. · OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow

arrow def

The intervertex map is precisely left multiplication by a. · OAI.ExternalTensor.Section4.ArrowVertex.arrow

arrow def

Arrow action is a natural transformation between the actual vertex functors. · OAI.LittleFinitistic.LeftVertexHomology.arrow

arrow def

The distinguished arrow acts by one, followed by the original generators. · OAI.LittleFinitistic.RelationBasisAction.arrow

arrow def

A supported arrow acts between its actual source and target subspaces. · OAI.LittleFinitistic.VertexModuleAssembly.arrow

arrow def

Left multiplication by an arrow a with target idempotent e'. · OAI.LittleFinitistic.VertexProjectives.arrow

arrow def

Nondependent labelled arrow; its codomain is shifted, not captured. · OAI.PureTypeSystem.Labelled.Expr.arrow

arrow01 def

Arrows s,a_1,...,a_d from vertex 0 to 1; index zero is s. · OAI.LittleFinitistic.QuadraticEncoding.arrow01

arrow01 def

The actual right-module arrow maps, given by left multiplication. · OAI.LittleFinitistic.SourceVerdier.arrow01

arrow01Map def

Left multiplication by the original first arrow on the actual vertex complexes. · OAI.LittleFinitistic.CanonicalArrowCompatibility.arrow01Map

arrow12 def

Arrows s',a'_1,...,a'_d from vertex 1 to 2; index zero is s'. · OAI.LittleFinitistic.QuadraticEncoding.arrow12

arrow12Map def

Left multiplication by the original second arrow on the actual vertex complexes. · OAI.LittleFinitistic.CanonicalArrowCompatibility.arrow12Map

arrowMap def

The actual arrow between BC vertex projectives. · OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.arrowMap

arrowMap def

Inclusion along an actual contraction, with its proof that exact availability is preserved. · OAI.PartitionConsistency.LocalDiagramSystem.System.arrowMap

arrowState def

Put the same orientation on the occupied positions of a frontier. This is used only for frontiers with exactly one occupied edge. · OAI.CriticalHoneycomb.Transfer.PlanarNormalization.arrowState

artinDescendingData def

Actual right-angled Artin descending cubes supplied by the proved signed trace normal form. None of the contractibility hypotheses are postulated. · OAI.EilenbergGanea.artinDescendingData

artinDescentSystem def

The actual RAAG satisfies every hypothesis of the descending-chain contraction, as a consequence of the independently proved trace normal form. · OAI.EilenbergGanea.TraceWords.CubeDescents.artinDescentSystem

artinEquiv def

The actual presented Artin group equals the word group constructed by confluence of individual-occurrence cancellations. · OAI.EilenbergGanea.TraceWords.artinEquiv

artinExponent def

Exponent sum, valid for every Artin matrix (including infinity labels). · OAI.ArtinCAT0.artinExponent

artinExponent def

The total exponent homomorphism for the Artin presentation. · OAI.HarmonicArtin.ParabolicIntersections.artinExponent

artinLift def

Universal property in commuting-generator form. · OAI.EilenbergGanea.artinLift

artinMap def

Renaming vertices along a graph isomorphism gives the expected group map. · OAI.EilenbergGanea.artinMap

artinRelations def

The defining commutators of the right-angled Artin group. · OAI.EilenbergGanea.artinRelations

artinRelators def

Infinity imposes no relation. Diagonal entries impose only trivial relations. · OAI.ArtinCAT0.artinRelators

ArvesonDistanceFormula def

The specialization of CSSW (2010), Equation (2.1), used for this operator. M is already equal to its double commutant by its VonNeumannAlgebra structure. · OAI.KadisonSimilarity.ArvesonDistanceFormula

ascendingCycleInTime def

A full positive-radix cycle performs n body visits and exactly 2*n counter transitions. This bound comes from the composed actual execution. · OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.ascendingCycleInTime

ascendingCycleInTime def

A full positive-radix cycle performs n body visits and exactly 2*n counter transitions. This bound comes from the composed actual execution. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.ascendingCycleInTime

asComplex def

The coercion to complex values preserves the actual conductor and character. · OAI.Ostmann.PrimitiveRealCharacter.asComplex

assemble def

Gluing of GLOBAL state labels along the running-intersection bags. · OAI.BoundedTreewidthL1.ExpandedTree.assemble

assemble def

The actual sum of all tensor-block inclusions in count r and degree n. · OAI.DerivedBar.Multibar.Indexed.assemble

assemble def

Gluing constructor. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.assemble

assemble def

Reassemble an actual matrix from its fixed visible base and private part. · OAI.MaxCutGames.Decoder.AdviceFibers.assemble

assemble def

Assemble the three blocks. The last coordinate vanishes on B. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.assemble

assemble def

The assembled prism is defined on the actual geometric realization times I. · OAI.Thomason.Construction.RealizationPrism.assemble

assemble def

Reassemble an actual matrix from its fixed visible base and private part. · OAI.UniqueGamesTheorem.Decoder.AdviceFibers.assemble

assemble def

Assemble the three blocks. The last coordinate vanishes on B. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.assemble

assembleBits def

Assemble the previously exposed low layers and the still-fresh high layers without identifying or resampling any switch coin. · OAI.CubeShuffle.assembleBits

assembled def

Assemble specified vertex isomorphisms into a vector-space isomorphism. · OAI.LittleFinitistic.VertexModuleAssembly.assembled

assembleLabel def

The full output is dummy exactly when some second-coordinate output is dummy. Stationary coordinates are supplied as some of their untruncated label; rotating coordinates use the actual truncated output. · OAI.QuantitativeVanDerWaerden.assembleLabel

assembleWord def

Pointwise reconstruction introduces no independent choice of a mask. · OAI.QuantitativeVanDerWaerden.assembleWord

AssemblyData structure

The concrete column/map interface. No composite or null-homotopy is assumed. The three equations are path naturality, the algebra relations, and the chosen relation homotopies after column induction. · OAI.ExternalTensor.Section4.AssemblyData

assign def

Logical assignment preserves the input values in the physical trace, but provides the standard overwritten-state interface to the next computation. · OAI.ExactQuantumFactoring.BooleanNetwork.assign

Assigned def

The assignment on all vertices, choosing a single chain per orbit of actual components. Its witnesses are local names and literal label indices. · OAI.PartitionConsistency.ProductForcing.ChainCode.Assigned

assignedCount def

Each nontrivial chain with c clique vertices represents c-1 paths. · OAI.CycleClique.Construction.ExpandedPathSystem.assignedCount

assignedIndicator def

Unassigned columns contribute zero; assigned columns use replacement pivots. · OAI.MetricEntropyDuality.CompressionLevels.assignedIndicator

assignedInhabitedBand def

This is the value supplied to the supported plane theorem. · OAI.LipschitzHilbert.PacketLatticeData.assignedInhabitedBand

assignedInhabitedBand def

This is the value supplied to the supported plane theorem. · OAI.LipschitzHilbert.SourceLabeledLattice.assignedInhabitedBand

assignedReferenceFamily def

The selected reference family has derived shear and carrier bounds. · OAI.LipschitzHilbert.PacketLatticeData.assignedReferenceFamily

assignedReferenceFamily def

The common-type recentered family used in the actual top envelopes. · OAI.LipschitzHilbert.SourceLabeledLattice.assignedReferenceFamily

assignedTopPacketEquiv def

No packet is copied to a second top, and no empty fiber adds a packet. · OAI.LipschitzHilbert.PacketLatticeData.assignedTopPacketEquiv

assignedTopPacketEquiv def

No packet is copied to a second top, and no empty fiber adds a packet. · OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopPacketEquiv

assignedTopReferenceLabel def

The reference label still points to its unique original label. · OAI.LipschitzHilbert.PacketLatticeData.assignedTopReferenceLabel

assignedTopReferenceLabel def

The reference label still points to its unique original label. · OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReferenceLabel

assignedValue def

The assigned mixture after pivot replacement. · OAI.MetricEntropyDuality.CompressionLevels.assignedValue

assignment def

The independent partition is assigned to vertices by parity. · OAI.InfiniteMatroidCounterexample.assignment

assignment def

Unique enumeration of a wellordered set after the single fixed choice of its ordinal indexing bijection. · OAI.PartitionConsistency.OrderAssignment.assignment

assignmentEquiv def

Balanced choices are the dependent product of the actual intervals. · OAI.ContingencyTables.LargePairEnumeration.assignmentEquiv

assignmentGraph def

The collected graph is a set-sized HS name with the single support D_q. · OAI.PartitionConsistency.ProductForcing.ChainCode.assignmentGraph

assignmentOfKey def

The global index map is an explicit equivalence, including all padding. · OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey

assignmentOfKey def

The global index map is an explicit equivalence, including all padding. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.assignmentOfKey

assignmentProbability def

The exact uniform probability on an explicit finite assignment space. · OAI.MaxCutGames.Quadratic.assignmentProbability

assignmentProbability def

The exact uniform probability on an explicit finite assignment space. · OAI.UniqueGamesTheorem.Quadratic.assignmentProbability

Assignments abbrev

The relaxed four-path assignments factor as a product over internal vertices. · OAI.Problem335.Pairings.Assignments

assignmentsEquiv def

Every function has exactly one equality pattern and an injection assigning distinct values to its blocks. No probabilistic premise is used. · OAI.MUB6.EqualityPatterns.Family.assignmentsEquiv

assignmentSplit def

The large-cell product is the tree-interval product times the original free-cell product, each with multiplicity one. · OAI.ContingencyTables.ForestAssignmentSplit.assignmentSplit

assignmentTerm def

Conjunction specifying one assignment on a selected block of bits. · OAI.TwoPointCorrelations.AC0Circuit.assignmentTerm

Associated def

Association is only used for increasing likelihood-threshold events. · OAI.TraceReconstruction.FiniteLaw.Associated

associatedGraded abbrev

The actual Rees associated graded algebra of the source image filtration. · OAI.StableCoordinate.AssociatedGradedPresentation.associatedGraded

associatedGradedEquiv def

The complete concrete associated-graded presentation, with no graded-domain or source-presentation hypothesis added. · OAI.StableCoordinate.AssociatedGradedPresentation.associatedGradedEquiv

associatePrincipalIdeal def

Send an associate class to its actual principal ideal. · OAI.Nagata.Workers.W30.associatePrincipalIdeal

associatingHomotopy def

Association is a continuous homotopy on the entire space of three paths. · OAI.Thomason.Construction.PathSpace.associatingHomotopy

associatingParameter def

The fixed interval map relating the two associations of three paths. · OAI.Thomason.Construction.PathSpace.associatingParameter

associativeTermEquiv def

Associativity on actual cochain terms, retaining the outside S-action. · OAI.LittleFinitistic.BimoduleComplexTensor.associativeTermEquiv

asUniformFamily def

A representative is the one-element case of a uniformly bounded family. · OAI.KadisonKastler.WeakOperatorRepresentative.asUniformFamily

AsymptoticActive def

Limit points of active parameters as the positive scale tends to zero. This neighborhood formulation needs no regularity of the activity predicate. · OAI.Problem326.AsymptoticActive

AsymptoticFixedWLBound def

The conventional big-O form: total correctness and one eventual n^r bound. This allows arbitrary behavior at the finitely many smaller graph orders. · OAI.ParityWL.Complexity.AsymptoticFixedWLBound

AsymptoticUniformWLBound def

Eventual time bounds may start at an arbitrary order depending on k; the same finite machine receives binary k and the two full adjacency matrices. · OAI.ParityWL.Complexity.AsymptoticUniformWLBound

At def

A failed finite prefix ends at the live retry label, while a successful prefix ends in the machine's halted configuration. · OAI.ContingencyTables.OnlineRetryPrefix.At

At def

A literal HS name represents a point of the glued component at w. The name, rather than its check-name code, is used in this predicate. · OAI.PartitionConsistency.ProductForcing.ChainCode.At

At def

Occurrence at this index and forced nonoccurrence at every smaller index in the fixed ground wellordering. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.At

at def

Sentences are usable as open hypotheses with any finite supply of variables. · OAI.PartitionConsistency.Theory.at

at def

The geometric state on a chain, using outgoing velocity at a collision. · OAI.TriangularBilliards.FlightChain.at

atBase def

Use at offset p. · OAI.PowerSaving.Slant.Reel.atBase

AtComap abbrev

The actual coefficient localization at the contracted prime. Maximality of the contraction is a separate input to the local comparison theorem, not an assumption needed to construct this map. · OAI.CirculantHadamard.AlternatingLocalization.AtComap

atLevel def

The literal collection at level j; a retained top keeps every fan slot. · OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.atLevel

atLevel def

The class-coordinate selected at depth i by a common leaf and an axis seed. · OAI.Problem348.TreeSampling.atLevel

AtMostOneNeighbor def

The combinatorial leaf condition, stated without assuming local finiteness. · OAI.TorsionFreeZeroDivisors.SystemLeaves.AtMostOneNeighbor

Atom structure

A represented atom includes its coefficients, rather than just its value. · OAI.DiamondDistortion.SegmentSystem.Atom

Atom abbrev

Actual names of the common-graded basis vectors, including empty cells. · OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.Atom

atom abbrev

Singleton segments, used only as a right inverse, not as a restriction on the allowed representations. · OAI.DiamondDistortion.StartModel.atom

atom def

Single star atoms as profiles in ambient coordinates. · OAI.HadwigerCounterexample.atom

atom def

Conversion of an actual signed atom back to the old ordinary orientation. · OAI.PlanarL1.Columns.Model.OrdinaryData.atom

atom def

The atom is the appropriate face of the corresponding globe's top cell. · OAI.Thomason.Construction.PastingGlobeBasis.atom

atom def

An actual bounded cell for every formal tensor basis vector. · OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom

atom def

The actual simplex atom indexed by an increasing tuple. · OAI.Thomason.Construction.SimplexAtomsInput.atom

atom0 abbrev

Cocoon. Universal micromoves on alpha 0. · OAI.ExactDerandomization.SiteX.Line.atom0

atomChart def

A finite globally consistent chart table for every possible spatial atom. Unused identifiers get a constant chart and can never be selected by pasted. · OAI.PlanarL1.Columns.Model.Point.RadialTree.atomChart

AtomConservative def

Occurrence-sensitive atom conservation, stronger than dimension conservation. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.AtomConservative

atomic def

The previously constructed recursive atomic relations, restricted to the actual HS class of this set symmetric system. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.atomic

AtomicConstruction def

The two atomic interpolation blocks and their summable correction reconstruct the minorant with the specified Gaussian normalization. · OAI.AtomicTriangular.AtomicConstruction

AtomicData structure

A literal local decomposition into labeled atoms. It remembers the same atom across every paired germ and the unique child containing each parent atom. In applications atoms are the actual simultaneous graded basis vectors, not just … · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData

AtomicData structure

Atomic forcing laws on a set of name codes. These are only the equality, substitution and monotonicity laws; this structure contains no ZF axioms, Choice or Partition Principle assertions. · OAI.PartitionConsistency.ForcingQuotient.AtomicData

atomicData def

A checked literal partition, derived from atom conservation at all ports. No coverage hypothesis about solution varieties is introduced here. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.atomicData

atomicMatchingPlan def

The coupling which matches equally indexed atoms without splitting mass. · OAI.Problem358.atomicMatchingPlan

atomicThresholdOutput def

A fixed one-electron unit nucleus with adjacent integer thresholds. · OAI.ContinuumCoulomb.atomicThresholdOutput

AtomIndex abbrev

An atom retains both its degree and its increasing vertex tuple. · OAI.Thomason.Construction.SimplexComplex.AtomIndex

AtomLaw structure

Finite convex atom laws, with explicit probabilities and mean. · OAI.DiamondDistortion.SegmentSystem.AtomLaw

atomLift def

Lift the canonical representative to the appropriate actual globe face. · OAI.Thomason.Construction.PastingGlobeBasis.atomLift

atomLift def

The chosen atom lift lies in an original globe-cylinder piece. · OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.atomLift

atomName def

Atom names use depth, portal column and type. Equal portals therefore have one name and one noise, including the root's single tentative atom. · OAI.PlanarL1.Columns.Model.Point.RadialTree.atomName

atomPairChecks def

Every prime constituent of one atom is compared to every constituent of each different atom. Repeated coordinates are deliberately retained. · OAI.Ostmann.atomPairChecks

atoms def

The five genuinely named small fibers in the manuscript normal form. These are names, not extra geometric constraints on an old subspace. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.atoms

AtomSource structure

The exact portal occurrence from which an atom identifier originates. · OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource

atomString def

Uniformly sized binary atoms concatenated without boundary marks. · OAI.TraceReconstruction.atomString

atomSynthesis def

Absolutely convergent signed synthesis from ℓ₁. · OAI.BoundedTreePotentials.atomSynthesis

atomTests def

The predual is the completion in the exact atom-testing norm. · OAI.BoundedTreePotentials.Segments.atomTests

atomThreshold def

The manuscript's threshold 2⁻¹⁰ for a dominant coefficient. · OAI.LipschitzHilbert.PhaseCombinatorics.atomThreshold

atomWeight def

The occupancy of a specified old simultaneous basis atom in a facet. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.atomWeight

atPath def

The subtree at a prefix (values beyond terminal nodes are immaterial). · OAI.IntrinsicMarks.atPath

atPath def

The subtree at a prefix (values beyond terminal nodes are immaterial). · OAI.SignedDisk.IntrinsicMarks.atPath

atPc def

Each call pushes one measured frame. No intermediate vector is scoped as scratch across pushes. After checkA release the lookup work area; only one accumulated scalar is needed (plus u etc). We compute w' (small) before the reverse push. · OAI.Fifths.Circuit.atPc

atPoint def

The only singularity test; all repeated algebra is materialized in dense tables. · OAI.RationalHitting.ExecutableGenerator.atPoint

atPoint def

The filtering step tests only Z_0, and receives no formula. · OAI.RationalHitting.Generator.atPoint

attach def

Append a network whose inputs are arbitrary already-computed wires. Repeated input sources are permitted and do not cause duplicated computation. · OAI.ExactQuantumFactoring.BoolNet.attach

attachEdges def

Successively attach the edges, retaining the component equivalence relation. · OAI.KervaireRibbon.attachEdges

AttachedResiduePositiveWord def

Positivity for a word attached at a fixed displacement from the main origin. · OAI.TwoPointCorrelations.AttachedResiduePositiveWord

attachForestLeaf def

Add a fresh leaf as the first child of its unique parent. · OAI.TwoPointCorrelations.attachForestLeaf

attachImperfectLabels def

References to represented perfect labels reuse those labels. A reference to an unrepresented imperfect class uses its first position. · OAI.TwoPointCorrelations.attachImperfectLabels

attachingHomologyEquiv def

The top-cell collar comparison in a contractible ordinary attachment is an actual integral H1 isomorphism, proved from singular subdivision. · OAI.EilenbergGanea.CWCollar.Attachment.attachingHomologyEquiv

Attachment structure

Single-dimensional ordinary disk attachment. All fields will be derived from the actual CW structure, not posited for the classifying-space theorem. · OAI.EilenbergGanea.CWCollar.Attachment

Attachment structure

An actual presentation cell, identified with a subobject of the very same terminal monoid. The identification fixes every old element. · OAI.PartitionConsistency.ConservativeMonoids.Attachment

attachment def

There is one two-cell per physical edge, NOT one per directed dart. · OAI.TorsionFreeZeroDivisors.GraphConePresentation.attachment

attachmentCapacity def

Nat truncated subtraction/division equals max(0,floor((h-d)/2)) for the manuscript's nonnegative integral heights. · OAI.ArithmeticTensorSquares.Capacity.attachmentCapacity

attachValue def

Glue the old skeleton map to a prescribed disk map on each new cell. · OAI.GroupRingTopology.Cellular.attachValue

attempt def

change orientation and multi-head moves, attempting to step (uses at interior, no overflow or underflow) · OAI.ExactDerandomization.Counter.attempt

AtTime def

A specified visit of a finite switching path, retaining its traveled arclength. Multiple visits of the same representative are not identified. · OAI.PlanarL1.Columns.Model.Path.AtTime

attractor def

The manuscript explicitly identifies its compact attractor with coding limits. · OAI.CorSetReference.attractor

attractor def

The actual coding attractor, including every address, not merely an a.e. carrier. · OAI.EntropyRateDimension.Extensions.attractor

atUnperturbedScale def

Only the numerical scale changes; the actual chart and inverse are fixed. · OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.atUnperturbedScale

atZero def

Zero-parameter specialization, bundled as a coefficient-algebra homomorphism. · OAI.StableCoordinate.NormalizedDeterminantLift.atZero

aucModulus def

The one-sided asymptotic uniform convexity modulus, with the order of infimum, supremum and infimum. · OAI.ForestSpace.aucModulus

aucValues def

The inner one-sided excess values and their infimum. · OAI.ForestSpace.aucValues

augInc def

The temporary boundary is an unlabelled black vertex. · OAI.KaplanskyCounterexample.Planar.augInc

augment def

A feasible endpoint event augments the prescribed holes by the uniquely determined auxiliary paths. The witness is used only to verify disjointness. · OAI.CoordinateSweeps.Grid.Holes.augment

augmentation def

The bar augmentation as a chain map to N concentrated in degree zero. · OAI.DerivedBar.augmentation

augmentation def

The augmentation of the terminal right projective. · OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.augmentation

augmentation def

The augmentation retains the actual right BC-action. · OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentation

augmentation def

The identity on O and the genuine terminal augmentation give a D-bimodule chain map. · OAI.LittleFinitistic.OrdinarySimulation.XResolution.augmentation

augmentation def

The sum of coefficients, or augmentation, of the complex group algebra. · OAI.TorsionFreeBass.augmentation

augmentationComparison def

The concrete augmentation comparison descends to the genuine chain localization. This constructs a map; it does not assert the still-unproved isomorphism property. · OAI.LittleFinitistic.BimoduleTotal.augmentationComparison

augmentationComparisonOnChains def

Actual comparison induced by the actual bimodule augmentation, before localization descent. Invertibility is a separate finite-total proof obligation. · OAI.LittleFinitistic.BimoduleTotal.augmentationComparisonOnChains

augmentationMap def

The actual B-extended resolution augmentation as a chain map. · OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentationMap

augmentationRank def

The integer-valued augmentation rank on the usual idempotent presentation of algebraic K₀: on a generator it is the complex dimension of the augmented image. · OAI.TorsionFreeBass.augmentationRank

AugmentationTrace def

A finite initial segment of an actual shortest-augmentation execution. It need not already have reached a maximum flow. · OAI.ContingencyTables.PublishedEdmondsKarp.AugmentationTrace

augmentConfig def

Embed an original configuration while reserving one state and one exit position. · OAI.TwoWayComplementation.TwoNFA.augmentConfig

AugmentedAccepts def

Only the single positions matter to the extracted incidence game. · OAI.MaxCutGames.Soundness.IncidenceExtraction.AugmentedAccepts

AugmentedAccepts def

Only the single positions matter to the extracted incidence game. · OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.AugmentedAccepts

augmentedChoices def

Conditioning on a placement transition is exactly conditioning on the full, unique augmented coordinate paths, not an endpoint approximation. · OAI.CoordinateSweeps.Grid.Holes.augmentedChoices

augmentedComplex def

The augmented chain complex, including N at homological degree zero. · OAI.DerivedBar.augmentedComplex

augmentedForcing def

The actual normalized forcing generated by a physical forcing F. Here n=1/μ, o=1/(λ+2μ), and c_i=-2(∂ᵢμ)/μ. The scalar entry contains the conjugated divergence. · OAI.ElasticityPhysicalEstimate.augmentedForcing

augmentedMap def

Total affine weights and their vector sum. · OAI.SharpLiebThirring.PLParity.augmentedMap

augmentedMatrix def

Entrywise augmentation. · OAI.TorsionFreeBass.augmentedMatrix

augmentedMove def

Augmented moves at one symbol, including the original endmarker restrictions. · OAI.TwoWayComplementation.TwoNFA.augmentedMove

AugmentedProjective structure

Actual bounded right-projective resolution data, including the bimodule augmentation and its quasi-isomorphism; no tensor comparison is assumed. · OAI.LittleFinitistic.BimoduleTotal.AugmentedProjective

augmentedStep def

Original moves, an accepting stay into the fresh state, and its rightward sweep. · OAI.TwoWayComplementation.TwoNFA.augmentedStep

augmentFixEquiv def

The point--placement stabilizer is the literal stabilizer of all augmented holes, not an abstract group with the same cardinality. · OAI.CoordinateSweeps.Grid.Holes.augmentFixEquiv

Aut structure

Automorphisms preserve the vertex and bond structure, including multiplicities. · OAI.CriticalPercolation.BondGraph.Aut

automatic def

The automatic empty/singleton rule is a genuine zero potential, not a singular marked potential evaluated at a zero side parameter. · OAI.KServer.SimplexFamilies.automatic

automorphicOfChartHolomorphic def

Extract a genuine holomorphic multiplier function from a chart-holomorphic actual section. · OAI.Nagata.W08.automorphicOfChartHolomorphic

automorphicSectionOfPeriodicFunction def

Package the descended actual function as a genuine holomorphic multiplier section. Entire holomorphy, deck invariance and the scalar shift law remain explicit inputs. · OAI.Nagata.W08.automorphicSectionOfPeriodicFunction

automorphicSections def

Holomorphic functions on ℂ* with the multiplier of D(n,γ). The zero extension at the omitted point is part of the representation. · OAI.Nagata.W08.automorphicSections

automorphicToEquivariant def

Restriction of the actual holomorphic section to its genuine unit-valued cover. · OAI.Nagata.W08.automorphicToEquivariant

automorphismIsometry def

Extension of the automorphism on bounded algebra vectors. · OAI.KadisonSimilarity.TracialCornerGeometry.automorphismIsometry

automorphismRepresentation def

A trace-preserving algebraic group action gives a unitary representation. · OAI.KadisonSimilarity.TracialCornerGeometry.automorphismRepresentation

automorphismUnitary def

The actual unitary implementation of a trace-preserving automorphism. · OAI.KadisonSimilarity.TracialCornerGeometry.automorphismUnitary

auxiliaryCharacter def

The character of the shared sampled column, before any Fourier average. · OAI.MUB6.auxiliaryCharacter

auxiliaryDenominator def

The auxiliary denominator from one fixed block and a family of paired blocks. · OAI.Problem337.ResidueConstruction.auxiliaryDenominator

auxiliaryEncoding def

The actual Section 2 selecting algebra has one fixed concrete finite encoding. · OAI.LittleFinitistic.SelectionEncoding.auxiliaryEncoding

auxiliaryF def

Manuscript F₀ and F₁; the latter averages the five nonzero labels. · OAI.MUB6.auxiliaryF

auxiliaryGroupAlgebraEquiv def

Section 2's complex group algebra, for the exact auxiliary group supplied by the manuscript. The stable finite model has 18 generators, including the three redundant diagonal W generators killed by its relations. · OAI.LittleFinitistic.GroupAlgebraPresentation.auxiliaryGroupAlgebraEquiv

auxiliaryGroupAlgebraZeroEquiv def

Same explicit presentation expressed as polynomial zero relations. · OAI.LittleFinitistic.GroupAlgebraPresentation.auxiliaryGroupAlgebraZeroEquiv

auxiliaryMixedEntry def

The exact mixed-moment expression for a pair of auxiliary functions. · OAI.MUB6.auxiliaryMixedEntry

auxiliaryPiece abbrev

Actual auxiliary homogeneous pieces: deg(a,d,b,c,u) = (0,1,-1,0,1). · OAI.StableCoordinate.Obstruction.auxiliaryPiece

auxiliaryQuadraticEquiv def

Concrete quadratic quotient and actual algebra equivalence, retaining the proved stable group's generators and relators and eliminating its word auxiliaries. · OAI.LittleFinitistic.QuadraticPresentation.auxiliaryQuadraticEquiv

AuxiliarySample abbrev

Reference index, row bijection, nonreference-label bijection, and a column of the matrix assigned label zero. · OAI.MUB6.AuxiliarySample

auxiliaryWeight def

The second, auxiliary grading used only in the rigidity argument. · OAI.StableCoordinate.Obstruction.auxiliaryWeight

auxiliaryWeights def

The original law restricted to keys with zero retained demand. · OAI.UniformSparsestCut.FiniteWeights.auxiliaryWeights

availability def

Source availability-ideal lemma, common to symbolic elements and labels. The proof uses the already specified inclusion and intersection maps. · OAI.PartitionConsistency.LocalDiagramSystem.System.availability

Available def

Availability is existence of the same symbolic element at the specified subdiagram. It is not an independently assigned ideal. · OAI.PartitionConsistency.LocalDiagramSystem.System.Available

average def

Normalized average over one period. · OAI.ClosedSurfaceR4.CovarianceCorrector.average

average def

Conditional iid type/site labels, on the full fixed countable dictionary. · OAI.DilutedSpinGlass.CountableReservoir.average

average def

Signed averages needed by polarization stay in the SAME finite alphabet and in the unit-bounded rational table family. · OAI.DilutedSpinGlass.UniversalDictionary.average

average def

Rational expectation under uniform sampling on a finite space. · OAI.MaxCutGames.Gadget.Harmonic.average

average def

The uniform average on a finite type, with value zero on an empty type. · OAI.Problem335.IndependentCoordinates.average

average def

Rational expectation under uniform sampling on a finite space. · OAI.UniqueGamesTheorem.Gadget.Harmonic.average

averageCLM def

The normalized Haar average, bundled with its norm bound. · OAI.ClosedSurfaceR4.CovarianceCorrector.averageCLM

averageCode def

A real weighted averaging of all pulled-back odd long codes at a right question. The graph/test itself uses only rational probabilities. · OAI.OptimalMaxCut.LongCode.Game.averageCode

averageConjugation def

The unital completely positive invariant average of conjugates. · OAI.KadisonKastler.ScalarInvariantMean.averageConjugation

averageCost def

averaged defect form. · OAI.FourierLLogL.Dyadic.Thermal.averageCost

averagedIncrement def

Averaged increment for directions of norm at least one. · OAI.ExactModuli.averagedIncrement

averagedMap def

Explicit finite-group induction on a linear map. · OAI.Saxl.averagedMap

averagedMidpointModulus def

The averaged asymptotic midpoint modulus, with directions of norm at least 1. · OAI.IndependentProducts.averagedMidpointModulus

averagedModulus def

We take these infima and suprema in the extended reals, so their definitions are meaningful without tacit boundedness side conditions. On infinite dimensional normed spaces their values at positive radii are finite. · OAI.BoundedTreePotentials.averagedModulus

averagedModulusReal def

The real-valued averaged asymptotic modulus. · OAI.BoundedTreePotentials.averagedModulusReal

averagedRangeLinear def

The lower linear map is defined only by inversion on the embedded range. · OAI.KadisonKastler.averagedRangeLinear

averagedRangeMap def

Complete positivity is reflected through the faithful ambient embedding. · OAI.KadisonKastler.averagedRangeMap

averagedRowProducts def

Row sampling in an arbitrary number of retained nonzero coordinates. · OAI.MUB6.averagedRowProducts

averagedUpperMap def

The averaged upper map, still valued in all upper ambient operators. · OAI.KadisonKastler.averagedUpperMap

averageMarginal def

The common marginal of the cyclic average. · OAI.Problem356.Cyclic.averageMarginal

averageMatrix def

Literal finite averages and their adjoints have the same group-algebra word in every unitary representation. · OAI.CoordinateSweeps.UnitaryIrrep.averageMatrix

averageModulus def

The averaged asymptotic midpoint modulus. · OAI.ForestSpace.averageModulus

averagePhase def

The normalized interval average appearing in the dyadic majorant. · OAI.ExactQuantumFactoring.OrderTrial.averagePhase

averageSensitivity def

Sum of the uniform probabilities that a coordinate flip changes f. · OAI.LeanBlast.GotsmanLinial.averageSensitivity

averageValues def

Inner sets are kept explicit to make nonemptiness and conditional completeness visible. · OAI.ExactModuli.averageValues

averageValues def

The inner averaged signed excess; it is not replaced by a maximum. · OAI.ForestSpace.averageValues

averagingUF def

One fixed ultrafilter is used for all functions. · OAI.PlaneFiveColor.InvariantMean.averagingUF

avg def

Finite dimension-weighted sector average; no random choices enter a circuit. · OAI.ExactFourier.Amplification.avg

avg def

Weighted average (not normalized if the weights are not a probability law). · OAI.HadwigerCounterexample.avg

avoid def

Avoid a finite list of bad events. · OAI.KaplanskyCounterexample.FiniteLocalLemma.avoid

avoid def

Outcomes avoiding every bad event indexed by T. · OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.avoid

avoidanceIsometryEquiv def

An extension fixing S preserves separately each containment-and-avoidance condition A⊂L, L∩S=A used in the independent residual laws. · OAI.SidorenkoCounterexample.avoidanceIsometryEquiv

Avoids def

Cut an unused middle link on each private wire. End links need never be removed: the private interior alone is longer than any small support. · OAI.WLIdentification.ComparisonSchemas.Avoids

avoids def

At each endpoint at most q calls, with distinct labels and no label interacting with a short vector in the pinned projections. · OAI.HadwigerCounterexample.Volley.avoids

AvoidsCopy def

Arbitrary colorings and exact distance-preserving copies; no measurability, computability, continuity of the coloring, or extension of the copy is assumed. · OAI.GrahamSpherical.AvoidsCopy

avoidsSelected def

A point survives if none of its vanishing forms is selected. · OAI.JointDickman.avoidsSelected

away def

A principal open as an actual subalgebra of the fixed function field. · OAI.FieldPrincipalOpen.away

awayInFractionField def

The localization A[a⁻¹], realized as an actual subalgebra of a fraction field. · OAI.StableCoordinate.awayInFractionField

AwayLocal abbrev

The coefficient localization used in the prime-direction comparison. · OAI.CirculantHadamard.CyclotomicAwayLocal.AwayLocal

awayPrime abbrev

The actual prime ideal on the coefficient ring with one direction omitted. · OAI.CirculantHadamard.CyclotomicAwayLocal.awayPrime

awayRing abbrev

The literal coefficient ring with the p-direction omitted. · OAI.CirculantHadamard.CyclotomicRings.awayRing

awEdge def

The penultimate cut contributes an edge precisely when its interval vertices are 0 and 1. · OAI.Thomason.Construction.SimplexComplex.awEdge

awEnd def

The last vertex of a basis simplex decides its endpoint summand. · OAI.Thomason.Construction.SimplexComplex.awEnd

aX def

Generator images of the original polynomial presentation. · OAI.StableCoordinate.Obstruction.aX

axes def

Global basis and its restriction. · OAI.PowerSaving.Cluster.axes

axialLaw def

The axial image law, with variance parameter as in Mathlib's Gaussian. · OAI.BoltzmannNonuniqueness.GaussianSheets.axialLaw

AxialMoment structure

The exact axial hypothesis used throughout the sheet estimates. · OAI.BoltzmannNonuniqueness.SheetMeasures.AxialMoment

axialUnit def

Unit vector along the axis of symmetry. · OAI.StationaryNS.axialUnit

AxisConditions structure

The ten order facts used by the sampled-path construction. These are separate from matrix entries and can be supplied by any correct enumeration of the two recursively ordered axes. · OAI.Problem348.Construction.SampledSelection.AxisConditions

axisEnergy def

The surviving part of (19) when the first block and its energy vanish. This expression has no division by the norm of that vanished block. · OAI.PositiveEinsteinFour.QuarticClosed.axisEnergy

axisStep def

A signed step is rejected at the boundary of the declared finite grid. · OAI.ContingencyTables.GridBoundary.axisStep

axisSwap def

Exchange the first and second Euclidean axes, leaving the third fixed. · OAI.Problem356.IsometryTransport.axisSwap

axisVector def

Unit coordinate vector for either local Coulomb branch. · OAI.Problem356.CoulombCalculus.axisVector

AxisymmetricSwirlFree def

Invariance under the full orthogonal group fixing the vertical axis pointwise. Unlike invariance under rotations alone, this includes reflections in vertical planes and excludes a swirl component. · OAI.StationaryNS.AxisymmetricSwirlFree

A₀ def

The deterministic constant in the manifestation of the diameter lemma. · OAI.TorsionFreeZeroDivisors.TypedDiameter.A₀