Glossary: I

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

I abbrev

The coordinates and Cohen length specified in the source. · OAI.PartitionConsistency.ConcreteSystem.I

I def

Closed form of the integral of M'(a)^2 over [1,z], or zero below 1. · OAI.PettyProjection.Scalar.I

ID abbrev

Types used by the spine of the system. · OAI.ExactDerandomization.Helix.ID

ideal def

The prime ideal (2) in the integers. · OAI.CirculantHadamard.IntegerTwoLocal.ideal

ideal def

eB, represented in the opposite regular module to encode right linearity. · OAI.LittleFinitistic.VertexProjectives.ideal

idealAction def

The multiplication morphism for a line ideal inside the structure sheaf. Its kernel and cokernel are the Cartier Tor and restriction objects. · OAI.ActualSheafTensor.idealAction

idealBaseChange def

The canonical morphism from the pulled-back ideal to the ideal. · OAI.SourcePullbackChart.idealBaseChange

idealCharacterCoeff def

Real ideal coefficients evaluated against a character of primary Eisenstein elements. · OAI.CubicFirstMoment.idealCharacterCoeff

idealCutoff def

The ideal state at a cutoff immediately after a whole block has switched. · OAI.ReflexiveFixedPoints.TreeEvaluation.idealCutoff

idealDirichletTail def

The tail is the tail of the full ideal series, with all Euler factors. · OAI.CubicFirstMoment.idealDirichletTail

idealEmbed def

Literal insertion of a leading X and its following D block. · OAI.DerivedBar.ParityBridge.idealEmbed

idealEquiv def

Match the opposite-regular presentation of eB to the fixed-point presentation. · OAI.LittleFinitistic.ConcreteTensorEvaluation.idealEquiv

idealExponentGenerator def

A generator of the ideal represented by its prime exponent vector. · OAI.CubicFirstMoment.idealExponentGenerator

idealExponentOf def

The exponent vector of every nonzero Eisenstein principal ideal. · OAI.CubicFirstMoment.idealExponentOf

idealLayers abbrev

The coherent layers of the ideal-adic image filtration. · OAI.ActualCartier.idealLayers

idealMoebiusSeries def

The ideal Möbius function, characterized as the Dirichlet inverse of the constant-one arithmetic function. · OAI.CubicFirstMoment.idealMoebiusSeries

idealMultiple abbrev

Repeated images of the Cartier ideal action on a coherent sheaf. · OAI.ActualCartier.idealMultiple

idealOrderIso def

The actual ideal-poset isomorphism induced by a cone equivalence. · OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso

idealOutput def

The ideal cutoff immediately after the current descendant block switches. · OAI.ReflexiveFixedPoints.CandidateLedger.idealOutput

idealPrimaryGenerator def

Canonical primary generator on the ideals prime to three. We use it only for exponent vectors below an actual primary principal ideal. · OAI.CubicFirstMoment.idealPrimaryGenerator

idealReferenceLaw def

The ideal reference draw is transported from the nonempty physical completion fibre, so no additional existence assumption is needed. · OAI.ContingencyTables.SmallGraphProfiles.idealReferenceLaw

idealRestrictionIso def

The kernel ideal of the closed morphism commutes with actual restriction, by preservation of kernels and the structure-map square. · OAI.ActualCartier.idealRestrictionIso

idealSheaf def

The ideal sheaf of a closed immersion, defined as a sheaf kernel. · OAI.ActualCartier.idealSheaf

idealSuffixEmbed def

Literal X coefficient followed by any D block and any recursive suffix. · OAI.DerivedBar.ParityBridge.idealSuffixEmbed

idealVonMangoldt def

The usual convolution definition of the ideal von Mangoldt function. · OAI.CubicFirstMoment.idealVonMangoldt

IdempotentTrace def

Precisely the additive idempotents, not a chosen subclass of traces. · OAI.TraceConeClassification.IdempotentTrace

idempotentTraceEquiv def

An additive bijection of extended trace cones identifies their additive idempotents. · OAI.TraceConeClassification.idempotentTraceEquiv

IdentifiedBand structure

A named simultaneous splitting of two frames. · OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand

identifiedDyck def

The precise source identification: each type separately is a genuine Mathlib Dyck word, with no assumption about flexible marks. · OAI.FKCRT.Inventory.identifiedDyck

identifiedEndHom def

Evaluation of endomorphisms, expressed in a specified identification of the target. · OAI.LittleFinitistic.QuadraticEncoding.identifiedEndHom

Identifies def

There is no restriction to mates from a graph construction or to a selected order. · OAI.WLIdentification.Identifies

identity def

The one-term average. · OAI.KadisonKastler.FiniteInnerAverage.identity

identity def

Identity has no operation of unbounded cost. · OAI.RationalHitting.StackLanguage.Procedure.identity

identity def

Identity boundary diagram. · OAI.TwoWayComplementation.Diagram.identity

identityCoordinate def

Identity-coordinate projection on the induced Hilbert space. · OAI.NuclearUltrapower.identityCoordinate

identityDifferential def

Differential at the identity, with the codomain identified using the homomorphism's identity law. · OAI.PolycyclicRecognition.identityDifferential

identityOperatorCycle def

Any representation with the identity operator is degenerate. · OAI.CoarseAssembly.Analytic.identityOperatorCycle

identityPowerIso def

The recursively iterated identity functor is canonically the identity. · OAI.CartierImageFiltration.identityPowerIso

identityVector def

The identity vector in component i. · OAI.GroupRingDeterminant.identityVector

idx def

First grid index in a fitting node. · OAI.FourierLLogL.Dyadic.Node.idx

iid def

Independent repeated sampling, including the single empty tuple at n=0. · OAI.MaxCutGames.Foundations.Games.FiniteDistribution.iid

iid def

Independent repeated sampling, including the single empty tuple at n=0. · OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.iid

IidEnvironment structure

An independent, identically distributed edge environment with marginal law ν. · OAI.GammaFPP.IidEnvironment

iidProductLaw def

The product law of the edge weights. · OAI.GammaFPP.iidProductLaw

image def

The image has the dimension of the parameter space. · OAI.MaxCutGames.Quadratic.UniformSubspaces.image

image def

Existential projection, with the regular forcing meaning of existence. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.image

image def

The actual finite image of a finite parameter space. · OAI.TreeEdit.BinaryLower.ParameterImage.image

image def

The image has the dimension of the parameter space. · OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.image

imageAmbientEquiv def

Keep the selected first factor and split the remaining space along its prescribed compressed image. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageAmbientEquiv

imageAmbientEquiv def

Keep the selected first factor and split the remaining space along its prescribed compressed image. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageAmbientEquiv

ImageBasic def

Every actual image of a depth-n uniform cell is a basic interval. · OAI.ThompsonNonamenability.ImageBasic

imageBoundaries def

The small family consists of the literal images of simplex boundaries. · OAI.Thomason.Construction.imageBoundaries

imageCell def

The unique basic interval with the actual image endpoints. · OAI.ThompsonNonamenability.imageCell

imageClassRelation def

Graph of the representative-free correspondence h(a) ↦ [a]. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.imageClassRelation

imageCombination def

The output map of the wk possible component images. · OAI.RationalHitting.Rectangular.imageCombination

imageCoordinates def

Coordinates adapted to a prescribed image and any chosen complement. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageCoordinates

imageCoordinates def

Coordinates adapted to a prescribed image and any chosen complement. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageCoordinates

imageEquiv def

A computable numbering using idxOf; its inverse looks up that index. It involves no chosen Fintype.equivFin. · OAI.MaxCutGames.Reduction.Encoding.imageEquiv

imageEquiv def

A computable numbering using idxOf; its inverse looks up that index. It involves no chosen Fintype.equivFin. · OAI.UniqueGamesTheorem.Reduction.Encoding.imageEquiv

ImageF def

The dense local meaning of ∃x∈σ, φ(x,y). · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ImageF

imageFormula def

The image predicate, with the set-domain as one extra parameter, retaining all quantifiers of the original formula. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.imageFormula

imageHorns def

A single countable index type packages the literal images of all horns. · OAI.Thomason.Construction.imageHorns

imageInvariantMean def

An invariant mean descends along a surjective group homomorphism. · OAI.PolycyclicRecognition.imageInvariantMean

imageKernelEquiv def

Every range fibre is one translate of the same kernel. · OAI.MaxCutGames.Clean.AdviceImageLaw.imageKernelEquiv

imageKernelEquiv def

Every range fibre is one translate of the same kernel. · OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.imageKernelEquiv

imagePartition def

The actual images, with coverage and disjoint open interiors proved. · OAI.ThompsonNonamenability.imagePartition

imagePartitionOption def

The genuine partial image of the uniform partition, made total with none. · OAI.ThompsonNonamenability.imagePartitionOption

imagePiece def

The image filtration under a polynomial presentation. In particular this is the quotient filtration when φ is an ideal quotient homomorphism. · OAI.StableCoordinate.Filtration.imagePiece

imagePieceMap def

The presentation map restricted to one source filtration piece. · OAI.StableCoordinate.GradedPresentationMap.imagePieceMap

imagePullback def

The original function expressed in the adapted primal coordinates. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imagePullback

imagePullback def

The original function expressed in the adapted primal coordinates. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imagePullback

ImageRankFrequency abbrev

Frequencies of an exact rank. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency

ImageRankFrequency abbrev

Frequencies of an exact rank. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency

Images structure

General, address-dependent image consistency, as extracted from arbitrary WL mates. It is deliberately weaker than simultaneous pointwise solvability. · OAI.WLIdentification.ProductCircuit.Images

ImagesDisjointModulo def

Disjointness of the images of Q_A X|_B and Q_A Z|_B, written without quotient objects. Equality of the two cosets means their sum lies in A, in which case both cosets must be zero. · OAI.MaxCutGames.Appendix.Identities.ImagesDisjointModulo

ImagesDisjointModulo def

Disjointness of the images of Q_A X|_B and Q_A Z|_B, written without quotient objects. Equality of the two cosets means their sum lies in A, in which case both cosets must be zero. · OAI.UniqueGamesTheorem.Appendix.Identities.ImagesDisjointModulo

ImageSet def

Site-ring images are defined by all stable responses, not by a selected memoryless strategy or by a simultaneous choice of endpoint vectors. · OAI.WLIdentification.RingLayout.ImageSet

imageSieve def

A concrete BoundingSieve attached to any polynomial image, with exact fiber weights rather than an unjustified injectivity assumption. · OAI.Problem337.PrimePairSieve.imageSieve

imageSpace abbrev

Literal range of the selecting operator on the canonical universe lift of Y. · OAI.LittleFinitistic.SourceImageEvaluation.imageSpace

imageSubalgebra def

The canonical map's image is a B-subalgebra, since the base map is a section on constant Laurent polynomials. · OAI.StableCoordinate.ModificationEmbedding.imageSubalgebra

imageTensorEquiv def

The eigenspace e(M tensor N) is exactly (eM) tensor N as a right module. · OAI.LittleFinitistic.TensorProjection.imageTensorEquiv

imageTotalHomeomorph def

A homeomorphism with the subspace topology inherited from the actual ambient bundle, not a separately declared topology on an abstract image. · OAI.Kaplansky.ContinuousOrthonormalStageFrame.imageTotalHomeomorph

imageTranslate def

The same affine translate expressed in adapted coordinates. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageTranslate

imageTranslate def

The same affine translate expressed in adapted coordinates. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageTranslate

imageVertices def

Canonical vertex bodies are compared using their actual decidable equality. List.dedup fixes a deterministic order by retaining the last occurrence. · OAI.MaxCutGames.Reduction.Encoding.imageVertices

imageVertices def

Canonical vertex bodies are compared using their actual decidable equality. List.dedup fixes a deterministic order by retaining the last occurrence. · OAI.UniqueGamesTheorem.Reduction.Encoding.imageVertices

imaginaryDerivation def

The infinitesimal rotation as a bundled derivation. · OAI.PolycyclicRecognition.ComplexCartan.imaginaryDerivation

imaginaryOperator def

Imaginary semisimple part of a Cartan adjoint operator. · OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator

imaginaryPart def

Imaginary part as an additive homomorphism, for coefficient sums. · OAI.DefocusingNLS.SeparatorArithmetic.imaginaryPart

imaginaryPart def

The imaginary part, viewed as a purely imaginary complex number. · OAI.PolycyclicRecognition.ComplexCartan.imaginaryPart

immBlock def

Each block of layer labels represents the product of its matrices. · OAI.Problem335.immBlock

immCoefficientMatrix def

A finite submatrix of the genuine normalized IMM operator. · OAI.Problem335.immCoefficientMatrix

immersedLabels def

Only one filter of the global string set; it does not discard comparisons between sides or enlarge that set to the product of projections. · OAI.TorsionFreeZeroDivisors.TwoSideStage.immersedLabels

immFinitePathShift def

A finite target index for each path. The fallback is used only for a zero-amplitude path, and is therefore invisible in the operator matrix. · OAI.Problem335.immFinitePathShift

immFirstMomentLoss def

The explicit finite-size occupation loss, before parameter specialization. · OAI.Problem335.immFirstMomentLoss

immFirstMomentMean def

The independent geometric benchmark for one IMM path. · OAI.Problem335.immFirstMomentMean

immIdentityEvaluation def

Evaluation assigning every matrix layer the identity matrix. · OAI.Problem335.immIdentityEvaluation

immInternalCoordinate def

The coordinate in one layer of a genuine endpoint-fixed internal path. · OAI.Problem335.immInternalCoordinate

immInternalPathEdges def

The edge list associated to the tuple of internal vertices. · OAI.Problem335.immInternalPathEdges

immInternalPathVertices def

Extend internal vertex choices by the two fixed endpoint vertices. · OAI.Problem335.immInternalPathVertices

immLayerUCount def

The number of multiplication layers in a layerwise partition. · OAI.Problem335.immLayerUCount

immLayerVCount def

The number of derivative layers in a layerwise partition. · OAI.Problem335.immLayerVCount

immNormalizedMatrix def

The actual finite IMM map written in factorial-normalized source and target bases. · OAI.Problem335.immNormalizedMatrix

immPathAmplitude def

The normalized coefficient contributed by one endpoint path of IMM. · OAI.Problem335.immPathAmplitude

immPathOccupation def

The final occupation vector of one path operator. · OAI.Problem335.immPathOccupation

immPaths def

The canonical labelled paths contributing to the endpoint IMM entry. · OAI.Problem335.immPaths

immPathSignedShift def

The signed exponent displacement of an actual IMM path. · OAI.Problem335.immPathSignedShift

immProfile def

The canonical layer profile of a list-indexed IMM path. · OAI.Problem335.FockLayerProfile.immProfile

immRealNormalizedMatrix def

The real, nonnegative matrix underlying the actual normalized IMM map. · OAI.Problem335.immRealNormalizedMatrix

ImmSourceIndex abbrev

Source exponent vectors for the finite IMM operator. · OAI.Problem335.ImmSourceIndex

ImmTargetIndex abbrev

Target exponent vectors for the finite IMM operator. · OAI.Problem335.ImmTargetIndex

immTargetShift def

The genuine target occupation, with an irrelevant fallback for zero-amplitude paths. · OAI.Problem335.immTargetShift

immUpperCircuit def

The canonical block circuit at block width ceilSqrt n. · OAI.Problem335.immUpperCircuit

imperfectColumnReferences def

Imperfect positions store one representative each, in their original order. · OAI.TwoPointCorrelations.imperfectColumnReferences

Implementation def

A finite-state implementation with polynomial transition count. · OAI.RationalHitting.ExecutableGenerator.Implementation

implicitDerivative def

The derivative supplied by the implicit-function theorem, with parameter first. · OAI.Problem356.LocalImplicit.implicitDerivative

in11 def

Diagonal corner inclusions, as continuous real linear maps. · OAI.KervaireIncidenceCurrent.in11

InAffineLimitFamily structure

Literal full-dimensional affine local-limit family of geometry.tex:87. The affine maps may vary along the approximating sequence. · OAI.AffineBernstein.InAffineLimitFamily

InBand def

A half-open band on a multiplicative dyadic scale. · OAI.Problem337.DyadicBands.InBand

Incidence def

An unoriented nearest-neighbor bond, in its unique positive-axis indexing. · OAI.CriticalZ3.Incidence

Incidence inductive

Every incidence of the signed tensor differential, indexed by its sign. false denotes negative and true denotes positive. · OAI.Thomason.Construction.RightCylinderBasis.Incidence

incidence def

The incidence map is polynomial in the redundant compact-group coordinates. · OAI.KervaireIncidenceCurrent.incidence

incidenceColor def

The color of a slot. · OAI.PixtonChow.incidenceColor

incidenceEquation def

The affine incidence equation, now polynomial jointly in point coordinates and form coefficients. · OAI.Nagata.W27.incidenceEquation

incidenceEquiv def

At a point, assign the incident lines bijectively to all slopes. · OAI.KaplanskyCounterexample.IncidenceDirections.incidenceEquiv

incidenceEquiv def

The incidence fibre used in the Euler-exponent proof is the exact colour fibre used in the chain/block first moment. Both chain orientations count once. · OAI.TorsionFreeZeroDivisors.ChainMultiplicity.incidenceEquiv

incidenceGraph def

The bipartite incidence graph; its extended girth is infinite for a forest. · OAI.KaplanskyCounterexample.Planar.incidenceGraph

incidenceHomeomorph def

The constructed smooth real bundle realizes the exact complex kernel incidence subset, including its ambient subspace topology. · OAI.Kaplansky.SmoothKernel.SurjectiveFamily.incidenceHomeomorph

IncidenceIndex abbrev

Every positive degree and every nonnegative multiplicity vector, without bounds. · OAI.Nagata.Workers.W25.IncidenceIndex

incidenceLaw def

The retained position is internal; the actual right question is its name. · OAI.MaxCutGames.Clean.IncidenceGap.incidenceLaw

incidenceLaw def

The retained position is internal; the actual right question is its name. · OAI.UniqueGamesTheorem.Clean.IncidenceGap.incidenceLaw

incidenceMode def

Decode the canonical six-mode enumeration into the incidence labels. · OAI.Problem348.Construction.incidenceMode

IncidenceReduced def

Adjacent run labels differ, and consecutive transition points differ. The latter is exactly the nonzero run-increment condition. · OAI.TwoPointCorrelations.IncidenceReduced

incidenceVertices def

Each pair records a transition point and the next run label. · OAI.TwoPointCorrelations.incidenceVertices

Incident def

Lines are the kernels of the seven nonzero linear functionals. · OAI.HyperbolicObstruction.IncidenceTemplate.Incident

incident def

Clique vertices incident with at least one assigned path. · OAI.CycleClique.Construction.ExpandedPathSystem.incident

incidentSlice def

Incidences in a single period slice of the concrete event index. · OAI.QuantitativeVanDerWaerden.EligiblePatternTests.incidentSlice

include1 def

The original summand inclusion, as a triple preserving the specified homotopy. · OAI.ExternalTensor.Section4.SourceFiltration.include1

includeComplement def

An embedding, together with all unconsumed objects, is an exact disjoint partition. This is used on whole ports, never on independent child germs. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.includeComplement

includeHom def

Include the four retained variables and all the extra variables. · OAI.StableCoordinate.Presentation.includeHom

includeMap def

The inclusion of a corner into its ambient algebra. · OAI.BoundedHochschild.CentralCorner.includeMap

includesAll def

Each bad event requires one specified nonzero vector in each of its specified direction planes. · OAI.KaplanskyCounterexample.FiniteGeometry.includesAll

includeU def

Inclusion of the induced intersection grade into the old grade. · OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.includeU

includeUnit def

Unit partitions use the ambient identity, with no transport of the underlying finite index set. · OAI.Generator.Tracial.CornerPartition.includeUnit

inclusion def

The concrete inclusion preserves the underlying complex number. · OAI.CirculantHadamard.CyclotomicAdjoin.inclusion

