Glossary: E

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

E abbrev

The exact double-dual construction in the manuscript, lines 328. · OAI.CoherentModelActual.E

E def

Polynomial evaluation rows before dividing by (1+T²)(1+U²). · OAI.EuclideanRamsey.NineGrid.E

E def

E_i = e_i B as an actual finite projective right module. · OAI.LittleFinitistic.SourceVerdier.E

E def

Internal membership is literal membership, restricted to the collection. · OAI.PartitionConsistency.TransitiveSets.E

E abbrev

The formalization proves one-third Hölder stability of Brenier maps from the uniform measure on a compact convex body with nonempty interior in $\mathbb R^d$, for every $d\ge2$. For targets supported in one fixed nonempty compact set, the … · OAI.Problem358.E

E abbrev

The actual real Banach space E of the CH construction. · OAI.SeparableQuotient.ActualSpace.E

eachF def

Restrict pure form to individual diagonal blocks. · OAI.HadwigerCounterexample.eachF

Earlier abbrev

Earlier candidates include discarded entries and omit the current entry. · OAI.ReflexiveFixedPoints.CandidateLedger.Earlier

Earlier def

Earlier a z means that the move from a to z only lowers colors. · OAI.TalagrandThreshold.Selector.Earlier

EarlierA abbrev

Earlier codomain constraints inside the final codomain constraint. · OAI.MaxCutGames.Appendix.A5ReverseIndex.EarlierA

EarlierA abbrev

Earlier codomain constraints inside the final codomain constraint. · OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.EarlierA

EarlierB abbrev

Earlier retained domains containing the final retained domain. · OAI.MaxCutGames.Appendix.A5ReverseIndex.EarlierB

EarlierB abbrev

Earlier retained domains containing the final retained domain. · OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.EarlierB

earlierLabels def

Labels occurring before b in a fixed enumeration. · OAI.QuantitativeVanDerWaerden.earlierLabels

earliestChildDepth def

First available proper-child branching depth, with terminal value L when every proper child is a leaf. This handles the induction endpoint. · OAI.DilutedSpinGlass.ReducedTopology.earliestChildDepth

early def

The attaching deformation is completed during [a/2,a]. · OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.early

ears def

A comparison replacing very positive first coordinates by a bounded comparison sentinel. · OAI.ExactDerandomization.Buf.ears

eastRun def

Enter from the EAST wall on the bottom fresh row, ending immediately below the original source. This direction matches the checked flux bound. · OAI.CriticalHoneycomb.FiniteContinuation.eastRun

ed def

Ordinary unit-cost edit distance. The set is nonempty (delete then insert). · OAI.TreeEdit.ed

Edge abbrev

`x.Edge` is a dependent pair: an endpoint-pair index `i`, followed by a copy index below `x.multiplicity i`. · OAI.AlgorithmicThinTrees.BinaryInput.Edge

Edge def

Stage edges, retaining their parent, child number, and side. · OAI.DiamondDistortion.Diamond.Edge

Edge def

Every nonroot vertex is retained, including unary vertices. · OAI.DilutedSpinGlass.PrescribedTree.Edge

Edge abbrev

All incidences except Y_D--CD. Both sides have fixed named positions. · OAI.HyperbolicObstruction.IncidenceTemplate.Edge

Edge abbrev

Coordinates are attached only to nonroot vertices. · OAI.IndependentProducts.Edge

Edge def

Actual finite directed moment-graph edges, including the non-cover reflection edges. No reconstruction from the abstract poset is assumed. · OAI.KLInvariance.BruhatGraph.Edge

Edge abbrev

The unordered non-loop edges of the complete graph on n vertices. · OAI.LeanBlast.SecondKahnKalai.Edge

Edge abbrev

Edges of all crossing and stay candidates, together with all outward slots. Every outward slot is an edge to its own external leaf. · OAI.OneWayLiveness.CellNetwork.Edge

Edge def

The finite type of tree edges, represented by nonempty bounded-depth paths. · OAI.Problem310.TreePreorder.Edge

Edge def

One actual child-label coordinate of an arbitrary ordered occupied shape. Unlike a complete r-ary padding, this contains no unused edges. · OAI.TraceReconstruction.OccupiedParityTree.Edge

Edge abbrev

A finite free variable for each displayed source p and allowed f. · OAI.UniformKServer.EffectiveLP.Edge

edge def

The actual parent departure followed by the actual child incoming update. · OAI.BoundedTreewidthL1.ReservedSuffix.edge

edge def

The internal graph relation ⟨x,y⟩ ∈ f. · OAI.PartitionConsistency.SetLanguage.edge

edge def

A harmless total extension of the edge index; it equals i for i<h. · OAI.Problem348.Construction.SampledSelection.edge

edge def

An actual oriental cell from i to j. · OAI.Thomason.Construction.NormalizedSimplexIdentities.edge

edge def

The forced binary tree is embedded in the actual occupied edge set. · OAI.TraceReconstruction.OccupiedParityTree.Forced.edge

edge def

Row-major access, with a total default outside the matrix. · OAI.WLIdentification.NumericGraph.edge

edgeAccept def

labelAt is a fixed finite lookup table determined by the reduction parameters, for example decodeLabel a (allAddresses.get i). · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.edgeAccept

edgeAccept def

labelAt is a fixed finite lookup table determined by the reduction parameters, for example decodeLabel a (allAddresses.get i). · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.edgeAccept

EdgeAdjacent def

Undirected adjacency in a graph presentation. · OAI.PixtonChow.EdgeAdjacent

edgeAt def

The dart at the indicated time, computed by the actual preceding steps. · OAI.MaxCutGames.Foundations.PCP.PoweringWalks.edgeAt

edgeAt def

The dart at the indicated time, computed by the actual preceding steps. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.edgeAt

edgeBoundary def

The boundary of a positive lifted edge. · OAI.HyperbolicObstruction.IntegralIncidence.edgeBoundary

EdgeCell def

Anchor and signature cells for the four modes at one edge. · OAI.Problem348.GuardedPath.Selection.EdgeCell

EdgeChain inductive

A genuine finite vertex edge path. · OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain

edgeChain def

Signed contribution of a lifted dart to the free integral edge module. A negative dart is indexed at the start of its positive reverse. · OAI.HyperbolicObstruction.IntegralIncidence.edgeChain

edgeChain def

An oriented edge is represented in a free module on the positive orientations. · OAI.Release075.BlockPresentation.edgeChain

edgeCircuit def

The surface and regular seam part of the diagram equations. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.edgeCircuit

EdgeClosed def

A collection of literal names is hereditary for edges using conditions in P. Countability and this property impose no bound on name-rank. · OAI.PartitionConsistency.SetForcingNames.AtomicForcing.EdgeClosed

EdgeConnected def

`G.EdgeConnected k` says each nonempty proper vertex set has a whole-graph cut containing at least `k` edge copies. · OAI.StrongThinTree.MultiGraph.EdgeConnected

EdgeCoordinate abbrev

The finite matrix presentation of this portion of the local-system scheme, including inverses and all oriented boundary/facet equations. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.EdgeCoordinate

edgeCoordinates def

Edges of a path with at least one edge. · OAI.Problem335.Pairings.edgeCoordinates

edgeCount def

The number of unordered edges, each counted once. · OAI.LeanBlast.SecondKahnKalai.edgeCount

edgeCount def

The formula in Equation (4.21). · OAI.MaxCutGames.Reduction.Explicit.edgeCount

edgeCount def

Number of edges in the complete tree. · OAI.Problem310.TreePreorder.edgeCount

edgeCount def

The finite number of edge coordinates at a given child height. · OAI.TraceReconstruction.OccupiedParityTree.edgeCount

edgeCount def

The formula in Equation (4.21). · OAI.UniqueGamesTheorem.Reduction.Explicit.edgeCount

edgeDecode def

A partial inverse proves separation without a default element of Fin k. It therefore applies unchanged at k = 0. · OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.edgeDecode

edgeDecode_inline_AddressMachineSpace def

A partial inverse proves separation without a default element of Fin k. It therefore applies unchanged at k = 0. · OAI.MaxCutGames.Reduction.AddressMachineSpace.edgeDecode_inline_AddressMachineSpace

edgeDistribution def

Fixed explicit vertex enumeration, supplied as a finite equivalence. The semantic theorem does not hide an unweighted conversion or an edge multiset. · OAI.OptimalMaxCut.LongCode.Game.edgeDistribution

edgeEnds def

An edge's unordered endpoints; representatives do not change this pair. · OAI.FKCRT.edgeEnds

edgeEquiv def

`edgeEquiv` chooses an equivalence between the finite type `x.Edge` and consecutive indices `Fin (Fintype.card x.Edge)`. · OAI.AlgorithmicThinTrees.BinaryInput.edgeEquiv

edgeEquivFin def

The preorder gives the canonical enumeration of finite tree edges. · OAI.Problem310.TreePreorder.edgeEquivFin

edgeEvaluation def

Evaluation in the displayed group presentation, before quotienting faces. · OAI.Release075.BlockPresentation.edgeEvaluation

edgeFactor def

The manuscript's actual product of reduced root forms, with its proved nonnegative integral plane exponents. No abstract invariant is substituted. · OAI.KLInvariance.TitsSpace.edgeFactor

edgeFactorMap def

Multiplication by the genuine plane product on the actual edge module. · OAI.KLInvariance.BruhatGraph.edgeFactorMap

edgeFirst def

First occurrence of an edge in a fixed rooted one-cycle tour. · OAI.FKCRT.edgeFirst

EdgeFlabby def

Extension for sets closed under actual edges. It implies the source's ordinary flabbiness, and is convenient for the descending construction. · OAI.KLInvariance.MomentGraph.GradedSheaf.EdgeFlabby

edgeFlow def

Supported on the two ends of one band, including the harmless loop case. · OAI.KervaireFlow.edgeFlow

edgeForm def

The directed bilinear edge form (twice the quadratic mass on the diagonal). · OAI.CliqueFreeIndependence.WeightedGraph.edgeForm

edgeHeight def

Numeric incoming-window height for an edge path. · OAI.Problem310.WindowMetadata.edgeHeight

edgeInc def

Locate an oriented incidence in its cell, or at its external leaf. · OAI.OneWayLiveness.CellNetwork.edgeInc

edgeIndex def

The canonical preorder index of an edge. · OAI.Problem310.WindowMetadata.edgeIndex

edgeKey def

An edge is uniquely determined by the cell, move and states of its source proposal, or by its outward slot. · OAI.OneWayLiveness.CellNetwork.edgeKey

edgeLaw def

Exact edge law induced by fiber sampling; no independence of fiber labels or levels is postulated. · OAI.WeakPinned.SmallFiber.edgeLaw

edgeLength def

Extension by zero, only used to write the sum over Walk.edges. It does not add edges or change any graph-walk length. · OAI.BoundedTreewidthL1.edgeLength

edgeListShift def

Differentiated coordinates have sign -1, multiplied coordinates sign +1. · OAI.Problem335.edgeListShift

edgeLoop def

Every edge yields the actual loop obtained by the fixed endpoint routes. · OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.edgeLoop

edgeMass def

Unordered edge mass, written as half the directed edge mass. · OAI.CliqueFreeIndependence.WeightedGraph.edgeMass

edgeMid def

The midpoint lies in both endpoint stars, even for a collapsed edge. · OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.edgeMid

edgeOrder def

The ordinal map selecting a possibly degenerate edge. · OAI.Thomason.Construction.NormalizedSimplexIdentities.edgeOrder

edgePair def

A choice of orientation for each actual edge; only this choice, not an independent matching event for its reverse, is counted. · OAI.TorsionFreeZeroDivisors.ChainRealization.edgePair

edgePartition def

Connected components of a graph presented as a list of edges. · OAI.KaplanskyCounterexample.Planar.edgePartition

edgePath def

The actual linear path inside the geometric one-simplex of an edge. · OAI.Thomason.Construction.RealizationPrism.edgePath

edgePaths def

Edge paths in the complete ordered q-ary tree, in depth-first preorder. · OAI.Problem310.TreePreorder.edgePaths

edgeProfile def

Convert an edge list ordered by layer into its finite coordinate profile. · OAI.Problem335.edgeProfile

EdgeProjection structure

A weight-preserving, directed-edge-injective projection. · OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection

edgeRank def

Zero-based rank among edges, obtained by removing the root's rank. · OAI.Problem310.TreePreorderRank.edgeRank

edgeRoot def

Geometric label of an intrinsic graph edge, taken in the actual ambient root plane rather than an abstract alternate representation. · OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot

edgeRoutes def

Actual edge-chain routes exist in every path-connected finite realization. · OAI.HyperbolicObstruction.FinitePolyhedron.edgeRoutes

Edges def

Edges of a set name, with no choice of a presentation of that set. · OAI.PartitionConsistency.SetForcingNames.Edges

edges def

Literal undirected stage edges; both orientations name a single edge. · OAI.TorsionFreeZeroDivisors.StageSubgraphs.edges

edgeSetoid def

Physical unoriented edges, retaining loops and parallel edges. · OAI.TorsionFreeZeroDivisors.GraphConePresentation.edgeSetoid

EdgeState abbrev

Oriented edges, the disjoint union of the neighborhood state spaces. · OAI.CliqueFreeIndependence.WeightedGraph.EdgeState

edgeSubgraph def

The subgraph containing exactly the given edges and their incident vertices. For the empty edge set this has no vertices, as required for internal copies. · OAI.LeanBlast.SecondKahnKalai.edgeSubgraph

edgeSum def

The cost of a deterministic finite set of distinct undirected edges. · OAI.GammaFPP.edgeSum

edgeSupportGraph_copy_of_subset def

A selected edge subset of an embedded graph pulls back to an actual copy inside the original graph, using only incident vertices of the selection. · OAI.LeanBlast.SecondKahnKalai.edgeSupportGraph_copy_of_subset

EdgeTame def

Normal form with one radial segment at each endpoint. · OAI.HyperbolicObstruction.FinitePolyhedron.EdgeTame

EdgeTouches def

An edge is free in a block restriction when it touches the block. · OAI.Problem313.EdgeTouches

edgeTransport def

Two compatible pieces, rather than a chosen homotopy class of paths, suffice. · OAI.EilenbergGanea.AffineTransport.edgeTransport

EdgeTrim structure

Truncate one actual drawn edge outside disjoint small vertex disks. The middle arc stays outside every disk, with equality only at its own ends. · OAI.PlanarL1.Topology.Drawing.EdgeTrim

EdgeTuple def

An ordered tuple of distinct members of a finite edge family. · OAI.TalagrandDiscreteConvexity.Covering.EdgeTuple

edgeValue def

The signed displacement of an oriented original edge, with the two tree edges already killed in the actual presentation. · OAI.Release075.BlockPresentation.edgeValue

edgeWeight def

Nonnegative symmetric length on the subdivision; spokes cost zero. · OAI.TorsionFreeZeroDivisors.WeightedPortMoore.edgeWeight

Edit structure

Structural facts of the source short-roster expected parameter at an insertion; its explicit finite-law construction is separate from this local analytic gain. These are ramp/retirement facts, not a pilot gain premise. · OAI.UniformKServer.TierPilot.Edit

edit def

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

edit def

The signed editing charge, evaluated after filtering and drift but before the final minimizing update. Preparation payments are allowed to lower it. · OAI.KServer.AdaptiveMinimization.edit

EditScript inductive

An edit script with no restriction on intermediate word lengths. · OAI.TreeEdit.EditScript

EditScript inductive

A script of precisely n edits. There is no restriction on its intermediate lengths. · OAI.TreeEdit.EditScript

EditStep inductive

A single unit-cost insertion, deletion, or substitution at any position. · OAI.TreeEdit.EditStep

EditStep inductive

A single unit-cost insertion, deletion or substitution, at any position. · OAI.TreeEdit.EditStep

EdmondsKarp1972Theorem1 def

The shortest-augmenting-path bound for integral skew flows. Every finite initial segment has at most n³ augmentations, independently of the rule used to break ties between shortest paths. · OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1

effective def

effective test space on endpoint i. · OAI.HadwigerCounterexample.effective

effectiveBracket def

The defect of horizontal integrability is vertical and is absorbed by T. · OAI.KervaireIncidenceCurrent.effectiveBracket

EffectiveCouplingBound def

External fields do not increase the two-terminal effective coupling. · OAI.BufferedIsing.EffectiveCouplingBound

effectiveForm def

First-order low compression together with its second-order inverse term. · OAI.ContinuumCoulomb.Perturbation.effectiveForm

EffectivePlaneCurve def

Nonzero finite cycles of homogeneous prime plane ideals, with natural weights. · OAI.Nagata.Workers.W10.EffectivePlaneCurve

EffectivePlaneCurve def

A nonzero finite effective cycle of genuine homogeneous prime principal ideals in C[X0,X1,X2]. The weights retain repeated components. · OAI.Nagata.Workers.W10.EffectivePlaneCurve

effectiveSource def

The true source after moving the drift derivatives off the heat kernel. · OAI.ForcedComputation.PlaneScalarMild.CompatibleData.effectiveSource

effectiveSourceValue def

The common scalar effective source. · OAI.ForcedComputation.PlaneScalarMild.CompatibleData.effectiveSourceValue

Efine structure

Final matrix port operations, including paired information for echoes. · OAI.ExactDerandomization.SiteX.Line.Fabric.Efine

eigenSpace def

The true eigenspace, including the operator-domain condition. · OAI.SharpLiebThirring.OperatorProof.eigenSpace

eigenspace def

All vectors on which the central subgroup acts by the selected character. · OAI.LittleFinitistic.CharacterModule.eigenspace

eigenvalue def

The source eigenvalue, with its exact pinned normalization. · OAI.HarmonicCounterexample.Certificate.eigenvalue

eigenvalue def

The eigenvalue is the empirical bias of the generator characters. · OAI.MaxCutGames.Foundations.PCP.CayleySpectral.eigenvalue

eigenvalue def

The spherical Laplace eigenvalues. · OAI.PettyProjection.Spherical.eigenvalue

eigenvalue def

Eigenvalue of the inverse-distance Hessian at a unit coordinate vector. · OAI.Problem356.LocalHessian.eigenvalue

eigenvalue def

The eigenvalue is the empirical bias of the generator characters. · OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.eigenvalue

eigenvalueMoment def

The entire negative eigenvalue moment, with multiplicity, of an actual partially defined operator. Energies here are the eigenvalues e, not scales. · OAI.SharpLiebThirring.OperatorProof.eigenvalueMoment

eigenvalueSum def

The extended sum over every negative eigenvalue, repeated once for each member of a full Hilbert basis of its eigenspace. This is a literal spectral sum with multiplicities; no enumeration and no finiteness assumption is made. · OAI.SharpLiebThirring.OperatorProof.eigenvalueSum

eigenvector def

Both signs use the same three nonzero first coordinates. · OAI.DistinctLifts.eigenvector

eightLeafCounts def

Four children, each split into its two consecutive leaf parts. · OAI.LowSpaceSubsetSum.eightLeafCounts

ein abbrev

Constant scalar polymer. fourth powers of rising · OAI.ExactDerandomization.Arena.Song.ein

einsteinCurvatureTensor def

Ric=3g removes the off-diagonal curvature blocks. · OAI.PositiveEinsteinFour.Angular.einsteinCurvatureTensor

eisensteinNormPolynomial def

Finite polynomial before collecting the equal rational norms. · OAI.CubicFirstMoment.eisensteinNormPolynomial

ek def

Polynomial coefficient D as in angle_est. · OAI.GeneralMahler.ek

EKLPrimeInput def

The published rigidity input, on the actual lattice space and with actual diagonal ergodicity and measure-theoretic entropy. · OAI.DukePrimeDegree.EKLPrimeInput

elasticityTensor def

The isotropic elasticity tensor in fixed (orthonormal) coordinates. · OAI.ElasticityBoundaryLayerOperator.elasticityTensor

Elementary def

Elementary smooth homotopy; equalities only concern the unitary domain. · OAI.KervaireUnitaryHomotopy.Elementary

elementary def

Elementary matrices over an arbitrary, possibly noncommutative, ring. · OAI.FiniteAlgebraicEnvelopes.Steinberg.elementary

elementary def

The subgroup generated by the elementary integer matrices. · OAI.NuclearUltrapower.SOS.elementary

ElementaryAmenableFinitenessInput def

The precise finiteness/solvability consequence of Kropholler–Martínez-Pérez– Nucinkis used in the manuscript. This does not assert polycyclicity. · OAI.PolycyclicRecognition.ElementaryAmenableFinitenessInput

elementaryAuxiliary def

One Fourier factor, labelled s, multiplied by the inverse character of the same auxiliary column used by all factors. · OAI.MUB6.elementaryAuxiliary

elementaryBoundary def

Full boundary certificate for the actual elementary two-cells. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryBoundary

elementaryComparison def

The original presentation maps to the elementary edge-bouquet group. No fundamental-group equivalence, asphericity, or infinitude is assumed here. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryComparison

ElementaryCreationFormulas structure

Elementary multiplication on two opposite reduced-word subspaces. This record carries no normalization or complete-prefix assumption. · OAI.KadisonSimilarity.ElementaryCreationFormulas

elementaryDecodePicture def

Decode only the edge alphabet. Every cell, side, face and coefficient is unchanged. The geometric incidence conditions follow from the actual target. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryDecodePicture

elementaryEncodedBoundary def

Same individual cells and deck coordinates as elementaryLetterLiftedBoundary, encoded using signed positive lifted edges rather than shifted dart reversal. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryEncodedBoundary

elementaryFiniteComplex def

Literal conversion into the finite complex type. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryFiniteComplex

elementaryFreeComparison def

Inclusion of original letters in the literal elementary edge bouquet. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryFreeComparison

elementaryGauge def

The gauge at a top apex is based at the fixed macro root. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryGauge

elementaryHigherCoverEquiv def

This is the literal cover already proved simply connected, not an abstract cover named in a premise. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryHigherCoverEquiv

elementaryLetterLiftedBoundary def

The actual original quotient supplies every triangle and frozen-cell lift; no relator equations or nonvacuity properties are added as hypotheses. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryLetterLiftedBoundary

elementaryLiftedBoundary def

Literal elementary boundary incidence in the voltage cover, at every deck translate, including the wraparound side. No covering-space or CW-realization assertion is made by this finite incidence construction. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryLiftedBoundary

elementaryMacroPicture def

A constructed macro picture, not an extra producer hypothesis. Exact coordinate equality and frozen indexing are proved separately below. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryMacroPicture

elementaryOffset def

Deck offset from the specified basepoint of each literal elementary cell. For a triangle, that basepoint is its top apex; for a frozen cell it is the initial vertex of the fixed boundary indexing. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryOffset

elementaryOldRoutes def

Only literal radial edges are chosen as old-vertex routes. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryOldRoutes

ElementaryPolygonGroup abbrev

The literal edge-bouquet presentation of the elementary cells. · OAI.HyperbolicObstruction.ConeSkeleton.ElementaryPolygonGroup

elementaryPositiveVoltage def

Positive voltages of the genuine elementary indexed edges. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryPositiveVoltage

elementaryPositivityWitness def

The elementary-positivity part of the Shareshian–Wachs conjecture asks whether the chromatic quasisymmetric function of every natural unit interval graph has nonnegative coefficients in the elementary basis. The formalization proves this … · OAI.elementaryPositivityWitness

elementaryRawTarget def

Raw cellular target: coefficients always identify actual lifted elementary cells; the boolean used here only disables unrelated normalization machinery. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryRawTarget

elementaryTopologyEquiv def

The actual letter group equals the actual topological pi1-op of the finite literal elementary polygon realization. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryTopologyEquiv

elementaryTriangle def

The three literal sides of a top cone triangle, including its two new radial edges; arbitrary repeated OLD endpoints remain allowed. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryTriangle

ElementaryVertex abbrev

The actual pre-compression finite incidence data: old fan apices, separate top apices, every labelled radial edge, and elementary triangles. This data is not claimed to be a constructed topological CW space. · OAI.HyperbolicObstruction.ConeSkeleton.ElementaryVertex

elementaryVoltage def

Extension to the actual top radial edges. Deck coordinates of a top lift are measured at its apex, so all of its elementary triangles have the same apex coordinate used by LiftedCellularChain. · OAI.HyperbolicObstruction.ConeSkeleton.elementaryVoltage

Eligible def

The class assertion descends to the actual local name quotient. · OAI.PartitionConsistency.ProductForcing.Eligible

Eligible def

The actual eligibility test in : both unrestricted closed radius-five balls, with one common identifier in each of the two systems. · OAI.PlanarL1.Columns.Model.VertexTests.Eligible

eligible def

Internal stacks are freshest-first. The source's surviving-burger list is Evaluation.burgers.reverse, so source chronology is unchanged. · OAI.FKCRT.Inventory.eligible

EligibleClasses def

D_F(r), before restricting diagrams to lie below a fixed supporting root. Its only membership test is the forcing assertion that a name is a class of some element of A. · OAI.PartitionConsistency.ProductForcing.EligibleClasses

eligibleLabel def

Every label in the range has its canonical eligible class name. · OAI.PartitionConsistency.ProductForcing.eligibleLabel

EligibleName def

Actual forcing eligibility, not the existence of a preselected class representative or a coding witness. · OAI.PartitionConsistency.ProductForcing.EligibleName

eligibleOptionFullLabel def

The word itself is the pattern. Distinct realizing parameters do not give distinct eligible objects. · OAI.QuantitativeVanDerWaerden.AnchoredPatterns.eligibleOptionFullLabel

eligiblePairs def

Actual step/word pairs, rather than a family of realizing parameters. · OAI.QuantitativeVanDerWaerden.AnchoredPatterns.eligiblePairs

eligibleSystem def

The actual symbolic class system below q. Outside the cone below q the object type is empty, so no meaningless eligibility assertions are needed. All maps retain representative names and all axioms are proved. · OAI.PartitionConsistency.ProductForcing.eligibleSystem

eligibleSystemTransport def

The source and target here are the actual systems of eligible classes. Transport of the filter, names and diagrams supplies every axiom of the reindexing isomorphism. Since the permutation fixes q, it fixes E literally. · OAI.PartitionConsistency.ProductForcing.eligibleSystemTransport

eligibleTransportEquiv def

Transport of actual eligible classes, without assumptions that an arbitrary model is generic or that E's quotient has chosen representatives. · OAI.PartitionConsistency.ProductForcing.eligibleTransportEquiv

eliminateHom def

Set the transformed variable u equal to -J and retain all other variables. · OAI.StableCoordinate.Presentation.eliminateHom

eliminateQuotientEquiv def

The shifted hypersurface is a five-variable polynomial ring, with p as its first coordinate. This is the explicit final variable elimination. · OAI.StableCoordinate.Stabilization.eliminateQuotientEquiv

eliminationRootHomeomorph def

One Gaussian coordinate, restricted to the already eliminated entries and nonzero pivots. The new transverse slice records the next zero and pivot exactly. · OAI.DukePrimeDegree.eliminationRootHomeomorph

ell def

The source logarithm is binary. Levels here are numbered i+1. · OAI.SmoothObstruction.WordParameters.ell

ELMVConstantSequenceCriterion def

The constant-sequence specialization of the published two-sided tube criterion. The application must use the source's actual flow and tubes. · OAI.DukePrimeDegree.ELMVConstantSequenceCriterion

emb def

The canonical embedding of the old variables into a stronger condition. · OAI.PartitionConsistency.Completeness.Condition.emb

embed def

Inclusion of each D/X tensor into the actual A bar term. · OAI.DerivedBar.Multibar.embed

embed def

Pad a finite conditional law along an injection with a specified retraction. Off-support children are harmless but are specified, rather than postulated. · OAI.DilutedSpinGlass.KernelTower.embed

embed def

The fresh handoff is one state, not two copies joined by an artificial edge. · OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.embed

embed def