inclusion def

Insert a literal nested term into the actual recursive total. · OAI.DerivedBar.RecursiveTotal.inclusion

inclusion def

Inclusion of the block into the ambient algebra is linear. It is not generally a unital homomorphism of rings, since the identities differ. · OAI.Donovan.BlockIdempotent.inclusion

inclusion def

The maps below operate on the actual rotation-cycle quotients. · OAI.FKCRT.PermutationWedge.inclusion

inclusion def

Inclusion in the core does not alter the orientation or the literal random field used by an edge. · OAI.HyperbolicObstruction.CoreWordGraph.inclusion

inclusion def

The inclusion is continuous for the inherited operator norm. · OAI.KervaireCentralizer.inclusion

inclusion abbrev

Its full and faithful inclusion into the ambient homotopy category. · OAI.LittleFinitistic.FiniteProjectiveHomotopy.inclusion

inclusion def

The entire zero column has its original chain inclusion. · OAI.LittleFinitistic.InducedRectification.inclusion

inclusion def

Inclusion of the copy of Y at each vertex. · OAI.LittleFinitistic.QuadraticEncoding.Representation.inclusion

inclusion def

The original zero column includes by an actual chain map. · OAI.LittleFinitistic.RectificationTotal.inclusion

inclusion def

The canonical, dense star algebra map to the universal completion. · OAI.NuclearUltrapower.UniversalCompletion.inclusion

inclusion def

The inclusion of an initial finite segment into a larger finite segment. · OAI.ReflexiveFixedPoints.FinitePrefix.inclusion

inclusion def

Inclusion of the underlying finite chains, with no re-enumeration. · OAI.Thomason.Construction.ChainOrdinal.inclusion

inclusion def

The two actual positive chain inclusions into the pasted basis complex. · OAI.Thomason.Construction.PastingGlobeBasis.inclusion

inclusion def

The actual inclusion of the two cylinder ends. · OAI.Thomason.Construction.SimplicialCylinder.inclusion

inclusion def

The fully faithful inclusion of strict n-categories into omega-categories. · OAI.Thomason.Construction.StrictOmegaCategory.inclusion

inclusion def

Literal inclusion into the actual source graph subdivision. · OAI.TorsionFreeZeroDivisors.SupportedImage.inclusion

inclusion def

Componentwise edge inclusion, as a relation on diagrams. · OAI.TwoWayComplementation.Diagram.inclusion

inclusionHom def

The self-contained construction includes its support proofs. · OAI.CoarseAssembly.DiscreteRoe.inclusionHom

inclusionMoment def

The inclusion moment of the random marked set F. · OAI.CubeShuffle.inclusionMoment

inclusionProbability def

The common one-vector inclusion probability. · OAI.KaplanskyCounterexample.FiniteGeometry.inclusionProbability

inclusiveCache def

Incoming cache plus current proposal, before the release at this bag. · OAI.BoundedTreewidthL1.AnchorCache.inclusiveCache

incomingKey def

At incoming updates, the entire state is retained on protected particles. Every remaining state is pooled in one free class. · OAI.BoundedTreewidthL1.ExpandedParticleLaw.incomingKey

incomingSwitch def

Joining incoming germs is postcomposition of the old successor with the transposition of its two new targets. This does not identify facet labels. · OAI.IntegralCharacterVarieties.BoundaryBand.incomingSwitch

InCommutant def

The finite matrix group von Neumann algebra, before bundling. · OAI.KervaireMatrix.InCommutant

InCommutant def

The commutant of the right regular representation. · OAI.KervaireRegular.InCommutant

Incomparable def

Incomparability is of starts, equivalently of every node in different segments; mere disjointness is not used as a substitute. · OAI.BoundedTreePotentials.Segments.Incomparable

Incomparable def

Every node of one admissible segment is incomparable with every node of another. This is strictly more restrictive than disjointness. · OAI.DiamondDistortion.IncomparableModel.Incomparable

InCone def

Membership in an old left-translation cone of letters. · OAI.PartitionConsistency.ProbeAlgebra.Path.InCone

inCoordinates def

Write a full-column operator in the finite matrix-unit coordinates. · OAI.KadisonSimilarity.FullColumnCoordinates.inCoordinates

increasingFiniteScalarInvariantMean def

The scalar invariant mean for a group exhausted by an increasing sequence of finite subgroups. · OAI.KadisonKastler.increasingFiniteScalarInvariantMean

IncreasingOrderLaw def

Corollary 2 (cor:comparison), first strict ordering. · OAI.JointDickman.IncreasingOrderLaw

IncreasingPositions abbrev

A choice of positions for a subsequence, in their original order. · OAI.TreeEdit.BinaryLower.RandomMatching.IncreasingPositions

increasingStrip def

A horizontal strip below the strict ordering diagonal. · OAI.JointDickman.increasingStrip

increasingSubgroupUnion def

The union of a monotone sequence of subgroups, as a subgroup. · OAI.KadisonKastler.increasingSubgroupUnion

IncreasingTuple abbrev

An increasing tuple enumerates a monomial's distinct observed ranks. · OAI.TraceReconstruction.IncreasingTuple

increasingUnionStage def

The original stages, regarded inside their union. · OAI.KadisonKastler.increasingUnionStage

increment def

The oscillatory increment, written directly as an ambient four-space map. · OAI.ClosedSurfaceR4.ManifoldFreeChart.increment

increment def

Add one D slot in block j. Every nonzero block differential starts at such a tuple. · OAI.DerivedBar.Multibar.increment

increment def

The increment of the actual quenched physical system with the complete Poisson dictionary, not a pressure-rate proxy. Its size is N+1. · OAI.DilutedSpinGlass.ConcreteReservoir.increment

increment def

Entry-to-child-corner distance in the actual isolated core map. · OAI.FKCRT.Inventory.Core.increment

increment def

Actual angular increment of a period, zero on both open round collars. · OAI.HarmonicCounterexample.AngularStream.increment

increment def

Controls are arbitrary across periods; only each individual scalar bump is smooth. · OAI.HarmonicCounterexample.Pulses.increment

increment def

The first relative increment includes the entire first ball. · OAI.KServer.ScaleMass.increment

increment def

Unary successor needs one physical push and no unbounded register. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Fuel.increment

increment def

Relative increments of positive monotone masses have only logarithmic total. · OAI.UniformKServer.PilotScales.increment

increment def

Unary successor needs one physical push and no unbounded register. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Fuel.increment

incremented def

Precisely the first deficit indices in decreasing remainder order. · OAI.MaxCutGames.Explicit.Rounding.incremented

incremented def

Precisely the first deficit indices in decreasing remainder order. · OAI.UniqueGamesTheorem.Explicit.Rounding.incremented

incrementHistory def

Ordinary identifiers record no increments. Ordered identifiers keep the entire old list and append precisely the new signed region-tapered term. · OAI.PlanarL1.Columns.Model.BData.incrementHistory

incrementLaw def

One initial uniform shift followed by independent fair coarsening bits, before introducing phase and orientation. · OAI.WeakPinned.Grid.incrementLaw

incrementLimit def

A canonical local limit; no pointwise convergence or smooth limit is assumed. · OAI.ThreeTorus.incrementLimit

increments def

Discrete derivative with dummy parent value zero above the root. · OAI.BoundedTreePotentials.TreeCalculus.increments

InCutCell def

Closed cells include tied transition points. · OAI.Problem326.Affine.InCutCell

ind def

Real indicator. · OAI.HadwigerCounterexample.ind

IndependenceBound def

Every independent set has at most a vertices. · OAI.CycleClique.Construction.IndependenceBound

independent def

Independent laws on finitely many (possibly different) finite spaces. · OAI.CoordinateSweeps.FiniteLaw.independent

independentKernel def

Products of Markov kernels, with measurability proved on the generating finite cylinders and extended to the entire product sigma algebra. · OAI.FiniteFactor.independentKernel

independentMean def

Independent draws use the product of the two uniform laws. · OAI.MaxCutGames.Soundness.SubsetIntersection.independentMean

independentMean def

Independent draws use the product of the two uniform laws. · OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.independentMean

independentNormPrimeSum def

Actual weighted independent prime convolution, before collecting products. · OAI.CubicFirstMoment.independentNormPrimeSum

independentSplitProducts def

The independent model is (C E₁, C E₂). If two categories contain the same prime, its square is retained in the corresponding product. · OAI.JointDickman.independentSplitProducts

independentWeightCone def

The nonnegative span of an independent finite family is closed. · OAI.PolycyclicRecognition.independentWeightCone

Index def

Every index records every bar length and the final input degree. · OAI.DerivedBar.RecursiveTotal.Index

Index abbrev

Finite rank-array choices and finite old-branch matchings together, with NO identification of occurrences sharing their facet name. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.FiniteRoutedFamily.Index

Index def

Small carrier for the prescribed ground wellordering; no rearrangement of code order occurs when conditions or components move. · OAI.PartitionConsistency.ProductForcing.ChainCode.Index

Index abbrev

The exponent index set for the source of the mixed operator. · OAI.Problem335.BidegreeAverages.Index

Index abbrev

A group and an index in that group. · OAI.ReflexiveFixedPoints.OrderedGroupConcat.Index

Index abbrev

The base point and all finite-net labels form one countable index set. · OAI.RegularPointCoordinates.MovingRescalingNetFamily.Index

Index abbrev

The base point and all finite-net labels form one countable index set. · OAI.RegularPointCoordinates.RescalingNetFamily.Index

index def

All natural-number addresses are valid; only the first count receive mass. · OAI.CircleDomainRigidity.HitFusionSplit.index

index def

All natural-number addresses are valid; only the first count receive mass. · OAI.CircleDomainRigidity.MarkedHit.HitFusionSplit.index

index def

Source and sink occupy zero and one, then rows and columns. · OAI.ContingencyTables.NetworkVertexCode.index

indexAt def

The unique maximal allowed dyadic cell containing a given point. · OAI.LipschitzHilbert.SourceWhitney.indexAt

indexedCircuit def

The actual homogeneous five-layer block-expansion circuit, before finite reindexing. · OAI.Problem335.BlockData.indexedCircuit

IndexedDepth5Circuit structure

A depth-five circuit whose gates are indexed by arbitrary finite types. This representation is convenient for products, sums, and path-indexed gates; toDepth5Circuit transports it to the qualified circuit representation. · OAI.Problem335.IndexedDepth5Circuit

indexedDeshiftedCountIso def

A genuine chain isomorphism using the standard integer shift differential, not a newly stipulated shift or transported count differential. · OAI.DerivedBar.ParityBridge.indexedDeshiftedCountIso

indexedDifferential def

The independently recursive multibar faces in the exact Shape coordinates. This uses the horizontal/vertical differential of RecursiveTotal, not the count complex differential. · OAI.DerivedBar.RecursiveTotal.indexedDifferential

indexedExtraAverage def

Extra-leaf index set version of the whole-bit-law sum. · OAI.TraceReconstruction.indexedExtraAverage

IndexedFaceMap structure

An indexed cellular face map. Commutation records EACH indexed side (not just its edge label); injectivity on a face rules out wrapping a cell twice. · OAI.HyperbolicObstruction.PictureSwitch.IndexedFaceMap

IndexedFanData structure

The same local finite-link data, with natural geometric index types. toFin is only a change of finite coordinates, not an additional assumption. · OAI.HyperbolicObstruction.FanLink.IndexedFanData

indexedFanData def

The actual selected fragment of an actual normalized genus-zero mapped picture supplies EVERY field of the local fan-link data. No apex bound, no triangle-link normality and no contact separation is assumed. · OAI.HyperbolicObstruction.ConeSkeleton.indexedFanData

indexedFanData def

The actual selected fragment of an actual normalized genus-zero mapped picture supplies EVERY field of the local fan-link data. No apex bound, no triangle-link normality and no contact separation is assumed. · OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.indexedFanData

indexedFlatIso def

Chain isomorphism from the exact tensor-block direct sum to the recursive flat model. · OAI.DerivedBar.RecursiveTotal.indexedFlatIso

indexedGraph def

The canonical internal graph of a small ground-indexed name family. Uniform support is used only to prove that this actual set name is HS. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedGraph

indexedImage def

The value of a function at the (at most one) point of a given ordinal index in an injection of its domain. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedImage

indexedLeadingIso def

Actual chain isomorphism flattening the recursive leading total into the same Shape-indexed block tensors as the square-zero count decomposition. · OAI.DerivedBar.RecursiveTotal.indexedLeadingIso

indexedMultibar def

Exact tensor-block coordinates, with the unshifted multibar total degree n. · OAI.DerivedBar.RecursiveTotal.indexedMultibar

indexedOutcomes def

The executable edge experiment for an arbitrary explicitly ordered noise index type. Equal noise vectors still have separate indices and entries. · OAI.MaxCutGames.Reduction.ActualEnumeration.indexedOutcomes

indexedOutcomes def

The executable edge experiment for an arbitrary explicitly ordered noise index type. Equal noise vectors still have separate indices and entries. · OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.indexedOutcomes

indexedProduct def

Independent emissions indexed by the actual token IDs of the layout. · OAI.TraceReconstruction.FiniteLaw.indexedProduct

indexedResidueCollisionCount def

The number of ordered pairs in an indexed list with the same residue. The indices, rather than the image set, retain all multiplicities. · OAI.Problem337.indexedResidueCollisionCount

indexedSection def

A preimage for the (possibly absent) value at one ordinal index. · OAI.PartitionConsistency.SetLanguage.indexedSection

IndexedTree structure

An ordinary finite rooted tree in topological node order. · OAI.ParityWL.IndexedTree

indexedWord def

Finite-indexed form of the balanced layer partition. · OAI.Problem335.BalancedSchedule.indexedWord

indexInclusion def

Rectangular coordinate inclusion for an actual injective index map. · OAI.RowColumn.MatrixState.indexInclusion

indexingTarget def

Zero coefficients specify the base indexing target only: the cover has arbitrary independent weights for each lifted step. · OAI.HyperbolicObstruction.ConeSkeleton.indexingTarget

indexLaw def

Choose a potential new index uniformly and an independent old fallback. Only the zero new index uses the fallback; all other old indices coincide. · OAI.DilutedSpinGlass.SizeCoupling.indexLaw

indexOfBlocks def

Recover the successive diagonal choices from the literal block lengths. · OAI.DerivedBar.RecursiveTotal.indexOfBlocks

indexPairing def

Pairing an odd analytic class with an actual scalar unitary. · OAI.CoarseAssembly.Analytic.indexPairing

indexWord def

The signed coordinate evaluates both alternating rays in the same group. The Euclidean quotient also gives the correct odd negative coordinates. · OAI.KLInvariance.Dihedral.indexWord

indicator def

Real indicator of the circuit accepting its input. · OAI.TwoPointCorrelations.AC0Circuit.indicator

indicatorVectorLinear def

A fixed finite-measure indicator as a continuous linear function of its vector coefficient. · OAI.WeakPureInfiniteness.indicatorVectorLinear

indices def

Transfer the fixed table's indices to ordinal initial segments. · OAI.PartitionConsistency.OrderAssignment.indices

indices def

The global finite-index set may include every edge window. · OAI.Problem310.WindowData.indices

InDipole def

The darts of the two particular face occurrences being cancelled. · OAI.HyperbolicObstruction.PictureSwitch.PictureMap.InDipole

Indiscrete def

A type endowed with the indiscrete preorder, used only for endpoint labels. · OAI.Thomason.Construction.StrictOmegaCategory.Indiscrete

individualPlan def

A single upper layer satisfies exactly the ordinary individual-link conditions. The short contact is proved by the three-window path. · OAI.Superstring.Hierarchical.LayerCollection.individualPlan

inducedBoundedProjective def

Build the complete derived-tensor model from the actual native rectification, with no tensor-comparison assumption. · OAI.LittleFinitistic.BimoduleTotal.inducedBoundedProjective

inducedData def

All columns and components are induced from actual modules, paths and maps. · OAI.ExternalTensor.Section4.inducedData

inducedDerived def

Native P is fixed before the arbitrary derived input is supplied. · OAI.LittleFinitistic.BimoduleTotal.inducedDerived

inducedInclude1 abbrev

Actual Section 4 source filtration inclusion; no decomposition is assumed. · OAI.ExternalTensor.Section4.SourceFiltration.inducedInclude1

inducedMap def

The trace-preserving embedding induced by the coordinate embeddings. · OAI.KadisonKastler.VaryingTraceQuotient.inducedMap

inducedPairFun def

Keep a pair precisely when both its actual endpoint darts satisfy P. · OAI.TorsionFreeZeroDivisors.MapEuler.inducedPairFun

inducedQuotient0 abbrev

Actual Section 4 source quotient; homotopy compatibility is proved above. · OAI.ExternalTensor.Section4.SourceFiltration.inducedQuotient0

InducedSigned structure

Signed roots for the induced system. The vectors are the original ambient roots, and membership in the actual plane is part of the relation. · OAI.KLInvariance.TitsSpace.PlaneBasis.InducedSigned

inducedUnitary def

Unitary induction with no finite-index assumption. · OAI.NuclearUltrapower.inducedUnitary

inductionAmbientQuotientIso def

The quotient action is the induction action, including its inverse convention. · OAI.PolycyclicRecognition.inductionAmbientQuotientIso

inductionInclusion def

The original representation embeds on the identity coordinate. · OAI.NuclearUltrapower.inductionInclusion

inductionTerm def

The fixed finite list of induced tensor coordinates. · OAI.NuclearUltrapower.inductionTerm

inductiveMean def

The ordered inductive mean, with the harmless value vertex for an empty list. For a list of length j+1, append its last point with weight 1/(j+1). · OAI.HyperbolicObstruction.ConeData.inductiveMean

inf def

Conservative intersections exist at every original tower cut. · OAI.PartitionConsistency.ConservativeMonoids.Subobject.inf

InFan def

Membership of an (unoriented) core edge in the fan over i. Adjacency is imposed separately. The exceptional loose edge belongs to no fan. · OAI.HyperbolicObstruction.CoreGeometry.InFan

infiniteAncestry def

Prefix order on all finite words, explicitly distinct from their lexicographic order. · OAI.DiamondDistortion.infiniteAncestry

infiniteFrameIndexEquiv def

Increasing enumeration identifies an infinite rank stratum with ℕ. · OAI.KadisonKastler.infiniteFrameIndexEquiv

InfinitePath structure

Actual infinite paths retain all original Type I expressions, weights, and uncropped metadata. No completion of the coding tree is inserted as a path. · OAI.SeparableQuotient.Norming.InfinitePath

infiniteProjectionBasis def

The infinite-dimensional coordinate basis on the infinite rank stratum. · OAI.KadisonKastler.infiniteProjectionBasis

InfiniteRanks def

Infinitude refers to ranks of actual finite hypergraphs. · OAI.RyserOdd.Specification.InfiniteRanks

infiniteSegments def

The infinite-height tree of all finite words; this includes the empty root. · OAI.DiamondDistortion.infiniteSegments

Inflated def

The source module M(Y), supported on the first D-block and inflated to A. · OAI.LittleFinitistic.SelectedOrdinaryModules.Inflated

inflated_realization def

The already proved Phi realization, transported by the actual first-block inflation, with no ordinary F² identity assumed or asserted. · OAI.LittleFinitistic.SelectedFirstBlockFamily.inflated_realization

inflatedModule def

The original D module is inflated by the actual projection, without a new action hypothesis. · OAI.DerivedBar.ParityBridge.inflatedModule

inflateHom def

Inflate a corner operator by the same operator on every matrix summand. · OAI.KadisonKastler.FullMatrixCorner.inflateHom

inflateUnitary def

The actual unitary on the whole Hilbert space obtained from a corner unitary. · OAI.KadisonKastler.FullMatrixCorner.inflateUnitary

inflation abbrev

The actual exact inflation functor from B-modules to the first D-block. · OAI.LittleFinitistic.SelectedFirstBlockFamily.inflation

influence def