The canonical inclusion of L(E/W,C') into L(E,C). · OAI.MaxCutGames.Fourier.MatrixRestrictions.embed

embed def

The inclusion into the usual complex plane, with no continuity assertion needed on its discrete domain. · OAI.PlaneFiveColor.Spectral.embed

embed def

The larger-dimensional label used for a fixed-minimum type. · OAI.Problem326.Affine.Label.embed

embed def

The original t indeterminate embeds into the fresh Laurent indeterminate. · OAI.RationalHitting.TestPolynomial.embed

embed def

Choose the left or right inclusion of a globe basis. · OAI.Thomason.Construction.PastingGlobeBasis.embed

embed def

Normalize the source of a later globe to the preceding target. · OAI.Thomason.Construction.TripleGlobeBasis.embed

embed def

The physical embedding at mesh delta. · OAI.TriangularSurface.Lattice.embed

embed def

The canonical inclusion of L(E/W,C') into L(E,C). · OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.embed

embedApp def

Extend a basis inclusion linearly. · OAI.Thomason.Construction.PastingGlobeBasis.embedApp

embedCoordinates def

Extend coordinates along an injection, using the constant baseline on its complement. · OAI.Problem326.Affine.embedCoordinates

embeddedCall def

A call on an ordered tuple of distinct coordinates; all other values are fixed. · OAI.ExactFourier.embeddedCall

embeddedConfiguration def

Composition with a supplied genuine injective projective map. · OAI.Nagata.W06.TorusConfiguration.embeddedConfiguration

embeddedConfigurationForR def

For every r≥9 the literal choice q=r−9 gives an actual r-tuple. · OAI.Nagata.W06.TorusConfiguration.embeddedConfigurationForR

embeddedConfigurationOfEq def

The source equality r=9+q is retained exactly, with no unused or repeated points. · OAI.Nagata.W06.TorusConfiguration.embeddedConfigurationOfEq

embeddedConj def

Restrict ambient conjugation to an embedded subgroup, without assuming that conjugation preserves the larger group into which that subgroup embeds. · OAI.FiniteLattice.RetainedCore.embeddedConj

embeddedExecution def

The checked disjoint-stack embedding transports a complete successful run with no additional transitions, including its final jump to a bridge label. · OAI.MaxCutGames.Foundations.Complexity.MachineComposition.embeddedExecution

embeddedExecution def

The checked disjoint-stack embedding transports a complete successful run with no additional transitions, including its final jump to a bridge label. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.embeddedExecution

embeddedLookupInTime def

An optional disjoint-stack placement preserves arbitrary extra tapes and state. It reuses the same generic lookup and introduces no extra transitions. · OAI.MaxCutGames.Reduction.SourceEquationLookup.embeddedLookupInTime

embeddedLookupInTime def

An optional disjoint-stack placement preserves arbitrary extra tapes and state. It reuses the same generic lookup and introduces no extra transitions. · OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.embeddedLookupInTime

embeddedMatrixStage def

The stage of a nested embedded matrix algebra. · OAI.KadisonSimilarity.embeddedMatrixStage

embeddedMatrixUnit def

The image of an ordinary matrix unit in the ambient C-star algebra. · OAI.KadisonSimilarity.embeddedMatrixUnit

embeddedWordMatrixActions def

The action record for the invariant classification, obtained from actual representations and the two raw word inclusion formulas alone. · OAI.KadisonSimilarity.embeddedWordMatrixActions

Embedding structure

A legal mode-preserving change of names. No hypotheses about convertibility or proof existence are packed into the map. · OAI.PureTypeSystem.Labelled.Embedding

Embedding structure

An injective realization in a fixed sampled matching. These are actual maps on vertices and ports; no random-event bound is part of the data. · OAI.TorsionFreeZeroDivisors.RealizationTransport.Embedding

embedding def

The perturbation inclusion is itself a binary linear map. · OAI.MaxCutGames.Fourier.MatrixRestrictions.embedding

embedding def

The literal realization of this prescribed-side active stage follows from an actual embedding of the original prescribed side. All labels stay the restrictions of ONE global word. · OAI.TorsionFreeZeroDivisors.ActualSideRealization.embedding

embedding def

An actual sampled graph embedding yields the exact stage realization counted by the conditional-matching first moment. · OAI.TorsionFreeZeroDivisors.ActualStageRealization.embedding

embedding def

Restrict a realized prescribed side to an injectively immersed subgraph whose target vertices really lie on that side. · OAI.TorsionFreeZeroDivisors.SideRestriction.embedding

embedding def

Actual embeddings restrict to the used image, with the exact side/root pin. · OAI.TorsionFreeZeroDivisors.SupportedImage.embedding

embedding def

The perturbation inclusion is itself a binary linear map. · OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.embedding

EmbeddingBound def

The distortion convention, including its arbitrary positive scale. · OAI.ForestSpace.Diamond.EmbeddingBound

EmbeddingOrder abbrev

An ordering of all embeddings; total reality makes their values real. · OAI.DukePrimeDegree.EmbeddingOrder

embeddingRelativeChainsIso def

The inverse-image pair of an embedding is the actual intersection pair in its image, including its inherited subspace topology. · OAI.Kaplansky.embeddingRelativeChainsIso

embeddingSheet def

A sheet is the actual embedding on its domain; the arbitrary outside value is zero. · OAI.DoublingHilbert.embeddingSheet

embedLast def

The injection chosen by the last block, keeping the first two blocks fixed. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.embedLast

embedLast def

The injection chosen by the last block, keeping the first two blocks fixed. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.embedLast

embedPosition def

Positions and trials embed in the unchanged original arrays. · OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.embedPosition

Embeds def

Isometric inclusion as a subrepresentation: no quotients of representations. · OAI.NuclearUltrapower.FiniteUnitaryRep.Embeds

Embeds def

A compositional (not oracle) embedding of all source control locations. · OAI.WLIdentification.StackModel.Command.Embeds

EmbedsInFinitelyPresentedSimpleGroup def

The nontriviality in IsSimpleGroup is part of Mathlib's definition. · OAI.FiniteAlgebraicEnvelopes.EmbedsInFinitelyPresentedSimpleGroup

emission def

Every entry is a fixed finite output word, indexed by the fixed control state. · OAI.UniqueGamesTheorem.MachineTranslationTable.emission

emissionAssignmentEquiv def

Actual arrays and slot observations are bijective, not a lossy interface. · OAI.TraceReconstruction.emissionAssignmentEquiv

EmissionSlot abbrev

Each paired mechanism owns two distinct side slots; fillers and old leaf oracles have their own IDs. This type is independent of every orientation. · OAI.TraceReconstruction.EmissionSlot

emit def

Emit independent scalar operations, one cost unit per coordinate, with original operands still available after the whole layer. · OAI.ExactFourier.Program.emit

emit def

Exactly the cleanup letter prescribed in the finite compiler. Output marks on nonanchors are deliberately ignored even on dirty configurations. · OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.emit

emit def

All top and background validity checks are redundant on the intended layout, but keep the subset-witness invariant explicit on arbitrary data. · OAI.LowSpaceSubsetSum.RepresentationParentData.emit

emit def

A residue-indexed literal instruction; its length is bounded by d+b. · OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.emit

emit def

Two fixed exits, each containing only literal push instructions. · OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.emit

emit def

A residue-indexed literal instruction; its length is bounded by d+b. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.emit

emit def

Two fixed exits, each containing only literal push instructions. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.emit

emitDescriptor def

Concrete finite-table statement. Its state is the finite signature/tape pair; every branch leaf contains a fixed finite push chain. · OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.emitDescriptor

emitDescriptor def

Concrete finite-table statement. Its state is the finite signature/tape pair; every branch leaf contains a fixed finite push chain. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.emitDescriptor

emitDescriptorInTime def

One actual TM2 transition emits the descriptor and enters the chosen continuation label. Only a program-definition equation is required. · OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.emitDescriptorInTime

emitDescriptorInTime def

One actual TM2 transition emits the descriptor and enters the chosen continuation label. Only a program-definition equation is required. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.emitDescriptorInTime

emitInTime def

Execute the complete fixed row emission plan against physical unary tapes. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.emitInTime

emitInTime def

One actual transition emits the table entry and enters the continuation. The caller supplies its program equation, not an execution assumption. · OAI.MaxCutGames.Foundations.Complexity.MachineFiniteTable.emitInTime

emitInTime def

Execute the actual emitted row block through the finite register equivalence. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.emitInTime

emitInTime def

Execute the complete fixed row emission plan against physical unary tapes. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.emitInTime

emitInTime def

One actual transition emits the table entry and enters the continuation. The caller supplies its program equation, not an execution assumption. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteTable.emitInTime

emitInTime def

Execute the actual emitted row block through the finite register equivalence. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.emitInTime

emitLow def

Emits one least-significant bit, supplying zero for an exhausted operand. · OAI.RationalHitting.StackLanguage.emitLow

Emits def

Existence of a charged, clean, finite-alphabet stack procedure. · OAI.ExactQuantumFactoring.BitStackProgram.Emits

emitStatement def

The fixed literal push chain executes in one TM2 transition. · OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.emitStatement

emitStatement def

The fixed literal push chain executes in one TM2 transition. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.emitStatement

emitSteps def

One scaled scan/restore, one bounded offset, the delimiter, and final jump. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.emitSteps

emitSteps def

One scaled scan/restore, one bounded offset, the delimiter, and final jump. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.emitSteps

emittedMarkExpectation def

Every emitted mark is counted, including the empty primitive output. · OAI.TraceReconstruction.emittedMarkExpectation

emittedWord def

Every tape except the accumulator is literally retained. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.emittedWord

emittedWord def

Every tape except the accumulator is literally retained. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.emittedWord

emitter def

Each emitter is a fixed finite statement indexed by one of the d residues. · OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.emitter

emitter def

Each emitter is a fixed finite statement indexed by one of the d residues. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.emitter

emitterWithFinish def

A fixed table on finite ambient control may retain the residue before local reset. · OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinish

emitterWithFinish def

A fixed table on finite ambient control may retain the residue before local reset. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.emitterWithFinish

empirical def

Empirical law of the replica pattern at a uniformly sampled site. · OAI.DilutedSpinGlass.Pattern.empirical

empirical def

Empirical probability vector formed from a single group. · OAI.SmoothObstruction.WordLaw.empirical

empiricalCount def

Ordinary counting on the paper's interval 2 ≤ n ≤ N. · OAI.JointDickman.empiricalCount

empiricalDensity def

Ordinary, unweighted density normalized by the counting endpoint. · OAI.JointDickman.empiricalDensity

empiricalVector def

Empirical-site amplitudes. Their exact squared norm is one when there is at least one slot. Zero-count letters are allowed and have zero amplitude. · OAI.CoordinateSweeps.OrdinaryTensor.empiricalVector

empty def

No faces are required to fill the empty word. · OAI.HyperbolicObstruction.WordPictures.WordPicture.empty

empty def

a = ∅. · OAI.PartitionConsistency.SetLanguage.empty

empty def

Start with the empty chronological history. · OAI.ReflexiveFixedPoints.HistoryState.empty

empty_interval_wedge def

The two graph pieces retain every edge, including both matching colours. This is the actual all-edge graph at an arbitrary insertion interval. · OAI.FKCRT.Inventory.StackMatching.empty_interval_wedge

empty_prefix_wedge def

A genuine successful inserted interval of the actual typed matching creates a one-vertex union for the full, all-edge map graph. The local graph metric conclusions now follow unconditionally from GraphWedge.Data. · OAI.FKCRT.Inventory.StackMatching.empty_prefix_wedge

emptyBack def

Empty fibres have the unique map into the categorified cosieve. · OAI.Thomason.Construction.CosieveSimplex.emptyBack

emptyBack def

Empty fibres have the unique map into the categorified sieve. · OAI.Thomason.Construction.SieveSimplex.emptyBack

emptyEndpoint def

The first endpoint with no centered tail letters. · OAI.KadisonSimilarity.emptyEndpoint

emptyFormulaEquation def

A satisfiable totalization for the empty input formula, without changing or diluting the occurrence list of a nonempty formula. · OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation

emptyFormulaEquation def

A satisfiable totalization for the empty input formula, without changing or diluting the occurrence list of a nonempty formula. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation

emptyMetricPolynomial def

The exact-correction stage has no polynomial perturbation. · OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.emptyMetricPolynomial

emptyTable def

An empty cloud has a total, vacuous rotation table. · OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.emptyTable

emptyTable def

An empty cloud has a total, vacuous rotation table. · OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.emptyTable

EnclosesPolynomial def

An enclosure for every coefficient, with exact zero beyond the list. · OAI.DefocusingNLS.GaussianEnclosure.EnclosesPolynomial

EnclosingLoop abbrev

Length n+1 avoids a spurious zero-length contour in the countable union. · OAI.PlanarFPP.EnclosingLoop

encode def

The encoding writes `n`, the number `p` of endpoint pairs, and `k`, followed by each pair's endpoints and multiplicity. · OAI.AlgorithmicThinTrees.BinaryInput.encode

encode def

The encoding concatenates framed natural numbers for `n`, `m`, and `k`, then for every edge index concatenates its two endpoint indices. · OAI.AlgorithmicThinTrees.ExplicitInput.encode

encode def

`Input.encode` prefixes `false` for an explicit input and `true` for a binary-multiplicity input, then appends that branch's encoding. · OAI.AlgorithmicThinTrees.Input.encode

encode def

K n-bit words in consecutive little-endian fields, followed by one zero word. This fits exactly the source's W=n(K+1) output cap. · OAI.ExactQuantumFactoring.TransitionWords.encode

encode def

Encoding the shifted reversal of a voltage cover as a true signed edge. The negative generator is based at the initial point of its positive reverse. · OAI.HyperbolicObstruction.VoltageWords.encode

encode def

The encoder keeps the actual earlier pair and actual earlier map. · OAI.MaxCutGames.Appendix.A5ForwardIndex.encode

encode def

The initial letter and switch set encode a nonempty word. · OAI.Problem335.WordSwitches.encode

encode def

The actual concatenation ordinal, with its bound proved from the sum. · OAI.ReflexiveFixedPoints.OrderedGroupConcat.encode

encode def

Explicit encoding of all source pattern data after suppression. The graph and path carriers can be arbitrary finite types: their old vertex names do not survive. Empty padding is not counted as an actual chain or path. · OAI.TorsionFreeZeroDivisors.PatternCoding.encode

encode def

The concatenation extension of a fixed-width symbol code, on all finite words. · OAI.TreeEdit.encode

encode def

The encoder keeps the actual earlier pair and actual earlier map. · OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.encode

encodedBit def

A bit of the actual concatenation, with its prescribed-length indexing. · OAI.TreeEdit.BinaryLower.Code.encodedBit

encodedBlockAt def

Only this instruction block is translated into the common state. · OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.encodedBlockAt

encodedBlockAt def

Only this instruction block is translated into the common state. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.encodedBlockAt

encodedMember def

The map from source membership witnesses into membership witnesses of the encoded finite set, with no choice of an inverse. · OAI.TreeEdit.BinaryLower.encodedMember

encodedSet def

The actual finite image, rather than an abstract copy of the source set. · OAI.TreeEdit.BinaryLower.encodedSet

encodedWord def

Canonical output's self-delimiting natural-number encoding, applied to an already canonical little-endian binary word. · OAI.RationalHitting.StackLanguage.encodedWord

encodedWord def

The concatenation extension, viewed in its exact-length target type. · OAI.TreeEdit.BinaryLower.encodedWord

encodeEdges def

Each output edge is encoded by its endpoint-pair index and its copy index within that pair's multiplicity. · OAI.AlgorithmicThinTrees.BinaryInput.encodeEdges

encodeEdges def

`encodeEdges` concatenates the framed natural-number value of every explicit edge index in the proposed output list. · OAI.AlgorithmicThinTrees.ExplicitInput.encodeEdges

encodeGraphs def

This is a full row-major adjacency matrix, not an adjacency oracle or a colored-graph promise. Both matrices and their common order appear on the tape. · OAI.ParityWL.Complexity.encodeGraphs

encodeHistory def

Only the label coordinates of a history are relabeled. · OAI.MatroidProphet.Labeling.encodeHistory

encodeHistory def

Reindex the labels of an observed history without changing any observed value. · OAI.MatroidProphet.Relabeling.encodeHistory

encodeInput def

Explicit sparse graph encoding, then the two rational parameters. · OAI.MatchingFPRAS.encodeInput

encodeInputs def

Encode each residue input using a truth table on its own selected bits. · OAI.TwoPointCorrelations.AC0Circuit.encodeInputs

encodeList def

Prefix markers encode the list spine, including its final boundary. · OAI.Superstring.encodeList

encodeMatrix def

Row-major entries; a matrix-record delimiter retains explicit list length also for order-zero matrices. This constant-per-matrix framing is polynomially equivalent to dense binary matrix listing in positive dimension. · OAI.CurrentKS.Input.encodeMatrix

encodeNat def

`encodeNat n` applies the file's self-delimiting `frame` to Mathlib's computability-oriented Boolean encoding of `n`. · OAI.CurrentKS.encodeNat

encodeNat def

Binary numeral followed by a delimiter. Tape blank is 0; bits use 1 and 2. · OAI.MatchingFPRAS.encodeNat

encodeNat def

Self-delimiting binary natural numbers, followed by the explicit formula. The clause width is encoded even for an empty clause. · OAI.ParityWL.Complexity.encodeNat

encodeNat def

Little-endian unsigned binary, prefixed by a unary bit-length and a zero terminator. This is a self-delimiting binary encoding, including zero. · OAI.RationalHitting.encodeNat

encodeNat def

Binary, not unary, representation of a natural number, with a length prefix. · OAI.UniformSparsestCut.encodeNat

encodeNet def

Each field is wired into its fixed source layout, and the final unused word is explicitly zeroed. The cap K and all placements are independent of inputs. · OAI.ExactQuantumFactoring.TransitionWords.encodeNet

encodeRat def

A rational encoded by its reduced numerator and positive denominator. · OAI.MatchingFPRAS.encodeRat

encodeRat def

Sign bit, binary numerator magnitude, and positive binary denominator. Rat.num and Rat.den are the canonical reduced numerator and denominator. · OAI.RationalHitting.encodeRat

encodeRat def

Signed numerator and positive denominator, both in binary. · OAI.UniformSparsestCut.encodeRat

encodeResidueCircuit def

The actual truth-table circuit used for encoded residue testing. · OAI.TwoPointCorrelations.encodeResidueCircuit

encodeSmallSet def

Canonical padded enumeration encodes a subset of size at most r in r optional entries. This supplies the source's (number-of-lines+1)^r union count. · OAI.CoordinateSweeps.Coverage.encodeSmallSet

encodeState def

Embed a logical finite state in concrete basis words, including clean work. · OAI.ExactQuantumFactoring.encodeState

encodeSymbol def

The encodings have the same two distinct endmarkers. · OAI.TwoWayComplementation.CompanionBridge.encodeSymbol

encodeUnary def

Unary electron counts use one true bit per electron and a false terminator. · OAI.ContinuumCoulomb.BinaryEncoding.encodeUnary

encodeWeights def

Reindex all weights, retaining every label including loops and zero weights. · OAI.MatroidProphet.Relabeling.encodeWeights

encodeWord def

`encodeWord n` is `n` copies of `true` followed by one `false`. · OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

encodeWords def

`encodeWords` maps each natural to `encodeWord` and joins the framed words in list order. · OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

Encoding structure

Concrete finite coefficient data, with an exact presentation equivalence. · OAI.LittleFinitistic.SelectionEncoding.Encoding

Encoding structure

A concrete, reversible finite encoding. Constructors below specify the actual arithmetic; no arbitrary Fintype.equivFin is used. · OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding

Encoding structure

A concrete, reversible finite encoding. Constructors below specify the actual arithmetic; no arbitrary Fintype.equivFin is used. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding

encoding def

Exactly the elementary symmetric functions of degrees 1,…,m. · OAI.EuclideanFiveColor.PhaseEncoding.encoding

encoding def

A concrete encoding for the fixed alphabet, suitable for the existing TM2 computation interface. · OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.encoding

encoding def

A concrete encoding suitable for the existing TM2 computation interface. · OAI.MaxCutGames.Foundations.PCP.GraphTables.encoding

encoding def

A genuine roundtripping encoding of the fixed-port executable input family. · OAI.MaxCutGames.Foundations.PCP.PortTables.encoding

encoding def

A concrete encoding for the fixed alphabet, suitable for the existing TM2 computation interface. · OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.encoding

encoding def

A concrete encoding suitable for the existing TM2 computation interface. · OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.encoding

encoding def

A genuine roundtripping encoding of the fixed-port executable input family. · OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.encoding

encounters def

Total number of shared switches along the distinct marked routes. · OAI.CubeShuffle.encounters

endName def

Thus all the actual comparison endpoints with a ≤H bound fit literally. · OAI.TorsionFreeZeroDivisors.PatternCoding.endName

endomorphismMatrix def

An actual intertwining endomorphism has its coefficient matrix in the signed commutant. This is not an assumed decomposition of the tensor action. · OAI.CoordinateSweeps.SignedTensor.endomorphismMatrix

endpoint def

The first integer whose scaled value can be at least β. · OAI.ContingencyTables.FairBits.endpoint

endpoint def

The two oriented endpoint maps of the transported cylinder. · OAI.Thomason.ConstructedInterval.endpoint

endpoint def

Both inclusions of K into its right chain cylinder are positive chain maps. · OAI.Thomason.Construction.DirectedComplex.RightCylinder.endpoint

endpoint def

The two endpoint restrictions of an arbitrary chain-cylinder map. · OAI.Thomason.Construction.DirectedComplex.RightPath.endpoint

endpoint def

Density extends the literal endpoint maps to every strict category. · OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.endpoint

endpoint def

The opposite end of the maximal chain, given as its outgoing port. · OAI.TorsionFreeZeroDivisors.ChainSuppression.endpoint

endpoint def

Terminal vertex of a literal path, including the empty path at z. · OAI.TorsionFreeZeroDivisors.ShortClosure.endpoint

endpointAmplification def

The actual operator I_E ⊗ A on completed endpoint tensors. · OAI.KadisonSimilarity.endpointAmplification

endpointAtom def

Endpoint tensor generators are also actual bounded positive cells. · OAI.Thomason.Construction.PastingGlobeBasis.endpointAtom

endpointBackward def

The past short segment of the true forward gauge, centered at its long endpoint. Rates are merely negated; the original starting threshold remains available, and no new stationary witness is chosen. · OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.endpointBackward

endpointCoefficient def

The coefficient in either endpoint copy. · OAI.Thomason.Construction.PastingGlobeCylinderBasis.endpointCoefficient

endpointCoincidence def

Equality of both normal coordinates at all indicated internal endpoints. · OAI.Problem335.Pairings.endpointCoincidence

endpointCompression def

Compress the endpoint of a bounded operator to the chosen trace vector. · OAI.KadisonSimilarity.endpointCompression

endpointData def

Keep the actual prescribed hole paths, recording their endpoints. · OAI.CoordinateSweeps.Grid.Holes.endpointData

endpointData def

The finite endpoint quotient supplies the full binary symmetric structure. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointData

endpointDegree def

The number of edge endpoints at a vertex, counting both ends of a loop. · OAI.Problem335.SwitchRestoration.endpointDegree

endpointEvent def

Endpoint events are equivalent to the unique additional trajectory's line assignments. No feasibility or injectivity is postulated. · OAI.CoordinateSweeps.Grid.endpointEvent

EndpointGap def

A rational coordinate gap between two filled rectangles. · OAI.ForcedComputation.PlanarRouting.EndpointGap

endpointHeadAction def

A bounded operator acting only on the unrestricted endpoint. · OAI.KadisonSimilarity.endpointHeadAction

endpointInsert def

Insert an endpoint in front of a completed tail vector. · OAI.KadisonSimilarity.endpointInsert

EndpointLetters abbrev

The pair of endpoint letters and all centered tail letters. · OAI.KadisonSimilarity.EndpointLetters

endpointMask def

An actual endpoint comparison; it has no reachability oracle input. · OAI.MaxCutGames.Foundations.PCP.PoweringRowData.endpointMask

endpointMask def

An actual endpoint comparison; it has no reachability oracle input. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.endpointMask

endpointMatching def

Add a fixed distinguished endpoint to a tail matching. · OAI.KadisonSimilarity.endpointMatching

endpointMatchingClassEquiv def

The endpoint supplies one additional singleton orbit. · OAI.KadisonSimilarity.endpointMatchingClassEquiv

endpointMatchingEquiv def

Surviving permutations are in bijection with tail matchings. · OAI.KadisonSimilarity.endpointMatchingEquiv

endpointMatrix def

Actual endpoint-coordinate matrix; columns are the represented starting vectors. Unlike the exterior-coordinate scalar formula, this uses the usual matrix convention (output row, input column). · OAI.SmoothObstruction.ExteriorStability.endpointMatrix

EndpointPairing def

The cycle structure remaining after the endpoint and centering estimates. · OAI.KadisonSimilarity.EndpointPairing

EndpointPath def

Vertex paths with both external endpoints fixed. · OAI.Problem335.EndpointPath

endpointPathEquiv def

Adjoining the two endpoints identifies arbitrary internal-vertex tuples with endpoint-fixed vertex paths. · OAI.Problem335.endpointPathEquiv

endpointPathIndexEquiv def

Representation bridge from endpoint-fixed vertices to canonical list-based paths. · OAI.Problem335.endpointPathIndexEquiv

EndpointPossible def

Very same endpoint feasibility event as the conditioned finite sample space. · OAI.CoordinateSweeps.Grid.Holes.EndpointPossible

EndpointQuotient abbrev

A finite presentation with a surjection to the concrete simple table group. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.EndpointQuotient

endpointRelations def

Explicit finite presentation candidate: structure, stabilizer, generator bindings, and one orbit representative of distinct-colour interchange. Its completeness is not built into this definition. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointRelations

endpointRunCount def

In a mixed word, the number of true runs touching an endpoint. · OAI.Problem335.WordRuns.endpointRunCount

Endpoints structure

These are the actual attained minima and maxima after the paper's integer bound-tightening step. They are feasible tables, not marginal mass or signature assumptions. · OAI.ContingencyTables.CompanionTerminalMass.Endpoints

endpoints def

The endpoint assumption in the terminal proof follows from the executed searches. The witnesses here are mathematical proof data. · OAI.ContingencyTables.ComputedCompanionInstance.endpoints

endpoints def

Flatten the pair endpoints without imposing an artificial pair order. · OAI.FKCRT.MapCycles.endpoints

endpointsInTime def

Read the two fields actually stored in a graph row: tail and reverse dart. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.endpointsInTime

endpointsInTime def

Read the two fields actually stored in a graph row: tail and reverse dart. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.endpointsInTime

EndpointStatement def

Exact endpoint, including finiteness before passing to the real representative. Quantifying the input gradient makes the norm bound independent of a choice of representative of its weak derivatives. · OAI.CenteredDiskEndpoint.EndpointStatement

EndpointStatement def

Exact endpoint, including finiteness before passing to the real representative. Quantifying the input gradient makes the norm bound independent of a choice of representative of its weak derivatives. · OAI.SignedDisk.CenteredDiskEndpoint.EndpointStatement

endpointTailMatching def

Remove the distinguished fixed endpoint from a surviving permutation. · OAI.KadisonSimilarity.endpointTailMatching

EndpointTensor abbrev

An unrestricted endpoint followed by a completed centered tail. · OAI.KadisonSimilarity.EndpointTensor

endpointTensorMap def

The completed tensor product of an endpoint map and a bounded tail operator. · OAI.KadisonSimilarity.endpointTensorMap

endpointWeight def

Uniform product weight on the full pair of endpoints, with replacement. · OAI.CoordinateSweeps.Grid.endpointWeight

endpointWitness def

The actual pivot dart is marked and both endpoint opinions pass their tests. For indicator opinions this is the indicator of their conjunction. · OAI.MaxCutGames.Foundations.PCP.PoweringWitness.endpointWitness

endpointWitness def

The actual pivot dart is marked and both endpoint opinions pass their tests. For indicator opinions this is the indicator of their conjunction. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWitness.endpointWitness

endpointWord def

The elementary word with an unrestricted first endpoint. · OAI.KadisonSimilarity.endpointWord

ends def

Two disjoint copies of a simplicial set, in each degree. · OAI.Thomason.Construction.SimplicialCylinder.ends

ends def

Endpoints of walks of exactly k steps. · OAI.TorsionFreeZeroDivisors.BallCount.ends

endsEquiv def

The open-end matching is produced, bijective, and retains every corner of every path. There are no concealed circular lower strips. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.endsEquiv

endSLMatrixHom def

Actual trace-free coordinate matrices in an arbitrary basis. · OAI.HarmonicCounterexample.Control.endSLMatrixHom

EndsWith def

A maximal occurrence of a trace, retaining its sign. · OAI.EilenbergGanea.TraceWords.EndsWith

energy def

The exact volume-one Bernoulli energy, not just Dirichlet energy. · OAI.Bernoulli.energy

energy def

Literal physical spin weight, with the independent physical root inputs kept as a recursive product only for the variance calculation. · OAI.DilutedSpinGlass.PhysicalRoot.energy

energy def

Energy of the actual merged derivative coefficients. · OAI.MaxCutGames.Appendix.WeightedFourthMoment.energy

energy def

Squared coefficient energy, averaged using the supplied question weights. · OAI.MaxCutGames.Fourier.MatrixEnergy.energy

energy def

Squared Hilbert norm, with the actual right-question marginal. · OAI.MaxCutGames.Repetition.ProjectionKernel.energy

energy def

The Dirichlet form, expressed without local coordinates by rotations. · OAI.PettyProjection.Spherical.energy

energy def

The energy metric of the three Bianchi parameters. · OAI.PositiveEinsteinFour.HessianAlgebra.energy

energy def

Energy of the actual merged derivative coefficients. · OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.energy

energy def

Squared coefficient energy, averaged using the supplied question weights. · OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.energy

energy def

Squared Hilbert norm, with the actual right-question marginal. · OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.energy

energyColor def

Native integer floor and Euclidean remainder, reindexed into Fin 50. · OAI.GrahamSpherical.energyColor

energyFormMap def

Form of H+a on H¹. · OAI.SharpLiebThirring.OperatorProof.energyFormMap

EnergyOrbit structure

Actual normalized orbit points along a symmetric finite generator list. · OAI.HyperbolicObstruction.EnergyOrbit

energyRadius def

The radius of the squared-speed interval appearing in the uniform sphere law. · OAI.BoltzmannNonuniqueness.ReferenceGeometry.energyRadius

energyRatio def

The prediction ratio with a fixed positive denominator. · OAI.LipschitzHilbert.energyRatio

energyWeight def

Squared modulus as a nonnegative measure density. · OAI.ThreeTorus.energyWeight

enlarge def

Whole-graph sets that contain most of the walk. · OAI.CliqueFreeIndependence.WeightedGraph.enlarge

enlargeBound def

The energy function and its full measure equation are unchanged. · OAI.RegularPointCoordinates.LocalHarmonicEnergy.enlargeBound

enlargedFunction def

The representation used in the whole-ball argument. · OAI.ExactModuli.KW.enlargedFunction

EnlargedLensExcluded def

Exact exclusion of infinite separated families in every enlarged unit-center lens, retaining the radius and separation as independent parameters. · OAI.DiamondDistortion.Diamond.EnlargedLensExcluded

enlargedOutput def

Sum of the injectively relabeled base outputs before quotienting. · OAI.MaxCutGames.Gadget.Enlargement.enlargedOutput

enlargedOutput def

Sum of the injectively relabeled base outputs before quotienting. · OAI.UniqueGamesTheorem.Gadget.Enlargement.enlargedOutput

enlargePolynomialBound def

Increasing a polynomial bound preserves the actual execution witness. · OAI.MaxCutGames.Foundations.Complexity.enlargePolynomialBound

enlargePolynomialBound def

Increasing a polynomial bound preserves the actual execution witness. · OAI.UniqueGamesTheorem.Foundations.Complexity.enlargePolynomialBound

Ensemble structure

All finite ensembles, without any product or purity restriction. · OAI.GAD.Ensemble

entrances def

The actual entrance midpoints of a radial high component. The adjacent low column, rather than a separate entrance-range hypothesis, is part of the definition. · OAI.PlanarL1.Columns.Model.Point.entrances

entries def

The twenty-one free coordinates after the actual tensor constraints. · OAI.PositiveEinsteinFour.HighestHessian.entries

entropy def

Weighted row entropy, with the 0 log 0 = 0 convention. · OAI.CliqueFreeIndependence.FiniteEntropy.entropy

entropy def

−Tr ρ log ρ, using the continuous extension of −t log t at zero and continuous functional calculus for the positive operator ρ. · OAI.EntropyPhotonNumber.entropy

entropy def

The spectral definition of -Tr(P log P), with 0 log 0 = 0. · OAI.GAD.entropy

entropyBound def

The summable majorant for the absolute entropy of one annulus. · OAI.BoltzmannNonuniqueness.DatumBounds.entropyBound

entropyBudget def

The scalar upper bound, with radius and pivot count fixed by a alone. · OAI.MetricEntropyDuality.entropyBudget

entropyFunctional def

Equation (1.6). Infinite suprema are retained as extended real values. · OAI.InvariantIsing.entropyFunctional

entropyLineD def

The explicit first derivative along a supported affine marginal path. · OAI.MatchingEntropy.entropyLineD

EntropyPair structure

A constructed body with its actual geometric and entropy properties. No matrix, compression theorem, or abstract entropy function is a field. · OAI.MetricEntropyDuality.EntropyPair

entropyProduction def

The entropy-production integrand for strictly positive incoming and outgoing products. · OAI.BoltzmannNonuniqueness.Published.entropyProduction

entropyRatio def

The actual quotient of dual covering entropy by primal covering entropy. · OAI.MetricEntropyDuality.entropyRatio

entropyRatioBound def

An asymptotic upper bound for the entropy ratio. · OAI.MetricEntropyDuality.entropyRatioBound

entropyTail def

The absolute-entropy scalar remainder after the first N annuli. · OAI.BoltzmannNonuniqueness.DatumBounds.entropyTail

entropyTerm def

Shannon entropy in bits; the value at mass zero is zero. · OAI.SmoothObstruction.entropyTerm

entropyValue def

Entropy plus the linear objective, with the manuscript's scaling. · OAI.EditApproximation.entropyValue

Entry def

Literal entry and successful exit tests, both finite data predicates. · OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Entry

Entry def

An entry has clean D immediately right of its I head. · OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Entry

Entry abbrev

Each table has a distinct type, but all its coordinate fields use the same alphabet. Coinciding numerical values at different fields are permitted. · OAI.HyperbolicObstruction.TableModel.Entry

Entry abbrev

Every transport and every chosen split frame has its own occurrence index. The sign distinguishes its matrix from its inverse, not a second occurrence. · OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Entry

Entry structure

A dictionary key retains the exact weight and the entire top-block mask. · OAI.LowSpaceSubsetSum.Entry

Entry structure

A finite independently sampled chronological family. Each coordinate can include a collapsed continuous radius law, so no count of random bits is claimed at this existence-only stage. · OAI.UniformKServer.FirstHit.Entry

entry def

Matrix entries of an operator in the number basis. · OAI.EntropyPhotonNumber.entry

entry def

The matrix entries associated to the explicit common-source legs. · OAI.Generator.Tracial.EquivalentPartition.entry

entry def

A single matrix entry with the C*-matrix norm. · OAI.Kaplansky.entry

entry def

The horizontal arrow map retains its left action and exact degree transport. · OAI.LittleFinitistic.BimoduleComplexTensor.entry

entry def

The actual horizontal matrix entry, zero unless the right degrees are consecutive. · OAI.LittleFinitistic.ComplexTensor.entry

entry def

The actual entry guard bypasses an empty positive-dimensional Cartesian product. Dimension zero always enters its one empty-tuple emitter. · OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.entry

entry def

The fixed signed-monomial integer formula for M times a regular lift entry. · OAI.RationalHitting.IntegralLift.entry

entry def

The actual entry guard bypasses an empty positive-dimensional Cartesian product. Dimension zero always enters its one empty-tuple emitter. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.entry

entryCLM def

Entry evaluation is a continuous linear functional even for the operator norm. · OAI.SharpLiebThirring.MatrixProof.entryCLM

entryCount def

Computed by the falling-factorial formula to avoid expanding Pascal's recursion at 10^60; entryCount_eq_choose proves the specified value. · OAI.PixtonChow.entryCount

entryExponent def

Analysis scale for distinct valid parent entries. · OAI.LowSpaceSubsetSum.entryExponent

entryFromParts def

The counting target has one key per top mask, background subset and local distinct weight, independent of the number of raw representations. · OAI.LowSpaceSubsetSum.RepresentationUniverse.entryFromParts

entryMatrixAlgebra def

The finite matrices whose entries belong to a specified star algebra. · OAI.KadisonKastler.entryMatrixAlgebra

entryMatrixHom def

Entrywise application of the original representation to ordinary matrices. · OAI.KadisonSimilarity.entryMatrixHom

entryPattern def

Every nonzero commuting matrix entry has literal valid exceptional data. · OAI.CoordinateSweeps.SignedTensor.entryPattern

entryVector def

The complete level coordinate, including zero. · OAI.DoublingHilbert.entryVector

entrywiseCStarMatrixEquiv def

An equivalence of coefficient algebras induces the entrywise matrix equivalence. · OAI.KadisonSimilarity.entrywiseCStarMatrixEquiv

enumerate def

Raw leaves retain the three subset choices, including repeated weights. · OAI.LowSpaceSubsetSum.RepresentationLeaf.enumerate

enumerate def

Computable increasing-code enumeration. No finite-choice oracle. · OAI.UniformKServer.EffectiveLP.enumerate

enumeratedGraph def

Explicit enumerations determine every vertex name, dart position, and predicate label. No hidden choice of a graph representation is made. · OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.enumeratedGraph

enumeratedGraph def

Explicit enumerations determine every vertex name, dart position, and predicate label. No hidden choice of a graph representation is made. · OAI.MaxCutGames.Foundations.PCP.GraphTables.enumeratedGraph

enumeratedGraph def

Explicit enumerations determine every vertex name, dart position, and predicate label. No hidden choice of a graph representation is made. · OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.enumeratedGraph

enumeratedGraph def

Explicit enumerations determine every vertex name, dart position, and predicate label. No hidden choice of a graph representation is made. · OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.enumeratedGraph

enumeratedProjectionFrame def

Ascending enumeration of the nonzero projected frame, with a harmless library default outside its genuine index range. · OAI.KadisonKastler.enumeratedProjectionFrame

enumeratedSpectralDegree def

First m coordinates are spectral degrees; the final coordinate is the tree degree. The constant kernel can be retained harmlessly. · OAI.InvariantIsing.enumeratedSpectralDegree

enumerateRetainedPassage def

Enumerating the concrete rational/compact indices gives the natural indexing expected by finite-retention and unconditional sausage lemmas. · OAI.SLEExactGauge.PassageRetention.enumerateRetainedPassage

enumeration def

Indexed boundary order: all old circles remain in their old order, the single mirror circle is appended at the selected parent, and every newly created strip disk has exactly one boundary. · OAI.IntegralCharacterVarieties.CutCircleIndex.enumeration

enumeration def

Every side occurrence appears once, even in self-incidence cycles. · OAI.IntegralCharacterVarieties.FiniteCycles.enumeration

enumeration def

The enumeration of the prescribed root subfield is in inherited coefficient order. · OAI.KaplanskyCounterexample.Prescription.enumeration

enumeration def

The executable equivalence consumed by Finish and DrainMany. · OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.enumeration

enumeration def

Exact color-fibre enumeration, identifying the literal path traversals with the multiplicity-indexed traversal type used in every stage estimate. · OAI.TorsionFreeZeroDivisors.ChunkComparisons.enumeration

enumeration def

The executable equivalence consumed by Finish and DrainMany. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.enumeration

enumerationIso def

Transport only the finite indexing type; every degree and both signed maps are unchanged. · OAI.LittleFinitistic.BimoduleTotalPresentation.enumerationIso

enumList abbrev

A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.) · OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Control.enumList

enumList abbrev

A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.) · OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList

enumList abbrev

A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.) · OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.Label.enumList

enumList abbrev

A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.) · OAI.PerfectCompleteness.TargetHeaderMachine.Label.enumList

enumList abbrev

A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.) · OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Label.enumList

enumList abbrev

A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.) · OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.Tape.enumList

enumList abbrev

A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.) · OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.Clock.enumList

enumList abbrev

A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.) · OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadPresenceMachine.CopyContext.enumList

enumList abbrev

A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.) · OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.Extra.enumList

Env abbrev

Canonical roles: X,Y,Z, then raw (unreduced) salt bits. · OAI.ExactDerandomization.Analysis.Env

envelope def

The literal capped frontier extension; the empty frontier contributes +infinity before taking the minimum, so the finite result is the cap. · OAI.PlanarL1.Clipping.envelope

envelope def

A capped geometric envelope with the integer frequencies accounted for explicitly, rather than assigning an invalid reciprocal at distance zero. · OAI.Problem337.RealPhase.envelope

envelope def

A compact set produces one compact envelope on the reference plane. · OAI.Problem358.MovingPlaneEnvelope.envelope

envelope def

The signed envelope over the entire compact real-radius interval. · OAI.RadiusEnvelope.envelope

envelope def

The signed envelope over the entire compact real-radius interval. · OAI.SignedDisk.RadiusEnvelope.envelope

envelope def

A single, choice-independent numerical envelope for all the relative exterior errors at a given dyadic scale. · OAI.SmoothObstruction.RelativeAsymptotics.envelope

envelope def

Actual unsigned coefficient envelope on one ordered occupied shape. No bits are resampled for the additional leaves. · OAI.TraceReconstruction.OccupiedParityTree.Forced.envelope

envelopeCore def

A slower Gaussian, used to dominate bounded translations of the heat kernel. · OAI.ForcedComputation.PlaneHeat.envelopeCore

envelopingDerivation def

The unique associative derivation extending the given Lie derivation. · OAI.PolycyclicRecognition.envelopingDerivation

envelopingDerivationRepresentation def

Derivations act on the enveloping algebra by a Lie representation. · OAI.PolycyclicRecognition.envelopingDerivationRepresentation

Environment structure

Typed raw substitutions with precisely one observation parameter per active actual declaration and none at inactive declarations. · OAI.PureTypeSystem.ObservationValues.Environment

epoch def

Epoch labels record the actual wholesale test. · OAI.KServer.AllocationSchedule.epoch

epochTrace def

Exact finite product of the fresh bits assigned to the deterministic kept word. Extra shadow bits after a switch are analytical only. · OAI.UniformKServer.EpochExpectation.epochTrace

epsilon def

The error threshold is fixed using only the universal weight constants. · OAI.TorsionFreeZeroDivisors.StageFusion.epsilon

EqG def

Equality of codes after adjoining the generic filter. · OAI.PartitionConsistency.ForcingQuotient.AtomicData.EqG

EqRel def

Equality and membership of constant codes in the canonical term model. · OAI.PartitionConsistency.Completeness.EqRel

Equal structure

Equality of path classes together with equality of both endpoint labels. · OAI.GroupRingTopology.PathExtension.Q.Equal

equality def

Equality is the least congruence. · OAI.FiniteCongruence.Congruence.equality

equalityAcceptance def

The actual equality test, including zero perturbation factors. · OAI.MaxCutGames.Decoder.PositiveMultiplier.equalityAcceptance

equalityAcceptance def

Both perturbation factors are independent uniform vectors, including zero. The matrix is sampled independently as well. · OAI.MaxCutGames.Inverse.Shortcode.equalityAcceptance

equalityAcceptance def

The actual equality test, including zero perturbation factors. · OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.equalityAcceptance

equalityAcceptance def

Both perturbation factors are independent uniform vectors, including zero. The matrix is sampled independently as well. · OAI.UniqueGamesTheorem.Inverse.Shortcode.equalityAcceptance

equalityBits def

This literal is independent of the graph input. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.equalityBits

equalityBits def

This literal is independent of the graph input. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.equalityBits

equalityInTime def

Timed correctness has only concrete input-tape and instruction premises. · OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.equalityInTime

equalityInTime def

Timed correctness has only concrete input-tape and instruction premises. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.equalityInTime

equalityRelation def

The fixed, complete 64-label equality predicate. · OAI.MaxCutGames.Foundations.PCP.PreprocessingInternalRows.equalityRelation

equalityRelation def

The fixed, complete 64-label equality predicate. · OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.equalityRelation

EqualLabelPairs def

All pairs of departures carrying the same label. A caller may restrict ι to the lit occurrences before applying this construction. · OAI.TwoPointCorrelations.EqualLabelPairs

EqualRestrictedTransports def

This is equality of the two restricted bottom rows, not a DN hypothesis. Deriving it from the actual DN maps is still required by the full theorem. · OAI.ElasticityRecovery.EqualRestrictedTransports

Equation def

Actual planar first-order equation on distributions, not an abstract regularity or frame existence interface. · OAI.ElasticityPlanarDistribution.Equation

Equation inductive

Explicit equation patterns of the paper's infinite presentation. Diagonal W generators are set to one, so the total-index notation introduces no additional group generators compared with the manuscript. · OAI.LittleFinitistic.Presentation.Equation

equation def

Principal equation obtained from the trivialized ideal inclusion by the fully faithful associated-sheaf functor. · OAI.AffineCartierNilpotence.equation

equation def

Finite seed equation patterns. Vacuous index combinations give 1=1. · OAI.LittleFinitistic.FinitePresentation.equation

equation def

Two inverse equations per generator, and one polynomial per group relator. · OAI.LittleFinitistic.GroupAlgebraPresentation.equation

equation def

The dummy appears twice. Its assigned bit cancels in the equation. · OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equation

equation def

One sampled test becomes exactly one three-occurrence equation. · OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.equation

equation def

The dummy appears twice. Its assigned bit cancels in the equation. · OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equation

equation def

One sampled test becomes exactly one three-occurrence equation. · OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.equation

equationAcceptance def

Actual weighted acceptance of the emitted equation family. · OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.equationAcceptance

equationAcceptance def

Actual weighted acceptance of the emitted equation family. · OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.equationAcceptance

equationBit def

The three actual equation coordinates, including the homogeneous term. · OAI.UniqueGamesTheorem.Clean.LocalReplay.equationBit

equationFactors def

An actual multiset of irreducible polynomial factors; repetitions retain multiplicity. · OAI.Nagata.Workers.W30.equationFactors

equationFor def

One local descriptor, reusing the existing folded and empty-context equations. The first-valid search is over the fixed explicit answer encoding. · OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.equationFor

equationFor def

One local descriptor, reusing the existing folded and empty-context equations. The first-valid search is over the fixed explicit answer encoding. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.equationFor

equationForm def

The curve equation itself is an element of its degree's homogeneous space. · OAI.Nagata.Workers.W24.equationForm

equationIdealCycle def

A finite effective cycle of actual principal ideals, with natural weights. · OAI.Nagata.Workers.W30.equationIdealCycle

EquationInput structure

The equation player's canonical two-free-coordinate advice input. · OAI.UniqueGamesTheorem.Clean.LocalReplay.EquationInput

equationMultiplicity def

Canonical multiplicities indexed by polynomial associate classes. · OAI.Nagata.Workers.W30.equationMultiplicity

Equations structure

These are precisely the independent scalar trace and Bianchi equations. · OAI.PositiveEinsteinFour.HighestHessian.Equations

equations def

The literal integer reversal equation, with the two selected bulk products. · OAI.Ostmann.PivotDependencyScheme.equations

equationVanishes def

Vanishing of a multihomogeneous equation on a tuple. Quantifying over representatives makes independence of the chosen homogeneous coordinates explicit in the definition. Such representatives exist for every point. · OAI.Nagata.ProjectiveGeometry.equationVanishes

equiv def

Affine-coordinate derivations and sheaf derivations are equivalent. · OAI.AffineDerivation.equiv

equiv def

A coordinate permutation leaves the common denominator unchanged. · OAI.ContingencyTables.IntegerLaw.equiv

equiv def

No homotopy classes are collapsed by this change of representation. · OAI.HyperbolicObstruction.PathHomotopyTopology.equiv

equiv def

Any additive module-valued functor preserves the actual image of a split idempotent. · OAI.LittleFinitistic.AdditiveSplitImage.equiv

equiv def

Vertex extraction commutes with actual balanced tensoring, without a flatness assumption. · OAI.LittleFinitistic.BalancedVertexImage.equiv

equiv def

The full B-valued tensor functor has exactly the previously constructed vertex spaces, with scalar restriction accounted for explicitly. · OAI.LittleFinitistic.BimoduleTensorVertexBridge.equiv

equiv def

Reconstruct a full module isomorphism from the three actual vertex-space isomorphisms and the two finite arrow families. Its underlying vector-space map is precisely the direct-sum assembly of the supplied vertex isomorphisms. · OAI.LittleFinitistic.EncodingModuleAssembly.equiv

equiv def

The vertex of the actual evaluation module is exactly the original vector space. · OAI.LittleFinitistic.EvaluationVertexDiagram.equiv

equiv def

Canonical actual quotient equivalence, on representatives d tensor v. · OAI.LittleFinitistic.PDBarQuotient.equiv

equiv def

Actual balanced associativity S tensor_D (D tensor_A V) = S tensor_A V, with the right A action restricted along f. · OAI.LittleFinitistic.PDResidueAssociativity.equiv

equiv def

The radical quotient-ring comparison also respects the actual k action. · OAI.LittleFinitistic.PDResidueProjection.equiv

equiv def

The evaluator's range is canonically the primary's actual H(Y), as a complex vector space. · OAI.LittleFinitistic.SelectedImageComparison.equiv

equiv def

A module decomposes into its actual vertex subspaces. This is a vector-space isomorphism; off-diagonal arrows act between its factors. · OAI.LittleFinitistic.VertexDecomposition.equiv

equiv def

Uniform free quotient maps parametrize exactly the original affine slice. · OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.equiv

equiv def

Exact origin scalar base change, including its canonical maps. · OAI.OriginScalarBaseChange.equiv

equiv def

Apexes of two actual pushout squares are isomorphic over both bases. · OAI.PartitionConsistency.MonoidPushout.IsPushout.equiv

equiv def

The concatenation is exhaustive: injectivity and the exact finite cardinality prove that every global ordinal has a group and a local index. · OAI.ReflexiveFixedPoints.OrderedGroupConcat.equiv

equiv def

Two successive principal quotients are the quotient by the pair of equations. · OAI.StableCoordinate.IteratedQuotient.equiv

equiv def

The exact Laurent presentation of the localized graded hypersurface. · OAI.StableCoordinate.LaurentPresentation.equiv

equiv def

The exact determinant-one L,N change is a polynomial algebra automorphism. · OAI.StableCoordinate.Linearization.equiv

equiv def

The quotient by L-u+p*w is the five-variable polynomial algebra. · OAI.StableCoordinate.StabilizedQuotient.equiv

equiv def

The prescribed offsets define an actual equivalence. In particular, this partition covers every old letter even when a path is empty. · OAI.TorsionFreeZeroDivisors.FiniteChunking.equiv

equiv def