Full influence, with the same probability normalization. · OAI.OptimalMaxCut.Analytic.influence

influence def

The pivotal influence, with the redundant pivotal coordinate included in the sum. · OAI.Problem313.RestrictionInfluence.influence

InfluenceBound def

The nonnegative-increment influence bound for a fixed finite coupling array. · OAI.BufferedIsing.DSS.InfluenceBound

InGraphChart def

A plane is in a splitting's graph domain exactly when its projection to the horizontal factor is bijective. This is independent of its chosen basis. · OAI.Kaplansky.ComplexGrassmann.InGraphChart

InHook def

Zero-based form of the manuscript's (h,h)-hook. · OAI.RowColumn.InHook

init def

`M.init input` starts in `M.initial`, places the entire Boolean input on `M.inputStack`, and makes every other stack empty. · OAI.CurrentKS.Machine.init

Initial def

Cutting needs only ancestry, so it applies to finite heads and whole components. · OAI.BoundedTreePotentials.Segments.Initial

Initial def

Head sets are predecessor-closed. The empty set is allowed for block heads. · OAI.BoundedTreePotentials.TreeCalculus.Initial

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

initial def

The initial frontier consists solely of the identity map at the root. · OAI.ReflexiveFixedPoints.AnchoredCandidateContext.initial

initial def

The initial homogeneous polynomial, including zero. · OAI.SectionCompletion.initial

initial def

The class of a in degree d. · OAI.StableCoordinate.FilteredRees.initial

initial def

The inclusion of stage zero, written recursively for the deformation construction. · OAI.Thomason.Construction.TopologicalDeformation.Sequential.initial

initialBraidInclusion def

Initial B3 inclusion in every B_(n+1), for n≥2. · OAI.ArtinCAT0.initialBraidInclusion

initialClamp def

Retraction to that initial segment, by clamping above its last vertex. · OAI.Thomason.Construction.SimplexComplex.initialClamp

initialCompleteGraph def

The level-zero graph has exponent one on every distinct ordered pair. · OAI.Ostmann.initialCompleteGraph

initialCompleteIndexEquiv def

Separate all fixed spectators, then the two giants and the moving slots. · OAI.Ostmann.initialCompleteIndexEquiv

initialConfiguration def

All constant configuration data is computed from the public margins. · OAI.ContingencyTables.ProfilePrograms.initialConfiguration

initialContraction def

The simultaneous contraction is an actual simplicial homotopy. · OAI.Thomason.Construction.RealizedCube.initialContraction

initialContractionMap def

Simultaneously expand all interval coordinates from the initial vertex. · OAI.Thomason.Construction.RealizedCube.initialContractionMap

initialCopyEmbedding def

The natural initial-coordinate inclusion is a special case of arbitrary coordinate padding. · OAI.KadisonSimilarity.initialCopyEmbedding

initialCountAdmissible def

This is the literal count-typicality condition; it does not change the central count's original binomial law. · OAI.TraceReconstruction.initialCountAdmissible

initialExtra def

The extra tapes initially contain only the live serialized table. · OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra

initialExtra def

The extra tapes initially contain only the live serialized table. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.initialExtra

initialFace def

Inclusion of an initial segment of a finite ordinal. · OAI.Thomason.Construction.SimplexComplex.initialFace

initialFaceIso def

The full strict subcategory on an initial segment is its smaller oriental. · OAI.Thomason.Construction.SimplexComplex.initialFaceIso

initialFamily def

The high weighted-degree sets used as the initial generators. · OAI.TalagrandDiscreteConvexity.Covering.initialFamily

initialHeatPath def

The initial heat evolution as a continuous path, including time zero. · OAI.ForcedComputation.PlaneScalarMild.initialHeatPath

initialIdeal def

The initial ideal contains leading forms at the actual largest weights, not all homogeneous components of the relation ideal. · OAI.StableCoordinate.WeightedInitial.initialIdeal

initializedFiniteDraw def

Greedy arithmetic supplies all feasible fallbacks and the starting state. Each word returns a member of the original margin fibre. · OAI.ContingencyTables.SmallGraphProfiles.initializedFiniteDraw

initializedTableHeaderInTime def

The same bounded phase begins at the machine's genuine initial configuration. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.initializedTableHeaderInTime

initializedTableHeaderInTime def

The same bounded phase begins at the machine's genuine initial configuration. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.initializedTableHeaderInTime

initializedTableInTime def

The concrete machine starts at its genuine initial configuration on a full graph table and leaves every output field on the stated physical tape. · OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.initializedTableInTime

initializedTableInTime def

The concrete machine starts at its genuine initial configuration on a full graph table and leaves every output field on the stated physical tape. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.initializedTableInTime

initializeInTime def

The actual initialized loop counters and fresh numeric vertex IDs are proved outputs of unary arithmetic, including the runtime vertex header. · OAI.MaxCutGames.Explicit.MachineSubdivisionInit.initializeInTime

initializeInTime def

Complete actual initialization, including width zero and the optional continuation. The radix, scratch, ambient state and unrelated tapes survive. · OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.initializeInTime

initializeInTime def

Initialization of the actual global program from its literal input list. Every work-tape readiness property follows from the explicit final frame. · OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.initializeInTime

initializeInTime def

Actual initialization of the complete finite driver, ending at its first guard with the exact input, counter, cursor, index, and reversed headers. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.initializeInTime

initializeInTime def

The actual initialized loop counters and fresh numeric vertex IDs are proved outputs of unary arithmetic, including the runtime vertex header. · OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.initializeInTime

initializeInTime def

Complete actual initialization, including width zero and the optional continuation. The radix, scratch, ambient state and unrelated tapes survive. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.initializeInTime

initializeInTime def

Initialization of the actual global program from its literal input list. Every work-tape readiness property follows from the explicit final frame. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.initializeInTime

initializeInTime def

Actual initialization of the complete finite driver, ending at its first guard with the exact input, counter, cursor, index, and reversed headers. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.initializeInTime

initialJoint def

The image of a greedily filled original table is an actual positive small state with its own successful retained completion. · OAI.ContingencyTables.SmallGraphProfiles.initialJoint

initialJunctionFree def

The unswept free sites and the literal occupied junction board are identified by the actual reference first-half sweep. · OAI.CoordinateSweeps.Grid.Holes.initialJunctionFree

initialLinear def

The homogeneous symbol is linear within a fixed filtration degree. · OAI.StableCoordinate.GradedPresentationMap.initialLinear

initialMinimumWithWork def

The local initial-cone arithmetic after the center list has been constructed and the corresponding seed values gathered. · OAI.EditApproximation.BinaryFraction.initialMinimumWithWork

initialMotifDensity def

The density in the actual base experiment, not an independent model. · OAI.TraceReconstruction.initialMotifDensity

initialMovingDataCutoff def

Internal states use the same total function, while only terminal data are evaluated as leaves. The fallback is never used on a genuine template. · OAI.Ostmann.initialMovingDataCutoff

initialNet def

Literal clean initialization: retain the runtime controller word and create only zero history/output/scratch fields. No query result is precomputed. · OAI.ExactQuantumFactoring.NodeMachine.initialNet

initialNet def

Literal clean initialization: retain the runtime controller word and create only zero history/output/scratch fields. No query result is precomputed. · OAI.ExactQuantumFactoring.SplitMachine.initialNet

initialOverlapLower def

The common-mass constant depends only on the working deletion rate. · OAI.TraceReconstruction.initialOverlapLower

initialPeriod def

A period of m primitives with its unique 1 defect at zero-based slot d. · OAI.TraceReconstruction.initialPeriod

initialPoint def

The input-dependent loading endpoint is a finite rational expression. · OAI.ForcedComputation.Recorder.Planar.initialPoint

initialPrefactorCap def

All q dependence of a fixed rank-difference estimate is exposed here. The powers of u and m are retained exactly, including both large-gap gains. · OAI.TraceReconstruction.initialPrefactorCap

initialPrefixPeriods def

Exact initial paired prefix and complementary suffix sizes. · OAI.TraceReconstruction.initialPrefixPeriods

initialPureDegreeBound def

The pure comparison retains all low-degree cancellation, not just its total defect density. · OAI.TraceReconstruction.initialPureDegreeBound

initialRank def

Explicit threshold depending only on the requested nonlinear error. · OAI.MaxCutGames.Gadget.Parameters.initialRank

initialRank def

Explicit threshold depending only on the requested nonlinear error. · OAI.UniqueGamesTheorem.Gadget.Parameters.initialRank

initialRetainedIndexEquiv def

The left giant is true; fixed cells precede bulk in the moving template. · OAI.Ostmann.initialRetainedIndexEquiv

initialSideCount def

The actual base count, with no redefinition of the working channel. · OAI.TraceReconstruction.initialSideCount

initialSignedCap def

Scalar budgets independent of every actual report and count. The finite signed-pattern restriction is retained to preserve its three-difference gain. · OAI.TraceReconstruction.initialSignedCap

initialSpectatorCofactor def

The fixed spectator units are their true cofactors in the spectator list. · OAI.Ostmann.initialSpectatorCofactor

initialSpectatorSlotEquiv def

In one original half-list, separate the spectator block from the giant, bulk and fixed cell blocks. · OAI.Ostmann.initialSpectatorSlotEquiv

initialSpectralInterval def

Start the construction with the actual operator norm bounds in any corner. · OAI.Generator.Tracial.initialSpectralInterval

initialState def

Initial state for an arbitrary preserved family-state component. · OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialState

initialState def

Initial state for an arbitrary preserved family-state component. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.initialState

initialTape def

Initial finite representation after copying, before adding blank quota. · OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.initialTape

initialTapes def

Before initialization, the fixed-relation tape is empty. · OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.initialTapes

initialTapes def

Before initialization, only the old table and remaining-count word are populated. The program itself creates the initial vertex delimiter. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.initialTapes

initialTapes def

Only the unary request is initially present. · OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes

initialTapes def

Tape roles: original table, unary query, scan work, output, copy scratch. · OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.initialTapes

initialTapes def

Before initialization, the fixed-relation tape is empty. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.initialTapes

initialTapes def

Before initialization, only the old table and remaining-count word are populated. The program itself creates the initial vertex delimiter. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.initialTapes

initialTapes def

Only the unary request is initially present. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes

initialTapes def

Tape roles: original table, unary query, scan work, output, copy scratch. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.initialTapes

initialVertex def

The initial vertex in every coordinate of the finite simplicial cube. · OAI.Thomason.Construction.RealizedCube.initialVertex

initialVertexChain def

The initial segment ending at a vertex of a finite ordered simplex. · OAI.Thomason.Construction.initialVertexChain

initialVertexChainHom def

Initial segments form a monotone section of the maximum operation. · OAI.Thomason.Construction.initialVertexChainHom

InitOp structure

Nine fixed affine passes initialize headers, the loop counter, and all three private vertex indices. none means accumulate into the existing unary word. · OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.InitOp

InitOp structure

Nine fixed affine passes initialize headers, the loop counter, and all three private vertex indices. none means accumulate into the existing unary word. · OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.InitOp

Injection def

A linear parameter map with its injectivity proof. · OAI.MaxCutGames.Quadratic.UniformSubspaces.Injection

Injection def

A linear parameter map with its injectivity proof. · OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.Injection

injection def

Internal set injection f : d ↪ r. · OAI.PartitionConsistency.SetLanguage.injection

injectionDraw def

A code with no preimage is an explicit hold. · OAI.ContingencyTables.FairBits.injectionDraw

injectionEquivOfDomainEquiv def

Changing the domain by a linear equivalence preserves the set of actual injective linear maps. · OAI.MaxCutGames.Inverse.KMSKernelFiberCard.injectionEquivOfDomainEquiv

injectionEquivOfDomainEquiv def

Changing the domain by a linear equivalence preserves the set of actual injective linear maps. · OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.injectionEquivOfDomainEquiv

InjectiveBasisMap abbrev

The sample space after explicitly conditioning on full column rank. · OAI.MaxCutGames.Inverse.KMSBasisComparison.InjectiveBasisMap

InjectiveBasisMap abbrev

The sample space after explicitly conditioning on full column rank. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.InjectiveBasisMap

injectiveEquivIndependent def

A domain basis turns injective maps into independent image families. · OAI.MaxCutGames.Inverse.KMSInjectionCount.injectiveEquivIndependent

injectiveEquivIndependent def

A domain basis turns injective maps into independent image families. · OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.injectiveEquivIndependent

InjectiveFields def

The only injectivity imposed is within one field across branches. · OAI.HyperbolicObstruction.StarModel.InjectiveFields

InjectiveInducedSpace abbrev

Induction along an honest subgroup inclusion; the index may be infinite. · OAI.NuclearUltrapower.InjectiveInducedSpace

injectiveRangeFiberEquiv def

The fiber of the actual range-vertex map is the injective range fiber defined above. Both injectivity and the subspace equality are preserved. · OAI.MaxCutGames.Inverse.KMSBasisComparison.injectiveRangeFiberEquiv

injectiveRangeFiberEquiv def

The fiber of the actual range-vertex map is the injective range fiber defined above. Both injectivity and the subspace equality are preserved. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injectiveRangeFiberEquiv

injectivityDomain def

The open injectivity domain, defined by extendible minimizing vectors. · OAI.WeakMTWTransport.injectivityDomain

Ink structure

birth chamber precondition · OAI.ExactDerandomization.Stem.Cage.Ink

inl def

The kernel inclusion into the group with the given factor system. · OAI.PolycyclicRecognition.FactorExtension.inl

InLargePrefixClass def

The large-prime class, including integers already below the prefix cutoff. The existential witnesses need not be chosen canonically. · OAI.Problem337.InLargePrefixClass

inLeft def

Zipper fragments of a literal cell instruction, before and after the specified cross/stay move. · OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Literal.inLeft

InLift def

Membership in the lift, expressed by the actual linear-map range. · OAI.MaxCutGames.Inverse.KMSBasisComparison.InLift

InLift def

Membership in the lift, expressed by the actual linear-map range. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.InLift

inner def

The strict intrinsic inner ball, with reachability explicitly imposed. · OAI.BoundedTreewidthL1.Annulus.inner

inner def

The subgroup of inner automorphisms. · OAI.SimpleInnerAutomorphisms.inner

innerDerivation def

The spatial derivation implemented by T. · OAI.KadisonKastler.innerDerivation

innerDerivation def

Inner derivation on the full bounded-operator algebra. · OAI.KadisonSimilarity.innerDerivation

innerEmbedding def

Literal recursive suffix embedding on every summand, including zero input degrees. · OAI.DerivedBar.ParityBridge.innerEmbedding

innerEquiv def

A nonabelian simple group is canonically isomorphic to its inner automorphism group. · OAI.SimpleInnerAutomorphisms.innerEquiv

innerGridInterval def

Natural lattice points in a half-open normalized interval. · OAI.Problem337.innerGridInterval

innerHomeomorph def

Actual pairwise-disjoint open top-dimensional cells, including arbitrary index universes, with their ordinary disk interiors. · OAI.EilenbergGanea.CWCollar.Attachment.innerHomeomorph

innerLevelSubspace def

A level set of a real scalar product is an affine subspace. · OAI.Problem358.innerLevelSubspace

innerPattern def

The literal slots from the X bars, ordered outside to inside. · OAI.DerivedBar.RecursiveTotal.innerPattern

innerRotation def

Conjugate the disjoint union of cloud rotations into global dart coordinates. · OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.innerRotation

innerRotation def

Conjugate the disjoint union of cloud rotations into global dart coordinates. · OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.innerRotation

innerSize def

The inner dimension of an n × n^k by n^k × n multiplication. · OAI.MatrixMultiplication.Arithmetic.innerSize

innerSlice def

A fixed outer derivative, retaining its actual tangent-vector entries. · OAI.PositiveEinsteinFour.HighestHessian.innerSlice

innerSummandIso def

Every inner summand is isomorphic, D-linearly, to its literal field tensor. · OAI.DerivedBar.RecursiveTotal.innerSummandIso

innerTotalEmbedding def

The same canonical embedding on the actual recursive total, through the previously proved finite-sum flattening. · OAI.DerivedBar.ParityBridge.innerTotalEmbedding

innerVector def

Indicator of the small-coordinate subgroup of one line. · OAI.ContingencyTables.innerVector

innovation def

The standardized regression innovations at arbitrary increasing interior times. · OAI.FKCRT.Radial.innovation

InNP def

NP is defined independently of SAT or any hardness assertion. · OAI.DirectedFeedback.InNP

InNP def

NP is specified by polynomial witnesses and genuine finite-machine verification, independently of any reduction or satisfiability problem. · OAI.MaxCutGames.Foundations.Complexity.CookLevin.InNP

InNP def

NP via a deterministic polynomial-time verifier and a polynomial-length certificate. · OAI.UniformSparsestCut.InNP

InNP def

NP is specified by polynomial witnesses and genuine finite-machine verification, independently of any reduction or satisfiability problem. · OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InNP

inp def

choose s=g t profiles · OAI.GeneralMahler.SCal.Mid.inp

inplace def

Return the result to one fixed public register. Both word movements are implemented by two reversals; no output-to-input renaming is a TM operation. · OAI.ExactQuantumFactoring.BitStackProgram.Procedure.inplace

InPolygon def

Membership in the enclosing polygon D_lambda, with a left explicit. · OAI.Nagata.W04.InPolygon

inPolynomialTime def

Polynomial initialization in the literal incoming instance-code length. · OAI.MaxCutGames.Explicit.MachineProductHeaders.inPolynomialTime

inPolynomialTime def

Polynomial initialization in the literal incoming instance-code length. · OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.inPolynomialTime

Input inductive

`Input` is a tagged union whose `explicit` branch contains every edge copy and whose `binary` branch contains endpoint pairs with multiplicities. · OAI.AlgorithmicThinTrees.Input

Input abbrev

(number of bins, range size, bin index). · OAI.ContingencyTables.BinIntervalProgram.Input

Input abbrev

The fixed frame, the acceptance precision, current code, and fresh word. · OAI.ContingencyTables.CompanionMetropolisWordProgram.Input

Input abbrev

Unary trial count; denominator, failure count, success count, fallback match. · OAI.ContingencyTables.RetryNumeratorPrograms.Input

Input abbrev

(K,(precision,dimension)) and the catalog metadata/current bin. · OAI.ContingencyTables.RootedBinFramesProgram.Input

Input abbrev

Trial marker, denominator, success counts, fallback index. · OAI.ContingencyTables.VectorRetryPrograms.Input

Input structure

Current held parameters and raw ranks. The latter are used only for the initial minimizing selection, never substituted for the affine rank input. · OAI.KServer.CausalSimplex.Input

Input abbrev

The bipartition is proof-side data. Its codec is exactly the underlying instance code and the fixed program does not inspect it. · OAI.MaxCutGames.Explicit.MachineProductRuntime.Input

Input structure

The input graph and dart index occur only as physically stored tape data. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Input

Input abbrev

Variable vertex count, with the port count fixed by the input family. · OAI.MaxCutGames.Foundations.PCP.PortTables.Input

Input abbrev

The bipartition is proof-side data. Its codec is exactly the underlying instance code and the fixed program does not inspect it. · OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.Input

Input structure

The input graph and dart index occur only as physically stored tape data. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Input

Input abbrev

Variable vertex count, with the port count fixed by the input family. · OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Input

input def

Inspect the current activation in the presence of immutable integer parameter cp. · OAI.Fifths.Flow.input

input def

The incoming/outgoing main ports at one allowed event. Every remaining port (the split branch) is still present in the original table. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.input

input abbrev

The actual first-block D-module underlying the inflated A-module. · OAI.LittleFinitistic.SelectedBaseIterates.input

input def

Actual finite posterior input for each child rank. · OAI.UniformKServer.ConditionalRank.input

inputAlphabet def

Identity alphabet encodings at both ends of the concrete machine. · OAI.MaxCutGames.Reduction.AddressMachineProgram.inputAlphabet

inputAlphabet def