Uniform free quotient maps parametrize exactly the original affine slice. · OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.equiv

equivalence def

The complete explicit relative bridge. For a Laurent coefficient ring, c is its Laurent variable and d its inverse. Both composites are proved. · OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.equivalence

equivalence def

The explicit scalar-preserving polynomial cylinder isomorphism. · OAI.ComplexCancellation.Cylinder.equivalence

equivalence def

Exact finite algebra presentation: replace the monoid equations by the same free-algebra equations and set a representative of monoid zero equal to zero. · OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.equivalence

equivalence def

The natural affine quotient has no additional kernel. · OAI.FiniteAlgebraicEnvelopes.FiniteAffine.equivalence

equivalence def

Associativity of the actual noncommutative balanced tensor, with no flatness hypotheses. · OAI.LittleFinitistic.BalancedAssociativity.equivalence

equivalence def

The actual free balanced tensor, for arbitrary index sets and arbitrary modules N. · OAI.LittleFinitistic.BalancedTensor.Free.equivalence

equivalence def

Tensor with an arbitrary free left module is the direct sum of the right module. · OAI.LittleFinitistic.BalancedTensor.FreeLeft.equivalence

equivalence def

Ordinary balanced associativity retains the actual outside left action. · OAI.LittleFinitistic.BimoduleAssociativity.equivalence

equivalence def

A product with all but one coordinate zero is exactly its remaining coordinate. · OAI.LittleFinitistic.FinitePiSupport.equivalence

equivalence def

Changing finite support indices adds or removes only zero terms. The maps are the actual coordinate inclusions/projections, including all degree transports. · OAI.LittleFinitistic.FiniteSupportReindex.equivalence

equivalence def

Tensor on the first block selects O and has its actual output on the second block. · OAI.LittleFinitistic.OrdinarySimulation.FirstBlockTensor.equivalence

equivalence def

Tensor on the second block selects T and has its actual output on the first block. · OAI.LittleFinitistic.OrdinarySimulation.SecondBlockTensor.equivalence

equivalence def

The source term B tensor eC is the actual right ideal (1 tensor e)(B tensor C). · OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.equivalence

equivalence def

Opposite interval labelling is an involutive slice equivalence. · OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.equivalence

equivalenceOfConcreteRange def

A faithful normal realization with precisely this represented range supplies the star equivalence; no tracial input is needed for this step. · OAI.KadisonSimilarity.equivalenceOfConcreteRange

Equivalent def

Full Hadamard equivalence, with arbitrary unit complex phases. · OAI.MUB6.Equivalent

Equivalent def

The orbit relation for (x,w) ↦ (λx,λ^k w). · OAI.Nagata.W16.AssociatedBundle.Equivalent

Equivalent def

Unitary equivalence, not merely equality of dimensions. · OAI.NuclearUltrapower.FiniteUnitaryRep.Equivalent

Equivalent def

Logical equivalence retains two actual typed open proof transformers. No data term is ever replaced using this relation. · OAI.PureTypeSystem.Labelled.Equivalent

EquivalentNorm def

Two-sided comparison makes this seminorm a genuine norm equivalent to the original. · OAI.ExactModuli.EquivalentNorm

EquivalentNorm structure

An equivalent norm is kept as its exact real seminorm, with explicit positive comparison constants. The lower inequality makes it a norm. · OAI.ForestSpace.EquivalentNorm

EquivalentPartition structure

A partition of p with actual partial isometries from a common projection. The cross identities encode orthogonality. This structure is constructed below. · OAI.Generator.Tracial.EquivalentPartition

Equivariant def

Equivariance under every allowed shift; no linearity of C is assumed. · OAI.MaxCutGames.Gadget.Quotient.Equivariant

Equivariant def

Equivariance under every allowed shift; no linearity of C is assumed. · OAI.UniqueGamesTheorem.Gadget.Quotient.Equivariant

EquivariantFunctions def

Scalar functions with the literal one-step multiplier law on the genuine cover. · OAI.Nagata.W08.EquivariantFunctions

equivariantMix def

Union of an equivariant family of active arbitrary-rank names. No choice of a common strengthening occurs in the definition. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.equivariantMix

equivariantOfQuotientSection def

Extract an equivariant function from an actual quotient section. · OAI.Nagata.W08.equivariantOfQuotientSection

equivariantQuotientSectionEquiv def

The actual algebraic section/function equivalence of the actual quotient projection. Holomorphic compatibility is not asserted by this set-level equivalence. · OAI.Nagata.W08.equivariantQuotientSectionEquiv

equivFundamentalGroup def

A genuine isomorphism to the actual topological fundamental group. · OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.equivFundamentalGroup

equivInvariantMultilinear def

Free multiset coefficients and genuine symmetric multilinear maps describe exactly the same vector space. · OAI.MetricEntropyDuality.SymmetricForm.equivInvariantMultilinear

equivProd def

The product coordinates are an actual equivalence of sets. · OAI.PolycyclicRecognition.FactorExtension.equivProd

equivVal def

The symmetric coherence value of a bijection of two positive finite ordinals. Both sides may use different (provably equal) numeral expressions. · OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equivVal

erase def

Forget success declarations, retaining the exact adaptive query tree. · OAI.MatroidProphet.MarkedQueryProgram.erase

erased def

The positive-weight part, all of whose supported terms have weight one. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.erased

eraseEdge def

Delete exactly one unordered edge. · OAI.CliqueFreeIndependence.WeightedGraph.eraseEdge

eraseEdge def

Deletion of an actual paired edge: its incident face boundaries are spliced and the two indexed sides erased. No label or surface premise is hidden in this finite permutation construction. · OAI.HyperbolicObstruction.PictureSwitch.PictureMap.eraseEdge

eraseInput def

Required cleanup before Mathlib's exact halt-list convention. · OAI.OptimalMaxCut.CounterMachine.eraseInput

eraseLoop def

Remove a closed loop in a segment chain. · OAI.PlanarL1.Topology.SegmentChain.eraseLoop

ErgodicDecompositionInput def

The invariant specialization of Greschonig--Schmidt Theorem 5.2. All topological and standard-Borel hypotheses are retained in the binder. · OAI.PolycyclicRecognition.ErgodicDecompositionInput

error def

The corresponding global error, written entirely in coordinate residuals. · OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.error

error def

Positive error is zero on insertion steps here; those steps are separately charged to the actual retirement and pilot budgets. · OAI.KServer.LevelNoInsert.error

error def

Uniform finite input and the stage's actual uniform finite noise choices. · OAI.MaxCutGames.Gadget.StageNoiseRecurrence.error

error def

An explicit error that tends to zero. · OAI.Problem335.PowerPerturbation.error

error def

One explicit approximation error controls both the measured coordinates and the actual radial quadratic error. · OAI.RegularPointCoordinates.ActualProjectionConfiguration.error

error def

Uniform finite input and the stage's actual uniform finite noise choices. · OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.error

errorEnvelope def

A uniform majorant for the unscaled E_m, independent of r₀. · OAI.SymmetricMahler.errorEnvelope

errorIntegrand def

The unscaled error integrand. · OAI.SymmetricMahler.errorIntegrand

errors def

Counted mismatches, before any normalization of the retained law. · OAI.SmoothObstruction.SymbolMass.errors

EssentialExpression inductive

A generated expression with every identity factor removed. · OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression

essentialLocalSet def

Points having a fixed essential color on some ambient neighborhood. · OAI.EuclideanFiveColor.essentialLocalSet

eStar def

The coordinate functional on J(T). · OAI.ForestSpace.eStar

estimate def

Literal sum of the independently maintained size-rank references. · OAI.KServer.CoarseProcess.estimate

estimatorWordBits def

The complete input length, with one independent walk for each ratio sample and one walk plus integer-bin draw for each correction sample. · OAI.ContingencyTables.CompanionOracleDensity.estimatorWordBits

estimatorWordEquiv def

This equivalence partitions, rather than reuses, the random bits of all the individual experiments in the estimator. · OAI.ContingencyTables.CompanionOracleDensity.estimatorWordEquiv

et def

trace-and-expectation paper notation · OAI.GeneralMahler.et

eta def

Coercivity margin, η = .29. · OAI.StationaryNS.eta

etaleBasis def

differentials of polynomial coordinates remain a basis after an étale map. This is used below on the Kummer normalization chart. · OAI.CanonicalCoordinates.etaleBasis

etalePartial def

The partial derivatives on a formally étale coordinate chart, obtained from the cotangent-space base-change isomorphism. · OAI.CartierSections.etalePartial

etaO def

all O testers. · OAI.HadwigerCounterexample.etaO

etaOf def

The single generator of a finite prime-root ring. · OAI.CirculantHadamard.CyclotomicRings.etaOf

eTwo def

Extended Euclidean aggregation, with no finiteness assumption. · OAI.BoundedTreePotentials.Segments.eTwo

euclidConvergent def

Euclid's finite convergent recurrence, entirely natural/rational arithmetic. · OAI.ExactQuantumFactoring.OrderTrial.euclidConvergent

euclidean def

The actual scalar image of the cube-plus-diagonal body in Euclidean space. · OAI.DiagonalZonotope.euclidean

euclideanColumnMap def

The continuous linear map with the specified Euclidean columns. · OAI.RegularPointCoordinates.euclideanColumnMap

EuclideanGevreyCutoff structure

A single fixed radial-scale cutoff with all-order Gevrey-two bounds. · OAI.RegularPointCoordinates.EuclideanGevreyCutoff

EuclideanGevreyCutoffInput def

The precise compact Gevrey specialization needed by the chart proof. · OAI.RegularPointCoordinates.EuclideanGevreyCutoffInput

euclideanGradientSquare def

Euclidean norm squared of the gradient, written in the fixed orthonormal coordinate basis. · OAI.AffineBernstein.euclideanGradientSquare

EuclideanGraphComplete def

Sequential completeness for the induced Euclidean path metric. This states that every intrinsic Cauchy sequence of points in Ω has an intrinsic limit in Ω. It imposes no growth condition and no completeness condition on the affine metric. · OAI.AffineBernstein.EuclideanGraphComplete

EuclideanHarmonicHessianInput def

Evans, PDE (second edition), §2.2.3(c), Theorem 7, degree two, combined with Cauchy--Schwarz on the outer ball. The input only bounds the second derivative of a normalized Euclidean harmonic function. · OAI.RegularPointCoordinates.EuclideanHarmonicHessianInput

EuclideanHarmonicModel structure

An L²-normalized harmonic function on the limiting Euclidean ball. · OAI.RegularPointCoordinates.EuclideanHarmonicModel

EuclideanInvarianceOfDomain def

Precisely the Euclidean open-image assertion of Hatcher, Theorem 2B.3. · OAI.RegularPointCoordinates.EuclideanInvarianceOfDomain

EuclideanMeasuredRescalingConvergence def

The Euclidean-limit specialization of noncollapsed measured volume convergence, including approximation maps and normalized test integrals. · OAI.RegularPointCoordinates.EuclideanMeasuredRescalingConvergence

euclideanProduct def

The two-block product of explicit Euclidean zonotopes. · OAI.DiagonalZonotope.euclideanProduct

EuclideanRescalingVolumeConvergence def

Volume convergence for the normalized Hausdorff measure of an n-dimensional noncollapsed RCD space. omega is the Euclidean unit-ball volume. The source metric is unchanged: a rescaled radius R is s i * R in the original metric. · OAI.RegularPointCoordinates.EuclideanRescalingVolumeConvergence

euclideanSpherePole def

A fixed unit vector used to make the recursive sphere calculation a definition. · OAI.Kaplansky.euclideanSpherePole

euclideanSphereTopGenerator def

The normalized integral class determined by the recursive orientation. · OAI.Kaplansky.euclideanSphereTopGenerator

euclideanSphereTopHomologyIso def

The full top integral homology calculation for every positive-dimensional Euclidean sphere. The recursive pole charts and ordered H₀ components fix a sign. · OAI.Kaplansky.euclideanSphereTopHomologyIso

euclideanValueMoments def

The affine moment family is already meaningful before harmonicity of the limit is identified. · OAI.RegularPointCoordinates.euclideanValueMoments

EuclideanVariations structure

The first two variational equations for a transition map. The second time argument is elapsed time; the first is its initial phase. · OAI.ForcedComputation.EuclideanVariations

EuclideanVelocityPair abbrev

The Euclidean velocity-pair space, whose norm squared is total kinetic energy. · OAI.BoltzmannNonuniqueness.EuclideanVelocityPair

euclideanVolumeFactor def

Calibration of Hausdorff measure to Euclidean volume. · OAI.WeakMTWTransport.euclideanVolumeFactor

EuclideanWeakHarmonicOn def

The compact-test distributional Laplace equation on one Euclidean ball. · OAI.RegularPointCoordinates.EuclideanWeakHarmonicOn

euclidSize def

The ordinary Euclidean size of a finite real coefficient list. · OAI.IndependentProducts.euclidSize

Euler def

Only Euler planarity is needed in the interval-count argument. This file proves neither Euler planarity for an abstract pairing nor its PL realization. · OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.Euler

euler def

Euler's operator for one block. · OAI.Problem346.PolynomialShift.euler

eulerFactors def

Euler factors selecting one boundary exponent among those bounded by N. · OAI.CartierSections.eulerFactors

eulerStep def

The Euler differential operator minus a scalar. · OAI.CartierSections.eulerStep

Eval inductive

Evaluation in any rational algebra; a unary inverse requires an actual two-sided inverse of the evaluated operand, not a totalized inverse. · OAI.RationalHitting.Formula.Eval

eval def

Evaluation in the original coordinate chart. · OAI.ClosedSurfaceR4.JetPolynomial.TensorExpression.eval

eval def

An acceptable word-program numbering obtained from the pinned universal partial-recursive evaluator. Invalid decoded results remain undefined. · OAI.FiniteAlgebraicEnvelopes.WordProgramming.eval

eval def

Coordinate evaluation is bounded by singleton segment tests. · OAI.ForestSpace.TestVector.eval

eval def

Evaluation of the rational convex syntax. · OAI.KadisonKastler.RationalConvexExpr.eval

eval def

Evaluation sums over ordered basis tuples; repeated indices are retained. · OAI.MetricEntropyDuality.SymmetricForm.eval

eval def

Evaluate a sparse rational linear form on a real vector. Repeated keys add. · OAI.MUB6.Certificate.Sparse.eval

eval def

Evaluation is an actual unital star homomorphism. · OAI.NuclearUltrapower.VariableUltra.eval

eval def

Evaluate a word by its successive left multipliers. · OAI.PartitionConsistency.ProbeAlgebra.Raw.eval

eval def

Evaluation at the exact algebraic argument. · OAI.PlaneFiveColor.Spectral.eval

eval def

Both choices are tested at each binder. Specialization will select the extreme choice given by the unique internal support path. · OAI.PureTypeSystem.OneChildInterpretation.eval

eval def

Interpret a quotient cell in any cocone. · OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.eval

eval def

Evaluation in any given cocone. On inadmissible expressions the first factor supplies a harmless totalization; admitted terms never use it. · OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Term.eval

eval def

Evaluation on a Boolean input vector. Empty AND/OR gates are true/false. · OAI.TwoPointCorrelations.AC0Circuit.eval

eval def

A clause is true when at least one of its three signed literals evaluates to true under the assignment. · OAI.UniqueGamesTheorem.BinaryFormula.Clause.eval

eval def

Given `assignment : Nat → Bool`, a positive literal returns the assigned bit and a negative literal returns its Boolean complement. · OAI.UniqueGamesTheorem.BinaryFormula.Literal.eval

evalBilinearWord def

Evaluate a bracket word with a specified continuous bilinear bracket. · OAI.PolycyclicRecognition.evalBilinearWord

evalHom def

Evaluation is a star algebra homomorphism. · OAI.KadisonKastler.WeakOperatorRepresentative.evalHom

evalHom def

Evaluation in any monoid satisfying the letter equivariance and exit relations. This will give the presentation's universal property. · OAI.PartitionConsistency.ProbeAlgebra.Word.evalHom

evalLocal def

A terminating local interpreter for the finite table. · OAI.ForcedComputation.Recorder.evalLocal

evalNat def

Evaluation over the integers of an integer polynomial at natural inputs. · OAI.SingleFold.evalNat

evalOn def

Restriction of the canonical evaluation embedding to a subspace of the dual. · OAI.SeparableQuotient.evalOn

evalPolynomialMap def

Evaluation of a vector polynomial on complex affine space. · OAI.KahlerUniformization.evalPolynomialMap

evalPredBody def

The predicate-variable callback P ↦ P@y. · OAI.PureTypeSystem.Labelled.ChannelCode.evalPredBody

evaluate def

Evaluation at a multiplicative character of the additive cyclic group. · OAI.CirculantHadamard.CyclicRing.evaluate

evaluate def

An assignment is evaluated from retained record data only. · OAI.MaxCutGames.Reduction.ActualCompleteness.evaluate

evaluate def

A unitary group representation evaluates finite linear combinations. · OAI.NuclearUltrapower.GroupStarAlgebra.evaluate

evaluate def

Interpretation of an actual merger normal form. New letters are evaluated in their displayed order; the target is an arbitrary monoid. · OAI.PartitionConsistency.MergerAlgebra.Word.evaluate

evaluate def

Interpretation of actual set-name codes. At no point is the forcing order or a maximum principle used in this recursion. · OAI.PartitionConsistency.SetForcingNames.evaluate

evaluate def

Evaluate a cutoff assignment, applying maps strictly above its level. · OAI.ReflexiveFixedPoints.TreeEvaluation.evaluate

evaluate def

The polynomial map with prescribed homogeneous Laurent images. · OAI.StableCoordinate.LaurentWeightedMap.evaluate

evaluate def

The degree n component extracted from a strict functor to nu K. · OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluate

evaluate def

The candidate map is defined on every actual cell, independently of a bound. · OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.evaluate

evaluate def

An assignment is evaluated from retained record data only. · OAI.UniqueGamesTheorem.Reduction.ActualCompleteness.evaluate

evaluateArray def

Evaluation of any rational array, not only chosen normers. · OAI.SeparableQuotient.NormConstruction.NormingSet.evaluateArray

evaluateAt def

Evaluate the polynomial quotient at a proved nth root of unity. · OAI.CirculantHadamard.CyclicRing.evaluateAt

evaluateBilinear def

Coordinate evaluation of a free right module tensor N. · OAI.LittleFinitistic.BalancedTensor.Free.evaluateBilinear

evaluateCell def

Evaluate a bounded mapping representative on a cell of its source globe. · OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.evaluateCell

evaluatedAction def

The quotient action, evaluated and identified with the stalk of Y. · OAI.LittleFinitistic.QuadraticEncoding.evaluatedAction

evaluatedImage def

The actual image eY, represented in the same universe as tensor evaluation. · OAI.LittleFinitistic.QuadraticEncoding.evaluatedImage

evaluatedImageK def

The image vector space, as an actual bounded finite-dimensional stalk complex. · OAI.LittleFinitistic.QuadraticEncoding.evaluatedImageK

evaluatedPrediction def

Apply the parent maps once, then the actual evaluation strictly above the cutoff. · OAI.ReflexiveFixedPoints.Prediction.evaluatedPrediction

evaluatedPrediction def

The actual prediction evaluates the current frontier maps on its residual inputs. · OAI.ReflexiveFixedPoints.Prediction.Prefix.evaluatedPrediction

evaluatedSummandIso def

The evaluated formal summand has precisely the idempotent induced by r on Y. · OAI.LittleFinitistic.QuadraticEncoding.evaluatedSummandIso

evaluatedTransferLeaf def

Preserve the actual leaf frequency as well as its sign and word value. · OAI.Ostmann.evaluatedTransferLeaf

evaluateFrom def

Evaluate only between the two indicated depths. · OAI.ReflexiveFixedPoints.TreeEvaluation.evaluateFrom

evaluateHom def

The augmented positive chain map obtained from an arbitrary strict map. · OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluateHom

evaluateInitializedForce def

The two finite shear expressions are evaluated by their existing certified algorithms; the extra time test only selects between overlapping exact germs. · OAI.ForcedComputation.evaluateInitializedForce

evaluateMotion def

Evaluate a polynomial homogeneous-coordinate motion at a parameter. · OAI.Nagata.Workers.W14.evaluateMotion

evaluateOne def

Evaluation at one, used only on degree-zero homogeneous fractions. · OAI.SectionCompletion.evaluateOne

evaluateRow def

Pure row semantics: exactly two lookups in the input table. The two fixed H lookups occur inside start and receiveSecond. This is not a machine trace. · OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.evaluateRow

evaluateRow def

Pure row semantics: exactly two lookups in the input table. The two fixed H lookups occur inside start and receiveSecond. This is not a machine trace. · OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.evaluateRow

Evaluates inductive

Timed operational semantics. Loop termination and the number of iterations must be proved by the caller; there is no hidden bounded-search oracle. · OAI.OptimalMaxCut.CounterMachine.Command.Evaluates

evaluateSingularCylinder def

A singular-valued simplicial cylinder gives an actual continuous cylinder. · OAI.Thomason.Construction.evaluateSingularCylinder

Evaluation def

Three copies of Y, with its representation kept in the type. · OAI.LittleFinitistic.QuadraticEncoding.Representation.Evaluation

evaluation def

Evaluation of the free induced module. · OAI.LittleFinitistic.DirectedBound.DirectedSystem.evaluation

evaluation def

Evaluation of the actual BC-balanced tensor. · OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.evaluation

evaluation def

The induced functor from the actual quotient. · OAI.LittleFinitistic.TwoConeVerdier.ConePair.evaluation

evaluation def

Canonical evaluation into the dual of the coordinate span. · OAI.SeparableQuotient.NormConstruction.NormingSet.evaluation

evaluation def

Evaluation on the closed span G. · OAI.SeparableQuotient.PrefixNormers.evaluation

evaluation def

Every model evaluation is an actual strict functor. · OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.evaluation

evaluation def

Natural maps into the cylinder give strict evaluations; in particular this constructs both interval endpoint evaluations. · OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.evaluation

evaluationCharacter def

Evaluation of a uniformly chosen linear functional is a binary character. · OAI.MaxCutGames.Fourier.MatrixNoise.evaluationCharacter

evaluationCharacter def

Evaluation of a uniformly chosen linear functional is a binary character. · OAI.UniqueGamesTheorem.Fourier.MatrixNoise.evaluationCharacter

evaluationMatrix def

Rows are reindexed by an actual equivalence; entries are the exact images of the two augmented-coordinate tensor factors in FieldCriterion. · OAI.EuclideanRamsey.NineLinearObstruction.evaluationMatrix

evaluationNatTrans def

Evaluation is natural under postcomposition. · OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.evaluationNatTrans

evaluationTermIso def

The finite total and the native module evaluation agree in every degree, provided every nonzero P-degree is included. · OAI.LittleFinitistic.BimoduleTotal.evaluationTermIso

evaluationTerms def

Terms in the denominator-cleared evaluation of an axis polynomial at w = ε (q/100)². The coordinate is 0 for real and 1 for imaginary. · OAI.DefocusingNLS.SeparatorArithmetic.evaluationTerms

evaluationToZ def

Evaluation with codomain the closed coefficient span. · OAI.SeparableQuotient.PrefixNormers.evaluationToZ

evaluationUnit def

The actual local unit attached to one evaluated Gaussian norm element. · OAI.CirculantHadamard.BinaryLocalFamily.evaluationUnit

evaluationVertexEquiv def

The natural identifications for the actual tensor functor. · OAI.LittleFinitistic.QuadraticEncoding.evaluationVertexEquiv

evalWord def

Evaluation in the specified finite generating family. · OAI.FiniteAlgebraicEnvelopes.evalWord

evenBlockFamily def

The concrete disjoint-block family underlying the commuting coordinates. · OAI.WeakPureInfiniteness.evenBlockFamily

evenBlockMode def

Consecutive disjoint geometric blocks, with block zero reserved for the reference. · OAI.WeakPureInfiniteness.evenBlockMode

evenCoefficients def

The degree-30 real-even truncation. Its use requires the structural proof. · OAI.DefocusingNLS.BoundaryCertificate.evenCoefficients

EvenDensity def

Even means positive trace-one and block diagonal for E,O, exactly as in05. · OAI.CoordinateSweeps.SignedTensor.EvenDensity

evenEntries def

Incidence supports start with a line and alternate line/point. · OAI.TwoPointCorrelations.evenEntries

evenGrid def

Even grid time immediately below t, for the odd duration 2n+1. · OAI.FKCRT.SimpleWalk.evenGrid

evenIteration def

Section 6's even-iterate formula, for an actual endofunctor and an objectwise two-step split. · OAI.ExternalTensor.Binomial.evenIteration

evenIteration def

Exact Section 5 even-iteration formula, with both presentation distinctions discharged. · OAI.LittleFinitistic.SelectedOrdinaryOrbit.evenIteration

evenKernelTwist def

The conductor-eight twist accounts for both the sign and the factor two. · OAI.Ostmann.evenKernelTwist

evenMomentSq def

Squared L^(2k)-norm for a finite law, expressed without measure coercions. · OAI.TraceReconstruction.FiniteLaw.evenMomentSq

evenOffset def

Common unit neighbor for the transverse chord of length t. · OAI.EuclideanFiveColor.evenOffset

evenOffspring def

Doubling block edge counts gives exactly the corner offspring law. The support span is two, and sizes in the tree theorem are all 2n+1. · OAI.FKCRT.BlockCritical.evenOffspring

evenRohlinClock def

The actual occupation clock for the supplied even row. · OAI.WeakPureInfiniteness.evenRohlinClock

evenRohlinCoordinate def

Commuting two-level coordinates of the actual even row. · OAI.WeakPureInfiniteness.evenRohlinCoordinate

evenRohlinProjection def

The kth cell at dyadic level m. · OAI.WeakPureInfiniteness.evenRohlinProjection

evenSubsetProduct def

Numerator before introducing any inverse, available in a coefficient ring. · OAI.CirculantHadamard.evenSubsetProduct

Event inductive

One edge actually seen. · OAI.FourierLLogL.Dyadic.Procedure.Event

event def

Probability of an event. · OAI.CoordinateSweeps.FiniteLaw.event

event def

The event reads the literal original path label, and pins the actual initial vertex of the exceptional interval on its prescribed side. · OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.event

eventDistance def

Event-level l1 distance, independent of the representation and therefore suitable for a single bounded-grid perturbation interval. · OAI.CoordinateSweeps.Grid.eventDistance

eventIndicator def

A fixed indicator convention keeps equivalent event descriptions independent of the decision procedures inferred for their propositions. · OAI.ContingencyTables.CompanionTraceWords.eventIndicator

eventProb def

Real probability of any event in the finite bit space. · OAI.HyperedgeComparison.eventProb

eventQueries def

The actual six oracle addresses for each test. Unused slots repeat an address already queried, so every event has the same fixed six-slot format. · OAI.MaxCutGames.Foundations.PCP.AssignmentTester.eventQueries

eventQueries def

The actual six oracle addresses for each test. Unused slots repeat an address already queried, so every event has the same fixed six-slot format. · OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.eventQueries

evenTriangle def

The manuscript's one-based L_s, translated to zero-based Fin indices. · OAI.Paper170.evenTriangle

eventsAt def

A materialized list of all three slot events at an occurrence. · OAI.MaxCutGames.Foundations.PCP.eventsAt

eventsAt def

A materialized list of all three slot events at an occurrence. · OAI.UniqueGamesTheorem.Foundations.PCP.eventsAt

EventualHeatControls structure

A common starting index, decrement constant and small-mass tolerance. These estimates are proved from the heat equation and splitting data. · OAI.RegularPointCoordinates.EventualHeatControls

EventuallyPrimeSumset def

Both prime coverage and exclusion of composite sums beyond one threshold. · OAI.Ostmann.EventuallyPrimeSumset

eventuallySmallChains def

Chains whose iterated subdivisions eventually lie in the actual image of the small-chain inclusion. · OAI.Kaplansky.eventuallySmallChains

EventualOddRanks def

The base-prime threshold is uniform; the odd-degree threshold may depend on the base prime. Every sufficiently large odd degree is included. · OAI.RyserOdd.Specification.EventualOddRanks

eventualSetoid def

Equality after discarding a finite initial segment of a sequence. · OAI.PartitionConsistency.TailSelector.eventualSetoid

eventVertex def

Vertex visited after the named interval occurrence. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.eventVertex

evenWord def

The exact alternating word for the unnormalized even moment. · OAI.CoordinateSweeps.BlockCycles.evenWord

Evolution structure

Finite fundamental matrices, with the output time first. · OAI.SmoothObstruction.FiniteGreen.Evolution

evolution def

Actual continuous evolution, defined by the invertible weighted Volterra operator. The coefficient need only be continuous in time. · OAI.ElasticityODE.evolution

evolution def

A genuine synchronous radius-one automaton on the cyclic address alphabet. · OAI.WLIdentification.CellularCircuit.evolution

evolutionOperator def

The heat operator at nonpositive time is the identity. Only strong, applied continuity at zero is asserted; operator-norm continuity there is unnecessary. · OAI.ForcedComputation.PlaneHeat.evolutionOperator

evolve def

Exact pointwise action of the H/conditional-forward-translation sequence. There is no projection or forced-success operation in this evolution. · OAI.ExactQuantumFactoring.Triangular.evolve

evolve def

Evolution retains the complete state, which can itself contain the past. · OAI.PlanarL1.Execution.evolve

evolveGiantValues def

This is the actual forward update: the reconstructed pivot becomes one giant, and the giant on the selected branch is retained. · OAI.Ostmann.evolveGiantValues

Exact def

A real edge cocycle is exact. This algebraic formulation allows the fold-deletion proof to avoid any appeal to an unformalized planar theorem. · OAI.ArtinCAT0.TriangleMesh.Exact

exactFiberEquiv def

An actual complex algebra equivalence for each fiber. · OAI.StableCoordinate.exactFiberEquiv

exactFirstRetraction def

The same retraction for mathlib's exact derived inflation. · OAI.LittleFinitistic.BlockModule.exactFirstRetraction

exactGate def

The gate retains the margins for either branch. · OAI.ContingencyTables.ProfilePrograms.exactGate

exactMatrixRank def

Exact rank of the square matrix multiplication tensor. · OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank

exactMul def

Interval multiplication with floor and ceiling at the common integer grid. · OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.exactMul

exactNonzeroFiberEquiv def

Every nonzero complex fiber of the exact polynomial has affine-three-space coordinate algebra. The zero fiber is treated in ZeroFiberExact. · OAI.StableCoordinate.exactNonzeroFiberEquiv

exactObservedRatio def

The exact empirical ratio written as the plain-state sum divided by its integer plain-state population. · OAI.ContingencyTables.CompanionPhaseWords.exactObservedRatio

exactObservedRatio def

The exact empirical ratio written as the plain-state sum divided by its integer plain-state population. · OAI.ContingencyTables.RootedPhaseWords.exactObservedRatio

exactOrdinaryBits def

The ordinary branch needs precisely the existing public sampler's word. · OAI.ContingencyTables.ProfilePrograms.exactOrdinaryBits

ExactOverlap def

The pairwise hypothesis of the diagram amalgamation lemma. · OAI.PartitionConsistency.DiagramForcing.Diagram.ExactOverlap

ExactPair structure

Exact pairs with uncropped child legality and support bounds in both orders. · OAI.SeparableQuotient.ActualSpace.ExactPair

ExactPairs def

The leaf pairs are precisely the two incidences of each original non-tree edge, not extra shortcuts. · OAI.PlanarL1.Weighted.EnlargedTree.ExactPairs

exactRank def

Exact rank of a finite complex coefficient tensor. · OAI.MatrixMultiplication.AuxiliarySeparation.exactRank

exactRankExponent def

The exact-rank exponent ν = inf_{n ≥ 2} log(R(Tₙ))/log(n). · OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent

exactRankExponentSet def

The set of finite exact-rank exponents in the definition of ν. · OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponentSet

ExactRespects def

The exact (disjoint) pairing classes before relaxing the diagonal inequality. · OAI.Problem335.Pairings.ExactRespects

exactRetainedPacketDensity def

The finite retained spectral density of one actual signed Fourier packet. · OAI.ThreeTorus.exactRetainedPacketDensity

ExactSamplingStatement def

Paper 200-01, Theorem main(ii): every halted output is feasible, each table has limiting mass 1/|Ω|, termination has probability one, and the expected number of bit operations is bounded by a uniform polynomial. · OAI.ContingencyTables.Algorithms.ExactSamplingStatement

exceptional def

All subsets contained in no union of k members of the given family. · OAI.TalagrandDiscreteConvexity.exceptional

exceptional def

Sets contained in no union of k members of D. · OAI.TalagrandDiscreteConvexity.exceptional

exceptionalCenters def

Centers at which some normalized scale avoids all the selected tests. · OAI.Problem310.Auxiliary.exceptionalCenters

exceptionalEquiv def

The exceptional zero section is the ORIGINAL coefficient chart. · OAI.PolynomialFieldChart.exceptionalEquiv

exceptionalFirst def

Exactly the non-row, non-column shapes: defect is size minus the maximum of first row length and first column length. For size≥1 defect=0 precisely for the row or column; at size=1 they coincide and are counted once. · OAI.Thorp.Current.exceptionalFirst

ExceptionalRealZeroExclusion def

The real exceptional-zero assertion in Stark's Lemma 8, after excluding quadratic subfields. · OAI.DukePrimeDegree.ExceptionalRealZeroExclusion

ExceptionalTest def

The three-field, two-fractional-geodesic inequality in the source's configuration proposition, at the exceptional missing incidence. · OAI.HyperbolicObstruction.CoreGeometry.ExceptionalTest

exceptionalUnion def

Union of exactly the members of A which are proper subsets of the ambient type. · OAI.Nagata.Workers.W25.exceptionalUnion

ExceptionPattern structure

Valid pinned exceptional data. Injectivity is essential: it is supplied by the proved repeated-mismatch cancellation, not imposed on the kernel. · OAI.CoordinateSweeps.SignedTensor.ExceptionPattern

ExcessAssignments def

One distinguished ordinary pair has occupancy U+1. · OAI.ContingencyTables.IntegerWeightedTransport.ExcessAssignments

excessConstant def

The Gaussian excess constant at threshold twice the parameter. · OAI.IndependentProducts.excessConstant

exchange def

Symmetry of the two subtrees, with its literal untwisted cube chart. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move.exchange

exchange def

Exchange the past coordinates and leave the future coordinates fixed. · OAI.SmoothObstruction.EndpointBranch.exchange

ExchangeCost def

The local Lipschitz property needed by the repair objective. It will be instantiated by Hamming distance from the state's preliminary rounding. · OAI.KServer.Rounding.ExchangeCost

exchangedConvolution def

Exchange the two outer convolution legs while retaining the original input order in the displayed coefficient equation. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.exchangedConvolution

exchangeEquiv def

Exchange two consecutive positive blocks. · OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.exchangeEquiv

exchangeTarget def

The ordered pair records the coordinate raised and the coordinate lowered. · OAI.ContingencyTables.IntegerWeightedTransport.exchangeTarget

excludedPrimeCount def

The integers 1 ≤ n ≤ N with no factor among the excluded primes. · OAI.JointDickman.excludedPrimeCount

excludedSmoothnessPrimes def

The primes that prevent an integer up to N from being y-smooth. · OAI.JointDickman.excludedSmoothnessPrimes

excludedTimes def

Away from the first/last third of an incident edge, every vertex is uniformly separated from that edge. The set is closed even at both cutoffs. · OAI.PlanarL1.Topology.Drawing.excludedTimes

exclusion def

Exclusion cost for the faithful threefold port subdivision. · OAI.TorsionFreeZeroDivisors.GirthAsymptotics.exclusion

exclusiveProductKernel def

Kernel of two conditionally independent exclusive outputs sharing the common variable. The denominators are the output-cell masses. · OAI.JointDickman.exclusiveProductKernel

excursionDist def

Source excursion pseudometric, with the closed interval minimum. · OAI.FKCRT.excursionDist

excursionLaw def

Uniform binary walks conditioned on their first hit of -1 at the odd endpoint. · OAI.FKCRT.SimpleWalk.excursionLaw

Excursions structure

The genuine pair of short low/high paths in : no scalar separation or arc conclusion is included as an assumption. · OAI.PlanarL1.Columns.Model.Field.Excursions

excursions_of_rejected def

Literal rejection of both sphere tests provides actual narrow-band paths with opposite excursions of the fixed ordered part. No excursion hypothesis is substituted for the geometric admission test. · OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.excursions_of_rejected

excursionTreeMetric def

The excursion quotient, with the genuine induced metric. · OAI.FKCRT.excursionTreeMetric

Exec inductive

Big-step semantics with the exact number of primitive bit instructions. · OAI.Superstring.BitCode.Block.Exec

Exec inductive

Execution costs count actual finite-control stack instructions. · OAI.WLIdentification.StackModel.Command.Exec

executableCapExponent def

Integer division computes the rational floor used by the size test. · OAI.LowSpaceSubsetSum.CompressionSetup.executableCapExponent

execute def

The executing version retains a work counter even when the budget test aborts. The guard precedes every counted read/key/report call. · OAI.LowSpaceSubsetSum.BudgetedReplay.execute

execute def

An execution of each component yields an actual execution of the combined machine. The two transfer loops add exactly twice the intermediate length plus two. · OAI.MaxCutGames.Foundations.Complexity.MachineSequential.execute

execute def

An execution of each component yields an actual execution of the combined machine. The two transfer loops add exactly twice the intermediate length plus two. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.execute

executeCounted def

The action's value (which may itself contain its work counter) and the separate number of fair words read. This does not charge continuations as free machine operations. · OAI.LowSpaceSubsetSum.WordSeedRealization.executeCounted

Executes inductive

Contract of one activation. B upper bounds the sum of fees of frames simultaneously suspended by (or under) this invocation. Current frame not included; uniformly small active frame will also be required. · OAI.Fifths.Flow.Executes

executeSequenceSum def

The sum of supplied body budgets and explicit linear transfer overheads. · OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.executeSequenceSum

executeSequenceSum def

The sum of supplied body budgets and explicit linear transfer overheads. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.executeSequenceSum

Execution inductive

Finite adaptive execution trees. Every node makes an actual uniform finite choice; its continuation, including the number of later choices, may depend on that choice. This is the finite probability law used by the manuscript. · OAI.PlanarL1.Execution

execution def

The complete three-phase program executes from the original serialized input alone, with a polynomial bound in that input's full unary length. · OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.execution

execution def

The exact time count is the sum of the physically executed row loops. Its polynomial bound is derived separately from this recurrence. · OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.execution

execution def

Transport an actual runtime witness without changing its step count or budget; the final option may be either a configuration or none. · OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.execution

execution def

A bounded execution witness, obtained from the physical trace above. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.execution

execution def

Whole-machine execution on the concrete input and output encodings. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.execution

execution def

Fresh offsets and cell coins are sampled as a finite product, after the bands and radial origins; unavailable cells simply discard their sample. · OAI.PlanarL1.Columns.Model.MainFamily.execution

execution def

Sampling all orientations, group coins, interpolation atoms and branches is a finite execution determined from the old geometric groups. · OAI.PlanarL1.Columns.Model.SecondaryGeometry.execution

execution def

The complete three-phase program executes from the original serialized input alone, with a polynomial bound in that input's full unary length. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.execution

execution def

The exact time count is the sum of the physically executed row loops. Its polynomial bound is derived separately from this recurrence. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.execution

execution def

Transport an actual runtime witness without changing its step count or budget; the final option may be either a configuration or none. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.execution

execution def

A bounded execution witness, obtained from the physical trace above. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.execution