Identity alphabet encodings at both ends of the concrete machine. · OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.inputAlphabet

inputBasis def

Input wires are first, least significant bit first; all other wires start zero. · OAI.ExactQuantumFactoring.inputBasis

inputBimoduleIso def

An actual bimodule isomorphism induces a natural isomorphism of input tensor functors. · OAI.LittleFinitistic.BimoduleTotal.inputBimoduleIso

inputBit def

Read one bit at a unary index; a missing bit is false. Input is restored. · OAI.OptimalMaxCut.CounterMachine.Command.inputBit

InputBound def

The map carries a two-derivative prefix, while the metric defect has none. · OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.InputBound

inputChange def

The input matrix has adapted vectors as columns in the original basis. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.inputChange

inputDegree def

The final input degree, separated from all bar lengths. · OAI.DerivedBar.RecursiveTotal.inputDegree

inputEquiv def

The tensor input's scalar structure agrees with the original bimodule's scalar restriction through the two algebra homomorphisms. · OAI.LittleFinitistic.FullTensorProperties.inputEquiv

inputFunctor def

Tensor by one genuine bimodule, varying the left-module input and retaining the outside action. · OAI.LittleFinitistic.BimoduleTotal.inputFunctor

inputMap def

The actual map induced by an input chain map in a single balanced tensor term. · OAI.LittleFinitistic.ComplexTensor.inputMap

inputNumber def

The input word is reversed physically, while the output wire j is k_j. · OAI.ExactQuantumFactoring.Triangular.inputNumber

inputPairTape def

The coordinate value of the paired input codeword before masking. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.inputPairTape

inputPairTape def

The coordinate value of the paired input codeword before masking. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.inputPairTape

inputPosition def

The input point is rational and can be used as the loading target. · OAI.ForcedComputation.BalancedPlanar.inputPosition

inputProgram def

Strip the false unary terminator with two actual reversals and one pop. · OAI.ContinuumCoulomb.AmplificationProgram.inputProgram

inputReject def

One original input query and two proof-oracle queries. · OAI.MaxCutGames.Foundations.PCP.AssignmentTester.inputReject

inputReject def

One original input query and two proof-oracle queries. · OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.inputReject

Inputs structure

Common read-only inputs. · OAI.Fifths.Inputs

inputScale def

Polynomial diagonal maps; scaling the quotient input by X clears the negative input-kernel weight without changing the leading tensor. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.inputScale

inputSet def

Input positions; ancillas occupy the other positions. · OAI.QAC.inputSet

inputSize def

The least nonnegative bound for the joint map/metric input. · OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.inputSize

inputSize def

The variable-size input is exactly the two physical unary fields and existing output. The relation field is a fixed program constant. · OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.inputSize

inputSize def

Exact variable-size input: two unary fields, unary fuel, and old output. · OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.inputSize

inputSize def

The variable-size input is exactly the two physical unary fields and existing output. The relation field is a fixed program constant. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.inputSize

inputSize def

Exact variable-size input: two unary fields, unary fuel, and old output. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.inputSize

inputSpan abbrev

The literal bounded input segment, with one head marker. · OAI.WLIdentification.Machine.inputSpan

inputsPrefix def

One real AIG atom per input bit. The initial graph has one false node. · OAI.ExactQuantumFactoring.AIGCompiler.inputsPrefix

inputTables def

Dense, staged integer input tables. No quotient-field element is computed. · OAI.RationalHitting.ExecutableGenerator.inputTables

InputTree inductive

A recursively paired input routing that may stop at any central block. The leaf maps are genuine permutations, not probabilistic hypotheses. · OAI.CubeShuffle.InputTree

inputWires def

The original input is the n-wire interval immediately following the fresh branch coin. This definition is independent of N. · OAI.ExactQuantumFactoring.PhysicalTree.inputWires

inputWord def

The computational-basis input with the remaining qubits initialized to zero. · OAI.QAC.inputWord

inputWord def

Unary order header, row-major binary matrix, then most-significant-first binary k. · OAI.WLIdentification.inputWord

InQMA def

Promise-QMA with completeness 2/3 and soundness 1/3. · OAI.ContinuumCoulomb.InQMA

InRationalArc def

Real representatives of the rational arcs; translating a numerator by an integer retains the corresponding arc on the unit circle. · OAI.JointDickman.InRationalArc

inSamplingBox def

Reexpress an actual probe chain in the enlarged sampling basis. The word-basis comparison gives a constant radius for every prefix; all endpoints, coefficients and generator edges are preserved. · OAI.PolycyclicRecognition.CartanWordModel.BoxProbeChains.inSamplingBox

insert def

The inverse inserts a unit A coefficient before taking the balanced quotient. · OAI.DerivedBar.Balanced.insert

insert def

Insert a matrix entry into a word with distinct sites. · OAI.KadisonKastler.MatrixSiteWord.insert

insert def

Coordinate insertion is linear over the full coefficient algebra A. · OAI.LittleFinitistic.OrdinarySimulation.Compression.insert

insert def

Introduce one unassigned coordinate with a specified Boolean value. · OAI.PartitionConsistency.CohenForcing.Condition.insert

insertAt def

Inserting a freely canceling pair is attaching a thickened edge at the specified exterior corner, including the formerly empty exterior. · OAI.HyperbolicObstruction.WordPictures.WordPicture.insertAt

insertCoordinate def

Put a distinguished evaluation coordinate back into its full parent cube, keeping every other branching coordinate literally unchanged. · OAI.DilutedSpinGlass.DepthAverage.insertCoordinate

inserted def

The element whose presence in the chain is toggled. · OAI.FiniteChain.inserted

insertedCycleLabelingsEquiv def

Removing an inserted vertex preserves the set of cycle-constant labels. · OAI.KadisonSimilarity.insertedCycleLabelingsEquiv

insertedLog def

The insertion keeps the complete original mark row in the base law. · OAI.DilutedSpinGlass.HeterogeneousMarks.insertedLog

insertedMarkedLog def

Logarithmic weight after one truly independent added factor on the base which still contains all original selected-type terms. · OAI.DilutedSpinGlass.insertedMarkedLog

insertedTreeScore def

Add-one score on an old n-factor model with an independent mark process. The old Gibbs tower includes every one of its original selected-type terms. · OAI.DilutedSpinGlass.HeterogeneousMarks.insertedTreeScore

insertEndpoint def

The continuous insertion of one endpoint coordinate. · OAI.Thomason.Construction.RealizedCube.insertEndpoint

insertion def

Insert one actual left-degree component into the finite total. · OAI.LittleFinitistic.BimoduleTotal.insertion

insertionCoefficient def

The actual independent index/fresh-label sampling for a fixed old replica array. A fresh label is one whole tree sample, not a new draw at each leaf. · OAI.DilutedSpinGlass.insertionCoefficient

insertionPerm def

Move the first coordinate to a specified slot, without changing the order of the others. · OAI.CubeShuffle.insertionPerm

insertKnotIndex def

Insertion map for the common M rows into the (sorted) interior-knot flag. · OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.insertKnotIndex

insertPermutationVertex def

Insert one new vertex after b in its permutation cycle. · OAI.KadisonSimilarity.insertPermutationVertex

insertSite def

Reinsert one fixed site into a configuration on the other sites. · OAI.JointDickman.insertSite

insertSpin def

The spin at the removed site is inserted without discarding any edge interaction. · OAI.BufferedIsing.DSS.insertSpin

insertTest def

The exact test in the manuscript. Its input is a qualifying request, not a condition involving lifetimes, radii, allocation, or rounding. · OAI.KServer.Chronological.insertTest

insertUnit def

The clear-and-insert competitor; the clearing radius is 5D*. · OAI.KServer.Pilot.insertUnit

insertWord def

Replace only the angular part of an incoming coefficient history on one new pulse. The formula is global and smooth, with no piecewise selector. · OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord

insertZero def

The coordinate isometry inserting a zero in slot i. · OAI.ProjectionCounterexample.insertZero

Inside def

At hidden positions the draw is unconstrained. · OAI.MaxCutGames.Soundness.ZeroInformation.Inside

Inside def

At hidden positions the draw is unconstrained. · OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Inside

inside def

The actual correction inside the tube. · OAI.ThompsonNonamenability.Analytic.CorrectionData.inside

insideAlgebra def

P, as a star subalgebra of M. Its completeness is derived, not assumed. · OAI.Generator.Tracial.insideAlgebra

insideFlip def

The measure-preserving simultaneous negation of all slice-entry signs. · OAI.OptimalMaxCut.TreeCode.insideFlip

InsideIntersectionProperty def

The inside-parabolic conclusion of §8. Its proof, for arbitrary Artin matrices, must come from the relative stabilizer argument. · OAI.HarmonicArtin.ParabolicIntersections.InsideIntersectionProperty

InSlice def

A simultaneous row fiber and column slice, based at M₀. Agreement on Z is exactly agreement with all column specifications spanning Z. · OAI.MaxCutGames.Inverse.AffineWitness.InSlice

InSlice def

A simultaneous row fiber and column slice, based at M₀. Agreement on Z is exactly agreement with all column specifications spanning Z. · OAI.UniqueGamesTheorem.Inverse.AffineWitness.InSlice

InStage def

Membership in a specified finite minus stage, not just in the limit. · OAI.PureTypeSystem.FreeObservations.InStage

install def

Install the spatial ordered branch O_F, with zero auxiliary history. The boolean is the conversion back to the old chart orientation. Negation exchanges, rather than discards, the two circular boundary columns. · OAI.PlanarL1.Columns.Model.OrderedData.install

install def

At a request boundary only the input/output interface is refreshed. Work tapes and control retain the complete internal state. · OAI.UniformKServer.BitMachine.install

installedTapes def

Only these four tape words change during installation. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.installedTapes

installedTapes def

Only these four tape words change during installation. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.installedTapes

Instance structure

Actual tightened bounded margins, a maximum large-cell forest, and one feasible baseline table determine the completion counts and factorial signatures. · OAI.ContingencyTables.CompanionFactorialApplication.Instance

Instance structure

A positive-integer input, with a nonnegative target. · OAI.LowSpaceSubsetSum.Instance

Instance structure

Constraint occurrences are list entries, so repeated parallel edges retain their multiplicity. No weights are hidden in this representation. · OAI.MaxCutGames.Foundations.Target.Instance

Instance structure

The rational threshold is additional to the graph. · OAI.UniformSparsestCut.Instance

Instance structure

Constraint occurrences are list entries, so repeated parallel edges retain their multiplicity. No weights are hidden in this representation. · OAI.UniqueGamesTheorem.Foundations.Target.Instance

instanceData def

The package consumed by the proved factorial, terminal, and oracle lemmas. Its forest and baseline are decoded executed values. · OAI.ContingencyTables.ComputedCompanionInstance.instanceData

Instant structure

Constant work setup of another environment. · OAI.PowerSaving.RAM.Bench.Instant

instantiate def

Substitution of a variable term for the variable just quantified. · OAI.PartitionConsistency.Formula.instantiate

Instr inductive

A finite-control bit-stack instruction. There is no unbounded internal state and no operation on an entire stack other than one push/pop/peek. · OAI.Superstring.BitCode.Instr

Instruction structure

An `Instruction k q` contains an optional next state among `q` states and one stack action for each of `k` stacks. · OAI.CurrentKS.Instruction

Instruction structure

A primitive is placed on distinct actual wires, with no operation of unbounded arity hidden in a circuit instruction. · OAI.ExactQuantumFactoring.Instruction

Instruction inductive

Static commands; all changing vertex identifiers remain inputs to evaluation. · OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.Instruction

Instruction inductive

Static commands; all changing vertex identifiers remain inputs to evaluation. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.Instruction

instruction def

Tapes: candidate stream, preserved key, candidate payload, key copy, scratch. · OAI.MaxCutGames.BinaryNameCompare.instruction

instruction def

Stack zero is the input, one the output, and two the reversed input. Branches inspect only the finite validator state and the popped symbol. · OAI.MaxCutGames.BinaryTotalInputMachine.instruction

instruction def

Every nonempty pop performs exactly one finite DFA transition. The empty pop emits the final acceptance bit, resets control, and halts. · OAI.MaxCutGames.BinaryValidatorMachine.instruction

instruction def

The row subprogram is a static label placement of the checked emitter. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.instruction

instruction def

Coefficient one, no seed: the destination already contains its offset. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.instruction

instruction def

The labels contain two fixed affine copies and one fixed list of drains. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.instruction

instruction def

The five finite initialization labels can be placed in a caller's program. The native halt becomes its chosen continuation in the very same transition. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.instruction

instruction def

Only the coefficient, word, and direction are built into finite control. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.instruction

instruction def

A concrete instruction for each of the n drain phases and the final reset. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.instruction

instruction def

Fixed concrete drain instructions on the actual shared address state. · OAI.MaxCutGames.Integration.AddressTupleCleanup.instruction

instruction def

Local finite labels are placed in an arbitrary caller label space, with an explicit continuation. Every instruction is determined by the fixed template. · OAI.MaxCutGames.Reduction.MachineFieldTemplate.instruction

instruction def

Fixed finite instruction assembly, with arbitrary placement and continuation. · OAI.MaxCutGames.Reduction.MachineTemplateAddress.instruction

instruction def

Tapes: candidate stream, preserved key, candidate payload, key copy, scratch. · OAI.UniqueGamesTheorem.BinaryNameCompare.instruction

instruction def

Stack zero is the input, one the output, and two the reversed input. Branches inspect only the finite validator state and the popped symbol. · OAI.UniqueGamesTheorem.BinaryTotalInputMachine.instruction

instruction def

Every nonempty pop performs exactly one finite DFA transition. The empty pop emits the final acceptance bit, resets control, and halts. · OAI.UniqueGamesTheorem.BinaryValidatorMachine.instruction

instruction def

The row subprogram is a static label placement of the checked emitter. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.instruction

instruction def

Coefficient one, no seed: the destination already contains its offset. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.instruction

instruction def

The labels contain two fixed affine copies and one fixed list of drains. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.instruction

instruction def

The five finite initialization labels can be placed in a caller's program. The native halt becomes its chosen continuation in the very same transition. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.instruction

instruction def

Only the coefficient, word, and direction are built into finite control. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.instruction

instruction def

A concrete instruction for each of the n drain phases and the final reset. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.instruction

instruction def

Fixed concrete drain instructions on the actual shared address state. · OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.instruction

instruction def

Local finite labels are placed in an arbitrary caller label space, with an explicit continuation. Every instruction is determined by the fixed template. · OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.instruction

instruction def

Fixed finite instruction assembly, with arbitrary placement and continuation. · OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.instruction

instructionTable def

Enumerate all control/read-symbol pairs by finite loops and execute the seven-row local interpreter. This is the finite table used by the geometry. · OAI.ForcedComputation.Recorder.instructionTable

intDistance def

Distance of a real phase to the nearest integer, expressed without a choice of nearest integer. · OAI.Problem337.RationalPhaseSpacing.intDistance

integerAcceptedSpaceTerms def

Scans and word-RAM preprocessing reserve eight scalar/control cells per charged step. Retained input/index cells are counted separately. Numerical setup, local programs and coarse initialization use their explicit allocation counters. … · OAI.EditApproximation.integerAcceptedSpaceTerms

integerAnswer def

The implementation clamps to the input length and rounds down. · OAI.EditApproximation.integerAnswer

integerAugmentation def

The terminal simple is in degree zero after the actual reindexing. · OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerAugmentation

integerBimoduleAugmentation def

The source's augmentation in degrees [-l,0], as a genuine bimodule map. · OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimoduleAugmentation

integerBimoduleComplex def

The genuine bimodule resolution in exactly the source interval [-l,0]. · OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimoduleComplex

integerBinaryAnswer def

The uniform implementation uses exact dynamic programming below the proved cutoff and the evaluated binary memo above it. · OAI.EditApproximation.integerBinaryAnswer

integerBinaryOutput def

Actual binary output on a fixed accepted finite draw. · OAI.EditApproximation.integerBinaryOutput

integerBinarySpace def

The space bound applies to all outcomes, including null-probability outcomes. The exact branch uses the concrete suffix-DP allocation counter. · OAI.EditApproximation.integerBinarySpace

integerBinaryWork def

Full integer-input runtime with concrete local, setup, and final-output routines. · OAI.EditApproximation.integerBinaryWork

integerBitSample def

The actual bits sampled from one uniformly chosen integer origin and independent finite jitters in every residue coordinate. · OAI.TwoPointCorrelations.integerBitSample

integerColumnDeparture def

Each step has one label in the selected column; its coefficient contains only its sign, padding, fixed shift and the primes in other columns. · OAI.TwoPointCorrelations.integerColumnDeparture

integerComplex def

Q_T in the manuscript's cohomological degrees -l,...,0. · OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerComplex

integerCyclotomicEvaluation def

Integer cyclic group-ring evaluation in the actual cyclotomic quotient. · OAI.CirculantHadamard.integerCyclotomicEvaluation

integerDerivedIterateIndexedIso def

The constructed finite derived iterate, now viewed in the actual integer cochain derived category, is represented by the exact indexed block complex. This does not assert an extension of the tensor functor to arbitrary integer inputs. · OAI.DerivedBar.integerDerivedIterateIndexedIso

integerDistance def

Distance to the nearest integer. The tie convention of round does not affect this distance. · OAI.Problem337.RealPhase.integerDistance

integerExtension abbrev

Nonnegative homological degree n is genuine integer cochain degree -n; positive cochain degrees are extended by zero. · OAI.DerivedBar.integerExtension

integerExtensionHomologyIso def

Exact homology-degree comparison for the integer construction. · OAI.DerivedBar.integerExtensionHomologyIso

integerFinalAllocation def

Final conversion allocates only its division and clamping workspace. · OAI.EditApproximation.integerFinalAllocation

integerIndexedCountShiftIso def

The manuscript's actual [r] cochain shift of the indexed recursive bar is isomorphic to the entire signed count complex. · OAI.DerivedBar.ParityBridge.integerIndexedCountShiftIso

integerIndexedDeshiftedCountIso def

Extension of the genuine recursive complex is the actual -r shift of the count complex. Strict support, not truncation by assumption, supplies the inverse. · OAI.DerivedBar.ParityBridge.integerIndexedDeshiftedCountIso

integerIndexedLeadingIso def

The entire leading-bar chain isomorphism survives in the integer derived category. · OAI.DerivedBar.integerIndexedLeadingIso

integerIndexedWeightShiftIso def

Identification with the original count subcomplex, using the actual integer cochain shift and the already verified component sign involution. · OAI.DerivedBar.ParityBridge.integerIndexedWeightShiftIso

IntegerLaw structure

Counts of equally likely slots. The denominator is explicit so that composition can reserve ignored bits without enumerating them. · OAI.ContingencyTables.IntegerLaw

integerNormPolynomial def

Ordinary Dirichlet polynomial, with positive integer frequencies. · OAI.CubicFirstMoment.integerNormPolynomial

integerOutput def

Convert signed-magnitude stack integers to the exact signed-coordinate convention whose negative payload is one less than its absolute value. · OAI.ContinuumCoulomb.EncodingPrograms.integerOutput

integerPairPayload def

Read and remove the actual sign bit, retaining the coordinate payload and the entire following encoded field. · OAI.ContinuumCoulomb.EncodingPrograms.integerPairPayload

IntegerPathLift structure

A real path lift normalized to start at zero, with integral endpoint. · OAI.CoarseAssembly.IntegerPathLift

integerPeriodize def

Integer-periodization of a subset of the line. · OAI.Problem310.Aux.integerPeriodize

integerPowerBlock def

Magnitude is encoded as predecessor, so every resulting block has positive length. · OAI.Generator.Tracial.integerPowerBlock

integerProgressionPartition def

Row/column transposition lists each residue class in increasing order. · OAI.Ostmann.integerProgressionPartition

integerQ def

The actual integer derived-category value of a nonnegative chain complex. · OAI.DerivedBar.integerQ

integerQHomologyIso def