execution def

Whole-machine execution on the concrete input and output encodings. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.execution

execution_reflect def

Conversely, a translated runtime witness determines the original witness at exactly the same number of transitions. · OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.execution_reflect

execution_reflect def

Conversely, a translated runtime witness determines the original witness at exactly the same number of transitions. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.execution_reflect

exit def

The old element h(s) = k(s)e at which a letter can be consumed. · OAI.PartitionConsistency.ProbeAlgebra.Path.exit

exitAt def

An optional continuation, without reading or writing any tape. · OAI.MaxCutGames.Foundations.Complexity.MachineCompare.exitAt

exitAt def

An optional continuation, without reading or writing any tape. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.exitAt

exitEquiv def

Convert the recursively joined cells and one terminal exit into tape coordinates. · OAI.TwoWayComplementation.ChainNode.exitEquiv

exits def

Exit ends of the unsorted primitive passages. · OAI.Superstring.Hierarchical.Threading.exits

Exp def

One-exponential realizability by a single finite word expression, with an explicit bound on all its intermediate words. · OAI.WLIdentification.WordExpressions.Exp

exp def

Exponential coordinates identify the underlying sets bijectively. · OAI.PolycyclicRecognition.PolynomialCoordinateGroup.exp

expand def

One effective expansion by undirected internal edges. · OAI.FiniteAlgebraicEnvelopes.Compiler.expand

expand def

Expand the whole target and pull every fibre back through its true label. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.expand

expand def

Replace each oriented edge by a prescribed genuine edge-path. Endpoints are enforced in the type, thereby preserving closedness exactly. · OAI.HyperbolicObstruction.GraphWordFilling.expand

expand def

Each elementary dart has its own retained old side, with the two radial copies kept separately until the final contraction. · OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.expand

expand def

Expand every macro-edge, preserving the ordered path occurrence data. · OAI.TorsionFreeZeroDivisors.SuppressedMoore.expand

expandColumnRuns def

The first bit marks an imperfect position; the second begins a new perfect run. Repetition consumes no extra run label. · OAI.TwoPointCorrelations.expandColumnRuns

expandedFractionValuation def

A genuine monomial valuation on a fraction field, constructed from an injective formal-coordinate expansion of its local ring. · OAI.CartierSections.expandedFractionValuation

ExpandedPathSystem structure

The nontrivial chains of a path system, after expanding assigned paths. · OAI.CycleClique.Construction.ExpandedPathSystem

expandedPrimeValues def

Unused internal coordinates start at one; each is overwritten before use. · OAI.Ostmann.expandedPrimeValues

expandedScheduledTemplate def

Actual atoms may have several prime constituents. An erased pivot is replaced by its single reconstructed total; all other atoms retain their lists. · OAI.Ostmann.expandedScheduledTemplate

expandingBilinearProduct def

The exact Y_L product is continuous bilinear, with norm bounded independently of L. · OAI.DefocusingNLS.expandingBilinearProduct

expandingCoefficientCLM def

Physical coefficient evaluation at a fixed radius is continuous linear. · OAI.DefocusingNLS.expandingCoefficientCLM

ExpandingCompactApproximation def

Uniform eventual approximation in the actual expanding norm by sampled compact functions. · OAI.DefocusingNLS.ExpandingCompactApproximation

expandingFourierCoefficient def

Physical Fourier coefficients for a vector whose ℓ² norm is the exact Y_L norm. · OAI.DefocusingNLS.expandingFourierCoefficient

expandingFreeStep def

The free moving-scale operator, including the scalar similarity factor. · OAI.DefocusingNLS.expandingFreeStep

expandingLinearReaction def

The real-linear potential enters with the exact Schrödinger factor -i. · OAI.DefocusingNLS.expandingLinearReaction

expandingObservationVector def

Inverse weights form an ℓ² vector with a uniform norm as the torus expands. · OAI.DefocusingNLS.expandingObservationVector

expandingOddPower def

The Fourier realization of the scalar polynomial |u|^(2m) u. · OAI.DefocusingNLS.expandingOddPower

expandingPhysicalLocalization def

χ(y/L) times the genuine continuous expanding-torus function. · OAI.DefocusingNLS.expandingPhysicalLocalization

expandingProduct def

Multiplication closes with the exact expanding-torus Fourier weight. · OAI.DefocusingNLS.expandingProduct

expandingProductCoefficient def

The physical coefficients of the product are the discrete convolution. · OAI.DefocusingNLS.expandingProductCoefficient

expandingProductMajorant def

The two unweighted Young convolutions which dominate the weighted product. · OAI.DefocusingNLS.expandingProductMajorant

expandingProfileReaction def

The actual real-linearized odd-power reaction along a moving profile. · OAI.DefocusingNLS.expandingProfileReaction

expandingRadiusCurve def

The radius follows exactly the manuscript's moving family L exp(t/2). · OAI.DefocusingNLS.expandingRadiusCurve

expandingScaleTransfer def

Continuous complex-linear transfer with the physical coefficients fixed. · OAI.DefocusingNLS.expandingScaleTransfer

expandingSobolevWeight def

The positive Fourier weight whose ℓ² norm is exactly the manuscript's Y_L norm. · OAI.DefocusingNLS.expandingSobolevWeight

ExpandingThrough def

Expansion restricted to the dimensions used by the sixteen small-subspace maps. · OAI.Kaplansky.ExpandingThrough

expandingToSobolev def

The physical Fourier coefficients are unchanged; only their weights change. · OAI.DefocusingNLS.expandingToSobolev

expandingWeightUnit def

Two-sided inverse of the canonical radius-one identification. · OAI.DefocusingNLS.expandingWeightUnit

expandSamples def

Independent complete samples: descendants, exits, and old coordinates. · OAI.IndependentProducts.expandSamples

expansion def

A representation with no repetitions is also one of the arbitrary countable representations, by placing all its coefficients in repetition row zero. · OAI.DiamondDistortion.StartModel.expansion

ExpansionClosed def

Head expansion, with exact typing and SN of every annotation/spine component. · OAI.PureTypeSystem.Candidates.ExpansionClosed

ExpansionPrinciple def

The parameter order needed from KMS, including a nonempty dense interval. OPEN: no inhabitant of this proposition is supplied. In particular r and alpha must be fixed before ell, and the ambient threshold may then depend on ell. A … · OAI.MaxCutGames.Inverse.KMS.ExpansionPrinciple

ExpansionPrinciple def

The parameter order needed from KMS, including a nonempty dense interval. The parameters r and alpha must be fixed before ell, and the ambient threshold may then depend on ell. A bound with alpha = 2^(-ell) does not meet this … · OAI.UniqueGamesTheorem.Inverse.KMS.ExpansionPrinciple

expansionRatios def

The two finite sets whose maxima define distortion. · OAI.TreeEdit.BinaryLower.expansionRatios

expansionValuation def

Pull back a formal monomial valuation along an expansion homomorphism. · OAI.CartierSections.expansionValuation

expCurve def

The actual one-parameter subgroup generated by a skew real matrix. · OAI.ArnoldCounterexample.CriticalBound.expCurve

expCut def

Actual Schwartz representatives of the exponential physical fields on a bounded region. No temperate behavior of the exponential is assumed. · OAI.ElasticityCGO.expCut

expectation def

Expectation in the unpinned finite Ising law. · OAI.BufferedIsing.expectation

expectation def

The trace-preserving expectation, constructed by weak compactness. · OAI.KadisonKastler.TraceQuotientMap.expectation

expectationCLM def

The constructed expectation is a bounded linear map. · OAI.KadisonKastler.TraceQuotientMap.expectationCLM

expectationConstant def

A single constant works for small disks, large disks, and the atom at zero. · OAI.BoltzmannNonuniqueness.TransverseAverage.expectationConstant

expectationVector def

Expectation vector of a cluster observable at the listed vertices. · OAI.HyperedgeComparison.expectationVector

Expected def

Expected types include unsorted literal sorts (the regularity alternative). · OAI.PureTypeSystem.Expected

expected def

Independent unbiased tapes are sampled at consecutive epochs. The actual entering configuration is retained as random state, never reset to u. · OAI.UniformKServer.ComputedSuffix.expected

expected def

Independent unbiased tapes are sampled at consecutive epochs. The actual entering configuration is retained as random state, never reset to u. · OAI.UniformKServer.OffsetSuffix.expected

expectedCopies def

Expected number of actual unlabelled non-induced copies in G(n,p). · OAI.LeanBlast.SecondKahnKalai.expectedCopies

expectedCost def

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

expectedCost def

Exact finite expected total movement against an oblivious input. · OAI.KServer.expectedCost

expectedEmbeddingOfStarAlgEquiv def

An algebra equivalence gives mutually inverse contractive expectation maps. · OAI.BoundedHochschild.expectedEmbeddingOfStarAlgEquiv

ExpectedMatrixSubfactorModel structure

Only the expected matrix subfactor data needed by preparation. The right action, neighboring inclusion and all estimates are constructed by the application. · OAI.KadisonKastler.ExpectedMatrixSubfactorModel

expectedTrace def

The functional obtained by composing a finite trace and an expectation. · OAI.KadisonKastler.expectedTrace

expFlow def

The genuine exponential flow in the unitary group. · OAI.KervaireHaarFlow.expFlow

explicitBarComputesDerivedTensor def

The literal arbitrary-bimodule two-sided bar computes genuine derived tensor of a module. There is no flatness assumption or ordinary tensor-power replacement. · OAI.DerivedBar.BimoduleTensor.explicitBarComputesDerivedTensor

explicitBarTotal def

The explicit two-sided total bar on a nonnegative chain complex. · OAI.DerivedBar.BimoduleTensor.explicitBarTotal

explicitBlockDifferential def

Literal multibar faces on the direct sum of actual tensor blocks, with the [r] sign. Only the degreewise tensor decomposition is used for coordinates. · OAI.DerivedBar.Multibar.Indexed.explicitBlockDifferential

explicitBoundaryRoeRepresentative def

A concrete class in the same reduced Roe algebra used by the conditional assembly diagram. Canonical assembly identification is not presumed here. · OAI.CoarseAssembly.explicitBoundaryRoeRepresentative

explicitCircleFamily def

The particular product class needed by the counterexample is an actual cycle. · OAI.CoarseAssembly.explicitCircleFamily

ExplicitFailureAt def

An actual finite partite uniform hypergraph witnessing strict failure of Ryser's inequality. · OAI.RyserOdd.Specification.ExplicitFailureAt

explicitGauge def

A fixed, deterministic continuous nondecreasing completion of the explicit exact Hausdorff gauge. · OAI.SLEExactGauge.explicitGauge

ExplicitInput structure

`ExplicitInput` packages the number of vertices `n`, number of edge copies `m`, connectivity parameter `k`, and an actual `MultiGraph n m`. · OAI.AlgorithmicThinTrees.ExplicitInput

explicitMatrix def

First block: three first-cell columns. Second block: two rows and two columns of the second cell; same-kind and mixed-kind entries differ. · OAI.DistinctLifts.explicitMatrix

explicitMultibar def

The independent recursive multibar. Every new block uses the explicit endpoint-minus-tail horizontal differential and the standard vertical total sign. · OAI.DerivedBar.explicitMultibar

explicitTesterReject def

One finite uniform sample space for the executable six-address test. · OAI.MaxCutGames.Foundations.PCP.AssignmentTester.explicitTesterReject

explicitTesterReject def

One finite uniform sample space for the executable six-address test. · OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.explicitTesterReject

explicitToAddress def

This inverse is a proof adapter only; the output constructor never calls it. · OAI.MaxCutGames.Decoder.TableKeysAddressGame.explicitToAddress

explicitToAddress def

Proof adapter only: the output constructor does not call this inverse. · OAI.MaxCutGames.Reduction.AddressGame.explicitToAddress

explicitToAddress def

This inverse is a proof adapter only; the output constructor never calls it. · OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.explicitToAddress

explicitToAddress def

Proof adapter only: the output constructor does not call this inverse. · OAI.UniqueGamesTheorem.Reduction.AddressGame.explicitToAddress

explicitVertexCount def

Exhaustive numbering of the same single-orbit vertex type. · OAI.MaxCutGames.Decoder.TableKeysGame.explicitVertexCount

explicitVertexCount def

Exhaustive numbering of the same single-orbit vertex type. · OAI.UniqueGamesTheorem.Decoder.TableKeysGame.explicitVertexCount

explicitVertexEquiv def

Executable vertex numbering from an exhaustive list, preserving the same realizable-body subtype used in the semantic statements. · OAI.MaxCutGames.Reduction.ActualOrbit.explicitVertexEquiv

explicitVertexEquiv def

Executable vertex numbering from an exhaustive list, preserving the same realizable-body subtype used in the semantic statements. · OAI.UniqueGamesTheorem.Reduction.ActualOrbit.explicitVertexEquiv

explorationActivity def

Number of forced bridge/loop decisions along the branch belonging to T. The next edge may depend on the entire previous partial branch, but not T. · OAI.FKCRT.explorationActivity

expMap def

Pointwise exponential of a continuous complex-valued function. · OAI.KervaireSpectral.expMap

ExpO def

Subexponential upper bound at scale n. · OAI.HadwigerCounterexample.ExpO

exponent def

This recursive sum is exactly Σⱼ (r-j)iⱼ. · OAI.DerivedBar.Multibar.exponent

ExponentBound def

The quantified dimension-exponent upper bound with every positive exponent slack. · OAI.LogConcaveSampling.ExponentBound

ExponentCode structure

A finite integer exponent matrix, with its dimensions retained. · OAI.MUB6.Certificate.ExponentCode

exponentCup def

The cup product of two integral exponent homomorphisms. · OAI.EilenbergGanea.exponentCup

Exponential def

A single exponential with a polynomial exponent (not an iterated exponential). · OAI.WLIdentification.ComputationBounds.Exponential

exponential def

An arbitrary complex linear frequency gives a genuine global smooth exponential on the physical real space. · OAI.ElasticityAugmented.exponential

exponential def

The polynomial exponential is a coefficient-field algebra homomorphism. · OAI.StableCoordinate.LNDExponential.exponential

exponentialAction def

The algebraic additive action corresponding to a locally nilpotent derivation. · OAI.StableCoordinate.exponentialAction

exponentialConjugate def

Conjugation through the intrinsic exponential as a bijection. · OAI.PolycyclicRecognition.exponentialConjugate

ExponentialConjugationLaw def

The usual adjoint-exponential identity written entirely in fixed coordinates. · OAI.PolycyclicRecognition.ExponentialConjugationLaw

exponentialCoordinateBox def

The exponential image of the coordinate cube of radius R. With the supremum norm on the coordinate functions this is exactly the usual box. · OAI.PolycyclicRecognition.exponentialCoordinateBox

exponentialCoordinates def

Coordinates use the given global exponential chart and the actual chosen basis; no topology on the abstract Lie algebra is needed. · OAI.PolycyclicRecognition.exponentialCoordinates

exponentialLaw def

The density exp(-w) on the positive half-line. · OAI.IndependentProducts.exponentialLaw

ExponentialLinearRealizationInput def

Faithful linear realization with its intrinsic exponential identity. No metric distortion estimate is included. · OAI.PolycyclicRecognition.ExponentialLinearRealizationInput

exponentialLog def

The logarithm in a specified Lie-algebra realization of a bijective group exponential. · OAI.PolycyclicRecognition.exponentialLog

exponentialPartialProduct def

The ordered product of the first m exponential increments. · OAI.PolycyclicRecognition.exponentialPartialProduct

exponentialProductLieModel def

The product is packaged solely to instantiate the existing published input. Its measurable structure is the Borel structure of the product. · OAI.PolycyclicRecognition.exponentialProductLieModel

exponentialQuotientSection def

The prescribed linear quotient section, transported through the two actual global exponential charts. · OAI.PolycyclicRecognition.exponentialQuotientSection

exponentialRemainder def

The exponential after removing its constant and linear terms. · OAI.KadisonKastler.exponentialRemainder

exponentialRescaleBasis def

The actual rescaled basis whose structure constants are being bounded. · OAI.PolycyclicRecognition.exponentialRescaleBasis

exponentPair def

Bivariate exponent vector in coordinate order (X,Y). · OAI.Nagata.Workers.W30.exponentPair

Exponents def

Admissible exponents 0<m_1<...<m_r<1; vacuous at r=0. · OAI.DilutedSpinGlass.Exponents

exponentSet def

The complete finite exponent set: positive first blocks, positive-degree second blocks, and the possible single degree-zero block. · OAI.Nagata.FiniteExponents.exponentSet

exponentSimplex def

The simplex on which the rounding subdivision is made; no face is omitted. · OAI.CartierSections.LocalMultiplier.exponentSimplex

expose def

b=false exposes main, true exposes the first (precursor) witness (for purposes of rank). · OAI.ExactDerandomization.At.Blob.expose

exposedCoins def

Fix all previously exposed bits, leaving every other bit independent fair. · OAI.CubeShuffle.exposedCoins

exposedFirstProduct def

The first word's exposed factor, with an explicit product over the non-fresh coordinates. · OAI.Problem337.RandomExposure.exposedFirstProduct

ExposedLabel abbrev

The exposed label set. · OAI.Problem337.RandomExposure.ExposedLabel

exposedOtherProduct def

All coordinates of the second word remain exposed. · OAI.Problem337.RandomExposure.exposedOtherProduct

exposedPaths def

Precisely the switch record produced by exposing a set of complete paths. · OAI.CubeShuffle.exposedPaths

exposeEquiv def

Move the outermost pair inside all the other still-summed pairs. · OAI.ContingencyTables.IntegerWeightedTransport.exposeEquiv

Exposure structure

Every complete orbit is retained. The residual fixes EACH removed occurrence, not merely its facet rank or its boundary-component count. · OAI.IntegralCharacterVarieties.BoundaryBand.Exposure

Expr inductive

Polynomially bounded arithmetic expressions with finite bounded summation. The only inspection of the input is by actual bit-read or length macros above. Bounded sums suffice for divisions, remainder, bounded minimization and every finite … · OAI.OptimalMaxCut.CounterMachine.Expr

Expr inductive

A finite, first-order word language. Loops capture a word length; their body sees both a unary iteration index and the previous accumulator. · OAI.WLIdentification.WordExpressions.Expr

Expression inductive

A sum of monomials. Jet factors are independent of the angular variable. · OAI.ClosedSurfaceR4.JetPolynomial.Expression

exprPackP def

Compiler runs in polynomial time in the expanded source syntax, dimensions and input networks. The environment contains no circuit-generation oracle. · OAI.ExactQuantumFactoring.NetworkEmission.Emission.exprPackP

ExprToken abbrev

Variables, scalar constants, and the fixed algebra instruction vocabulary. · OAI.ExactQuantumFactoring.NetworkEmission.ExprToken

ExpSmall def

Exponentially small at scale n. · OAI.HadwigerCounterexample.ExpSmall

expSub def

utilities (exp evaluation an external input) · OAI.GeneralMahler.Jet.expSub

expU def

Uniform probability average. · OAI.FourierLLogL.Dyadic.expU

extend def

Pull a corner cochain back along central compression. · OAI.BoundedHochschild.CentralCorner.extend

extend def

The original bottom/top chord trace, with two fresh disjoint rows. · OAI.CriticalHoneycomb.FiniteContinuation.extend

extend def

Constant continuation is used only to state derivatives within the closed time slab. · OAI.ForcedComputation.CoefficientTimeJets.extend

extend def

Genuine cubical homotopy extension, constructed by the explicit prism retraction. No extension or cellular-approximation premise is used. · OAI.HyperbolicObstruction.CubicalHomotopyExtension.extend

extend def

The complete square prism is extended, not merely its boundary class. · OAI.HyperbolicObstruction.SquareBoundaryExtension.Data.extend

extend def

Diagonal extension of a corner operator through matrix-unit coordinates. · OAI.KadisonSimilarity.FullColumnCoordinates.extend

extend def

Given the new stalk and its outgoing commuting squares, all new incoming edges are forced by the scalar quotient rule. · OAI.KLInvariance.MomentGraph.Sheaf.OnIso.extend

extend def

A finite extension with a normalized kernel retains the entire old state. · OAI.KServer.TreeRounding.Law.extend

extend def

Extend a tape on legal coordinates by false on every other coordinate. · OAI.MaxCutGames.Foundations.PCP.UniformRestriction.extend

extend def

Any continuous model map extends uniquely over the completed algebra. · OAI.NuclearUltrapower.UniversalCompletion.extend

extend def

Extend actual data on the finite parameters by its small colimit. · OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.extend

extend def

The strict extension of a functor from the actual zero fibre. · OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.extend

extend def

Homotopy extension for a genuine disk attachment with arbitrarily many cells. Currying into the compact-open path space respects the weak topology. · OAI.TorsionFreeZeroDivisors.AttachmentHEP.extend

extend def

Extend a tape on legal coordinates by false on every other coordinate. · OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.extend

extendActive def

Extend an arbitrary function on the active positions by zero. · OAI.MaxCutGames.Soundness.PartnerProjection.extendActive

extendActive def

Extend an arbitrary function on the active positions by zero. · OAI.UniqueGamesTheorem.Soundness.PartnerProjection.extendActive

extendAssignment def

A computable assignment extension: finite-sum splitting and quotient/remainder decoding recover the event, pattern, and auxiliary-bit indices. · OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.extendAssignment

extendAssignment def

A computable assignment extension: finite-sum splitting and quotient/remainder decoding recover the event, pattern, and auxiliary-bit indices. · OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.extendAssignment

extendBaseEquiv def

Append one real base coordinate, placing it first in Fin (k+1). · OAI.AffineBernstein.extendBaseEquiv

extendBitBlocks def

Extend selected blocks by zero bits outside the selection. · OAI.TwoPointCorrelations.extendBitBlocks

extendBlockPerm def

A permutation of a block, extended by the identity away from the block. · OAI.Problem313.extendBlockPerm

extendCoeff def

Zero extension, including the root; longer path sums freeze at height n. · OAI.BoundedTreePotentials.BlockCalculus.extendCoeff

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

extendComplex def

The final complex-linear extension, with no change of bound. · OAI.KadisonKastler.RationalComplexCore.extendComplex

extendComponent def

Add the untouched small components to a separator of the unique large component. The original deletion set and hence its sharp cost are retained. · OAI.TorsionFreeZeroDivisors.PlanarMap.extendComponent

extendCorner def

Extension of the corner change of basis to the actual bordered pencil. · OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendCorner

extended def

The new closure: keep the activated earlier closure and append β. · OAI.SeparableQuotient.CoherentClosures.extended

extendedBranch def

A local branch extended by a fixed value outside its source. · OAI.Problem356.LocalBranchMeasure.extendedBranch

extendedChartForm def

The oriented pullback, extended by zero outside the actual chart target. · OAI.MahlerStokes.extendedChartForm

extendedCut def

An arbitrary total extension is only used at valid cut indices. · OAI.Problem326.Affine.extendedCut

extendedEntropyProduction def

Lower semicontinuous extension of (A-B) log(A/B) on the nonnegative quadrant. The off-quadrant value is immaterial for nonnegative densities. · OAI.BoltzmannNonuniqueness.extendedEntropyProduction

extendedFunctional def

The continuous scalar functional associated with a core input. · OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.extendedFunctional

extendedKernel def

Extended expectation kernel, infinite on degenerate transverse slices. · OAI.BoltzmannNonuniqueness.GeometricSlice.extendedKernel

extendedLocalizationEquiv def

Complex-linear localization coordinates, with exactly n−1 independent polynomial variables and the original Laurent coefficient ring. · OAI.AbhyankarSathaye.CommutingDerivations.extendedLocalizationEquiv

extendedMarkedGood def

The stopped marked state at a finite extended stopping time. · OAI.SLEExactGauge.extendedMarkedGood

extendedMarkedPoints def

The concrete original marks together with the one extra point. · OAI.Nagata.W06.LineArrangement.extendedMarkedPoints

extendedPower def

The scalar line singularity retains its infinite value on a zero-distance slice. · OAI.BoltzmannNonuniqueness.GeometricSlice.extendedPower

extendedRees def

The coefficient realization of the extended Rees algebra R[T,I/T]. · OAI.StableCoordinate.ModificationPieces.extendedRees

extendedRelativeLocalizationEquiv def

The all-dimensional equivalence fixes precisely the specified Laurent coefficient map, as an actual relative algebra equivalence. · OAI.AbhyankarSathaye.CommutingDerivations.extendedRelativeLocalizationEquiv

extendedSimplexModelNatIso def

Naturality is inherited from the actual global comparison. · OAI.Thomason.Construction.NormalizedSimplexIdentities.extendedSimplexModelNatIso

extendedStmt def

Add one finite scratch register while preserving each raw transition. · OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.extendedStmt

extendedStmt def

Add one finite scratch register while preserving each raw transition. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.extendedStmt

ExtendedTrace structure

Extended lower semicontinuous traces, with no finiteness restriction. · OAI.TraceConeClassification.ExtendedTrace

extendedVertex def

Extending the source idempotents by zero keeps all right ideals in the same C. · OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.extendedVertex

extendEncoding def

The actual four-register completion, when the ordinary preparation has retained and injectively encoded its full history. · OAI.ExactQuantumFactoring.Completion.extendEncoding

extendEtale def

A derivation extends uniquely along any formally étale algebra. · OAI.Derivation.extendEtale

extendFacets def

Add the named fresh facet fibres before their boundary grafting. No old surface, orientation, side, rank or boundary ordering is modified. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.extendFacets

Extendible def

The current forest is contained in some globally optimal forest. · OAI.ContingencyTables.MaximumForestExchange.Extendible

extendKept def

Extend a coloring from the vertex-DELETED graph. The values at deleted vertices are immaterial: every incident edge is absent from keptEdges. · OAI.BufferedIsing.extendKept

extendLabeling def

A computable extension uses label zero on every dummy vertex. · OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling

extendLabeling def

The extension is only used as a semantic witness, not by the instance constructor. · OAI.MaxCutGames.Integration.VertexEmbedding.extendLabeling

extendLabeling def

A computable extension uses label zero on every dummy vertex. · OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.extendLabeling

extendLabeling def

The extension is only used as a semantic witness, not by the instance constructor. · OAI.UniqueGamesTheorem.Integration.VertexEmbedding.extendLabeling

extendOnScales def

Extend the data by a fixed value outside the sampled scales. · OAI.PolycyclicRecognition.extendOnScales

extendPath def

Constant continuation beyond the endpoints gives a global bounded continuous source. · OAI.ForcedComputation.WeaklySingular.extendPath

extendPerm def

Extend a permutation of the free slots by the identity on the exceptions. · OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.extendPerm

extendPrefix def

Coordinates indexed from one, extended by zero outside the prefix. · OAI.TotientAsymptotic.extendPrefix

extendPrefix def

Total extension of a node prefix to a full leaf path. Its unused tail is irrelevant to every vector at the depth of that prefix. · OAI.TreeEdit.BinaryLower.FiniteTree.extendPrefix

extendQuery def

Proof-only comparison map: extend the original legal-coordinate addresses. The executable query function above never calls this map. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.extendQuery

extendQuery def

Proof-only comparison map: extend the original legal-coordinate addresses. The executable query function above never calls this map. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.extendQuery

extendRational def

Extend a bounded rational-linear map on the dense core. · OAI.KadisonKastler.RationalComplexCore.extendRational

extendRestricted def

Extending by false gives a unique padded address to a restricted query. · OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.extendRestricted

extendRestricted def

Extending by false gives a unique padded address to a restricted query. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.extendRestricted

extendRow def

Only actual positions index rows; this extension is a device for reading an oriented word and cannot introduce duplicate row occurrences. · OAI.HyperbolicObstruction.ConeSkeleton.extendRow

Extends def

Augmented holes retain the ordered first h trajectories exactly. · OAI.CoordinateSweeps.Grid.Holes.Extends

extendSelfMap def

An explicit ambient representative of a subtype self-map. Its values outside the subtype are immaterial; only continuity on that subtype is used. · OAI.Tingley.extendSelfMap

extendSupportedPolicy def

Extend a policy defined on supported private questions to a total local answer function. The support decision uses only the displayed question. · OAI.MaxCutGames.Clean.AnswerBridge.extendSupportedPolicy

extendSupportedPolicy def

Extend a policy defined on supported private questions to a total local answer function. The support decision uses only the displayed question. · OAI.UniqueGamesTheorem.Clean.AnswerBridge.extendSupportedPolicy

extendValue def

A Lipschitz scalar on one intrinsic component, continued constantly on the other components, is a genuine vertical/switch-compatible field. · OAI.PlanarL1.Columns.Model.Point.extendValue

extendValues def

Extend finite equivariant vertex data by zero outside the invariant complex. · OAI.SharpLiebThirring.CubeFlags.extendValues

extendWeights def

Extend finite weights by zero, only to use natural-number prefix sums. · OAI.LipschitzHilbert.extendWeights

extendWord def

Append a prescribed increment, with irrelevant later increments fixed to it. · OAI.PolycyclicRecognition.extendWord

Extension abbrev

The genuine monic cyclotomic quotient, with no additional ring-data premise. · OAI.CirculantHadamard.RamifiedLocal.Extension

Extension abbrev

The unnormalized fiber of extensions of one compressed frequency. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.Extension

Extension abbrev

The domain of the extension is a quotient of a set of internal name codes. · OAI.PartitionConsistency.ForcingQuotient.AtomicData.Extension

Extension abbrev

The compact source extension is nonvacuous for the actual balanced, shift-separated, symplectically constrained recursively selected hierarchy. · OAI.SmoothObstruction.WordHierarchy.Extension

Extension abbrev

The unnormalized fiber of extensions of one compressed frequency. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.Extension

extension def

Executing a request uses the established literal normal forms. · OAI.PartitionConsistency.MonoidConstruction.ProbeData.extension

extension def

The actual unconditional extension, with the original radial function. · OAI.Tingley.extension

extension def

Literal homotopy extension for a cell, with no fibrancy premise. · OAI.TorsionFreeZeroDivisors.CellHEP.extension

extensionCoaugmentation def

The mate of a last-vertex transformation under the actual subdivision adjunction. Its components are the canonical maps to extension; their being weak equivalences remains a separate published input. · OAI.Thomason.Construction.extensionCoaugmentation

ExtensionCopy abbrev

Actual distinct extensions of the observed predecessor. Histories in a tree may index this same family separately; this type never merges histories. · OAI.LeanBlast.SecondKahnKalai.ExtensionCopy

extensionCylinder def

The natural comparison from the cylinder on Ex X into Ex of the cylinder on X. · OAI.Thomason.Construction.extensionCylinder

extensionEmbedding def

A faithful map of the original nonsplit extension into the group with completed nilpotent kernel and unchanged quotient. · OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.extensionEmbedding

extensionEquiv def

Specifying the value on the complementary block gives every extension exactly once. This will give the cardinality factor |Hom(C,W)|. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.extensionEquiv

extensionEquiv def

Specifying the value on the complementary block gives every extension exactly once. This will give the cardinality factor |Hom(C,W)|. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.extensionEquiv

extensionEvalIso def

Evaluation of extension at an index in its image is the original evaluation, naturally on all complexes and chain maps. · OAI.DerivedBar.extensionEvalIso

extensionEvaluationIso def

Evaluation of extension is represented by the actual subdivided simplex. · OAI.Thomason.Construction.extensionEvaluationIso

extensionFactorMap def

The original and completed factor systems agree on the kernel lattice. · OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.extensionFactorMap

ExtensionGood structure

The closure conditions at a new endpoint, relative to earlier closures. · OAI.SeparableQuotient.CoherentClosures.ExtensionGood

extensionHeightCost def

Source lem:mono-probe-heights: admissible heights and costs on the actual indexed probe extension, constructed by its normal forms and gates. · OAI.PartitionConsistency.ProbeAlgebra.Path.extensionHeightCost

extensionHomotopy def

Applying actual extension to both endpoints of a simplicial homotopy produces a simplicial homotopy. · OAI.Thomason.Construction.extensionHomotopy

extensionIterate def

Sum over all sequential genuine fresh-extension histories, with their signed products. This is not a law chosen to force the expansion. · OAI.DilutedSpinGlass.PrescribedTree.extensionIterate

extensionLangMap def

The twisted difference on the kernel, with the order needed for correcting left coset representatives. · OAI.PolycyclicRecognition.extensionLangMap

extensionLaw def

The uniform law on actual copies extending S, with positivity justified by the actual containment event. · OAI.LeanBlast.SecondKahnKalai.extensionLaw

extensionLocalizer def

The actual extension functor preserves realization weak equivalences. · OAI.Thomason.Construction.extensionLocalizer

extensionObjIso def

The extension is computed on the actual category of parameters over C. · OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.extensionObjIso

Extensions abbrev

One-dimensional extensions of a subspace. · OAI.MaxCutGames.Inverse.MatrixChart.Extensions

Extensions abbrev

One-dimensional extensions of a subspace. · OAI.UniqueGamesTheorem.Inverse.MatrixChart.Extensions

extensionsEquivLines def

The quotient correspondence identifies extensions with quotient lines. · OAI.MaxCutGames.Inverse.MatrixChart.extensionsEquivLines

extensionsEquivLines def

The quotient correspondence identifies extensions with quotient lines. · OAI.UniqueGamesTheorem.Inverse.MatrixChart.extensionsEquivLines

extensionShift def

Restriction to the genuine closed phase extension, in both directions. · OAI.SmoothObstruction.PhaseDynamics.extensionShift

extent def

volume of the first j axes · OAI.PowerSaving.Grove.extent

exterior def

The exterior power as a continuous operator on the canonical inner product space. · OAI.SmoothObstruction.ExteriorStability.exterior

exteriorBoundary def

The outside word is an arbitrary closed edge path, not an attaching word of a cell of the target. Its second orientation is solely bookkeeping. · OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget.exteriorBoundary

exteriorCellToWalk def

Transfer keeps the raw diagram and arbitrary outside word literally, while opening top polygon steps to the checked cone surgeries. · OAI.HyperbolicObstruction.ConeSkeleton.exteriorCellToWalk

exteriorCoeff def

Real physical coefficients and pointwise inverses are the actual smooth coefficients in the distribution formulation. · OAI.ElasticityDistribution.exteriorCoeff

ExteriorCoefficients abbrev

The exterior algebra on a freely specified set of generators. · OAI.PixtonChow.ExteriorCoefficients

ExteriorCutoff def

Every exterior count below the cutoff is zero. The cutoff is chosen from the actual finite family, independently of the harmonic minimum. · OAI.HarmonicArtin.ParabolicIntersections.ExteriorCutoff

ExteriorOmittedAreaBound def

The specialization of the published exterior area bound needed here. The map is evaluated only outside the closed source disk. Univalence and principal normalization are the hypotheses needed to obtain this bound from the exterior area … · OAI.CircleDomainRigidity.ExteriorOmittedAreaBound

ExteriorPorts structure

Actual disjoint exterior polygonal stems, not a promised contour order. · OAI.PlanarL1.Topology.ExteriorPorts

exteriorToDisk def

Radial inversion fixes the unit circle and puts the exterior into the disk. This avoids any one-point-compactification assumption in the complementary region of a prospective tree neighborhood. · OAI.PlanarL1.Topology.exteriorToDisk

externalHistory def

The actual old full reservoir is tilted first; the constrained history then samples only its physical paths, with no fresh prior marks left. · OAI.DilutedSpinGlass.UniversalDictionary.externalHistory

externalLineEquiv def

An external integer coordinate is unrestricted; the second coordinate is still a unit. · OAI.Ostmann.externalLineEquiv

externalTreeScore def

The old reservoir and the new insertion factor are distinct arguments. Keeping old fixed is essential when extracting a single analytic function from the entire countable dictionary of insertion parameter values. · OAI.DilutedSpinGlass.HeterogeneousMarks.externalTreeScore

extra def

Additional unlabelled steps after exit, continuing with a piece frozen. · OAI.FourierLLogL.Dyadic.Procedure.Wire.extra

Extract inductive

Remove an occurrence accessible from the left through independent letters. This retains the actual other occurrences, not merely their group value. · OAI.EilenbergGanea.TraceWords.Extract

extract def

Slotwise projection back to the prescribed tensor; this proves no tensor relations were lost. · OAI.DerivedBar.Multibar.extract

extract def

Extract the unique coordinates from an actual compressed-fiber element. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.extract

extract def

Extract the unique coordinates from an actual compressed-fiber element. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.extract

extractedSimplexCondition def

The weaker, unclamped simplex used in equation ford-simplex of the manuscript. · OAI.TotientAsymptotic.extractedSimplexCondition

extractInput def

Port-family checks applied after the full existing graph-table validation. · OAI.MaxCutGames.Foundations.PCP.PortTables.extractInput

extractInput def

Port-family checks applied after the full existing graph-table validation. · OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.extractInput

extractionProbe def

The exact probe sequence of pert:parameters, indexed from zero. · OAI.DilutedSpinGlass.extractionProbe

ExtraDart def

Each orientation is one distinct new branch incidence. Paired incidences are not identified until the column switch is installed. · OAI.PlanarL1.Weighted.ExtraDart

extraLabelAverage def

The complete bits law is arbitrary. All extra-leaf offsets may be mutually correlated and correlated with the retained forced-anchor kernel. Only the extra leaf label variables themselves are summed here. · OAI.TraceReconstruction.extraLabelAverage

extraLabelsEquiv def

Extra bottom labels are separated from all nonleaf labels without introducing any T₁ factor. · OAI.TraceReconstruction.OccupiedParityTree.Forced.extraLabelsEquiv

extraLineEvent def

A direct finite constraint event on one line for the extra particles. · OAI.CoordinateSweeps.Grid.extraLineEvent

extraOffsets def

Offsets for all extra leaf constraints, with only their labels replaced by zero. The location of each constraint is not changed by that replacement. · OAI.TraceReconstruction.OccupiedParityTree.Forced.extraOffsets

extraPoint def

A countably infinite explicit sequence of extra points on component zero. · OAI.Nagata.W06.LineArrangement.extraPoint

extraPrimeExponent def

The additional-prime exponent. · OAI.LowSpaceSubsetSum.extraPrimeExponent

extraPrimeParameter def

The actual integer sampling parameter, including both floors. · OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeParameter

extraPrimeRate def

This is the manuscript's maximum over the three ordered mixers. · OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeRate

ExtraPrimeSpace abbrev

The extra-prime draw is uniform on the concrete prime range. · OAI.LowSpaceSubsetSum.RepresentationSetup.ExtraPrimeSpace

extraProbability def

Product form of the exact conditional endpoint probability. The bridge to the original conditioned sweep event is proved below, not assumed. · OAI.CoordinateSweeps.Grid.Holes.extraProbability

extraTrialLaw def

The prime is drawn after the earlier layout, families, nested primes, and low residues; its law depends only on the prescribed layout parameter. · OAI.LowSpaceSubsetSum.RepresentationSetup.extraTrialLaw

extreme def

all b steps child · OAI.FourierLLogL.Dyadic.Procedure.extreme

extrusionMap def

A shear of the cube followed by translation by the ith unit vector. · OAI.DiagonalZonotope.extrusionMap

extWord def

Single fully augmented Boolean-word lookup. Compute word-valued rules coordinate by coordinate this way. · OAI.Fifths.Modulus.extWord

exWitness def

Adding a fresh local witness is consistent when existence is derivable. This is justified by the eigenvariable rule, not by a model assumption. · OAI.PartitionConsistency.Completeness.Condition.exWitness

E₀ def

The parameter-independent and linear parts of the actual scaled derivative. · OAI.ElasticityBoundaryParameter.E₀