Exact comparison of integer derived homology and the original chain degree. · OAI.DerivedBar.integerQHomologyIso

integerQueryWork def

Complete integer-input cost with the proved local program, rather than an unspecified per-key annotation. · OAI.EditApproximation.integerQueryWork

integerResidueSplit def

A and B contain only the known nonbulk factors. The two variable products are units in the full modulus, and determine the parent product. · OAI.Ostmann.integerResidueSplit

integerRow def

Recover the integer first row without changing the cyclic orientation. · OAI.CirculantHadamard.integerRow

integerSingleIso def

The chain stalk's integer extension is the native integer stalk. · OAI.LittleFinitistic.BimoduleTotal.integerSingleIso

integerSlice def

The literal integer slice before making any near-full grid approximation. · OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.integerSlice

integerStalkIso def

The original nonnegative stalk maps to the actual integer derived stalk. · OAI.DerivedBar.integerStalkIso

integerTemplateType def

Total Boolean type, also on failed layouts; no conditioning is hidden in the definition. · OAI.TraceReconstruction.integerTemplateType

integerTest def

Exact integer Taylor matrices, with the same fixed order of residues. · OAI.RationalHitting.Generator.integerTest

integerUnitIso def

Multiplication by an integer unit is an actual isomorphism in any additive category. · OAI.LittleFinitistic.OrdinarySimulation.integerUnitIso

Integral def

The labelled history is interpreted by the same positive integer pivots as the original sampler. No primality is imposed on a reconstructed giant. · OAI.Ostmann.MovingSlotData.Integral

Integral def

Membership in K[[t]], inside K((t)). · OAI.RationalHitting.LaurentReduction.Integral

IntegralAt def

This is exactly the integer equation at a supported reversal. · OAI.Ostmann.MovingSlotReversal.IntegralAt

integralBasis def

A full lattice has an integer basis indexed by the degree of the field. · OAI.DukePrimeDegree.FullLattice.integralBasis

IntegralCocycle structure

Integral charges with the two identities required on a Rips simplex. · OAI.CoarseAssembly.Rips.IntegralCocycle

IntegralFunctional def

A coordinate functional which is defined integrally on the full ambient integral lattice. · OAI.RationalHitting.LaurentReduction.IntegralFunctional

integralHomologyHomotopyIso def

An actual homotopy equivalence induces an integral homology isomorphism. · OAI.Kaplansky.integralHomologyHomotopyIso

integralInclusion def

The inclusion is literally integer coordinate inclusion into Z[1/2]. · OAI.NuclearUltrapower.Elementary.integralInclusion

integralInclusion def

The inclusion is literally integer coordinate inclusion into Z[1/2]. · OAI.NuclearUltrapower.integralInclusion

integralMap def

Actual projective scheme morphism induced by an integral homogeneous map of connected graded algebras. · OAI.GradedIntegralProj.integralMap

integralMultiplierLattice def

The multiplier order as a submodule of the maximal order. · OAI.DukePrimeDegree.integralMultiplierLattice

integralOperator def

The actual Volterra operator on continuous paths; its norm is bounded by 2 C sqrt T. · OAI.ForcedComputation.WeaklySingular.integralOperator

integralPiece def

The exact integral-coordinate polynomial, with the zero slope handled without division. · OAI.ExactQuantumFactoring.OrderTrial.integralPiece

integralPolynomial def

Integrating a uniformly bounded-degree polynomial coefficient by coefficient. · OAI.PettyProjection.FixedPoint.integralPolynomial

integralReal def

The scalar invariant integral in the manuscript, literally the invariant mean of the period sum on F/Z. · OAI.PlaneFiveColor.InvariantMean.integralReal

IntegralRepresentationFinite def

Finite generation refers to the group-ring action of the representation. · OAI.PolycyclicRecognition.IntegralRepresentationFinite

integralSimplicialChains def

Integral simplicial chains, using the same free-chain construction as the preserved integral singular chain complex. · OAI.Kaplansky.integralSimplicialChains

integralSingularChains def

The same integral singular chains underlying integralSingularHomology. · OAI.Kaplansky.integralSingularChains

integralSingularHomology def

Ordinary singular homology with integer coefficients. · OAI.Kaplansky.integralSingularHomology

integralSL def

The integer special linear group inside the real group. · OAI.DukePrimeDegree.integralSL

IntegralVector def

Coefficientwise integrality, not an arbitrary sublattice. · OAI.RationalHitting.LaurentReduction.IntegralVector

integrateNilpotentLieEquiv def

The group automorphism needed for exact weight dilation. · OAI.PolycyclicRecognition.integrateNilpotentLieEquiv

integrateNilpotentLieEquivContinuous def

Both directions of exponential conjugation are continuous, and the published finite Dynkin formula proves its multiplicativity. · OAI.PolycyclicRecognition.integrateNilpotentLieEquivContinuous

interaction def

Interaction constructed from the actual local pair mass, not assumed. · OAI.BoundedTreewidthL1.TreeMarkov.interaction

interactionBudget def

The deterministic pair-interaction allowance obtained by shells of max uᵢ uⱼ; see the interaction integral in the manuscript. · OAI.SLEExactGauge.Multipoint.interactionBudget

interactionGraph def

Relabeling a finite loop-deleted interaction by Fin does not introduce any assumption on the fields or on connectivity. Parallel edges are kept. · OAI.BufferedIsing.interactionGraph

InteractionSample abbrev

One interaction together with its factorization witness: theta,a,b,f. · OAI.DilutedSpinGlass.InteractionSample

interactionValue def

The interaction label includes the p uniform indices, with repetitions. · OAI.DilutedSpinGlass.PhysicalRoot.interactionValue

intercepts def

The canonical normalized intercept vector. It is zero on configurations with repeated sites; all uses of the prescribed-mass specification have distinct sites. · OAI.Problem358.FixedMassIntercepts.intercepts

intercepts def

The corresponding affine intercepts. · OAI.Problem358.Sharpness.intercepts

interchangeWord def

One coordinate-interchange relation, between the two literal grids. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.interchangeWord

interfaceFourEdge def

The four cyclic edges, with outsider label 4. This definition is local to this interface argument and agrees extensionally with fourEdge. · OAI.EuclideanFiveColor.interfaceFourEdge

interfaceGraph def

Reference-normal graph coordinates for a varying selected interface. · OAI.Problem358.AffinePlaneGraph.interfaceGraph

interfaceMeasure def

Intrinsic tie-plane measure for a pair of affine scores. · OAI.Problem358.IntrinsicSurface.interfaceMeasure

Interior def

Literal interior cells: the exterior cell kind is not selected. · OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.Interior

Interior def

Exactly the literal vertex interior predicate. Narrow containment follows from broad height padding and is included below as a checked consequence. · OAI.PlanarL1.Columns.Model.VertexBands.Interior

interior def

Interior selected positions are exactly those eligible for the two-switch flip. · OAI.Problem335.PathIsolatedWeight.interior

interiorConvolution def

The convolution with the two endpoint terms omitted. · OAI.RegularPointCoordinates.interiorConvolution

interiorCoordinatesEquiv def

The underlying set of a realization is the disjoint union of nondegenerate simplex interiors. This does not give the disjoint-union topology. · OAI.Thomason.Construction.RealizationPrism.interiorCoordinatesEquiv

interiorHeight def

Extra nonleaf numeric labels grouped by their actual child height. · OAI.TraceReconstruction.OccupiedParityTree.Forced.interiorHeight

interiorKnotLabels def

Literal complete labels of M + R C_t, with the C_t row inserted in order. · OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorKnotLabels

interiorLabelBudget def

Uniform arithmetic interior-label budget of a degree-r depth-(b+1) shape. This includes no factor for a bottom label. · OAI.TraceReconstruction.interiorLabelBudget

interiorPrefix def

Prefixes admitting an interior completion in the body. · OAI.Problem358.AffineSlice.interiorPrefix

interiorRunCount def

Number of true runs not touching an endpoint. · OAI.Problem335.WordRuns.interiorRunCount

InteriorSelection def

Only genuine disk-interior cells belong to a fragment. · OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.InteriorSelection

interiorTimes def

Strictly interior mesh, with the initial zero included only as a reference. · OAI.FKCRT.TreeCoding.interiorTimes

interiorVLayers def

The V positions eligible for isolated-position flips. · OAI.Problem335.BalancedSchedule.interiorVLayers

interleavedBasis def

The positively ordered real coordinate basis, using the same recursive slots as the exterior power. · OAI.Mahler.interleavedBasis

interleavedEuclidean def

Interleaved real coordinates: index 2i is real and index 2i+1 imaginary. · OAI.MahlerStokes.interleavedEuclidean

interleavedVolume def

The actual positive coordinate volume form, ordered dx_1,dy_1,... . · OAI.Mahler.interleavedVolume

interleavedWord def

The word e₀ v e₁ v ... v eᵣ₋₁, with an empty-word convention. · OAI.KadisonKastler.interleavedWord

IntermediatePrefixWitness def

Prime-factor prefix data defining one intermediate dyadic band. This does not assume either a divisor-count estimate or a lower bound on the prefix. · OAI.Problem337.DivisorMoment.IntermediatePrefixWitness

intermediateStart def

The operator for p maps the source into the proposed intermediate space. · OAI.Problem335.intermediateStart

Internal def

Internal vertices refer to labeled genealogy, not coincident sampled values. · OAI.DilutedSpinGlass.PrescribedTree.Internal

internal def

The complete set of unmarked internal vertices. · OAI.TorsionFreeZeroDivisors.ChainSubdivision.internal

internalColModes def

Four possible modes for an internal variable column. · OAI.Problem348.ModeIncidence.internalColModes

internalCopyCount def

Copies of F whose elements all lie in the fixed set I. · OAI.LeanBlast.SecondKahnKalai.internalCopyCount

InternalCycle structure

Explicit internal oriented polygon. Every field is finite combinatorial source data; no flag lift or geometric bundle property is a field here. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.InternalCycle

internalDescendantDefect def

The exact finite weighted sum over internal descendants of a node. · OAI.ReflexiveFixedPoints.TreeEvaluation.internalDescendantDefect

internalEdges def

The graph edges joining consecutive layers, indexed by internal vertices. · OAI.Problem335.BalancedSchedule.internalEdges

internalEndpointSet def

The internal vertices adjacent to a specified layer. · OAI.Problem335.Pairings.internalEndpointSet

internalEnds def

Internal vertices adjacent to a layer. Vertex j is between layers j and j+1. · OAI.Problem335.BalancedSchedule.internalEnds

internalFrequencyList def

Only internal frequencies enter the denominators of reconstructed words. · OAI.Ostmann.internalFrequencyList

internalHom def

The right internal hom whose cells are maps from concrete globe cylinders. · OAI.Thomason.ConstructedInterval.internalHom

internalHom def

The global right interval internal-hom functor. · OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.internalHom

internalHomMap def

Postcomposition as a strict functor on the actual mapping categories. · OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.internalHomMap

internalHomObj def

The strict mapping category of the actual interval model. · OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.internalHomObj

internalIsometryRow def

The actual row of a finite family of internal isometries. · OAI.KadisonSimilarity.internalIsometryRow

internalLineProbability def

The normalized count before the giant variables are integrated out. · OAI.Ostmann.internalLineProbability

InternalNode abbrev

All internal nodes of a complete tree of depth h. · OAI.TreeEdit.BinaryLower.FiniteActivity.InternalNode

internalPathContraction def

The internal path object contracts to its starting constant path in all simplicial sets. This fact requires no horn fillers. · OAI.Thomason.Construction.internalPathContraction

internalPathCylinder def

Evaluation, with the interval written as the second cylinder factor. · OAI.Thomason.Construction.internalPathCylinder

internalPathEdges def

Record the edges of a path from its internal vertices and fixed endpoints. · OAI.Problem335.internalPathEdges

internalPathEquiv def

The canonical matrix-path list and the tuple of internal vertices enumerate exactly the same paths. The edge list is preserved, not merely its cardinality. · OAI.Problem335.internalPathEquiv

internalPathEvaluationHomotopy def

The internal evaluation cylinder is an actual simplicial homotopy between its two evaluation maps. · OAI.Thomason.Construction.internalPathEvaluationHomotopy

internalPathIndex def

Locate the explicitly described path in the exact list enumeration. · OAI.Problem335.internalPathIndex

internalPathMinMap def

Evaluate a path at the minimum of its parameter and the contraction time. · OAI.Thomason.Construction.internalPathMinMap

internalPathShrinkingMap def

Internal path shrinking is obtained by transposing the actual min map. · OAI.Thomason.Construction.internalPathShrinkingMap

internalPathTranspose def

Currying a cylinder in this order reverses evaluation exactly. · OAI.Thomason.Construction.internalPathTranspose

internalPatternWeight def

The coefficient before the simultaneous line probabilities includes one factor of the prime for every original compensation occurrence. · OAI.Ostmann.internalPatternWeight

internalPreprocess def

Internal finite-component search, with entry priority. No invocation of the compiled machine as an evaluator occurs here. · OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.internalPreprocess

internalRowModes def

Three possible modes for an internal variable row. Boundary levels may remove some of these modes. · OAI.Problem348.ModeIncidence.internalRowModes

InternalStep def

The relation used for component search; the equation is used both ways in the presentation, but only this direction in the deterministic analysis. · OAI.FiniteAlgebraicEnvelopes.Compiler.InternalStep

internalToFixedPath def

Evaluation reverses this construction on a family in the actual fixed-endpoint internal path complex. · OAI.Thomason.Construction.internalToFixedPath

interpolate def

The weighted Minkowski interpolation with the manuscript convention. · OAI.ContingencyTables.PublishedInputs.interpolate

interpolate def

The literal locally finite tent interpolation, indexed by the whole grid. · OAI.DyadicHats.interpolate

interpolate def

The literal locally finite tent interpolation, indexed by the whole grid. · OAI.SignedDisk.DyadicHats.interpolate

interpolate def

The two homotopies from the lower clamping map. · OAI.Thomason.Construction.HornContraction.interpolate

interpolate def

Continuous interpolation in the barycentric image, with its actual finite-poset realization topology. · OAI.Thomason.Construction.PosetGeometry.interpolate

Interpolation structure

Numeric input to the literal interpolation hierarchy. · OAI.PlanarL1.Parameters.Interpolation

interpolationNode def

Distinct real interpolation nodes strictly between zero and one. · OAI.JointDickman.interpolationNode

interpolationNode def

An explicit set of D + 1 nonzero complex interpolation parameters. · OAI.MatrixMultiplication.AuxiliarySeparation.interpolationNode

interpret def

Total interpretation of a label; the certificate will establish det=1 at every label used. · OAI.NuclearUltrapower.SOS.interpret

interpreted def

A total proof-side interpretation. The fallback handles arbitrary malformed static specs; actual canonical rows always take the checked decoding branch. · OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.interpreted

interpreted def

A total proof-side interpretation. The fallback handles arbitrary malformed static specs; actual canonical rows always take the checked decoding branch. · OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.interpreted

interpretedCopy def

Interpretation of the actual prescribed quotient, not of a free collection of formal copies. · OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.interpretedCopy

interpretedLetter def

A family satisfying the original presentation's transition relations induces its equivariant interpretation on direct-limit letters. · OAI.PartitionConsistency.ProbeAlgebra.Path.interpretedLetter

intersectionEquiv def

Common graph vectors correspond exactly to the kernel of the difference. · OAI.MaxCutGames.Inverse.MatrixChart.intersectionEquiv

intersectionEquiv def

Common graph vectors correspond exactly to the kernel of the difference. · OAI.UniqueGamesTheorem.Inverse.MatrixChart.intersectionEquiv

intersectionSubtypeSwap def

The same intersection subspace, in the opposite order of its subtypes. · OAI.Kaplansky.intersectionSubtypeSwap

intertwinerMatrix def

Matrix in the actual orthonormal word basis, with no change of representation. · OAI.RowColumn.Signed.intertwinerMatrix

intertwinerMetricUnit def

The metric of a bounded linear isomorphism has an explicit inverse. · OAI.KadisonSimilarity.intertwinerMetricUnit

Intertwines def

An actual equivariant inclusion, not an unspecified overlap matrix. · OAI.RowColumn.Intertwines

intertwining def

Elements whose action commutes with a specified linear map form a subalgebra. · OAI.LittleFinitistic.EncodingLinearity.intertwining

Interval def

The unlabelled interval, including both endpoints. · OAI.KLInvariance.Interval

Interval abbrev

One interval uses one path index and two integer endpoints. · OAI.TorsionFreeZeroDivisors.PatternCoding.Interval

interval def

Every branch compares exact rational powers. The loop count is the explicit depth, independent of the comparison outcomes. · OAI.ContingencyTables.RationalRootBisection.interval

interval def

The actual interval A ≤ L ≤ B among the ell-dimensional vertices. · OAI.MaxCutGames.Inverse.KMS.interval

interval def

The actual interval A ≤ L ≤ B among the ell-dimensional vertices. · OAI.UniqueGamesTheorem.Inverse.KMS.interval

intervalBottom def

Named endpoints for an actual nonempty interval. · OAI.KLInvariance.intervalBottom

intervalBoundaryFamily def

Assemble two maps on the two components of an interval boundary. · OAI.Thomason.Construction.intervalBoundaryFamily

intervalCell def

Tensoring a cell with the edge produces an actual positive globular cell. · OAI.Thomason.Construction.DirectedComplex.RightCylinder.intervalCell

intervalCellTable def

The full table of the tensor of a globular cell with the oriented edge. · OAI.Thomason.Construction.DirectedComplex.RightCylinder.intervalCellTable

intervalDegrees def

A finite interval of actual right-complex degrees, including both endpoints. · OAI.LittleFinitistic.BimoduleTotal.intervalDegrees

intervalDensity def

Normalized restriction density, relative to the probability base measure. · OAI.FiniteFactor.intervalDensity

intervalDisplacement def

Displacement of the contiguous positions a, ..., b-1. · OAI.TwoPointCorrelations.intervalDisplacement

intervalDistance def

Distance from a physical value ell+n to [0,b]. This formula applies to the companion's unary tree penalties. · OAI.ContingencyTables.ScalarPenalty.intervalDistance

intervalEdge def

The nondegenerate edge of the simplicial interval, with its actual initial and final vertices. · OAI.Thomason.Construction.intervalEdge

intervalEdge def

The unique top-dimensional basis edge of the first simplex. · OAI.Thomason.Construction.SimplexComplex.intervalEdge

intervalEdgeSlope def

Restriction of the actual geometric root slope to a full plane interval. · OAI.KLInvariance.TitsSpace.PlaneBasis.intervalEdgeSlope

intervalEquiv def

Each offset is sent to its integer by adding the exact lower ceiling endpoint. This is the actual source interval, not a cardinality-only choice. · OAI.ContingencyTables.CompanionOracleDensity.intervalEquiv

intervalFamily def

The actual finite interval set used by the single admissibility condition. · OAI.ThompsonNonamenability.intervalFamily

IntervalFiniteShift def

Exact finite-cardinality translation on a fixed interval. · OAI.InfiniteMatroidCounterexample.IntervalFiniteShift

intervalFlip def

An automorphism of the unlabelled full dihedral interval, fixing its ends. It need not arise from a Coxeter-system automorphism at those ends. · OAI.KLInvariance.Dihedral.intervalFlip

intervalIso def

The exact unlabelled interval identification used in the finite-rank reduction; it arises from a proved embedding, not an added main hypothesis. · OAI.KLInvariance.StandardParabolic.intervalIso

intervalIso def

Reverse the strict interval together with all its directions. · OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.intervalIso

intervalIso_restrict def

Restriction of the actual interval isomorphism to any subinterval. This is the same unlabeled map, not a new isomorphism with extra structure. · OAI.KLInvariance.intervalIso_restrict

intervalLaw def

Lebesgue probability on a nondegenerate interval. · OAI.Problem358.IntervalMidpoint.intervalLaw

intervalLayers def

A finite interval of the schedule, with a specified layer type. · OAI.Problem335.BalancedSchedule.intervalLayers

intervalLo def

Clipped natural endpoints for the intersection of two rational intervals. · OAI.ExactQuantumFactoring.OrderTrial.intervalLo

intervalMass def

The mass of a closed frequency interval. · OAI.LipschitzHilbert.intervalMass

intervalMax def

Pointwise maximum of two simplices of the ordered interval. · OAI.Thomason.Construction.intervalMax

intervalMin def

Pointwise minimum of two simplices of the ordered interval. · OAI.Thomason.Construction.intervalMin

intervalPhase def

A phase sequence with zero extension outside a closed integer interval. · OAI.Problem337.intervalPhase

intervalPreimage def

Matrices whose chart images lie in an ambient interval. · OAI.UniqueGamesTheorem.Inverse.KMS.intervalPreimage

intervalProbability def

The normalized Lebesgue law on a closed interval. Endpoints have zero mass. · OAI.LipschitzHilbert.intervalProbability

intervalRelation def

A genuine interval relation; omitted steps have empty supports as well as zero coefficients. This matters for the later-variable exclusion. · OAI.TwoPointCorrelations.LabeledPrimeWord.intervalRelation

intervalSystem def

A finite interval in an ancestral order. This keeps the root in every tree. · OAI.DiamondDistortion.intervalSystem

intervalTerms abbrev

The genuine cochain differential on the selected finite interval. · OAI.LittleFinitistic.OrdinarySimulation.intervalTerms

intervalTrial def

One bounded trial rejects only the unused terminal indices. · OAI.ContingencyTables.ExactIntegerChoice.intervalTrial

intervalUniform def

The uniform probability law on one coordinate of the cube. · OAI.Problem358.intervalUniform

intervalWord def

Chronological concatenation between whole-piece boundaries. · OAI.FKCRT.Inventory.intervalWord

IntExpr structure

Balanced integers avoid a word-size-dependent signed representation. · OAI.ExactQuantumFactoring.IntExpr

IntExprPoly def

All balanced integer components have polynomial literal circuit syntax. · OAI.ExactQuantumFactoring.IntExprPoly

inTime def

A genuine finite-machine execution with a cubic input-length budget. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.inTime

inTime def

An actual-time certificate for the complete fixed-dimensional schedule. · OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.inTime

inTime def

Actual two-phase initialization from the concrete machine input. · OAI.MaxCutGames.Reduction.AddressMachineInitial.inTime

inTime def

Actual copying, two-field extraction, and complete disposal of the work copy. · OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.inTime

inTime def

A genuine finite-machine execution with a cubic input-length budget. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.inTime

inTime def

An actual-time certificate for the complete fixed-dimensional schedule. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.inTime

inTime def

Actual two-phase initialization from the concrete machine input. · OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.inTime

inTime def

Actual copying, two-field extraction, and complete disposal of the work copy. · OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.inTime

inTimeAt def

A timed certificate for the same actual trace, bounded by a single linear polynomial in the original table encoding length. · OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.inTimeAt

inTimeAt def

A timed certificate for the same actual trace, bounded by a single linear polynomial in the original table encoding length. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.inTimeAt

intrinsicAdjointCharacterHom def

The character is constructed from the actual adjoint action. · OAI.PolycyclicRecognition.intrinsicAdjointCharacterHom

intrinsicCutCoefficient def

The normalized intrinsic integral over an interface with additional affine cuts. Unlike the local faceCoefficient, this definition uses no reference normal or basepoint. · OAI.Problem358.AffinePlaneGraph.intrinsicCutCoefficient

intrinsicProductConditional def

The normalized intrinsic-product description of a box conditional. · OAI.DukePrimeDegree.RootPrefixBox.intrinsicProductConditional

intrinsicShadow def

Planar Lebesgue measure of the orthogonal shadow, intrinsically in the plane. · OAI.TriangularCovering.intrinsicShadow

Introspective def

The evaluation form of an introspective exponent modulo X^s-1. · OAI.ExactQuantumFactoring.Primality.Introspective

intToNatProgram def

Clamp a signed binary integer to a natural number. · OAI.ContinuumCoulomb.ChargePrograms.intToNatProgram

inv def

Reflection reverses every vertex, negates the traversal signs, and exchanges both sides of each band potential. · OAI.KervaireRibbon.OuterRibbon.inv

Invariant structure

The invariant concerns actual residual values, not numerical signs. · OAI.ContinuumCoulomb.ApproximateBisection.Invariant

invariantConditionalKernel def

Conditional probabilities over the complete invariant sigma algebra. · OAI.PolycyclicRecognition.invariantConditionalKernel

invariantConditionalMeasures def

Pull the conditional kernel back to the original space. · OAI.PolycyclicRecognition.invariantConditionalMeasures

invariantCurve def

The global integral curve starting at the identity. Its independence of the existence theorem's choice follows from ODE uniqueness. · OAI.PolycyclicRecognition.invariantCurve

invariantCurve def

The global integral curve starting at the identity. Its independence of the existence theorem's choice follows from ODE uniqueness. · OAI.PolycyclicRecognition.SmoothLie.invariantCurve

InvariantFactor structure

The measurable factor, without imposing any quotient topology. · OAI.PolycyclicRecognition.InvariantFactor

invariantFactorMap def

Identity on points, with the coarser invariant sigma algebra as codomain. · OAI.PolycyclicRecognition.invariantFactorMap

invariantMultilinearSubmodule def

The symmetry condition is a linear subspace condition on actual maps. · OAI.MetricEntropyDuality.SymmetricForm.invariantMultilinearSubmodule

invariantRicciGradient def

The uncompressed Ricci right side in an arbitrary frame. The first coefficient is 6 + 3; the remaining two terms are the differentiated matrix equation and the full bundle curvature contribution. · OAI.PositiveEinsteinFour.Geometry.invariantRicciGradient

invariantRootGeneratedGroup def

The group generated by all root groups preserving the actual measure. · OAI.PrimeDegreePackets.invariantRootGeneratedGroup

invariantRootSetoid def

The blocks are equivalence classes of actual root invariance. · OAI.DukePrimeDegree.invariantRootSetoid

invariantSigma def

The sigma algebra of measurable sets invariant under the entire action. · OAI.PolycyclicRecognition.invariantSigma

invariantStageCoefficient def

The coefficient with distinguished endpoint and two groups of tail letters. · OAI.KadisonSimilarity.invariantStageCoefficient

invariantStageForm def

Multilinearity of the actual finite-stage coefficient function. · OAI.KadisonSimilarity.invariantStageForm

invariantStarRepresentation def

Restriction of an invariant star subalgebra to the closed subspace. · OAI.KadisonSimilarity.invariantStarRepresentation

InvariantSubset def

Invariance for an ambient subset under a map of the norm subtype. · OAI.ReflexiveFixedPoints.InvariantSubset

inverse def

The actual inverse associativity map of balanced tensors. · OAI.LittleFinitistic.BalancedAssociativity.inverse

inverse def

A measurable total representative of the inverse conjugacy; it uses an arbitrary value only off the given invariant conull subset. · OAI.SmoothObstruction.ConullTransport.inverse

inverse def

Descending the compatible clamping maps gives the inverse of the cosieve map. · OAI.Thomason.Construction.CosieveSimplex.inverse

inverse def

Descending the compatible clamping maps gives the inverse of the sieve map. · OAI.Thomason.Construction.SieveSimplex.inverse

inverse def

Exchange the endpoints and literally negate both chord directions. · OAI.Tingley.AlignedConfiguration.inverse

inverseAt def

Reassociate a fixed first input through the actual B-balanced quotient. · OAI.LittleFinitistic.BalancedAssociativity.inverseAt

inverseAveragedTransfer def

Average the transfer over a whole probability fiber. · OAI.PolycyclicRecognition.inverseAveragedTransfer

inverseAverageError def

The error is the average of differences inside one fiber. · OAI.PolycyclicRecognition.inverseAverageError

inverseBandSolution def

Choose an inverse nonseparating arc and preserve all vertex, boundary, and surface equations over the coefficient algebra. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.inverseBandSolution

inverseCocycleError def

The actual inverse-height cocycle after adding the inverse transfer. · OAI.PolycyclicRecognition.inverseCocycleError

inverseCubeDensity def

The concrete normalized inverse-cube density, with an absolute width bound. · OAI.DiskKernels.inverseCubeDensity

inverseCubeDensity def

The concrete normalized inverse-cube density, with an absolute width bound. · OAI.SignedDisk.DiskKernels.inverseCubeDensity

inverseDerivative def

Explicit inverse coordinates of the differential; no finite-dimensional or genericity assumption is needed for this algebraic step. · OAI.KervaireFixedSpace.inverseDerivative

inverseEnclosure def

Second-order inverse enclosure, padded by the exact radius 2·10⁻¹⁷. · OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.inverseEnclosure

inverseF def

The inverse formula for F in terms of the slots now called L,N. · OAI.StableCoordinate.Linearization.inverseF

inverseFiberTransfer def

In inverse coordinates, subtract the proposed domain height. · OAI.PolycyclicRecognition.inverseFiberTransfer

inverseGeneratorWord def

Reverse a generator word and negate its one-parameter amplitudes. · OAI.PolycyclicRecognition.inverseGeneratorWord

InverseGoldbach def

Ostmann's main statement, including all finite modifications of the primes. · OAI.Ostmann.InverseGoldbach

inverseHessianTrace def

The actual inverse-Hessian linearized operator, without the harmless positive determinant factor in the frozen original PDE. · OAI.AffineBernstein.inverseHessianTrace

inverseJ def

The inverse formula for J in terms of the slots now called L,N. · OAI.StableCoordinate.Linearization.inverseJ

inverseMetricFrame def

A finite-dimensional inverse metric represented by an actual linear frame. · OAI.RegularPointCoordinates.inverseMetricFrame

inverseMetricPair def

Pairing of tangent covectors by the inverse first fundamental form. · OAI.ClosedSurfaceR4.RealModes.inverseMetricPair

inverseNodes def

The list retains occurrences, not just distinct subexpressions. · OAI.RationalHitting.Formula.inverseNodes

inverseNthRoot def

A convenient exact representation of the reciprocal n-th root, always used on a strictly positive directional Hessian. · OAI.AffineBernstein.inverseNthRoot

inversePairCoupling def

The coupling measure in inverse coordinates, defined by the actual chart. · OAI.PolycyclicRecognition.inversePairCoupling

InverseParameters structure

Fixed dimensions, density and sparse mask for one logical alphabet. The remaining gadget codimension may be arbitrary when choosing the cube. · OAI.MaxCutGames.Decoder.MatrixGapChoice.InverseParameters

InverseParameters structure

Fixed dimensions, density and sparse mask for one logical alphabet. The remaining gadget codimension may be arbitrary when choosing the cube. · OAI.UniqueGamesTheorem.Decoder.MatrixGapChoice.InverseParameters

InversePrinciple def

Dimension-uniform inverse statement. The constants α,r depend only on η; only the final input dimension threshold may depend on ell. There is no folding assumption, and no inverse-theorem certificate is hidden in f. · OAI.MaxCutGames.Inverse.Shortcode.InversePrinciple

InversePrinciple def

Dimension-uniform inverse statement. The constants α,r depend only on η; only the final input dimension threshold may depend on ell. There is no folding assumption, and no inverse-theorem certificate is hidden in f. · OAI.UniqueGamesTheorem.Inverse.Shortcode.InversePrinciple

InverseRepairInput abbrev

The three indices are the negative cell, positive cell and crossing cell. A crossing cell outside the small list has its length as index. · OAI.ContingencyTables.ProfilePrograms.InverseRepairInput

inverseRepairRow def

Undo the row transfer, using only additions, subtractions and tests against the two specified cells. · OAI.ContingencyTables.SmallGraphProfiles.inverseRepairRow

inverseShift def

The inverse of an injective bounded symmetric map, translated by a real scalar. · OAI.SharpLiebThirring.OperatorProof.inverseShift

inverseStripBase def

The first-coordinate projection of a compact strip in inverse coordinates. Its Haar mass is the constant in the local error bound. · OAI.PolycyclicRecognition.inverseStripBase

inverseTheta def

The inverse-section transfer with its required inverse linear coefficient. · OAI.PolycyclicRecognition.inverseTheta

inverseTranspose def

The adjoint of the inverse of a bounded linear equivalence. · OAI.RegularPointCoordinates.inverseTranspose

inverseTransposeVariation def

The first variation of an inverse transpose. · OAI.RegularPointCoordinates.inverseTransposeVariation

inversionEquiv def

The true ambient plane inversions are in bijection with the inversions of the canonical induced system. · OAI.KLInvariance.TitsSpace.PlaneBasis.inversionEquiv

inversions def

Number of ordered pairs consisting of a D slot followed by an X slot. · OAI.DerivedBar.Multibar.inversions

invertHom def

The projective involution (x,y) ↦ (1/x,y/x), constructed on its principal open before extending to the function field. · OAI.SourceSymmetry.invertHom

involution def

The Hamiltonian involution's underlying projective equivalence. · OAI.ArnoldCounterexample.Quadric.involution

involutionAdd def

Algebraic involution on the complex group ring: conjugate coefficients and invert group elements. This is not the pointwise star on coefficient functions. · OAI.NuclearUltrapower.GroupStarAlgebra.involutionAdd

involutionEquiv def

Regard a checked involution as a permutation with the same inverse. · OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.involutionEquiv

involutionEquiv def

Regard a checked involution as a permutation with the same inverse. · OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.involutionEquiv

involutionHamiltonianPath def

A complete explicit Hamiltonian witness for the actual quadric involution. No flow existence, moment-map theorem, or descent theorem is assumed. · OAI.ArnoldCounterexample.Quadric.involutionHamiltonianPath

involutionLinear def

The linear involution fixing the first coordinate. · OAI.ArnoldCounterexample.Quadric.involutionLinear

invPointMap def

The inverse polynomial map. · OAI.StableCoordinate.AmbientMaps.PolynomialEquiv.invPointMap

InW11 def

Real inhomogeneous W^(1,1) on the whole plane. · OAI.CenteredDiskEndpoint.InW11

InW11 def

Real inhomogeneous W^(1,1) on the whole plane. · OAI.SignedDisk.CenteredDiskEndpoint.InW11

InW11Loc def

Local W^(1,1), expressed using the same distributional gradient convention. · OAI.CenteredDiskEndpoint.InW11Loc

InW11Loc def

Local W^(1,1), expressed using the same distributional gradient convention. · OAI.SignedDisk.CenteredDiskEndpoint.InW11Loc

Inward def

An admissible velocity is strictly inward at every active half-plane. · OAI.TriangularBilliards.Triangle.Inward

inwardOne def

Coefficientwise clipping is done with the actual inward potentials, not an abstract substitute for a test or a changed cost. · OAI.BoundedTreePotentials.BlockCalculus.inwardOne

inwardOne def

The two different inward pieces; their difference is the original relative potential. The value at the inherited head c determines their direction. · OAI.BoundedTreePotentials.inwardOne

InwardPiece structure

The information delivered by inward clipping, with unnormalized block budgets. · OAI.BoundedTreePotentials.BlockCalculus.InwardPiece

inwardQuadratic def

The primitive equals dist²/2 - R²/2 inside the ball. · OAI.RegularPointCoordinates.inwardQuadratic

iota def

Original insertion through the zero-column inclusion of the actual total. · OAI.ExternalTensor.Section4.ArrowVertex.iota

iota def

The manuscript's original first-vertex insertion into the constructed total. · OAI.LittleFinitistic.FirstVertex.iota

iota def

The original vertex insertion after balanced tensoring and the canonical comparison. · OAI.LittleFinitistic.FullTensorRectification.iota

ipt def

local notation centered pairing with normalized inner product · OAI.GeneralMahler.ProjField.ipt

Irreducible def

Irreducibility with exactly the invariant-subspace convention of the source. · OAI.NuclearUltrapower.FiniteUnitaryRep.Irreducible

IrreducibleMatrixSource structure

The actual increasing irreducible matrix source in a fixed normal representation. · OAI.KadisonSimilarity.IrreducibleMatrixSource

IsAC2 def

Absolute continuity with a square-integrable metric control. · OAI.WeakHessian.IsAC2

IsAffineThreeSpaceFiber def

An isomorphism of affine coordinate algebras, not a set-theoretic bijection. · OAI.StableCoordinate.IsAffineThreeSpaceFiber

IsAntecedent def

Actual quotient-compression antecedents with the complement conditions in the passage from (A.15) to (A.16). · OAI.MaxCutGames.Appendix.AntecedentCount.IsAntecedent

IsAntecedent def

The actual complement conditions after choosing domain/codomain splittings. · OAI.MaxCutGames.Appendix.DerivativeInduction.IsAntecedent

IsAntecedent def

Actual quotient-compression antecedents with the complement conditions in the passage from (A.15) to (A.16). · OAI.UniqueGamesTheorem.Appendix.AntecedentCount.IsAntecedent

IsAntecedent def

The actual complement conditions after choosing domain/codomain splittings. · OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.IsAntecedent

IsAssociated def

The usual graph characterization of the operator associated with a closed semibounded form. The quantifier is over the entire weak H¹ domain. · OAI.SharpLiebThirring.OperatorProof.IsAssociated

IsAtomicGeneric def

Precisely the two families of dense sets needed for the atomic truth lemma. Their existence and density were proved above. · OAI.PartitionConsistency.SetForcingNames.AtomicForcing.IsAtomicGeneric

IsAUC def

AUC requires positivity at every strictly positive parameter. · OAI.ForestSpace.IsAUC

IsBadLeaf def

Equality at the threshold is bad, so a good leaf has a strict inequality. · OAI.ReflexiveFixedPoints.IsBadLeaf

IsBallApproximation def

Distortion and density for a ball approximation, without requiring the center to be preserved. This also covers ordinary, unpointed GH maps. · OAI.RegularPointCoordinates.IsBallApproximation

IsBasic def

A basic form annihilates the genuine circle-fiber direction. · OAI.ArnoldCounterexample.CriticalBound.IsBasic

IsBasisAtom def

Steiner's downward-recursive formula specifies every entry of an atom. · OAI.Thomason.Construction.SimplexComplex.IsBasisAtom

IsBeamSplitterOutput def

Reduced state after passive beam-splitter mixing of independent ports. The second row of the orthogonal rotation is (-√(1−η),√η); changing its sign has no effect on this reduced state. HasSum records the actual partial trace, not a … · OAI.EntropyPhotonNumber.IsBeamSplitterOutput

IsBinLabel def

All label checks precede evaluation of any retention expression. · OAI.ExactQuantumFactoring.OrderTrial.IsBinLabel

IsBlockHomogeneous def

A polynomial is homogeneous of the specified degree in one block. · OAI.Problem346.PolynomialWeights.IsBlockHomogeneous

IsBlockIdempotent def

A block is a nonzero primitive idempotent in the center, not necessarily a primitive idempotent of the whole ring. · OAI.Donovan.IsBlockIdempotent

IsBoundary structure

An enumerated literal face boundary; the empty outside is allowed. · OAI.HyperbolicObstruction.PictureSwitch.IsBoundary

IsBoundary def

A specified exterior cycle, including the empty boundary. Its entries are incidences (darts), not necessarily distinct vertices or geometric edges. · OAI.Release075.IsBoundary

IsBoundedField def

Globally bounded strongly measurable fields; all derivative selections below have this property. · OAI.DoublingHilbert.IsBoundedField

IsBranch def

All earlier coordinates of a branch are the actual ancestors. · OAI.ReflexiveFixedPoints.OrderedTree.IsBranch

IsCentralSupport def

The central support of a projection, expressed by its central annihilators. · OAI.BoundedHochschild.KadisonRingrose.IsCentralSupport

IsChartHolomorphic def

Standard local-coordinate holomorphy for an actual section of the quotient projection. · OAI.Nagata.W08.IsChartHolomorphic

IsCircuit def

The enlarged normal form of depth at most d. Identity local and reflection layers are allowed. · OAI.QAC.IsCircuit

isClassFormula def

τ is the E-class of some element of A. Slots are τ,A,E. · OAI.PartitionConsistency.SetLanguage.isClassFormula

IsClassicalLinearizedPair def

The physical coupled equation, with the actual odd-power coefficients. · OAI.DefocusingNLS.IsClassicalLinearizedPair

IsClassicalLinearizedSourcePair def

The coupled eigenvalue equation with an explicitly represented source. · OAI.DefocusingNLS.IsClassicalLinearizedSourcePair

IsCocycle def

The left cocycle convention for an isometric representation. · OAI.PolycyclicRecognition.IsCocycle

isColimit def

Its actual colimit universal property. · OAI.Thomason.Construction.RealizationPrism.isColimit

isColimit def

The small semantic quotient is the colimit of the original diagram. · OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.isColimit

isColimit def

Every strict category has the actual small globe-and-pasting presentation. · OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.isColimit

IsCommonSuperstring def

Ordinary contiguous substring containment, including the empty word. · OAI.Superstring.IsCommonSuperstring

IsComplementaryComponent def

An actual connected component of the closed complement. · OAI.CircleDomainRigidity.IsComplementaryComponent

IsComplete def

Completeness of the Riemannian length distance, not that of a chart norm. · OAI.KahlerUniformization.SmoothKahlerMetric.IsComplete

IsCompletelyBounded def

Complete boundedness in terms of the concrete matrix norm. · OAI.KadisonSimilarity.IsCompletelyBounded

IsComponent def

A full strongly connected component, not merely a connected subset. · OAI.PureTypeSystem.IsComponent

IsComponentArray def

Arrays on one labelled component, extended by zero to all other segments. This is exactly an array indexed by t≼v in that component. · OAI.BoundedTreePotentials.Segments.IsComponentArray

IsConfigurationZariskiClosed def

Relative Zariski closedness on the open subset of distinct tuples. · OAI.Nagata.ProjectiveGeometry.IsConfigurationZariskiClosed

IsConical class

Conicality is the condition from the source, not right cancellation. · OAI.PartitionConsistency.DiagramOrder.IsConical

IsConstantLaplacianOn def

The actual local weak equation with a constant source. · OAI.RegularPointCoordinates.IsConstantLaplacianOn

IsContinuousHeatKernel structure

The positive-time representative of the actual Cheeger heat semigroup. The representation is required only for data in L¹ ∩ L². The convolution fields are the Chapman--Kolmogorov identity in the same published Section 2.2; integrability … · OAI.RegularPointCoordinates.IsContinuousHeatKernel

IsControlledTuple def

All pairwise differences of a tuple belong to the indicated finite scale. · OAI.PolycyclicRecognition.IsControlledTuple

IsConvexBody def

Compact, convex, and full-dimensional in its specified Euclidean space. · OAI.ProjectionCounterexample.IsConvexBody

IsCoordinate def

A coordinate is sent to the first variable by some complex algebra automorphism. · OAI.StableCoordinate.IsCoordinate

IsCoupling def

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

IsCritical def

dh_q = 0, expressed using all local lifts, independent of normal extensions. · OAI.ArnoldCounterexample.IsCritical

IsCrossPairing def

Every tail pair joins one source slot to one test slot. · OAI.KadisonSimilarity.IsCrossPairing

IsCuntzTwoAlgebra def

The universal nonzero unital C*-algebra on the two Cuntz isometries. · OAI.NuclearUltrapower.IsCuntzTwoAlgebra

IsCut def

A nonempty proper subset of the vertices. · OAI.UniformSparsestCut.IsCut

IsCycle def

An actual simple directed cycle of positive length. A cyclic enumeration of r + 1 distinct vertices supplies every successive arc, including the closing arc. A 2-cycle is allowed; looplessness rules out length 1. · OAI.DirectedFeedback.Digraph.IsCycle

IsCyclic def

One connected cyclic order, including the one-element cycle. · OAI.HyperbolicObstruction.FanLink.IsCyclic

IsDefect def

The defect equation q=x-e_t+e_s identifies the sign convention. · OAI.ContingencyTables.IsDefect

IsDefectGroup def

Defect groups are maximal, under inclusion, among the p-subgroups with nonzero Brauer image. This does not impose a commutativity condition. · OAI.Donovan.IsDefectGroup

isDiagonal def

The diagonal flag used by the local geometric moment table. · OAI.Problem335.MomentPairing.isDiagonal

IsDimensionSpectralValue def

Approximation specification, not an assumed linear trace. · OAI.Generator.Tracial.IsDimensionSpectralValue

IsDirichletMeasureSource def

The distributional positive source on the Dirichlet Lipschitz core. The source is integrated only on continuous representatives. · OAI.RegularPointCoordinates.IsDirichletMeasureSource

IsDisjoint def

A recursive form of disjointness, equivalent to pairwise disjoint labels on every full path. · OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.IsDisjoint

IsDiskOrAtomLaw def

The component laws permitted in the manuscript's transverse mixtures. · OAI.BoltzmannNonuniqueness.GeometricSlice.IsDiskOrAtomLaw

IsDummy def

The raw dummy-position predicate. · OAI.Problem348.Construction.SelectedAnchors.IsDummy

IsDyadic def

Dyadic means an integer over a nonnegative integral power of two. · OAI.ExactQuantumFactoring.OrderTrial.IsDyadic

IsEigen def

Exact integrated real eigen-equation; no regularity of W beyond local L¹. · OAI.SharpLiebThirring.SobolevProof.C1L2.IsEigen

IsElementary def

The elementary class allows both zero transverse width and arbitrary axial atoms. · OAI.BoltzmannNonuniqueness.SheetClass.IsElementary

IsElementaryAmenable inductive

The elementary amenable class, with directed-union closure expressed by the canonical directed family of all finitely generated subgroups. · OAI.PolycyclicRecognition.IsElementaryAmenable

IsEnergySolutionModuloConstants def

A pressure class has an energy-regular representative satisfying the equations. Its spatially constant gauge may depend on time. · OAI.ForcedComputation.CompactEuclidean.IsEnergySolutionModuloConstants

IsEquivalentNorm def

A seminorm with these bounds is a genuine norm equivalent to the original norm. · OAI.IndependentProducts.IsEquivalentNorm

IsEstimator def

The estimator may depend arbitrarily on n, q and every complete sample. Its value is its conditional probability of reporting the given input. · OAI.TraceReconstruction.IsEstimator

IsExactMeanNormalization def

The adjoint of a coordinate normalization acts on the coefficients of the scalar Sobolev column. · OAI.RegularPointCoordinates.IsExactMeanNormalization

IsExit def

Minimal nodes outside an initial set, including roots of unused components. · OAI.BoundedTreePotentials.Segments.IsExit

isExterior def

Protect precisely the added exterior sides. · OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget.isExterior

IsFaithfulTracialState def

Naimark's problem asks whether a $C^*$-algebra whose nonzero irreducible representations are all unitarily equivalent must be an algebra of compact operators. The formalization gives a counterexample in ZFC: a unital infinite-dimensional … · OAI.NaimarkZFC.IsFaithfulTracialState

IsFanVertex def

The actual vertices of the seven fan templates. The punctured D fan has only its two non-CD ports. All representatives of its point are retained. · OAI.HyperbolicObstruction.CoreGeometry.IsFanVertex

IsFiniteAlgebra def

Finiteness: every isometry in the algebra is unitary. · OAI.FiniteFactor.IsFiniteAlgebra

IsFiniteBoxUnion def

The bounded finite unions of open coordinate boxes used by the bin conductance argument. Empty unions and empty coordinate boxes are allowed. · OAI.ContingencyTables.PublishedInputs.IsFiniteBoxUnion

IsFiniteCovolumeLattice def

A discrete subgroup with a normalized invariant measure on its coset space. · OAI.PolycyclicRecognition.IsFiniteCovolumeLattice

IsFiniteCovolumeLattice def

A discrete subgroup with finite covolume, expressed by the normalized invariant measure on the coset space. · OAI.PolycyclicRecognition.IsFiniteCovolumeLattice

IsFree def

Freeness: no finite subset of N belongs to the ultrafilter. · OAI.NuclearUltrapower.IsFree

IsFreePotential structure

Free scalar labels: the first field includes the root, but the second field only tests genuine child increments. No root label is set equal to zero. · OAI.BoundedTreePotentials.FreeRoot.IsFreePotential

IsFullGroupAlgebra def

The universal property defining the full, not the reduced, group C*-algebra. The dense generation clause makes the intended completion explicit. This is definition data, not a hypothesis silently supplied to the main claim. · OAI.NuclearUltrapower.IsFullGroupAlgebra

IsFullLift def

Every logical character is extended to the ambient input space. · OAI.MaxCutGames.Gadget.DetectionBridge.IsFullLift

IsFullLift def

Every logical character is extended to the ambient input space. · OAI.UniqueGamesTheorem.Gadget.DetectionBridge.IsFullLift

IsGeneric def

The complete genericity predicate. The universal linear map quantifier occurs inside the property of the selected subspace. · OAI.MaxCutGames.Quadratic.IsGeneric

IsGeneric def

A filter meets the decision and local-witness dense sets for each fixed standard formula and tuple. This property is constructed below; it is not a truth lemma or an assumption that any set-theoretic axiom is forced. · OAI.PartitionConsistency.ForcingQuotient.AtomicData.IsGeneric

IsGeneric def

The complete genericity predicate. The universal linear map quantifier occurs inside the property of the selected subspace. · OAI.UniqueGamesTheorem.Quadratic.IsGeneric

IsGeodesic def

The constant-speed minimizing parametrization, including constant curves. · OAI.WeakHessian.IsGeodesic

IsGeodesicWithInitialData def

Complete affinely parametrized geodesic with prescribed initial tangent. Local metric minimization is an intrinsic definition of Riemannian geodesics. · OAI.WeakMTWTransport.IsGeodesicWithInitialData

IsGHPTest def

Bounded continuous tests on compact metric probability spaces modulo measure-preserving isometry, expressed on presentations. · OAI.FKCRT.IsGHPTest

IsGoodTuple def

Witnesses are universally quantified; no arbitrary choice can turn a bad tuple into a good one. · OAI.TotientAsymptotic.IsGoodTuple

IsGraphWitness def

Symmetric colors separate vertices, satisfy the join triangle inequality, detect order, and connect every pair below the join of any nonempty finite set of seed colors. · OAI.FiniteCongruence.IsGraphWitness

IsGroupExponential structure

The exponential is characterized by its one-parameter subgroups and by their tangent vectors at the identity. · OAI.PolycyclicRecognition.IsGroupExponential

IsGroupExponential structure

The intrinsic exponential, characterized by its one-parameter subgroups and their tangent vectors at the identity. The Lie algebra here is the actual tangent Lie algebra of G, with its invariant-vector-field bracket. · OAI.PolycyclicRecognition.IsGroupExponential

IsHenkin def

A filter meeting every decision and every local quantifier-witness request. · OAI.PartitionConsistency.Completeness.IsHenkin

IsHyperfiniteWOT def

Hyperfiniteness witnessed by an increasing sequence of finite-dimensional star subalgebras with weak-operator dense union. · OAI.TraceConeClassification.IsHyperfiniteWOT

IsII1Factor structure

A nonzero finite diffuse factor, stated by its center, isometries, and projections. These hypotheses do not include any generation conclusion. · OAI.Generator.IsII1Factor

IsII1Factor structure

A nonzero, weakly closed, finite diffuse algebra with scalar center. · OAI.RelativeGeneration.IsII1Factor

IsInfinitePair def

Two embeddings of a common projection into orthogonal subprojections. · OAI.BoundedHochschild.KadisonRingrose.IsInfinitePair

IsInitialExponent def

A nonzero coefficient of least real weight. · OAI.CartierSections.IsInitialExponent

IsInjective def

Injectivity in the given representation, expressed as a contractive linear projection of the ambient bounded operators onto the algebra. Normality of the projection is not required. · OAI.KadisonKastler.IsInjective

IsIntegerSignRow def

An integer sign row with the full Hadamard Gram equation. · OAI.CirculantHadamard.IsIntegerSignRow

IsIntegralPoincareDualityGroup def

Integral Poincaré duality in dimension n, allowing an orientation twist. · OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup

IsIrreducible def

No nontrivial partition has every cross label equal to two. · OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible

IsIrreducible def

Naimark's problem asks whether a $C^*$-algebra whose nonzero irreducible representations are all unitarily equivalent must be an algebra of compact operators. The formalization gives a counterexample in ZFC: a unital infinite-dimensional … · OAI.NaimarkZFC.IsIrreducible

IsIsomorphicToCompacts def

Naimark's problem asks whether a $C^*$-algebra whose nonzero irreducible representations are all unitarily equivalent must be an algebra of compact operators. The formalization gives a counterexample in ZFC: a unital infinite-dimensional … · OAI.NaimarkZFC.IsIsomorphicToCompacts

IsIsotropic structure

Zero mean and identity covariance, with all moment integrability explicit. · OAI.LeanBlast.KLS.IsIsotropic

IsLaplacian def

Weak nonpositive generator convention, without a global L² assumption on F. · OAI.WeakHessian.IsLaplacian

IsLieBracket def

The defining identities of a real Lie bracket, with bilinearity supplied by its continuous-linear-map type. · OAI.PolycyclicRecognition.IsLieBracket

isLimit def

This is the actual strict limit universal property. · OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.isLimit

IsLinearOrthant def

Exact cone equality class in the proof: image of a coordinate orthant by an invertible linear map. Basis vectors serve as generating rays. · OAI.GeneralMahler.IsLinearOrthant

IsLocalizedPatchCover structure

Concrete geometric and smoothness properties needed before assigning positive operators and energy centers to the finite patches. · OAI.RegularPointCoordinates.IsLocalizedPatchCover

IsLocallyNilpotent def

A derivation is locally nilpotent if each element is killed by some iterate. · OAI.StableCoordinate.IsLocallyNilpotent

IsLocalSegment structure

A uniformly locally constant-speed geodesic on the unit interval. · OAI.HyperbolicObstruction.IsLocalSegment

IsLocalWeakUpperGradient def

Local weak upper gradients, in the integrated test-plan definition. · OAI.WeakHessian.IsLocalWeakUpperGradient

IsLogConcaveDensity structure

Probability-density and log-concavity conditions. ConcaveOn includes convexity of the positive support. · OAI.LeanBlast.KLS.IsLogConcaveDensity

IsMarkovLaw def

Same finite stochastic-product definition as the exact CKR obligation. · OAI.BoundedTreewidthL1.MarkovFlow.IsMarkovLaw

IsMartingale def

The one-step arithmetic martingale identity on fair dyadic histories. · OAI.BoundedTreePotentials.Dyadic.IsMartingale

IsMaximizingColumnBasis def

A genuine invertible column basis maximizing the prescribed total weight. · OAI.PolycyclicRecognition.IsMaximizingColumnBasis

IsMeasuredEuclideanApproximation structure

A pointed metric approximation together with the normalized measure comparison, tested against all bounded 1-Lipschitz functions. · OAI.RegularPointCoordinates.IsMeasuredEuclideanApproximation

IsMeasureLaplacian def

The weak measure-valued Laplacian, tested on continuous compactly supported Sobolev representatives. · OAI.RegularPointCoordinates.IsMeasureLaplacian

IsMeasureLaplacianOn def

Local distributional measure Laplacian, using continuous compactly supported Sobolev tests inside the indicated region. · OAI.RegularPointCoordinates.IsMeasureLaplacianOn

IsMinimalProjectionIn def

A nonzero projection with no proper nonzero subprojection in the algebra. The order is the existing order on algebra projections. · OAI.KadisonKastler.IsMinimalProjectionIn

IsMinimizerAt def

A global perimeter minimizer under the prescribed volume constraint. · OAI.CubicTorus.IsMinimizerAt

IsMixedWord def

A bracket word is mixed when at least one of its letters is outside the chosen cone. No property of that cone is needed for the ideal calculation. · OAI.PolycyclicRecognition.IsMixedWord

IsMixing def

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

IsModelShape structure

The geometric conditions of a k-model, in its distinguished coordinates. Membership in the affine local-limit family is separate from these conditions. · OAI.AffineBernstein.IsModelShape

IsModularStateGroup structure

The canonical implementation fixes the vector; together with the strip condition this identifies the represented modular state action. · OAI.KadisonKastler.IsModularStateGroup

IsMonomial def

A permutation matrix times an invertible diagonal matrix, literally P D. · OAI.ExactFourier.IsMonomial

IsMotifValue def

The literal unsigned/signed motif values at one child index. · OAI.TraceReconstruction.IsMotifValue

IsMultilinear def

Every exponent in every supported monomial is at most one. · OAI.LeanBlast.GotsmanLinial.IsMultilinear

IsName def

Well-formed set-forcing names. This is the usual hereditary recursive condition on sets of pairs, not a predicate on their interpreted values. · OAI.PartitionConsistency.SetForcingNames.IsName

IsNearest def

The predicate of being a global nearest parameter for the actual curve. · OAI.ThompsonNonamenability.Analytic.RegularCurveData.IsNearest

IsNegativeEigenfunction def

Weak eigenfunction at the negative energy -k². · OAI.SharpLiebThirring.IsNegativeEigenfunction

IsNormalFilter def

The normal-filter properties required by the set symmetric-system theorem. · OAI.PartitionConsistency.SupportFilter.IsNormalFilter

IsNormalizedHalfPlaneMap structure

The interior normalization fixes the value and the derivative norm at a unit semicircle waypoint. · OAI.SLEExactGauge.IsNormalizedHalfPlaneMap

IsNormalizedTrace structure

A faithful normal normalized trace, not an additional hypothesis on the inclusion. · OAI.RelativeGeneration.IsNormalizedTrace

IsNormalPrime def

Ford's Definition 1, equations (2.1)–(2.2). · OAI.TotientAsymptotic.IsNormalPrime

IsNormalTrace def

Normality is preservation of every existing directed positive supremum. · OAI.TraceConeClassification.ExtendedTrace.IsNormalTrace

IsNuclear def

Nuclearity in the tensor-norm convention of the tensor-norm formulation. The second C*-algebra need not be unital, nonzero, or separable. · OAI.NuclearUltrapower.IsNuclear

iso def

The edge isomorphism forced by an upper stalk isomorphism and exact quotient maps. · OAI.KLInvariance.QuotientEdge.iso

iso def

The adjacent arrow space is precisely the direct sum of its scalar arrow columns. · OAI.LittleFinitistic.ArrowBasisIso.iso

iso def

An actual finite basis gives the scalar-column isomorphism, including the empty basis. · OAI.LittleFinitistic.FiniteBasisIso.iso

iso def

An actual chain isomorphism commuting a zero-preserving functor with extension by zero. · OAI.LittleFinitistic.FunctorExtension.iso

iso def

An actual chain isomorphism, with support supplied by proved zero objects. · OAI.LittleFinitistic.OrdinarySimulation.SupportedExtension.iso

iso def

Group paths by their first traversed arrow; the later arrow is the first tensor factor. · OAI.LittleFinitistic.PathBasisIso.iso

iso def

Convert an identified evaluated-representative cohomology diagram into the full cohomology B-module of the one fixed selecting tensor. Only the reference diagram identification is an input; the tensor vertex comparisons are proved. · OAI.LittleFinitistic.SelectedCohomologyAssembly.iso

iso def

Identify the full tensor cohomology with the actual evaluation module from three coordinate models and their generator actions. · OAI.LittleFinitistic.SelectedReferenceCohomology.iso

iso def

Compatible categorical vertex isomorphisms determine a full B-module isomorphism. The hypotheses are exactly the two finite arrow squares; length-two actions follow. · OAI.LittleFinitistic.VertexCategoricalAssembly.iso

iso def

Homology of the actual vertex complex is the actual vertex of module homology. · OAI.LittleFinitistic.VertexHomology.iso

iso def

Atomic coverage and actual common-source overlaps imply the full strict pushout comparison is an isomorphism. · OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.iso

isoEquiv def

The underlying equivalence of stages of a construction isomorphism. · OAI.PartitionConsistency.MonoidConstruction.isoEquiv

isolated def

The selected edges that meet no other selected edge. · OAI.AsymptoticallyMinimalLittlewood.Nibble.isolated

isometricExtension def

The actual operator equal to T on the range of J and zero on its orthogonal complement. · OAI.KadisonSimilarity.isometricExtension

isometricLinearAction def

The bundled unitary representation of a real linear isometric action. · OAI.PolycyclicRecognition.isometricLinearAction

isometryCornerEquiv def

An isometry identifies the whole algebra with its range corner. · OAI.BoundedHochschild.KadisonRingrose.isometryCornerEquiv

isometryRangeCoordinates def

The adjoint of the second embedding gives coordinates for the first. · OAI.KadisonKastler.isometryRangeCoordinates

Isomorphism structure

Exact simultaneous equivalence of graph incidence, orientation, side, length, every path traversal, root path, and comparison intervals. · OAI.TorsionFreeZeroDivisors.PatternCoding.Isomorphism

isOne def

A total exact predicate compiler. All intermediate words are widened from an explicit expression-derived bound, including on rejected inputs. · OAI.ExactQuantumFactoring.NatExpr.isOne

IsOneStableCoordinate def

No requirement to preserve the original four-variable subring is imposed. · OAI.StableCoordinate.IsOneStableCoordinate

isoOfBijective def

A cellwise bijective strict functor has a strict inverse. · OAI.Thomason.Construction.StrictOmegaCategory.isoOfBijective

IsOperatorForm def

Algebraic identities for a matrix coefficient function, conjugate-linear in the operator's argument and linear in the test vector. · OAI.KadisonSimilarity.IsOperatorForm

IsOptimal structure

Maximize the total amount below k+1-|Q|, then minimize the number of assigned paths. Both optimization orders are on natural numbers. · OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal

IsOptimal def

Optimality among nonnegative matrices with the same two marginals. · OAI.Problem358.FiniteCoupling.IsOptimal

IsOptimalMap def

Optimality for the Monge minimization problem. · OAI.WeakMTWTransport.IsOptimalMap

isoRestrictEquiv def

Restriction along a scheme isomorphism is an equivalence of its module sheaf categories. · OAI.ActualOpenModules.isoRestrictEquiv

IsOriented structure

`IsOriented r` packages the two relation-level conditions needed throughout the development: no vertex points to itself, and an arc `u → v` rules out the opposite arc `v → u`. The Lean model uses a relation rather than a graph structure, … · OAI.SeymourSecondNeighborhood.IsOriented

isotropicExponent def

The exponent 2Dc-(3c²-c)/2, written without truncated half-integers. · OAI.SidorenkoCounterexample.isotropicExponent

isotypic def

The standard central character formula for the isotypic projection. Its projection properties require the signed action laws (not assumed here). · OAI.CoordinateSweeps.SignedTensor.isotypic

isoVertexStarHomeomorph def

The star correspondence uses the actual geometric-realization homeomorphism. · OAI.Thomason.Construction.RealizationPrism.isoVertexStarHomeomorph

IsP def

The four entries of the body pattern, in row-major order. · OAI.Problem348.ModeLocalization.IsP

IsParabolic def

Conjugates of standard subgroups, with no spherical-type restriction. · OAI.HarmonicArtin.ParabolicIntersections.IsParabolic

IsParallelFrameCurveOn def

A curve on an open time set is continuous and satisfies the genuine velocity and Levi-Civita parallel equations there. · OAI.PositiveEinsteinFour.Geometry.IsParallelFrameCurveOn

IsPiece def

Coordinates of a proposed prefix or interval coincide with the fixed g. · OAI.SeparableQuotient.ActualSpace.IsPiece

IsPlanar def

A topological drawing by simple plane arcs, with injective vertex placement, no vertex in an edge interior, and disjoint interiors for distinct unoriented edges. · OAI.PlanarL1.IsPlanar

IsPlanar def

A topological drawing of a simple graph in the real plane. Each edge is a simple arc, with no vertex in its interior; interiors of distinct unoriented edges are disjoint. Either orientation is available for each edge. · OAI.PlanarL1.IsPlanar

IsPlanarRegularValue def

The actual differential is nonzero at every point of the level. · OAI.CircleDomainRigidity.IsPlanarRegularValue

IsPolycyclic def

Polycyclicity expressed by an actual cyclic subnormal series. · OAI.PolycyclicRecognition.IsPolycyclic

IsPolycyclic def

A polycyclic group has a finite subnormal series from the trivial subgroup to the whole group with cyclic factors. · OAI.PolycyclicRecognition.IsPolycyclic

IsPotential def

A nonnegative potential has Euclidean child values bounded by its parent. · OAI.BoundedTreePotentials.Segments.IsPotential

IsPrimeAlgebra def

The ring-theoretic primeness condition used by the orientation proof. · OAI.KadisonKastler.IsPrimeAlgebra

IsProb def

A finite real-valued probability vector. · OAI.CliqueFreeIndependence.FiniteEntropy.IsProb

IsProbabilityWeights def

Nonnegative finite weights with total mass one. · OAI.ThompsonNonamenability.IsProbabilityWeights

IsProductZariskiClosed def

The common zero loci of multihomogeneous equations: the algebraic Zariski closed subsets of a product of projective planes. · OAI.Nagata.ProjectiveGeometry.IsProductZariskiClosed

IsProjection def

The left answer determines at most one accepting right answer. Partial projection predicates are included, as are total projection maps. · OAI.MaxCutGames.Repetition.IsProjection

IsProjection def

The left answer determines at most one accepting right answer. Partial projection predicates are included, as are total projection maps. · OAI.UniqueGamesTheorem.Repetition.IsProjection

IsQuadraticOptimalMap def

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

IsRamseyNumber def

Specifying the least forcing order avoids an existence convention for sInf. · OAI.CycleClique.Construction.IsRamseyNumber

IsRamseyNumber def

The exact least order forcing a cycle or a complementary clique. · OAI.CycleClique.IsRamseyNumber

IsReader def

A row reader's finite output law, used only in the correctness proof. · OAI.LowSpaceSubsetSum.RowMerge.IsReader

IsRealigned def

The realignment symmetry relevant to a Kraus decomposition. · OAI.MUB6.Weiner.IsRealigned

IsRealSigning def

Real signs in every consecutive degree 0,...,N-1. · OAI.AsymptoticallyMinimalLittlewood.IsRealSigning

IsRealSigning def

Every coefficient is a real sign. · OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.IsRealSigning

IsRealTriangulable def

The actual closed triangular matrix realization from CT Definition 1.1. · OAI.PolycyclicRecognition.IsRealTriangulable

IsRectifiableFiber def

Algebraic rectifiability of the closed hypersurface embedding. · OAI.StableCoordinate.IsRectifiableFiber

IsReduced def

Source immersion is exactly nonbacktracking of consecutive ports. · OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.Walk.IsReduced

IsReflexive def

Reflexive means the canonical embedding onto the continuous bidual is surjective, not merely that the space is isomorphic to some Hilbert space. · OAI.BoundedTreePotentials.IsReflexive

IsRegularOperator def

Exact coordinate specification of the bounded left-regular operator of A. · OAI.GroupRingDeterminant.IsRegularOperator

IsRestriction def

T is obtained from S by three linear maps on its coordinate spaces. · OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction

IsRoot def

A genuine real root, obtained from a simple root by the Tits action. · OAI.KLInvariance.TitsSpace.IsRoot

IsRound def

The round metric is the pullback of the Euclidean scalar product under inclusion of the unit sphere. This predicate specifies exactly that tensor. · OAI.YauCounterexamples.IsRound

IsSchemeRectifiableFiber def

Geometric rectifiability of the embedded image by an arbitrary ambient scheme automorphism over the complex base scheme. · OAI.StableCoordinate.GeometricInterpretation.IsSchemeRectifiableFiber

IsSegment def

A finite, order-convex chain. The empty chain is a harmless zero test. · OAI.ForestSpace.IsSegment

IsSegment def

A constant-speed metric segment, parametrized on [0,1]. · OAI.HyperbolicObstruction.IsSegment

IsSelected def

A small index is selected precisely when its actual ground name code is persistently least in its eventual-equality class. · OAI.PartitionConsistency.ProductForcing.ChainCode.IsSelected

IsSemifiniteTrace def

The usual semifiniteness condition, including boundary value infinity. · OAI.TraceConeClassification.ExtendedTrace.IsSemifiniteTrace

IsSimpleCStar def

Naimark's problem asks whether a $C^*$-algebra whose nonzero irreducible representations are all unitarily equivalent must be an algebra of compact operators. The formalization gives a counterexample in ZFC: a unital infinite-dimensional … · OAI.NaimarkZFC.IsSimpleCStar

IsSimplex def

Exact affine simplex family. · OAI.GeneralMahler.IsSimplex

IsSmoothNeighborhood def

The finite compact-chart derivative tests defining a C∞ neighborhood. A single positive tolerance suffices for the finitely many tests. · OAI.YauCounterexamples.IsSmoothNeighborhood

IsSmoothSphereAt def

Real smoothness in the same source and target charts as metric conformality. · OAI.CircleDomainRigidity.IsSmoothSphereAt

IsSobolevHarmonicOn def

Local harmonicity is tested against the existing zero-boundary Sobolev space, using the canonical Dirichlet energy. · OAI.RegularPointCoordinates.IsSobolevHarmonicOn

IsSourcePairClass def

A pair is entirely in the source precisely when its cycle contains no test slot. · OAI.KadisonSimilarity.IsSourcePairClass

IsState def

Naimark's problem asks whether a $C^*$-algebra whose nonzero irreducible representations are all unitarily equivalent must be an algebra of compact operators. The formalization gives a counterexample in ZFC: a unital infinite-dimensional … · OAI.NaimarkZFC.IsState

IsSubarcLawReduction def

The actual measurable selection and domination data retained by compact terminal subarc conditioning. · OAI.CircleDomainRigidity.IsSubarcLawReduction

IsSubspaceAntecedent def

Antecedents on arbitrary subspaces. Projection onto the chosen complement is the quotient compression expressed through quotientEquivOfIsCompl. · OAI.MaxCutGames.Appendix.DerivativeInduction.IsSubspaceAntecedent

IsSubspaceAntecedent def

Antecedents on arbitrary subspaces. Projection onto the chosen complement is the quotient compression expressed through quotientEquivOfIsCompl. · OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.IsSubspaceAntecedent

IsSupported def

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

IsSupportedSplitModel structure

Supports and the original orthant after a support-coordinate split. · OAI.AffineBernstein.IsSupportedSplitModel

IsSymmetric def

Symmetry as an actual property of a multilinear map. · OAI.MetricEntropyDuality.SymmetricForm.IsSymmetric

IsTangent def

The full tangent in the two ambient factors. · OAI.ArnoldCounterexample.ThreePoints.IsTangent

IsTestFunction def

The exact compactly supported smooth real test-function class. · OAI.LeanBlast.KLS.IsTestFunction

IsTestFunction def

Bounded globally Lipschitz Laplacian-domain functions with Sobolev Laplacian. · OAI.WeakHessian.IsTestFunction

IsTestPairClass def

A pair is entirely in the test precisely when its cycle contains no source slot. · OAI.KadisonSimilarity.IsTestPairClass

IsTestPlan def

A 2-test plan: bounded compression and finite average kinetic energy. · OAI.WeakHessian.IsTestPlan

IsThinElementary def

The actual elementary subclass with a prescribed upper transverse width. · OAI.BoltzmannNonuniqueness.SheetKernelLimits.IsThinElementary

IsTopDegree def

d is the largest weight of a nonzero polynomial, including negative weights. · OAI.StableCoordinate.WeightedInitial.IsTopDegree

IsTouchingMatching def

A finite matching whose edges are pairwise touching: each member is a two-vertex clique, and distinct members are disjoint and joined by an edge. · OAI.HadwigerMatching.IsTouchingMatching

IsTrace def

A simple center trace, with no premature boundary exit. · OAI.CriticalHoneycomb.IsTrace

IsTraceQuotient def

The precise quotient-kernel condition needed for discarded sequences. · OAI.KadisonKastler.IsTraceQuotient

IsTransitive def

Usual external transitivity of an actual collection of pure sets. · OAI.PartitionConsistency.TransitiveSets.IsTransitive

IsTranslationInstance def

After identifying labels with a binary vector space, `IsTranslationInstance coordinates g` requires each listed permutation to act as `x ↦ x+shift` for some shift depending on that constraint. · OAI.UniqueGamesTheorem.Integration.TranslationTarget.IsTranslationInstance

IsTruncated def

Strict n-categories are the full subcategory with a uniform dimension bound; no invertibility condition is imposed. · OAI.Thomason.Construction.StrictOmegaCategory.IsTruncated

IsTwo def

The extension is a 1-quasitrace, not a normalized 1-quasitrace. · OAI.Kaplansky.OneQuasitrace.IsTwo

IsTypeIFactor structure

A type I factor, expressed only in terms of its scalar center and the existence of a minimal projection. · OAI.KadisonKastler.IsTypeIFactor

IsUniformLattice def

A uniform lattice is discrete and has a compact fundamental cover. · OAI.PolycyclicRecognition.IsUniformLattice

IsUniformLattice def

A uniform lattice, expressed by discreteness and a compact fundamental cover. Over a locally compact group this is equivalent to compactness of the coset quotient. · OAI.PolycyclicRecognition.IsUniformLattice

IsUniqueQuadraticOptimalMap def

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

IsUnitary def

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

IsUnitTest def

Closed unit tests for the exact incomparable-segment norm. · OAI.BoundedTreePotentials.Segments.IsUnitTest

IsVirtuallyNilpotent abbrev

Virtual nilpotency means the existence of a nilpotent subgroup of finite index. · OAI.PolycyclicRecognition.IsVirtuallyNilpotent

IsVirtuallyPolycyclic def

Virtual polycyclicity means a polycyclic subgroup of finite index. · OAI.PolycyclicRecognition.IsVirtuallyPolycyclic

IsVirtuallyPolycyclic def

A virtually polycyclic group contains a polycyclic subgroup of finite index. · OAI.PolycyclicRecognition.IsVirtuallyPolycyclic

IsVisualSplit def

The presentation-graph condition in CMMW Definition 2.4. The vertex subgraphs are proper, cover every vertex, and omit no finite-label edge. · OAI.HarmonicArtin.ParabolicIntersections.IsVisualSplit

IsWeakHomotopyEquivalence def

The actual weak homotopy equivalences, using path components and all positive-dimensional homotopy groups of the source at all basepoints. · OAI.Thomason.Construction.IsWeakHomotopyEquivalence

IsWeakSubsolutionOn def

The distributional inequality Δu ≥ -a u, expressed using only the actual Sobolev energy form and L² pairing. · OAI.RegularPointCoordinates.IsWeakSubsolutionOn

IsWild def

The source's wild-law condition; probability is provided as a measure instance. · OAI.PlaneFiveColor.Spectral.IsWild

IsZeroFiber def

The zero fiber is independent of the representative. · OAI.Nagata.W16.AssociatedBundle.IsZeroFiber

IsZFAxiom inductive

Exactly the axioms and all schema instances of pure first-order ZF. · OAI.PartitionConsistency.SetLanguage.IsZFAxiom

itemGrade def

Full raw sectors have three structural letters alpha,Q,omega. · OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.itemGrade

iter def

Successively totalize the given module-to-chain functors. · OAI.DerivedBar.RecursiveTotal.iter

iterate def

Input-length-bounded iteration. The extra hypothesis is solely a size invariant along the already implemented iteration, not a computability oracle. · OAI.ExactQuantumFactoring.BitStackProgram.Procedure.iterate

iterate def

Iterating the very same edge replacement, starting from an arbitrary network. This recursion groups the first replacement before the remaining ones. · OAI.ForestSpace.Diamond.Network.iterate

iterate def

The finite stage at any natural height, using the same alphabet and block family at every level. Surjectivity and equivariance have been proved by the constructor, and hence are available at every height without extra hypotheses. · OAI.MaxCutGames.Gadget.Stage.iterate

iterate def

Bounded iteration is compiled to a real finite loop. The semantic size invariant is a proof obligation, not a loop oracle or added main hypothesis. · OAI.RationalHitting.StackLanguage.Procedure.iterate

iterate def

Actual nonautonomous coordinate composition. · OAI.SmoothObstruction.ShortDerivative.iterate

iterate def

The finite stage at any natural height, using the same alphabet and block family at every level. Surjectivity and equivariance have been proved by the constructor, and hence are available at every height without extra hypotheses. · OAI.UniqueGamesTheorem.Gadget.Stage.iterate

iterated def

Repeated images of the ideal action. · OAI.CartierImageFiltration.iterated

iteratedCarrierHomotopy def

The comparison with exact last vertex can be made wholly inside the original barycentric carrier at each point. · OAI.Thomason.Construction.SubdivisionBarycentric.iteratedCarrierHomotopy

iteratedCorrelation def

Successive multiplicative differences, in their order of application. · OAI.Problem337.iteratedCorrelation

iteratedInclusion def

The canonical inclusion of the iterated ideal image in the original object. · OAI.CartierImageFiltration.iteratedInclusion

iteratedMap def

The induced order map on every iterated chain stage. · OAI.Thomason.Construction.RelativeLabelCarrier.iteratedMap

iteratedSubdivision def

The iterates used in finite simplicial approximation, with zero iterate included so that exact factorization can be proved by induction. · OAI.Thomason.Construction.iteratedSubdivision

iteratedWeylDerivative def

Only three derivatives are used below, but retaining the natural number index makes the local covariance proof a single rank induction. · OAI.PositiveEinsteinFour.Geometry.iteratedWeylDerivative

iterateHom def

The iterated polynomial substitution in an additive coaction. · OAI.StableCoordinate.FrameLift.iterateHom

iterateLaw def

The pushforward of the initial probability by the jth iterate. · OAI.SmoothObstruction.CompactInvariant.iterateLaw

iterateMap def

Applying the lifted family twice, with two independent parameters. · OAI.StableCoordinate.FrameLiftCoassoc.iterateMap

iteration def

Fully specified finite-table reduction; divergence is retained for arbitrary (possibly nonterminating) tables. · OAI.FiniteAlgebraicEnvelopes.Bootstrap.iteration

iteration def

The actual full B-linear binomial formula for the genuine tensor functor. · OAI.LittleFinitistic.SelectedDerivedFunctor.iteration

iteration def

The exact binomial formula, instantiated with the actual finite module family. · OAI.LittleFinitistic.SelectedIteration.iteration

iterationChartRatio def

The chart ratio and pair radius are fixed before the final smallness parameter is chosen. · OAI.RegularPointCoordinates.iterationChartRatio

iterationInTime def

Timed execution of the concrete guard/body/halt program. This compositional interface is not a certificate for an unprovided graph-transformation body. · OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.iterationInTime

iterationInTime def

Timed execution of the concrete guard/body/halt program. This compositional interface is not a certificate for an unprovided graph-transformation body. · OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.iterationInTime

IterationPairGeometry def

Raw geometric information about the original coordinates and frozen metrics. No derivative, increment, or Taylor estimate occurs here. · OAI.RegularPointCoordinates.IterationPairGeometry

iterationRadius def

Dyadic radii, written without integer exponents. · OAI.RegularPointCoordinates.iterationRadius

iterDataPoint def

The actual geometric realization of every recursively constructed vertex. · OAI.Tingley.iterDataPoint

iterPoint abbrev

The coordinate form used by the simplex fixed-point argument. · OAI.Tingley.iterPoint

ivb def

profiles v' correction and v'' · OAI.GeneralMahler.SCal.Tail.ivb