Glossary: F

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

F def: Positive-indexed finite closures. · OAI.SeparableQuotient.CoherentClosures.F
F def: Defined by this formula on [0, L); no finite endpoint value at L is asserted. · OAI.SoftChannel204.F
f def: A polynomial with three constrained critical points. · OAI.ArnoldCounterexample.ThreePoints.f
f def: The even solution of (1-t²)f''-6tf'+6f=0 with f(0)=1. · OAI.Bernoulli.DeSilvaJerison.f
f def: The positive test vector in the manuscript's matrix argument. · OAI.TorsionFreeZeroDivisors.WordEstimate.f
F1₀ abbrev: Source at least one: the actual D1 and D2 vertex terms and D1 arrow terms. · OAI.ExternalTensor.Section4.SourceFiltration.F1₀
F2 abbrev: `F2` abbreviates `ZMod 2`, the field whose two elements encode binary addition and translation. · OAI.UniqueGamesTheorem.Integration.BinaryLinear.F2
face def: Closed coordinate face of the standard simplex. · OAI.EilenbergGanea.AffineTransport.face
face def: Each macro face walks through consecutive radial triangles around one actual apex. Frozen face cycles are unchanged. · OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.face
face def: Every positive-dimensional basis element has two canonical boundary bases. · OAI.Thomason.Construction.PastingGlobeBasis.face
face def: The coordinate face of a finite simplicial cube. · OAI.Thomason.Construction.RealizedCube.face
face def: A face vertex is sent to the uniform barycenter of its original vertices. · OAI.Thomason.Construction.SubdivisionBarycentric.face
FaceAnchor abbrev: Anchor is finite data; no choice of deck coordinate is lost. · OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.FaceAnchor
faceBase def: Canonical tangential parametrization of an affine hyperplane. · OAI.Problem358.TangentNormalCoordinates.faceBase
faceCell def: Finite collection containing every closed face of a fixed cube. · OAI.EilenbergGanea.CubeRealization.faceCell
faceChain def: The total lifted cellular chain (or any additive face statistic). A face is counted once, independent of its number of independently indexed sides. · OAI.HyperbolicObstruction.PictureSwitch.faceChain
faceChart def: Unit-normal displacement from the canonical hyperplane parametrization. · OAI.Problem358.TangentNormalCoordinates.faceChart
faceChart def: A continuous chart on each closed face. · OAI.Thomason.Construction.HornBarycentric.faceChart
FaceClosed def: A literal closed target walk on each source face: the next side starts where this side ends. This imposes no injectivity or normal form. · OAI.HyperbolicObstruction.PictureSwitch.PictureMap.FaceClosed
faceCoefficient def: A transverse face coefficient; the fixed-plane measure and transverse normal factor together are the disintegration coefficient in cell derivatives. · OAI.Problem358.AffinePlaneGraph.faceCoefficient
faceCorners def: The actual corners of a selected dual vertex (primal face). · OAI.HyperbolicObstruction.PictureSwitch.PictureMap.faceCorners
faceEval def: Cyclic evaluation of one oriented face. · OAI.Release075.BlockPresentation.faceEval
faceGenerator def: A face generator is defined with its canonical dimension witness. · OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.faceGenerator
faceHomeomorph def: The restriction identifies the actual subdivided face realization with its full coordinate face, not merely their interiors. · OAI.Thomason.Construction.SubdivisionBarycentric.faceHomeomorph
FaceIndex abbrev: Only finitely many parameter simplices of dimension at most n are needed. · OAI.Thomason.Construction.RealizationPrism.FaceIndex
faceIndex abbrev: An actual codimension-one simplex of the horn. · OAI.Thomason.Construction.HornBarycentric.faceIndex
faceIndex abbrev: Its codimension-one face at a cut between vertices. · OAI.Thomason.Construction.PrismBarycentric.faceIndex
FaceKind def: The indexed target occurrence stays constant around each source face. Distinct occurrence indices remain distinct even if their labels agree. · OAI.HyperbolicObstruction.PictureSwitch.PictureMap.FaceKind
faceMap def: The original simplex includes as the face omitting the new final vertex. · OAI.Thomason.Construction.ConePrism.faceMap
faceMap def: The chosen m-face of the universal n-cell. For m ≥ n this is its identity extension, so the same definition covers every pair of indices. · OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap
faceMoment def: The vector face coefficient used by both mass site-motion and stationary first-moment differentiation. The diagonal is zero by the normal-length factor. · OAI.Problem358.CellGeometry.faceMoment
faceOrbitEquiv def: New triangular faces are indexed by the old free sides, not merely by an unlabelled area count. All other face orbits are literally unchanged. · OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.faceOrbitEquiv
facePath def: A path in a single face of the cube boundary. · OAI.HyperbolicObstruction.HigherCovering.facePath
faceRaw def: Each coned face is the actual three-cycle old--center--radial. · OAI.TorsionFreeZeroDivisors.ConedMap.faceRaw
faceSimplex def: A simplex of the subcomplex obtained by applying an ambient face operator. · OAI.Thomason.Construction.RealizationPrism.faceSimplex
facesOf def: Faces of dimension i have exactly i + 1 vertices. · OAI.CoboundaryExpanders.Complex.facesOf
facesOf def: Faces of dimension i, i.e. with exactly i+1 vertices. · OAI.CoboundaryExpanders.Complex.facesOf
faceSpace def: The exact active degree and odd-cut kernel, on the positive edge support. · OAI.MatchingEntropy.LooplessGraph.faceSpace
facetEnumeration def: Historical facet labels survive grouping: several cycles may belong to one surface, and a side on that surface can occur any number of times. · OAI.IntegralCharacterVarieties.FiniteCycles.facetEnumeration
facetHit def: A facet is selected when its affine image contains zero. · OAI.SharpLiebThirring.PLParity.facetHit
faceTube def: An open rectangular neighbourhood of the positive i-face of a bin. · OAI.ContingencyTables.GridBoundary.faceTube
faceUnionHomeomorph def: Restriction to an arbitrary finite union of coordinate faces. · OAI.Thomason.Construction.SubdivisionBarycentric.faceUnionHomeomorph
faceValue def: The local chart on a chosen zero coordinate, with values in the actual realization. · OAI.Thomason.Construction.HornBarycentric.faceValue
faceVariation def: The signed face integral in a full affine-cell variation. · OAI.Problem358.PositiveCellFullDerivative.faceVariation
Factor abbrev: A finite product of signed conjugates is a certificate for normal closure. · OAI.FiniteAlgebraicEnvelopes.WordProblem.Factor
factor def: The local tensor along the actual ordered center path, with two selected wires and all other wires vacant. · OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.factor
factor def: The unique right factor when it exists, and 1 otherwise. · OAI.PartitionConsistency.DiagramOrder.ConservativeHull.factor
factor def: The unique right factor between two nodes of the path. · OAI.PartitionConsistency.ProbeAlgebra.Path.factor
factor def: This element measures the failure of the chosen section to multiply. · OAI.PolycyclicRecognition.GroupExtensionSection.factor
factor def: The auxiliary denominator factor changes only from C to 1. · OAI.Problem337.ResidueLevels.factor
factorAlgebra def: The bounded factor algebra, before taking its tracial L² closure. · OAI.KadisonSimilarity.TracialCornerGeometry.factorAlgebra
factorConditionalKernel def: The actual conditional probability kernel supplied by disintegration. · OAI.PolycyclicRecognition.factorConditionalKernel
FactorCorrect def: An actual nonempty feasible facility set, encoded by its membership mask. · OAI.MetricKMedian.FactorCorrect
factorCut def: Coordinatewise zero cutoff, retaining iid f and independence from b. · OAI.DilutedSpinGlass.factorCut
factoredPlaneFamily def: The actual polynomial in the original affine plane at fixed parameter s, with its finite G-adic coefficient decomposition made explicit. · OAI.Nagata.Workers.W28.factoredPlaneFamily
factorFrequency def: Compose the two factors and retain the proved rank. · OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.factorFrequency
factorGraphMeasure def: The graph measure, with the factor in the first coordinate. · OAI.PolycyclicRecognition.factorGraphMeasure
factorialBody def: One rising-product step: multiply accumulator by the copied current index, advance the binary index, and drop one symbol of the unary loop counter. · OAI.RationalHitting.StackLanguage.factorialBody
factorialCombination def: The unblocked finite factorial expression. · OAI.Problem337.ChebyshevLowerSharp.factorialCombination
factorialCore def: Factorial with clean local registers: only the unary counter and output register are changed. This is the binary subroutine for the Taylor binomials. · OAI.RationalHitting.StackLanguage.factorialCore
FactorialExpansion structure: A finite expansion with natural (hence nonnegative) coefficients, bounded total order, supported on a specified coordinate set. · OAI.Problem335.FactorialExpansion
factorialExpansionValue def: A finite expansion in the multivariate falling-factorial basis. · OAI.Problem335.factorialExpansionValue
factorialLift def: The factorial lift for capacities 3 and 2, with constant weight one. It is defined on all sets here and subsequently restricted to 5-subsets. · OAI.DistinctLifts.factorialLift
factorialMonomial def: Evaluation of a falling-factorial monomial at a natural occupation vector. · OAI.Problem335.factorialMonomial
factorialWeight def: Positive factorial monomial weights of the real Fischer form. · OAI.HarmonicCounterexample.Angular.factorialWeight
factorialWeight def: The bilinear Fischer form, over the actual complex polynomial algebra. · OAI.HarmonicCounterexample.ComplexAngular.factorialWeight
factorization def: The final factorization at B is relative to the already constructed A. No diagram model structure or gluing theorem is assumed. · OAI.Thomason.Construction.SimplicialSpan.factorization
factorizationFiberEquivFullKernel def: Once the surjective factor is fixed, the injective factor is unique. · OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.factorizationFiberEquivFullKernel
factorizationSpace def: The closed cyclic span of the range of the right factor. · OAI.KadisonSimilarity.factorizationSpace
factorMatrixUnits def: Fixed choices of the (j+1)-dimensional coordinate matrix algebras. · OAI.KadisonKastler.factorMatrixUnits
factorPoint def: A point at which the factors used by the rigidity argument are nonzero. · OAI.StableCoordinate.DeterminantRing.factorPoint
factorPrefix def: Factor first at C and then at the matching object over C. · OAI.Thomason.Construction.SimplicialSpan.factorPrefix
factorQuotientAction def: Translations and quotient automorphisms form the affine action of the actual semidirect product. · OAI.PolycyclicRecognition.factorQuotientAction
FactorRecord abbrev: The source's distinct positive-exponent factor records. Finsupp stores each prime once; its canonical serialization sorts its support in increasing order. · OAI.ExactQuantumFactoring.FactorRecord
factors def: Literal stored record projection, used only after complete-data validation. · OAI.ExactQuantumFactoring.FactorData.factors
factorStage def: Factoring through a stage preserves topology and equivariance, rather than only factoring an underlying set map. · OAI.GroupRingTopology.Milnor.factorStage
FactorsTraciallyGenerate def: Ordinary tracial generation by the two factors. This is geometric density of algebra vectors, independent of any operator intertwining statement. · OAI.KadisonSimilarity.TracialCornerGeometry.FactorsTraciallyGenerate
factorThroughFace def: A tuple whose entries lie in an ordinal face factors monotonically through it. · OAI.Thomason.Construction.SimplexComplex.factorThroughFace
factorThroughSurjection def: A map with the same kernel as a surjection descends to its target. · OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.factorThroughSurjection
FactorTraceUnitary structure: Same unitaries, with trace topology rather than the operator-norm topology. · OAI.Generator.FactorTraceUnitary
factorTranslate def: Semidirect left translation, written on the product of the factors. · OAI.PolycyclicRecognition.factorTranslate
factorTranslationEquiv def: Measurable automorphisms give measurable product-coordinate translations. · OAI.PolycyclicRecognition.factorTranslationEquiv
factorTwistGraph def: The graph embedding retains both coordinates of the original group. · OAI.PolycyclicRecognition.factorTwistGraph
failingWitnessFinset def: The finite witness space used to bound discarded tuples. · OAI.TotientAsymptotic.failingWitnessFinset
failureIndicator def: The actual output-change indicator before taking a finite average. · OAI.MaxCutGames.Gadget.ActualGadget.failureIndicator
failureIndicator def: The actual output-change indicator before taking a finite average. · OAI.UniqueGamesTheorem.Gadget.ActualGadget.failureIndicator
fairBalancingBad def: A support fails balancing when one bit occurs fewer than a quarter of its distinct labels. · OAI.QuantitativeVanDerWaerden.fairBalancingBad
fairBinomial def: Fair-binomial mass, extended by zero beyond its natural support. · OAI.TraceReconstruction.fairBinomial
fairFamilyMass def: Uniform measure on the Boolean cube with ground set s. · OAI.PlanarFPP.fairFamilyMass
fairField def: The unconditional orientation distribution on any actual finite trial ID set. · OAI.TraceReconstruction.fairField
fairLaw def: The actual fair law for selector table entries. · OAI.Problem310.ConcreteLabels.fairLaw
fairOrientations def: Bit orientations, prior to generating any emissions. · OAI.TraceReconstruction.PairedMechanisms.fairOrientations
fairRetentionBitMass def: One conditional retention bit. · OAI.JointDickman.fairRetentionBitMass
fairRetentionMass def: Conditional probability of a particular retained subset of a site. · OAI.JointDickman.fairRetentionMass
fairSelectedRemainingMass def: A site is sampled at density 1/p and split by fair coins; A and R are its selected and remaining prime sets. · OAI.JointDickman.fairSelectedRemainingMass
fairSetSwap def: Add an independent fair coin which chooses whether to transpose a and b. · OAI.CubeShuffle.fairSetSwap
fairSplitAverage def: Conditional expectation of a test of the retained subset. · OAI.JointDickman.fairSplitAverage
fairSplitPrimeCell def: The conditional probability p_A(S) that a fair split of the site has its retained prime product in the specified cell. · OAI.JointDickman.fairSplitPrimeCell
fairSplitTransition def: Actual transition probability to an output cell of the retained subset. · OAI.JointDickman.fairSplitTransition
faithfulCharacterZeroEquiv def: No dummy zeros, repetitions, or omitted multiplicity labels occur. · OAI.Ostmann.faithfulCharacterZeroEquiv
faithfulRightAction def: Faithfulness of the dense tracial algebra vectors makes right multiplication faithful, as required by the full-column theorem. · OAI.KadisonSimilarity.TracialCornerGeometry.faithfulRightAction
FaithfulStarDerivationsInner def: The bounded form of property (DP): innerness is tested in every faithful unital star representation, independently of a bounded homomorphism under test. · OAI.KadisonSimilarity.FaithfulStarDerivationsInner
FaithfulTracialState structure: The state data needed for faithful reduced free products. · OAI.KadisonKastler.FaithfulTracialState
faithfulVectorTrace def: A faithful unit vector which is tracial on an algebra gives its faithful trace. · OAI.KadisonKastler.faithfulVectorTrace
fallback def: The source's least allowed serving label, including zero marginal rows. · OAI.UniformKServer.FiniteTable.fallback
fallCount def: Number of transitions from true to false. · OAI.Problem335.WordRuns.fallCount
fallingMoment def: Source light-line factorial moment, with its exact finite-population shift. · OAI.CoordinateSweeps.MomentExpansion.fallingMoment
falseCircuit def: The constant false circuit, used for rejected rows of a truth table. · OAI.TwoPointCorrelations.AC0Circuit.falseCircuit
FalseFiber abbrev: The common fiber left after separating a Boolean character's sign. · OAI.MaxCutGames.Foundations.PCP.CayleySampling.FalseFiber
FalseFiber abbrev: The common fiber left after separating a Boolean character's sign. · OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.FalseFiber
falseNeighbors def: Internal neighboring positions of the same normal (false) type. · OAI.Problem335.IsolatedWeight.falseNeighbors
falseRelation def: The empty binary relation, with its regular interpretation. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.falseRelation
fame def: which query was invoked from this instruction · OAI.ExactDerandomization.Relay.Grid.fame
Family structure: The represented disjoint families in the definition of the primal segment norm. · OAI.DiamondDistortion.SegmentSystem.Family
Family structure: The actual finite machine used uniformly in the source bootstrap. Every field is constructed below from partial recursiveness of the universal word evaluator; none is an assumption on an input group. · OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.Family
Family abbrev: Bounded continuous candidate jets through order k. · OAI.ForcedComputation.BoundedSpatialJets.Family
Family structure: The source primitives are affine in the rank inputs when the held parameters and the state are fixed. Both simplex and side domains are compact. · OAI.KServer.AdaptiveMinimization.Family
Family structure: Each label p is a surjection onto the blocks of one partition. · OAI.MUB6.EqualityPatterns.Family
Family def: A raw callback with uniform stable instances in every subsequent context. This is an internal syntax interface, not a hypothesis on the PTS. · OAI.PureTypeSystem.LogicSetup.Family
Family structure: The chosen family stores the actual conditioning event and its mass, not merely the existence of enough labels. · OAI.SmoothObstruction.WordHierarchy.Family
family def: The literal tested class from the self-reference construction: zero precisely for the compiler zero output, and otherwise the compiler word together with a canonical, decidable coding of the actual auxiliary partial affine map. · OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.family
family def: A finite collection of open templates, before interface sewing. Internal seams never acquire identifications between different copies. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family
family def: Canonical sites with base coordinates zero, carrying the original raw waves at their actual translated sheared lattice centers. · OAI.LipschitzHilbert.SourceLatticePacket.family
family def: A bottom-up vector of rotation rows. The recursive result is passed once to step, whose row formula reads only that already materialized table. · OAI.MaxCutGames.Foundations.PCP.ExpanderTables.family
family def: A bottom-up vector of rotation rows. The recursive result is passed once to step, whose row formula reads only that already materialized table. · OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.family
familyCenter def: An arbitrary offset for every prime coordinate includes all product residue environments. The integer environment has every offset equal to zero. · OAI.TwoPointCorrelations.familyCenter
familyClass def: Assemble an integral family before any tensoring with the rationals. · OAI.CoarseAssembly.Analytic.familyClass
familyCleanInTime def: Complete clean-frame execution, from the caller's actual unary request. No callback, table-construction premise, or caller-supplied runtime is assumed. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.familyCleanInTime
familyCleanInTime def: Complete clean-frame execution, from the caller's actual unary request. No callback, table-construction premise, or caller-supplied runtime is assumed. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.familyCleanInTime
familyCloudTable def: Select the family level by the bounded multiplication search. · OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.familyCloudTable
familyCloudTable def: Select the family level by the bounded multiplication search. · OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.familyCloudTable
familyDecoration def: Old facet names may repeat while every new strip has its own copy. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyDecoration
familyEnd def: Inclusion of one occurrence-sensitive local patch into a disjoint family. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyEnd
familyIndicator def: The indicator of a family on the Boolean cube. · OAI.TalagrandDiscreteConvexity.familyIndicator
familyInOutputSizeTime def: The actual complete computation is polynomial in the final full vertex count; the level is never silently treated as an equally long input. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.familyInOutputSizeTime
familyInOutputSizeTime def: The actual complete computation is polynomial in the final full vertex count; the level is never silently treated as an equally long input. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.familyInOutputSizeTime
familyInterval def: Actual parent and second-generation intervals indexed by their occurrences. · OAI.ThompsonNonamenability.familyInterval
familyInTime def: Complete initialization, actual counted loop, and normalized halt. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.familyInTime
familyInTime def: The second phase executes the checked family program from the already materialized level. Its runtime is polynomial in the original vertex count. · OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyInTime
familyInTime def: The actual native family run, including geometric-level computation. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.familyInTime
familyInTime def: Complete initialization, actual counted loop, and normalized halt. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.familyInTime
familyInTime def: The second phase executes the checked family program from the already materialized level. Its runtime is polynomial in the original vertex count. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyInTime
familyInTime def: The actual native family run, including geometric-level computation. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.familyInTime
familyKind def: Separate copies of every vertex and port are retained under replacement. Even two uses of the very same template have disjoint sigma-indexed vertices. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyKind
familyLinearEquiv def: A finite family specifies exactly one linear map on its coordinate space. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.familyLinearEquiv
familyMeasure def: The probability of an arbitrary family, with no monotonicity condition. · OAI.TalagrandDiscreteConvexity.familyMeasure
familyMeasure def: The Bernoulli measure of an arbitrary finite family. · OAI.TalagrandDiscreteConvexity.familyMeasure
familyMember def: Auxiliary formula for a value selected from the set F(i). Its variables are the family graph, the index, and the selected value. · OAI.PartitionConsistency.SetLanguage.familyMember
familyName def: Retained old branches are shared (name zero). Every genuinely new group branch receives a distinct name including its group, not merely its formula. · OAI.PlanarL1.Interpolation.familyName
familyOfFintype def: Finite families with any finite index type give the same segment tests. · OAI.DiamondDistortion.SegmentSystem.familyOfFintype
familyOperator def: A finite sum of genuine Volterra integrals with continuous coefficient paths. · OAI.ForcedComputation.WeaklySingular.familyOperator
familyPairing def: Disjoint union of the passages of the individual path components. · OAI.TorsionFreeZeroDivisors.PathIncidences.familyPairing
familyPairVector def: The pair certificate coordinates averaged over ordered pairs of bases. · OAI.MUB6.Certificate.MixedSemantics.familyPairVector
familySize def: A uniform size for an arbitrary family, normalized to zero for an empty index set. This is a real supremum, not an attained maximum. · OAI.EilenbergGanea.familySize
familySource def: The family retains the completed ceiling machine's two finite registers. · OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familySource
familySource def: The family retains the completed ceiling machine's two finite registers. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familySource
familyTape def: The family unary guard consumes the padding machine's existing level. · OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyTape
familyTape def: Unused private shadows of the two public roles remain empty. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.familyTape
familyTape def: The family unary guard consumes the padding machine's existing level. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyTape
familyTape def: Unused private shadows of the two public roles remain empty. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.familyTape
familyUnion def: Regular union of an arbitrary indexed family of binary relations. The bounded graph constructor subsequently makes this relation an actual set. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.familyUnion
familyVertexEquiv def: Exact coordinate bridge to the proved geometric family. · OAI.MaxCutGames.Foundations.PCP.VertexPadding.familyVertexEquiv
familyVertexEquiv def: Exact coordinate bridge to the proved geometric family. · OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.familyVertexEquiv
Fan abbrev: Fan occurrences are the actual included rows, counted once even if several top occurrences use them. Positions are NOT identified by generator labels. · OAI.HyperbolicObstruction.ConeSkeleton.Fan
FanAdjacent def: The undirected fan graph is a literal simple bipartite subgraph, not its quotient by letter labels (which need not be injective). · OAI.HyperbolicObstruction.CoreGeometry.FanAdjacent
FanData structure: Combinatorial data at ONE fan occurrence in a fragment of a normalized picture. S indexes all selected top faces whose occurrence has this fan slot, including top faces that do not actually turn at this fan. The injectivity condition is … · OAI.HyperbolicObstruction.FanLink.FanData
fanRoute def: The source's fixed fan paths, length at most two, in the actual indexed fan before its edge labels are identified in the bouquet. · OAI.HyperbolicObstruction.CoreWordGraph.fanRoute
fanScore def: Each fan retains two units of critical exponent even when fully charged. · OAI.HyperbolicObstruction.IncidenceTemplate.fanScore
FanTriangle abbrev: Each fan triangle retains its original edge field and BOTH distinct radial ports, independently of repetitions in the assigned generator row. · OAI.HyperbolicObstruction.ConeSkeleton.FanTriangle
FarbWeinbergerLatticeInput def: The simply connected uniform-lattice specialization of Farb–Weinberger (2008), Proposition 3.4. · OAI.PolycyclicRecognition.FarbWeinbergerLatticeInput
farData def: The retained list and prescribed split determine the analytic data. No frequency assumption is supplied by the caller. · OAI.Falconer.PolicyJetData.farData
fastResidueProbability def: Constant-piece rational P: seven ramp sums, hence no loop of length Q or d. · OAI.ExactQuantumFactoring.OrderTrial.fastResidueProbability
favorableCount def: Closed form for the number of favorable unit residues. Only n+1 levels and the prime-power factors occur; there is no modulo-m residue enumeration. · OAI.ExactQuantumFactoring.favorableCount
FavorableTrial def: These work bounds refer to the entire hypothetical execution, including prefixes and counter iterations skipped after an early YES. · OAI.LowSpaceSubsetSum.RepresentationSetup.FavorableTrial
fc def: Averages against conj character. Evaluation form instead of linear notation. · OAI.FourierLLogL.Dyadic.fc
FCode inductive: A finite first-order functional language on binary trees. There are no function-valued atoms: only projections, pairing, composition, branching and an ordinary data-dependent loop. · OAI.ParityWL.Complexity.FCode
Fcore def: Length is the recursion argument; all color counts at the previous length are available before the next length is constructed. · OAI.QuantitativeVanDerWaerden.Fcore
Feasible def: Skew flows combine the two antiparallel directions. The upper capacity bound and skew symmetry give both directed residual bounds. · OAI.ContingencyTables.PublishedEdmondsKarp.Feasible
Feasible def: A compositional polynomial-time feasibility predicate. · OAI.RationalHitting.StackLanguage.Feasible
Feasible def: Feasibility retains membership in the given witness set. · OAI.ReflexiveFixedPoints.OrderedTree.Feasible
FeasibleNode abbrev: A feasible node contains only a node and a proposition, not extra witness data. · OAI.ReflexiveFixedPoints.OrderedTree.FeasibleNode
FeasibleProfile def: Semantic feasible profiles. Normal witnesses are retained, rather than assuming the manuscript's characterization of this finite set. · OAI.PureTypeSystem.FeasibleProfile
fee def: Cost to stack this frame in our fixed prefix encoding. · OAI.Fifths.Flow.fee
feed def: The first rejected record is retained, as is its newly allocated trie key. Further callbacks freeze both structures. · OAI.LowSpaceSubsetSum.RecordedDictionary.feed
Feedback def: A feedback set intersects EVERY actual directed cycle. · OAI.DirectedFeedback.Digraph.Feedback
feedback def: A middle traversal followed by any finite number of context returns and traversals. · OAI.TwoWayComplementation.Diagram.feedback
Feeds structure: Access another bench. b prepares q's inputs. · OAI.PowerSaving.RAM.Bench.Feeds
fexpo def: Abstract compression exponent packet with abundant room for both masked mean and false positives charges. · OAI.ExactDerandomization.Est.fexpo
Fiber def: The actual rank-order compression fiber; subtraction agrees with addition over the binary field. · OAI.MaxCutGames.Appendix.CompressionCount.Fiber
Fiber def: The genuine rank-additive compression fiber. In characteristic two, Y - X and Y + X are equal. · OAI.MaxCutGames.Appendix.FullCompression.Fiber
Fiber def: Exact fibers, defined using the proved availability ideal rather than an arbitrarily assigned classification. · OAI.PartitionConsistency.LocalDiagramSystem.System.Fiber
Fiber abbrev: The fiber as a scheme, with its full coordinate-ring structure. · OAI.StableCoordinate.GeometricInterpretation.Fiber
Fiber def: The actual rank-order compression fiber; subtraction agrees with addition over the binary field. · OAI.UniqueGamesTheorem.Appendix.CompressionCount.Fiber
Fiber def: The genuine rank-additive compression fiber. In characteristic two, Y - X and Y + X are equal. · OAI.UniqueGamesTheorem.Appendix.FullCompression.Fiber
fiber def: The proposal integers that produce a given output. · OAI.ContingencyTables.FairBits.fiber
fiber def: A vertical affine section of a set in a product vector space. · OAI.Problem358.AffineSlice.fiber
fiber def: The fiber of a product set over its first coordinate. · OAI.Problem358.SectionMeasure.fiber
fiber def: The elements of A with the specified key. · OAI.TalagrandDiscreteConvexity.FiniteFibers.fiber
fiberAngle def: The unique upper-half-disk angle, extended by zero outside its open radial domain. · OAI.SymmetricMahler.fiberAngle
fiberAssignmentEquiv def: Reorganize coordinates into the fibers of a grouping function. · OAI.Problem335.IndependentCoordinates.fiberAssignmentEquiv
fiberCoaction def: The genuine fiber-weight coaction on k[a,d,b,c,u]/(ac-bd-1). · OAI.StableCoordinate.DeterminantWeights.fiberCoaction
fiberCocone abbrev: Its full one fibre is therefore the colimit of the full simplex fibres. · OAI.Thomason.Construction.CosieveSimplex.fiberCocone
fiberCocone abbrev: Its full zero fibre is therefore the colimit of the full simplex fibres. · OAI.Thomason.Construction.SieveSimplex.fiberCocone
fiberCoconeIsColimit def: This uses the proved adjunction, with no published fibre-colimit input. · OAI.Thomason.Construction.CosieveSimplex.fiberCoconeIsColimit
fiberCoconeIsColimit def: This uses the proved adjunction, with no published fibre-colimit input. · OAI.Thomason.Construction.SieveSimplex.fiberCoconeIsColimit
fiberCoordinate def: Fiber coordinate w/x_c^k; used as a trivialization on the chart x_c ≠ 0. The quotient function itself is defined everywhere. · OAI.Nagata.W16.AssociatedBundle.fiberCoordinate
FiberCrosses def: A compact connected fiber joins both designated boundary sets. · OAI.EuclideanFiveColor.FiberCrosses
fiberDiagonal def: A bounded diagonal on the original l2(Z) fiber. · OAI.FiniteFactor.fiberDiagonal
fiberEmbedding def: The actual closed immersion defined by f - t. · OAI.StableCoordinate.GeometricInterpretation.fiberEmbedding
fiberEquiv def: No incidence or probabilistic assumption is hidden in the pinned-fiber bijection: free assignments extend uniquely, with the original fieldwise rule. · OAI.HyperbolicObstruction.PinnedAssignments.fiberEquiv
fiberEquiv def: Every constructed fiber is linearly identified with the actual kernel. · OAI.Kaplansky.SmoothKernel.SurjectiveFamily.fiberEquiv
fiberEquiv def: The exact compression fiber is in bijection with two independent spaces of linear maps. No rank or cardinality claim is an assumption of this equivalence. · OAI.MaxCutGames.Appendix.CompressionCount.fiberEquiv
fiberEquiv def: Coordinate transport is a bijection on the complete rank-additive fibers. · OAI.MaxCutGames.Appendix.FullCompression.fiberEquiv
fiberEquiv def: Isomorphism of the actual exact fibers at moved vertices. · OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso.fiberEquiv
fiberEquiv def: A canonical fiber equivalence. Its forward map is inclusion, not an independent chosen bijection. · OAI.PartitionConsistency.LocalDiagramSystem.System.fiberEquiv
fiberEquiv def: Ring-theoretic fibers have the expected simultaneous-equation presentation, with the scalar subtraction performed in the appropriate algebra at each stage. · OAI.StableCoordinate.IteratedQuotient.fiberEquiv
fiberEquiv def: The exact compression fiber is in bijection with two independent spaces of linear maps. No rank or cardinality claim is an assumption of this equivalence. · OAI.UniqueGamesTheorem.Appendix.CompressionCount.fiberEquiv
fiberEquiv def: Coordinate transport is a bijection on the complete rank-additive fibers. · OAI.UniqueGamesTheorem.Appendix.FullCompression.fiberEquiv
fiberEvent def: The part of an event in one actual visible-data fiber. · OAI.MaxCutGames.Decoder.VisibleTransfer.fiberEvent
fiberEvent def: The part of an event in one actual visible-data fiber. · OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.fiberEvent
fiberFiniteEmbedding def: Canonical inclusion of finite coordinate vectors in l2(Z). · OAI.FiniteFactor.fiberFiniteEmbedding
fiberGradient def: Fiber derivatives of the actual defining function. · OAI.AffineBernstein.fiberGradient
fiberIso def: The opposite of the reversed zero fibre is the original one fibre. · OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.fiberIso
fiberKernel def: The conditional source mass, totalized by a fixed point mass on empty fibers. The fallback only concerns observations of source probability zero. · OAI.MatroidProphet.Secretary.fiberKernel
fiberMap def: Translation by the logical kernel parametrizes a quotient fiber. · OAI.MaxCutGames.Gadget.Quotient.fiberMap
fiberMap def: The full-fibre map is the restriction of the original strict functor. · OAI.Thomason.Construction.SieveMap.fiberMap
fiberMap def: Translation by the logical kernel parametrizes a quotient fiber. · OAI.UniqueGamesTheorem.Gadget.Quotient.fiberMap
fiberMarginalPMF def: The observation marginal as an actual PMF, with its normalization proved. · OAI.MatroidProphet.Secretary.fiberMarginalPMF
fiberMass def: Finite pushforward weights. · OAI.MatchingEntropy.fiberMass
fiberMass def: The source mass of a fiber of the observation map. · OAI.MatroidProphet.Secretary.fiberMass
fiberMass def: Mass of a fiber of a map, for a measure supported on a finite set. · OAI.Ostmann.fiberMass
fiberMatrixFinite def: The finite matrix action takes values in actual l2, by the finite-sum bound. · OAI.FiniteFactor.fiberMatrixFinite
fiberMatrixLinear def: The algebraic action of a matrix on finite vectors. · OAI.FiniteFactor.fiberMatrixLinear
fiberNatIso def: The actual one-fibre functor is conjugate to the zero-fibre functor. · OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.fiberNatIso
fiberOfEquiv def: A first-coordinate fiber of a product decomposition is the second factor. · OAI.Problem348.TreeSampling.fiberOfEquiv
FiberPackage def: Complete second principal group, universally including the zero fiber. · OAI.StableCoordinate.FiberPackage
fiberPairResidual def: The actual bounded operator whose vanishing is the pair identity. · OAI.FiniteFactor.fiberPairResidual
fiberPerm def: Simultaneous permutations on disjoint coordinate lines. · OAI.CoordinateSweeps.Grid.fiberPerm
fiberPermEquiv def: Word-preserving permutations and independent permutations of its fibers are literally equivalent finite sets. This yields the factorial frame moments. · OAI.CoordinateSweeps.OrdinaryTensor.fiberPermEquiv
fiberPiece abbrev: Actual fiber-weight pieces: wt(a,d,b,c,u) = (1,1,-1,-1,0). · OAI.StableCoordinate.Obstruction.fiberPiece
fiberPMF def: A bona fide conditional probability mass function on the complete seed. · OAI.MatroidProphet.Secretary.fiberPMF
fiberPolynomial def: The ordinary fiber polynomial above the affine point with parameter U. · OAI.Nagata.W03.LowDegree.fiberPolynomial
fiberProductEquiv def: Trivializing equal-size fibers identifies the full sample space with a product; the first coordinate remains the original quotient map. · OAI.MaxCutGames.Inverse.KMSBasisComparison.fiberProductEquiv
fiberProductEquiv def: Trivializing equal-size fibers identifies the full sample space with a product; the first coordinate remains the original quotient map. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fiberProductEquiv
fiberQuotientEquiv def: The equivalence induced on the fiber over an arbitrary scalar c. No nonzero hypothesis is needed: this is equally valid for the zero fiber. · OAI.StableCoordinate.fiberQuotientEquiv
fiberRestrict def: The inclusion map underlying a contraction between exact fibers. · OAI.PartitionConsistency.LocalDiagramSystem.System.fiberRestrict
fiberRestriction def: Restriction to the marked base fiber is coefficientwise evaluation U=a. · OAI.Nagata.W18.fiberRestriction
FiberShift def: Exact infinitesimal formulation of a fixed fiber-weight shift. · OAI.ComplexCancellation.Determinant.FiberShift
fiberShiftVector def: Coordinate translation on the original l2 fiber. · OAI.FiniteFactor.fiberShiftVector
fiberSize def: The multiplicity of one image value, counting the distinct elements of X. · OAI.LowSpaceSubsetSum.fiberSize
fiberStreetSubcomplex def: The actual full-fibre Street subcomplex of a binary strict label. · OAI.Thomason.Construction.NormalizedSimplexIdentities.fiberStreetSubcomplex
fiberWeight def: Pushing a finite set through a noninjective map retains the multiplicity of each image value. In particular, the two ordered Goldbach pairs with coordinates exchanged must not be identified by the polynomial map. · OAI.Problem337.PrimePairSieve.fiberWeight
fiberWeight def: Fiber weights on a,d,b,c,u; these encode fiber scaling. · OAI.StableCoordinate.Obstruction.fiberWeight
Fibre def: The complete draw, constrained only by the observations outside the hidden set. · OAI.MaxCutGames.Soundness.ZeroInformation.Fibre
Fibre def: The complete draw, constrained only by the observations outside the hidden set. · OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Fibre
fibreChart def: Actual fibre substitution w=P(z)*v over an open base where P is nonzero. · OAI.Nagata.FiberCoordinateChange.fibreChart
fibreCoordinateEquiv def: A proved coordinate bijection for the actual quotient fibre over a fixed lift. · OAI.Nagata.W06.TorusConfiguration.fibreCoordinateEquiv
fibreEquiv def: The entire common outgoing set, not a quotient of its parallel steps. · OAI.TorsionFreeZeroDivisors.Factors.fibreEquiv
fibreRepresentative def: The vector with scalar c over the chosen nonzero lift z. · OAI.Nagata.W06.TorusConfiguration.fibreRepresentative
fibreScaleAtLift def: Scalar multiplication between the actual two fibres in the specified covering frames. This finite-fibre map does not assert that these maps glue into a global bundle morphism. · OAI.Nagata.W06.TorusConfiguration.fibreScaleAtLift
Field abbrev: The actual intermediate field generated over the rationals by s. · OAI.CirculantHadamard.CyclotomicAdjoin.Field
Field structure: A scalar field on the whole band, including all its components. Its only compatibility condition is equality at actual allowed switch heights. · OAI.PlanarL1.Columns.Model.Field
field def: Six preserved fields, scratch, and a reversed-output accumulator. · OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.field
field def: A finite stack layout: five preserved fields, scratch, and reversed output. · OAI.MaxCutGames.Explicit.MachineSubdivisionRows.field
field def: Six preserved fields, scratch, and a reversed-output accumulator. · OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.field
field def: A finite stack layout: five preserved fields, scratch, and reversed output. · OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.field
fieldActivity def: A simultaneous same-identifier update, defined by the actual new fields. The boundary estimate is exactly what the ambient complement taper provides. The name map is retained literally; it is not refined to a partition with better-behaved … · OAI.PlanarL1.Columns.Model.BState.fieldActivity
fieldAdjacentIncrements def: Actual increment list when a single nonterminal height is varied. · OAI.InvariantIsing.fieldAdjacentIncrements
fieldAmplitudeCurvature def: Its second derivative, written in the chain-rule product form. · OAI.InvariantIsing.fieldAmplitudeCurvature
fieldAmplitudeSlope def: First derivative of the square-root amplitude. · OAI.InvariantIsing.fieldAmplitudeSlope
fieldAppendIndex def: Index of a level in the suffix, after an unchanged prefix. · OAI.InvariantIsing.fieldAppendIndex
fieldAssignment def: The explicit field assignment performed by all k real lookup stages. Unrelated tapes, including the loader's empty index/work tapes, are unchanged. · OAI.MaxCutGames.Integration.AddressTupleLoaded.fieldAssignment
fieldAssignment def: The explicit field assignment performed by all k real lookup stages. Unrelated tapes, including the loader's empty index/work tapes, are unchanged. · OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.fieldAssignment
fieldAt def: A single finite field increment. · OAI.BufferedIsing.DSS.fieldAt
fieldBiasCurvature def: Actual second bias derivative, with the root exponent fixed at zero. · OAI.InvariantIsing.fieldBiasCurvature
fieldBiasMean def: The mean spin before the root increment, at an arbitrary bias. · OAI.InvariantIsing.fieldBiasMean
fieldBits def: Exact row field concatenation at the level of stored bits. · OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.fieldBits
fieldBits def: Exact row field concatenation at the level of stored bits. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.fieldBits
fieldBound def: One q-only bound covers every coefficient and every finite offset. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound
fieldBound def: One q-only bound covers every coefficient and every finite offset. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldBound
fieldBudget def: A common bound for either concrete field operation of radius at most max. · OAI.MaxCutGames.Foundations.Complexity.PoweringPlanBudget.fieldBudget
fieldBudget def: A common bound for either concrete field operation of radius at most max. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPlanBudget.fieldBudget
fieldCircle def: The ordinary circle quotient map, before passage to F/Z. · OAI.PlaneFiveColor.InvariantMean.fieldCircle
fieldCutSequence def: A clamped extension used only to express finite summation by parts. · OAI.InvariantIsing.fieldCutSequence
fieldDegree def: A deliberately simple explicit upper choice; optimization of the field size is irrelevant because these thresholds are fixed before the input. · OAI.MaxCutGames.Quadratic.fieldDegree
fieldDegree def: A deliberately simple explicit upper choice; optimization of the field size is irrelevant because these thresholds are fixed before the input. · OAI.UniqueGamesTheorem.Quadratic.fieldDegree
fieldEnergy def: Deterministic magnetic energy. · OAI.InvariantIsing.fieldEnergy
fieldFinalChart def: The analogous final-height chart changes the last increment and the normalizing diagonal covariance together. · OAI.InvariantIsing.fieldFinalChart
fieldFiniteObservableDifferential def: Derivative of the weighted observable. · OAI.InvariantIsing.fieldFiniteObservableDifferential
fieldFiniteWeightDifferential def: Derivative of the unnormalized Gaussian weight. · OAI.InvariantIsing.fieldFiniteWeightDifferential
fieldForQueryEvent def: The sole predicate-dependent component is a bounded finite-state offset. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent
fieldForQueryEvent def: The sole predicate-dependent component is a bounded finite-state offset. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent
fieldFunction def: A finite covariance step path, with arbitrary values assigned at its cuts. · OAI.InvariantIsing.fieldFunction
fieldHeightCoordinateValue def: The literal single-coordinate value, using exactly the Gaussian recursion of fieldValue with the updated height vector. · OAI.InvariantIsing.fieldHeightCoordinateValue
fieldIncrement def: Exponent and covariance increment for one backward step. · OAI.InvariantIsing.fieldIncrement
fieldInsertCut def: Inserting a cut strictly inside one existing cell keeps the field path unchanged. · OAI.InvariantIsing.fieldInsertCut
fieldInteriorChart def: This changes the height at an interior cell, keeping the final height and every other increment fixed. · OAI.InvariantIsing.fieldInteriorChart
fieldLevelIndex def: Last covariance interval whose lower endpoint has been passed. · OAI.InvariantIsing.fieldLevelIndex
fieldLevelPath def: Monotone unit level values become an admissible overlap path on the same partition as the actual field. · OAI.InvariantIsing.fieldLevelPath
fieldLevelSpinPair def: The field's root is shared by the two replicas. · OAI.InvariantIsing.fieldLevelSpinPair
FieldLine abbrev: Actual one-dimensional field directions, with proportional nonzero vectors identified. · OAI.MaxCutGames.Quadratic.FieldLine
FieldLine abbrev: Actual one-dimensional field directions, with proportional nonzero vectors identified. · OAI.UniqueGamesTheorem.Quadratic.FieldLine
fieldLineRestrictions def: All maps have the same binary dual codomain, despite their different blocks. · OAI.MaxCutGames.Quadratic.fieldLineRestrictions
fieldLineRestrictions def: All maps have the same binary dual codomain, despite their different blocks. · OAI.UniqueGamesTheorem.Quadratic.fieldLineRestrictions
fieldLogCoshSecondFamily def: The actual log-cosh terminal has zero covariance derivatives. · OAI.InvariantIsing.fieldLogCoshSecondFamily
fieldLoop def: Read one unary field, stopping at its zero delimiter. · OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldLoop
fieldLoop def: Read one unary field, stopping at its zero delimiter. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldLoop
fieldMagnetizationLevel def: The physical squared conditional spin means, averaged over the root Gaussian. These are the B_i(h) of the field derivative formula. · OAI.InvariantIsing.fieldMagnetizationLevel
fieldMagnetizationPath def: A globally defined admissible representative on the field partition. · OAI.InvariantIsing.fieldMagnetizationPath
fieldMajorant def: The function g_d used for the finite entropy-domain estimate. · OAI.InvariantIsing.fieldMajorant
fieldObservableDifferential def: Derivative of the weighted observable. · OAI.InvariantIsing.fieldObservableDifferential
fieldPairing def: The field-order-parameter pairing on (0,1). · OAI.InvariantIsing.fieldPairing
fieldPartitionConstant def: The finite constant coming from the positive exponents of a fixed trial partition. · OAI.InvariantIsing.fieldPartitionConstant
fieldRole def: Only the radix tape is switched between endpoint and alphabet fields. · OAI.MaxCutGames.Explicit.MachineProductRow.fieldRole
fieldRole def: Only the radix tape is switched between endpoint and alphabet fields. · OAI.UniqueGamesTheorem.Explicit.MachineProductRow.fieldRole
fieldRows def: Every field is selected from its actual retained location. Dummy rows are kept: the rectangular shape is a compile-time function only of n and t. · OAI.ExactQuantumFactoring.NodeMachine.fieldRows
fieldScalarOverlaps def: Root Gaussian averaging produces the level second moments B_i. · OAI.InvariantIsing.fieldScalarOverlaps
fieldScalarSquareAt def: The natural-index form of a scalar square. All indices used by the finite field are at most the length; the terminal extension avoids casts in zero-increment insertion. · OAI.InvariantIsing.fieldScalarSquareAt
fieldScalarSquares def: The entry indexed by i is the conditional expectation of the square of the physical spin mean at level i, given the starting position. · OAI.InvariantIsing.fieldScalarSquares
fieldSplitHeight def: Duplicate the old height on both sides of the new cut. · OAI.InvariantIsing.fieldSplitHeight
fieldStart def: Seed the destination delimiter before scanning the unary payload. · OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldStart
fieldStart def: Seed the destination delimiter before scanning the unary payload. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldStart
FieldStep structure: Positive intervals partitioning the unit interval, with monotone covariance heights. · OAI.InvariantIsing.FieldStep
fieldTailSpinKernel def: Spin law at the end of the actual successive tilted Gaussian transitions, starting from the given scalar field. · OAI.InvariantIsing.fieldTailSpinKernel
fieldTapes def: The three unary row fields, two empty work tapes, and accumulated output. · OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes
fieldTapes def: The three unary row fields, two empty work tapes, and accumulated output. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes
fieldTerminalIncrements def: The terminal height changes the final variance and the normalizing subtraction by the same amount. · OAI.InvariantIsing.fieldTerminalIncrements
fieldValue def: The canonical one-site value at initial bias b, with the diagonal covariance subtraction. · OAI.InvariantIsing.fieldValue
fieldValue def: The six actual serialized fields, in name/sign/name/sign/name/sign order. · OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.fieldValue
fieldValue def: The six actual serialized fields, in name/sign/name/sign/name/sign order. · OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.fieldValue
fieldWeightDifferential def: Derivative of the unnormalized Gaussian weight. · OAI.InvariantIsing.fieldWeightDifferential
Fieldwise def: Injectivity is imposed separately on each coordinate field, not globally. · OAI.HyperbolicObstruction.PinnedAssignments.Fieldwise
fieldWithHeights def: The original partition with an admissible updated height vector. · OAI.InvariantIsing.fieldWithHeights
files def: Throughout, binary order LSB to MSB, ordinary canonical bits, also on any supplied argument tapes. · OAI.Fifths.files
fill def: The actual square filling, with no extension assumption. · OAI.HyperbolicObstruction.SquarePathFilling.fill
fill def: Proof-level description of the finite register updates. · OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.fill
fill def: Fill only the as-yet-undefined places in a prescribed countable set. · OAI.PartitionConsistency.CohenForcing.Condition.fill
fill def: Source data for one recursive call (one batch). · OAI.PowerSaving.RAM.fill
fill def: choose dyad by doubling until ≥N · OAI.PowerSaving.Selection.fill
fill def: Proof-level description of the finite register updates. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.fill
Fillable def: Existence of a finite labelled genus-zero filling. This abbreviation contains no geometric assertion outside the fully specified finite map. · OAI.Release075.Fillable
FilledBetween def: Filling the two paths glued along their common endpoints. · OAI.Release075.FilledBetween
fillingCorrection def: The change on a selected base disk; it is zero off the disks. · OAI.CircleDomainRigidity.FiniteTransfer.fillingCorrection
fillSigns def: The mathematical result of the individual finite sign-register writes. · OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.fillSigns
fillSigns def: The mathematical result of the individual finite sign-register writes. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.fillSigns
fillTables def: Fill the slice with independently supplied complete Boolean tables, leaving all outside tables at their fixed values. · OAI.OptimalMaxCut.TreeCode.fillTables
filt def: Causal dyadic averaging, with both the present and the complete past. · OAI.GeometricFilter.filt
filt def: Causal dyadic averaging, with both the present and the complete past. · OAI.SignedDisk.GeometricFilter.filt
FilteredBy inductive: A finite filtration specified by short exact sequences, with a list recording its successive quotients. · OAI.CoherentK0.FilteredBy
FilteredRanks structure: Increasing history information, adapted ranks, and the literal finite conditional tower relation for old counts under the new observation. · OAI.KServer.RankTracking.FilteredRanks
FilteredSizes structure: Old and new membership counts shifted by one, with literal finite-fiber conditioning. There is no policy-existence or budget assumption in this data. · OAI.KServer.KeySizeTracking.FilteredSizes
filteredTotalHomology def: The induced filtration on the homology of the given total complex. · OAI.PolycyclicRecognition.filteredTotalHomology
filterEntry def: A normalized factor of a polynomial in a diagonal adjoint operator. · OAI.HarmonicCounterexample.Control.filterEntry
filterNet def: Literal deferred completion filter on retained registers. The input s and canonical-output circuits are to be computed from the verified full log; this compiler does not smuggle those quantities into the preparation. · OAI.ExactQuantumFactoring.Completion.filterNet
filtration def: The increasing filtration associated to an integer grading. · OAI.ComplexCancellation.GradedLND.filtration
filtration def: At level n, the sigma algebra consists precisely of unions of the concrete mesh-index fibers. The grid is frozen after its final depth. · OAI.LipschitzHilbert.FiniteLineGrid.filtration
fin9Equiv def: Concrete row/column enumeration of the nine tensor coordinates. · OAI.EuclideanRamsey.NineRational.fin9Equiv
finalCells def: Full cell list at readout, with the copied anchors on either side. · OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.finalCells
finalClamp def: Retraction to a final segment by clamping below its first vertex. · OAI.Thomason.Construction.SimplexComplex.finalClamp
finalContraction def: The simultaneous contraction is an actual simplicial homotopy. · OAI.Thomason.Construction.RealizedCube.finalContraction
finalContractionMap def: Simultaneously contract all interval coordinates to their final vertex. · OAI.Thomason.Construction.RealizedCube.finalContractionMap
finalDiagramCutoff def: A single diagonal cutoff for filling and the full LIFTED chain statement. Nothing about a future picture, action, word, or deck group is sampled later. · OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramCutoff
finalFace def: Inclusion of the final segment with q+1 vertices. · OAI.Thomason.Construction.SimplexComplex.finalFace
finalFaceIso def: The full strict subcategory on a final segment is its smaller oriental. · OAI.Thomason.Construction.SimplexComplex.finalFaceIso
finalProgramAnswer def: Equality is tested before the final query, so equal strings return zero on every execution, including executions with a bad seed. · OAI.EditApproximation.finalProgramAnswer
finalState def: The history after precisely one pass through all current parents. · OAI.ReflexiveFixedPoints.CandidateContext.finalState
finalTapes def: The exact tapes produced by repeatedly executing the actual vertex body. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes
finalTapes abbrev: Literal final arena; this abbreviation contains no execution assumption. · OAI.MaxCutGames.Integration.AddressTupleFrame.finalTapes
finalTapes def: The exact tapes produced by repeatedly executing the actual vertex body. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes
finalTapes abbrev: Literal final arena; this abbreviation contains no execution assumption. · OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.finalTapes
finalTimePolynomial def: Twelve private stacks are drained, then the finite state is reset. C is the fixed maximum number of pushes in a raw-program transition. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial
finalTimePolynomial def: Twelve private stacks are drained, then the finite state is reset. C is the fixed maximum number of pushes in a raw-program transition. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial
finalVertex def: The final vertex in every coordinate of the finite simplicial cube. · OAI.Thomason.Construction.RealizedCube.finalVertex
finalVertexEdgeOperator def: The ordinal edge from any vertex to the final one. · OAI.Thomason.Construction.finalVertexEdgeOperator
finColumnFamily def: The same actual frame on Fin(card(A s)), as required by finite Hilbert amplification and the full-column coordinate construction. · OAI.KadisonSimilarity.NestedTracialMatrices.finColumnFamily
finCoupling def: Range one is returned directly. Every other range uses exactly the fresh low-bit candidate sampler with at most n³ attempts. · OAI.LowSpaceSubsetSum.finCoupling
findAcc def: Tail-recursive matching with each scalar subtraction and comparison charged. · OAI.LowSpaceSubsetSum.StoredEntryTerminal.findAcc
finDeleteLeft def: Deleting a head coordinate commutes with the literal Fin concatenation. · OAI.CoordinateSweeps.finDeleteLeft
finDeleteRight def: Deleting a tail coordinate, in the same original head-then-tail order. · OAI.CoordinateSweeps.finDeleteRight
findIndex def: First-index search, expressed by one polynomial fold rather than an oracle. · OAI.ParityWL.Complexity.findIndex
findValid def: A terminating first-valid search on the explicitly ordered ambient list. · OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.findValid
findValid def: A terminating first-valid search on the explicitly ordered ambient list. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.findValid
fineKernel def: The fine density has the same fast argument and the slow argument frozen at t. · OAI.ThreeTorus.fineKernel
fineVariation def: Fine changes can be selected pathwise; wholesale changes are excluded only when the interpolation and scale parameters are actually held fixed. · OAI.KServer.FineCaps.fineVariation
finFold def: The same labelled right-comb tensor with its exact finite indexing. · OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.finFold
finIdeal def: The closed finite-domain ideal, with the absorption and closedness already proved. · OAI.TraceConeClassification.ExtendedTrace.finIdeal
finIntegerLabels def: The literal finite child labels embedded in the integer line. · OAI.TraceReconstruction.finIntegerLabels
finish def: false flag means still running at n. · OAI.Fifths.Single.finish
finish def: Clear both head registers and the mismatch flag after choosing the exit. · OAI.MaxCutGames.Foundations.Complexity.MachineCompare.finish
finish def: Zero remaining iterations still run the actual final transfers and halt with every tape other than the designated output empty. · OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.finish
finish def: Reset both the ambient finite state and the drain register before exiting. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.finish
finish def: Final labeled positions after the specified legal one-label service. · OAI.UniformKServer.finish
finish def: Clear both head registers and the mismatch flag after choosing the exit. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.finish
finish def: Zero remaining iterations still run the actual final transfers and halt with every tape other than the designated output empty. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.finish
finish def: Reset both the ambient finite state and the drain register before exiting. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.finish
finishBudget def: Cleanup after a preceding run bounded by prior, with fixed stack count and fixed maximum number of pushes per machine transition. · OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.finishBudget
finishBudget def: Cleanup after a preceding run bounded by prior, with fixed stack count and fixed maximum number of pushes per machine transition. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.finishBudget
finishEntry def: Finish first copies the dart-count field, then the vertex-count field. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.finishEntry
finishEntry def: Finish first copies the dart-count field, then the vertex-count field. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.finishEntry
finishExecution def: The terminal configuration has precisely the actual output stream and no remaining work tapes. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.finishExecution
finishExecution def: The terminal configuration has precisely the actual output stream and no remaining work tapes. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.finishExecution
finishFields def: Tail, selected global target, returned port, scratch, reverse field, equality field, row buffer, accumulated output. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.finishFields
finishFields def: Tail, selected global target, returned port, scratch, reverse field, equality field, row buffer, accumulated output. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.finishFields
finishInstruction def: The return port is copied from its physical unary tape before fixed-slope arithmetic adds the actual selected global target. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.finishInstruction
finishInstruction def: The return port is copied from its physical unary tape before fixed-slope arithmetic adds the actual selected global target. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.finishInstruction
finishInTime def: The entry hop reaches the actual cleanup list, then all work is drained, the accumulator is reversed, and the final finite register is reset. · OAI.MaxCutGames.Explicit.MachineProductFinish.finishInTime
finishInTime def: Clear precisely the three isolated temporary fields and increment the physical row counter before returning to the input guard. · OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.finishInTime
finishInTime def: Exact execution, including the real drain loops, reversal, and reset. The only program hypotheses identify the caller's actual placed statements. · OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.finishInTime
finishInTime def: Physical cleanup and canonical finite-state reset complete the body. · OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.finishInTime
finishInTime def: The entry hop reaches the actual cleanup list, then all work is drained, the accumulator is reversed, and the final finite register is reset. · OAI.UniqueGamesTheorem.Explicit.MachineProductFinish.finishInTime
finishInTime def: Clear precisely the three isolated temporary fields and increment the physical row counter before returning to the input guard. · OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.finishInTime
finishInTime def: Exact execution, including the real drain loops, reversal, and reset. The only program hypotheses identify the caller's actual placed statements. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.finishInTime
finishInTime def: Physical cleanup and canonical finite-state reset complete the body. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.finishInTime
finishSteps def: The actual final-copy/cleanup cost on the tapes obtained from the loop. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps
finishSteps def: The actual final-copy/cleanup cost on the tapes obtained from the loop. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.finishSteps
finiteAdjunction def: Finite fibre formation is a left adjoint inside the finite category itself. · OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.finiteAdjunction
finiteAffineCover def: Quasi-compactness gives a finite affine refinement of a line-bundle trivializing cover. · OAI.ActualSheafTensor.LineTrivialization.finiteAffineCover
FiniteAffineLineCover structure: Finite affine trivializations, with their ordinary ring schemes, covering maps and module-sheaf isomorphisms. · OAI.ActualSheafTensor.FiniteAffineLineCover
FiniteAlgebra def: The finite condition used in the von Neumann type decomposition. · OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra
FiniteAlphabet def: Finitely many stacks and control states are already part of FinTM2. This additionally excludes infinite stack alphabets. · OAI.DirectedFeedback.FiniteAlphabet
FiniteAlphabet def: Every physical tape has a finite alphabet. Together with M.kFin, this also makes the disjoint union of all physical tape alphabets finite. · OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet
FiniteAlphabet def: Every physical tape has a finite alphabet. Together with M.kFin, this also makes the disjoint union of all physical tape alphabets finite. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet
FiniteAppendingSupply def: This finite appending supply is a derived theorem of the published inputs, never introduced as an additional published assumption. · OAI.CircleDomainRigidity.FiniteAppendingSupply
finiteAssignmentProbability def: Uniform assignment probability for an arbitrary finite variable set. · OAI.MaxCutGames.Quadratic.finiteAssignmentProbability
finiteAssignmentProbability def: Uniform assignment probability for an arbitrary finite variable set. · OAI.UniqueGamesTheorem.Quadratic.finiteAssignmentProbability
finiteAverage def: Uniform average over a nonempty finite set. · OAI.KadisonKastler.finiteAverage
finiteAveragedDifferential def: The averaged differential, written as an actual bilinear map. · OAI.KadisonKastler.finiteAveragedDifferential
finiteBaseExpectation def: The actual trace projection, defined by solving the finite trace-pairing system. No conditional expectation existence theorem is assumed. · OAI.KadisonKastler.finiteBaseExpectation
FiniteBaseIndependence def: The finite-base specialization of the published independence theorem. Its domain remains a tracial ultraproduct in the input declarations below. · OAI.KadisonKastler.FiniteBaseIndependence
finiteBellmanSystem def: A finite system of node-specific action lists. Child states may belong to any lower level of the source tree. · OAI.EditApproximation.finiteBellmanSystem
FiniteBernsteinInput def: The finite centered-sum specialization of Tropp, Theorem 4.16. This is the exact Lean proposition to be passed explicitly to downstream concentration theorems. · OAI.EditApproximation.FiniteBernsteinInput
finiteBilinearProduct def: The bilinear amplification with arbitrary finite index types. · OAI.KadisonKastler.finiteBilinearProduct
FiniteBinDistributionInput def: Finite-bin specialization of Tenenbaum (2000), main Theorem (i),(iii), including the stated multiplicity version. · OAI.JointDickman.PublishedInputs.FiniteBinDistributionInput
finiteBlocks def: Literal row/block array of a concrete node word. · OAI.TreeEdit.BinaryLower.FiniteTree.finiteBlocks
finiteBoundaryPath def: A finite boundary chart acts measurably on continuous trace paths. · OAI.SLEExactGauge.finiteBoundaryPath
FiniteBoxPrekopaLeindler def: Precisely the previously published finite-box integral interpolation input. The functions need only be positive and continuous on the common compact coordinate box; all integrals are Lebesgue integrals. · OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler
FiniteBridgeMassEstimate def: Necessary estimate c:finite(1), inputs.tex:13, on the actual path sum. · OAI.CriticalHoneycomb.FiniteBridgeMassEstimate
FiniteBridgeMassEstimate def: Uniform two-sided bounds for the critical strict bridge path sum. · OAI.CriticalHoneycomb.FiniteBridgeMassEstimate
FiniteCentralAveragingInput def: Center-valued trace existence, restricted to the finite type-II central corners needed for this application. · OAI.BoundedHochschild.KadisonRingrose.FiniteCentralAveragingInput
FiniteCertificateCoverage def: The finite obligation discharged by concrete certificate coverage. · OAI.CycleClique.Construction.FiniteCertificateCoverage
finiteChainPreimage def: Pull a supported finite chain back through its original order embedding. · OAI.Thomason.Construction.finiteChainPreimage
finiteChart def: The image of the entire finite matrix domain. · OAI.UniqueGamesTheorem.Inverse.KMS.finiteChart
finiteChartSlice def: A finite union of formal-coordinate cones cut by normalized evaluation constraints. · OAI.CartierSections.finiteChartSlice
FiniteCheeger def: The smallest Cheeger consequence needed here. The cut inequality uses unnormalized stationary flow across each cut once; energy includes the usual factor one half in its symmetric pair-sum formula. · OAI.ContingencyTables.PublishedInputs.FiniteCheeger
finiteChoiceCoupling def: A bounded choice from an explicitly enumerated finite set. This is used only for the polynomial-size interval guesses and residue ranges. · OAI.LowSpaceSubsetSum.finiteChoiceCoupling
FiniteCircleGreenFormula def: Published input: the finite-round-hole planar specialization of Spivak's Theorem5-5. All geometric boundaries and integrals are explicit. · OAI.CircleDomainRigidity.FiniteCircleGreenFormula
finiteCochainAverage def: The linear cochain obtained by averaging the last argument. · OAI.KadisonKastler.finiteCochainAverage
finiteCochainModuleDefect def: Failure of the finite average to be a right module map in its last argument. · OAI.KadisonKastler.finiteCochainModuleDefect
finiteCodiscrete def: The codiscrete target used to test object sets is already a finite category. · OAI.Thomason.Construction.FiniteReflectionInput.finiteCodiscrete
finiteCodiscreteFunctor def: Codiscrete categories already satisfy every positive dimension bound. · OAI.Thomason.Construction.StrictOmegaCategory.finiteCodiscreteFunctor
FiniteCoefficientConjugations def: The finite coefficient condition supplied by separable restrictions in the manuscript. It asserts no global range inclusion for a local conjugacy. · OAI.KadisonKastler.FiniteCoefficientConjugations
finiteCoefficientMap def: The original affine coefficients, extended linearly from basis rows. · OAI.RegularPointCoordinates.finiteCoefficientMap
finiteCoefficientPolynomial def: Synthesize the polynomial from its finite tuple of actual coefficients. · OAI.Nagata.Workers.W10.finiteCoefficientPolynomial
finiteColorEmbedding def: Explicit recoloring into any sufficiently large standard finite palette. · OAI.QuantitativeVanDerWaerden.finiteColorEmbedding
FiniteColumnImplementers structure: Data obtained by implementing a derivation on finitely many cyclic summands, with strong convergence of the corresponding projections. · OAI.KadisonSimilarity.FiniteColumnImplementers
finiteColumnImplementers_of_summands def: Actual finite-column implementers obtained from implemented restrictions to the summands. Cyclicity is used to obtain the local implementers, not in their assembly. · OAI.KadisonSimilarity.finiteColumnImplementers_of_summands
finiteConstantFiberIso def: The constant-label fibre retains the original finite-dimensional object. · OAI.Thomason.Construction.StrictOmegaCategory.finiteConstantFiberIso
finiteConstantLabel def: A constant label in the finite category, on all cells. · OAI.Thomason.Construction.StrictOmegaCategory.finiteConstantLabel
finiteContraction def: Exact finite center contraction restricted to the occupied set of one literal chord. Vacant wires have the actual spin one; the first boundary arrow is fixed. No orientation coefficient has been supplied as an input. · OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.finiteContraction
finiteCoordinateReflection def: Reflection of the coordinate positions of a finite word. · OAI.WeakPureInfiniteness.finiteCoordinateReflection
FiniteCoordinates def: A common finite family of coordinates determines the whole subspace. · OAI.ExactModuli.KW.FiniteCoordinates
finiteCoordinates def: Polynomial coordinates on the finite chart of the actual constrained rank-three fiber, including its scalar component. · OAI.ElasticityConic.finiteCoordinates
finiteCoordinates def: Restriction to finitely many coordinate values. Its kernel is the particular closed finite-codimensional subspace used for the modulus. · OAI.ForestSpace.finiteCoordinates
finiteCoordinates def: A basis supplies the required coordinates for every finite-dimensional combined advice space; this choice is independent of the equation questions. · OAI.MaxCutGames.Clean.AnswerBridge.finiteCoordinates
finiteCoordinates def: A basis supplies the required coordinates for every finite-dimensional combined advice space; this choice is independent of the equation questions. · OAI.UniqueGamesTheorem.Clean.AnswerBridge.finiteCoordinates
finiteCoordinateState def: Extend a functional on a finite coordinate set by zero outside that set. · OAI.MatrixMultiplication.AuxiliarySeparation.finiteCoordinateState
finiteCoordinateTotalHomeomorph def: The finite-coordinate presentation is the same actual bundle, through an explicit base-preserving linear homeomorphism of total spaces. · OAI.Kaplansky.finiteCoordinateTotalHomeomorph
finiteCoordinateUnitary def: The finite-coordinate change preserves the actual Hermitian metric and the actual total-space topology simultaneously. · OAI.Kaplansky.finiteCoordinateUnitary
finiteCopyIsometry def: Insert a vector into a finite Hilbert coordinate. · OAI.KadisonSimilarity.finiteCopyIsometry
FiniteCorner def: Finiteness of a corner, expressed in the ambient algebra. · OAI.BoundedHochschild.KadisonRingrose.FiniteCorner
FiniteCouniversalStreetWeakEquivalence def: Cobase changes in the actual finite category are Street weak equivalences. · OAI.Thomason.Construction.NormalizedSimplexIdentities.FiniteCouniversalStreetWeakEquivalence
finiteCuntz def: Every positive matrix size is obtained from the same countable matrix units by the quotient-and-remainder bijection. · OAI.KadisonKastler.FullMatrixCorner.finiteCuntz
finiteCuntzCesaro def: Cesàro smoothing of the recursive intertwiner. · OAI.WeakPureInfiniteness.finiteCuntzCesaro
finiteCuntzDiagonalHom def: The diagonal corner sum is a genuine star homomorphism. · OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom
finiteCuntzTransfer def: The finite transfer operator from the family s to the family t. · OAI.WeakPureInfiniteness.finiteCuntzTransfer
finiteCuntzTransferIter def: Iteration is kept explicit to expose the last boundary term. · OAI.WeakPureInfiniteness.finiteCuntzTransferIter
finiteCutMap def: The coordinate function of a vertex in the finite weighted cut space. · OAI.BoundedTreewidthL1.finiteCutMap
finiteDegrees def: Exactly the manuscript's finite interval [-l,0] of Q_T. · OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.finiteDegrees
finiteDensity def: Counting density inside a finite block. · OAI.InfiniteMatroidCounterexample.finiteDensity
finiteDiagonalMap def: Applying a continuous linear map in each coordinate of a finite Hilbert sum. · OAI.KadisonKastler.finiteDiagonalMap
FiniteDiameterCover def: A finite family of sets of pairwise diameter at most the given radius. · OAI.Tingley.FiniteDiameterCover
finiteDimensionalSphereTopHomologyIso def: Top integral sphere homology for any finite-dimensional real normed space, using a chosen linear coordinate system and the recursive sphere normalization. · OAI.Kaplansky.finiteDimensionalSphereTopHomologyIso
FiniteDistinctLawBound def: The exact conclusion needed from source §10's episode amplification, on finite metrics only. This definition is an open obligation, not an assumption asserted by the development, and is not the main theorem. · OAI.KServer.FiniteDistinctLawBound
finiteDNF def: One conjunction for each accepted numerical word. · OAI.TwoPointCorrelations.AC0Circuit.finiteDNF
finiteDual def: On finite arrays this is exactly the coefficient functional in the full dual. · OAI.BoundedTreePotentials.Segments.finiteDual
finiteDynkinPolynomial def: A finite expansion of degree at most c in n input logarithms. · OAI.PolycyclicRecognition.finiteDynkinPolynomial
finiteEmbedding def: Coordinate finite vectors inherit the same exact full-representation infimum. · OAI.DiamondDistortion.PathModel.finiteEmbedding
finiteEmbedding def: The canonical linear embedding, presented on actual finitely supported arrays. · OAI.DiamondDistortion.SegmentSystem.finiteEmbedding
finiteEndFlow def: The polynomial is independent of a norm or coordinates on the algebra. · OAI.PolycyclicRecognition.finiteEndFlow
FiniteEnergy def: Exactly finiteness of the expectation of the nonnegative number operator. · OAI.EntropyPhotonNumber.FiniteEnergy
finiteEnergyDerivative def: First derivative of x R(x), in a form without cancellation at zero. · OAI.InvariantIsing.finiteEnergyDerivative
FiniteEntropyDatum def: The convention 0 |log 0| = 0 is automatic in this real-valued moment. · OAI.BoltzmannNonuniqueness.FiniteEntropyDatum
finiteEvaluation def: Evaluation with bounded finite-dimensional vector-space complexes as its actual target. · OAI.LittleFinitistic.QuadraticEncoding.finiteEvaluation
finiteExpectation def: Exact expectation under the finite law, with n+1 edges. · OAI.FKCRT.finiteExpectation
finiteExpectation def: Expectation with respect to an explicitly supplied finite mass function. · OAI.JointDickman.finiteExpectation
finiteExtension def: Extension by zero from a finite lower subforest. · OAI.ForestSpace.finiteExtension
finiteFactorError def: The total displacement, including the initial injective embedding. · OAI.KadisonKastler.finiteFactorError
FiniteFactorFreeCornerInputs structure: Exact remaining structural inputs for the fixed finite-factor application. Only the free position remains explicit. Stage commutation, source and generated-factor comparison, rounding and diffuse corners are constructed from the faithful … · OAI.KadisonSimilarity.FiniteFactorFreeCornerInputs
FiniteFactorModel structure: The complete finite-factor presentation required for the application. · OAI.KadisonSimilarity.FiniteFactorModel
FiniteFactorPresentation structure: All finite-factor presentation data except the local free position. The represented Hilbert space is bundled to keep the GNS implementation opaque. · OAI.KadisonSimilarity.FiniteFactorPresentation
FiniteFactorProjectionComparison def: The precise finite-factor comparison consequence needed for the chosen corner. This is the trace form of projection comparison: Blackadar, III.1.1.11, together with the faithful finite trace. · OAI.KadisonSimilarity.FiniteFactorProjectionComparison
FiniteFactorPublishedInputs structure: The published specializations used for the finite-factor application. Each field refers to a separately documented published input. · OAI.KadisonKastler.FiniteFactorPublishedInputs
finiteFactorTrace def: A fixed choice of the normalized normal trace, for the subsequent hyperfinite-subfactor construction. · OAI.KadisonSimilarity.finiteFactorTrace
finiteFiberMap def: This is the restriction to full zero fibres of the reflected map itself. · OAI.Thomason.Construction.SieveMap.finiteFiberMap
finiteFourierCoefficient def: A normalized finite Fourier average of one branch coefficient. · OAI.MatrixMultiplication.AuxiliarySeparation.finiteFourierCoefficient
finiteFrameIndexEquiv def: Increasing enumeration identifies a finite rank stratum with Fin n. · OAI.KadisonKastler.finiteFrameIndexEquiv
FiniteFullMatrixCornerData structure: The geometric corner data, including the proved II₁ structure of the initial represented corner. · OAI.KadisonKastler.FiniteFullMatrixCornerData
finiteGammaMeasure def: The iid Gamma law on a finite set of coordinates. · OAI.GammaFPP.finiteGammaMeasure
finiteGammaScaleLikelihood def: Product likelihood for coordinatewise scaling by a. · OAI.GammaFPP.finiteGammaScaleLikelihood
finiteGaussianLogPartition def: The finite-cutoff Gaussian log partition, with arbitrary probability weights and deterministic base energy. In the application the finite state space is a positive-mass restriction of the spin/cascade-leaf prior. · OAI.InvariantIsing.finiteGaussianLogPartition
FiniteGraph structure: A finite graph given by its edge list. Zero couplings can encode missing edges. Edges are indexed separately so parallel edges are counted separately. · OAI.BufferedIsing.FiniteGraph
finiteGroupAverage def: Normalized counting average on bounded functions. · OAI.KadisonKastler.finiteGroupAverage
finiteGroupBimoduleMean def: The finite-group mean, with both module identities. · OAI.KadisonKastler.finiteGroupBimoduleMean
FiniteGroupBlock structure: A block of a finite group algebra over K. The group is allowed to vary over all finite group types in the specified universe. · OAI.Donovan.FiniteGroupBlock
FiniteHasMonoAP def: A literal finite-coloring formulation of the same progression. · OAI.QuantitativeVanDerWaerden.FiniteHasMonoAP
FiniteHead structure: Finite predecessor-closed heads, including the root. · OAI.IndependentProducts.FiniteHead
FiniteHierarchy def: Genuine finitely branching laws at every level, not an altered trial class. · OAI.DilutedSpinGlass.FiniteHierarchy
finiteHilbertMap def: A general completion comparison, using both actual inequalities on c00. No finite dimensionality of the index set is asserted. · OAI.BoundedTreePotentials.finiteHilbertMap
finiteIdeal def: The closed ideal generated by the finite-trace positive elements. · OAI.TraceConeClassification.ExtendedTrace.finiteIdeal
finiteIndexCoarseEquivalence def: Finite-index subgroups are coarsely equivalent to their ambient groups. The coordinate map uses a finite right-coset transversal. · OAI.PolycyclicRecognition.finiteIndexCoarseEquivalence
finiteInduced def: Finite-index unitary induction, using the exact coset cocycle. · OAI.NuclearUltrapower.finiteInduced
FiniteInnerAverage structure: A finite convex average of inner automorphisms of one concrete algebra. · OAI.KadisonKastler.FiniteInnerAverage
finiteInterval def: The walking arrow as an actual strict positive finite category. · OAI.Thomason.Construction.StrictOmegaCategory.finiteInterval
finiteInvariantMean def: The normalized counting mean on a finite group. · OAI.PolycyclicRecognition.finiteInvariantMean
finiteInverse def: Inverse transform for a finite alphabet with positive masses. The value outside positive arguments is irrelevant to the application. · OAI.InvariantIsing.finiteInverse
FiniteIterationControl structure: Only the second normalized jet is needed for the final pair estimate. · OAI.RegularPointCoordinates.FiniteIterationControl
finiteJointCycleCoboundary def: This is the degree-zero cycle coboundary, with its shifted adjoint tail. · OAI.WeakPureInfiniteness.finiteJointCycleCoboundary
FiniteJordanModelUniformization def: Only the finite Jordan models, including their actual sphere chart changes, are needed by the downstream construction. · OAI.CircleDomainRigidity.FiniteJordanModelUniformization
finiteKernelAction def: Integral action of a kernel on a finite space with atom masses μ. · OAI.JointDickman.finiteKernelAction
FiniteKSEntropy def: All finite-partition entropy rates exist and have one finite real upper bound. This spells out sup_P lim_n H(join_{j<n} T^{-j}P)/n < ∞ without choosing a value for limits of nonconvergent sequences. Empty atoms are allowed. · OAI.SmoothObstruction.FiniteKSEntropy
finiteL1Distance def: The usual ℓ₁ distance in finite dimension, not the sup norm on a Pi type. · OAI.TreeEdit.BinaryLower.finiteL1Distance
finiteL2Basis def: The usual basis of the finite sum of scalar l² spaces. · OAI.KadisonKastler.finiteL2Basis
finiteLabelFiber def: A full endpoint fibre as an object of the original finite category. · OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiber
finiteLabelFiberFunctor def: Endpoint fibers of finite strict categories, formed by the same full subcategories of their ambient omega-categories. · OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiberFunctor
finiteLabelFiberMap def: Restriction of a finite-dimensional strict functor to its full fibres. · OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiberMap
FiniteLaw structure: A probability law on a finite sample space, with real-valued masses. · OAI.CoordinateSweeps.FiniteLaw
FiniteLaw structure: A finite conditional path law. Used only for the finite-kernel proof steps. · OAI.DilutedSpinGlass.FiniteLaw
FiniteLaw structure: A finite probability law, retaining real weights for the conditional couplings. Uniform laws are exactly the table match distributions. · OAI.HyperbolicObstruction.FiniteLaw
FiniteLaw structure: Finite probability laws used for the exact statistical transfer. · OAI.TraceReconstruction.FiniteLaw
finiteLaw def: A finite uniform experiment pushed forward by an arbitrary map. · OAI.CubeShuffle.finiteLaw
finiteLength def: Binary word length for the quadratic-width code, with source length (20 * k * k^(20*k))^k. · OAI.TreeEdit.BinaryLower.Parameters.finiteLength
FiniteLevelChain structure: The actual ordered levels of p on K, with zero included. · OAI.ThompsonNonamenability.FiniteLevelChain
finiteLevelUnion def: A finite list may repeat labels: its entries still have independent level parameters. · OAI.CircleDomainRigidity.finiteLevelUnion
finiteLieBracket def: Continuous bilinear realization of the given finite-dimensional bracket. · OAI.PolycyclicRecognition.finiteLieBracket
finiteLift def: The canonical c00 inclusion, used for each of the exact test families. · OAI.BoundedTreePotentials.finiteLift
finiteLineEvaluationHomeomorph def: Simultaneous evaluation trivializes the actual finite sum of dual lines, with the original finite-sum topology and linear fibers. · OAI.Kaplansky.finiteLineEvaluationHomeomorph
finiteLineEvaluationNormalization def: Fiber normalization defined even when the base is not contractible. · OAI.Kaplansky.finiteLineEvaluationNormalization
finiteLineEvaluationRelativeIso def: Relative pair coordinates on the ACTUAL finite sum of hyperplane lines. · OAI.Kaplansky.finiteLineEvaluationRelativeIso
finiteLineFrameRelativeIso def: Relative coordinates of any finite sum with genuine continuous line frames. · OAI.Kaplansky.finiteLineFrameRelativeIso
finiteLineSumCore def: A finite direct sum, with its ordinary vector-bundle topology and finite Hilbert-space fibers. Neither a trivialization nor a trivial bundle is asserted by the fact that the core uses a fixed model fiber. · OAI.Kaplansky.finiteLineSumCore
finiteLineSumFiberEquiv def: The direct sum has the actual line-core fibers as its components. · OAI.Kaplansky.finiteLineSumFiberEquiv
finiteList def: All finite choices below are literal lists. No finset or finite-connectivity decision is used as a computability oracle. · OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.finiteList
finiteLocalAmplification def: Amplification of a finite-dimensional operator by an identity. · OAI.KadisonKastler.finiteLocalAmplification
FiniteMachineHaltingUndecidable def: The standard halting undecidability specialization to finite one-tape machine tables. Correctness is required on every well-formed finite input. · OAI.ForcedComputation.FiniteMachineHaltingUndecidable
finiteMap def: Algebraic inclusion of the prescribed finitely supported vectors. · OAI.SeparableQuotient.NormConstruction.NormingSet.finiteMap
finiteMatrixAmbientEmbedding def: The coordinate finite model, now viewed directly as a matrix of operators on the original Hilbert space. · OAI.KadisonKastler.finiteMatrixAmbientEmbedding
finiteMatrixBlockSwap def: The unitary exchanging two equal finite tensor blocks. · OAI.KadisonKastler.finiteMatrixBlockSwap
finiteMatrixDifferential def: The degree-two Hochschild differential, already amplified to matrices. · OAI.KadisonKastler.finiteMatrixDifferential
finiteMatrixEmbedding def: The concrete finite model embeds by the chosen inner matrix units, with the outer matrix coordinates represented on the Hilbert direct sum. · OAI.KadisonKastler.finiteMatrixEmbedding
FiniteMatrixFactorModel structure: The structural data of a finite type-I factor in its given representation. · OAI.KadisonSimilarity.FiniteMatrixFactorModel
finiteMatrixHaarProbability def: Normalized Haar measure on each actual finite matrix-unitary group. · OAI.KadisonSimilarity.finiteMatrixHaarProbability
FiniteMatrixModel abbrev: The coordinate algebra M_n(M_(j+1)(C)) in the finite-matrix model. · OAI.KadisonKastler.FiniteMatrixModel
finiteMatrixModelTrace def: The normalized trace on the finite-matrix-model coordinate. · OAI.KadisonKastler.finiteMatrixModelTrace
finiteMatrixRepresentation def: The concrete Hilbert-space representation of each nested finite matrix model. · OAI.KadisonKastler.finiteMatrixRepresentation
finiteMatrixScalarSequence def: The same outer scalar matrix is inserted in every finite coordinate. · OAI.KadisonKastler.finiteMatrixScalarSequence
finiteMatrixTestAlgebra def: The norm-closed C-star algebra generated by the entries of one test. · OAI.KadisonSimilarity.finiteMatrixTestAlgebra
FiniteMatrixUltraproduct structure: The represented quotient of the particular finite-matrix sequence. Only its operator-algebra structure and the canonical trace formula are assumed; no independent unitary or controlled representative is a field. · OAI.KadisonKastler.FiniteMatrixUltraproduct
finiteMax def: The maximum of a nonempty finite family of real numbers. · OAI.Problem358.FiniteMaxDerivative.finiteMax
FiniteMcDiarmidInput def: McDiarmid, On the method of bounded differences, Surveys in Combinatorics 1989, Theorem (6.7), pp. 166–167 (proof p. 168), DOI 10.1017/CBO9781107359949.008. The one-sided estimate follows by applying that martingale theorem to the … · OAI.JointDickman.PublishedInputs.FiniteMcDiarmidInput
finiteMean def: Uniform expectation in a finite experiment, kept in the real numbers. · OAI.CubeShuffle.finiteMean
finiteMean def: Uniform average over a nonempty finite set. · OAI.KadisonSimilarity.finiteMean
finiteMeanState def: A literal uniform average over a finite set, as a linear functional on the actual space of bounded real functions. · OAI.PolycyclicRecognition.finiteMeanState
finiteMeasureTest def: Finite intersections, including the empty intersection. · OAI.PolycyclicRecognition.finiteMeasureTest
finiteMetricNeighborhood def: A source metric neighborhood is a right expansion by the finite identity ball. This is the exact finite set used in the boundary estimate. · OAI.PolycyclicRecognition.finiteMetricNeighborhood
finiteMixedOperator def: The finite-dimensional operator with its exact target bidegree. The map is zero when k > a, so no degree-inequality argument is needed. · OAI.Problem335.finiteMixedOperator
finiteMixture def: Literal finite average of empirical pure product tensors, grouped first by histogram and then by independent roots. · OAI.CoordinateSweeps.OrdinaryTensor.finiteMixture
finiteMixtures def: Points represented by probability weights and one point in each member of a finite family of sets. Membership is required even at zero-weight indices. · OAI.Tingley.finiteMixtures
finiteModelQuotientUnitary def: The represented unitary associated with a finite-model lift. · OAI.KadisonKastler.finiteModelQuotientUnitary
finiteModelUnitaryLift def: The actual bounded sequence of finite-matrix representatives. · OAI.KadisonKastler.finiteModelUnitaryLift
FiniteModule structure: Finite-dimensional actual left modules, retaining the scalar compatibility. · OAI.LittleFinitistic.PDMinimal.FiniteModule
finiteName def: Total conversion; membership proofs below establish that every index used by the construction is already below 48, so the remainder changes none. · OAI.MaxCutGames.Reduction.FiniteSource.finiteName
finiteName def: Total conversion; membership proofs below establish that every index used by the construction is already below 48, so the remainder changes none. · OAI.UniqueGamesTheorem.Reduction.FiniteSource.finiteName
finiteNodeSpace def: The actual finite node support, not only finite component support. · OAI.BoundedTreePotentials.ForestCoordinates.finiteNodeSpace
finiteNormEvaluation def: The underlying normed tuple at a prescribed family of arguments. This is a linear map, without a claim of weak-to-norm continuity. · OAI.ReflexiveFixedPoints.finiteNormEvaluation
finiteObjectAdjunction def: The direct adjunction in the actual finite category. · OAI.Thomason.Construction.StrictOmegaCategory.finiteObjectAdjunction
finiteObjectFunctor def: The actual object functor on positive finite strict categories. · OAI.Thomason.Construction.StrictOmegaCategory.finiteObjectFunctor
FiniteObstructionData structure: The specific subconfiguration used by the source obstruction. This is metric input to a contradiction, not an assumed existence assertion. All its conditions are consequences asserted by source Proposition configuration; the … · OAI.HyperbolicObstruction.FiniteObstructionData
finiteOperatorCoefficient def: A finite sum of vector coefficient functionals on bounded operators. · OAI.KadisonKastler.finiteOperatorCoefficient
finiteOperatorTensor def: The finite-dimensional Hilbert tensor representing an operator. · OAI.NuclearUltrapower.finiteOperatorTensor
finiteOptimizerSelection def: The finite rational optimizer: every operation here is rational arithmetic, finite enumeration, or the prescribed finite logarithm sum. · OAI.EditApproximation.finiteOptimizerSelection
finiteOptimum def: The same offline maximum as MatroidProphet.optimum, on an arbitrary finite ground type. The empty independent set is among the competitors. · OAI.MatroidProphet.Labeling.finiteOptimum
finiteOptimum def: The offline benchmark on an arbitrary finite label type. · OAI.MatroidProphet.Relabeling.finiteOptimum
FiniteOrbitAverage structure: A finite probability distribution on acting elements. · OAI.PolycyclicRecognition.FiniteOrbitAverage
finiteOrbitEmbedding def: All group translates, recorded in a finite Euclidean product. · OAI.PolycyclicRecognition.finiteOrbitEmbedding
finiteOrderPosition def: The normalized timestamp lies in the actual finite position set. · OAI.MatroidProphet.Pivots.finiteOrderPosition
FiniteOrthogonalColumns structure: The elementary operator equations supplied by a complete finite system of matrix-unit columns. · OAI.KadisonSimilarity.FiniteOrthogonalColumns
FiniteOuterHead structure: A finite ancestral subset of the disjoint union of the finite-height trees. · OAI.BoundedTreePotentials.FiniteOuterHead
finiteOutputs def: The dense class of representations whose coordinate output is finite. · OAI.DiamondDistortion.StartModel.finiteOutputs
finiteOverFunctor def: The terminal cone stays in the given positive finite dimension. · OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.finiteOverFunctor
finitePacketLaurent def: A literal finite Laurent polynomial in the Koopman orbit of a measurable packet vector. · OAI.ThreeTorus.finitePacketLaurent
finitePacketSpectralMeasure def: The spectral measure is the pushforward of the coefficients' actual energy. · OAI.ThreeTorus.finitePacketSpectralMeasure
finitePart def: Restriction of a sphere probability measure to the complex plane. This is a probability measure when there is no mass at infinity. · OAI.WeakPinned.Bounded.finitePart
FinitePath def: A finite path space. All probability kernels in the bounded auxiliary perturbation construction are finite, conditional on the physical root. · OAI.DilutedSpinGlass.FinitePath
FinitePerimeter def: Finite-perimeter measurable regions, including all null-set modifications. · OAI.CubicTorus.FinitePerimeter
finitePerturbationRow def: Literal B_k in the free group on the finite label set S. · OAI.Generator.finitePerturbationRow
finitePoint def: The zero-dimensional oriental is terminal also in the full finite category. · OAI.Thomason.Construction.FiniteReflectionInput.finitePoint
FinitePolyTime def: Polynomial-time computation with every physical work alphabet finite. · OAI.MetricKMedian.Complexity.FinitePolyTime
finitePortSelector def: A fully executable selector from the explicit bounded address list. · OAI.MaxCutGames.Foundations.PCP.PoweringAddresses.finitePortSelector
finitePortSelector def: A fully executable selector from the explicit bounded address list. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringAddresses.finitePortSelector
finitePosetSubdivisionHomeomorph def: For every finite poset, including the empty one, subdivision retains the actual realization space homeomorphically. · OAI.Thomason.Construction.SubdivisionBarycentric.finitePosetSubdivisionHomeomorph
FinitePositiveVolume structure: Compact Riemannian volume has positive finite mass. The normalization argument below only needs these two facts, and does not assume a volume bound. · OAI.PositiveEinsteinFour.Geometry.FinitePositiveVolume
finitePrimitiveOperator def: The actual finite supported primitive operator, in one fiber. · OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finitePrimitiveOperator
finitePrism def: Compose the omega prism with the finite reflection unit, then descend its source cylinder by the published internal-hom truncation theorem. · OAI.Thomason.Construction.RelativePrismData.finitePrism
finiteProbability def: Event mass for the same finite law. · OAI.JointDickman.finiteProbability
finiteProductDensity def: Actual finite product of the chosen coordinate densities. · OAI.FiniteFactor.CouplingParameters.finiteProductDensity
finiteProductMass def: Product mass on a finite family of coordinate spaces. · OAI.JointDickman.finiteProductMass
finiteProjection def: The projection onto any finite collection of summands. · OAI.KadisonSimilarity.OrthogonalSummandDecomposition.finiteProjection
finiteProjectionBasis def: The finite-dimensional coordinate basis on the rank n stratum. · OAI.KadisonKastler.finiteProjectionBasis
FiniteProjectionIn def: Finiteness of a projection: an isometry with initial projection p and range under p has range exactly p. · OAI.KadisonKastler.FiniteProjectionIn
FiniteProjectiveBimoduleComplex structure: A finite model for tensoring a genuine bimodule complex, with its support and right projectivity proved. · OAI.LittleFinitistic.FiniteProjectiveBimoduleComplex
finitePushMass def: Finite pushforward of a real mass function. · OAI.JointDickman.finitePushMass
finiteQuotientEvaluation def: The fixed quotient Q evaluates directly into bounded finite-dimensional complexes. · OAI.LittleFinitistic.QuadraticEncoding.finiteQuotientEvaluation
FiniteQuotientMoments def: All bounded finite words in the centered coefficient family vanish. · OAI.KadisonSimilarity.FiniteQuotientMoments
finiteQuotientTuple def: The actual quotient group tuple from the varying finite-dimensional family. · OAI.NuclearUltrapower.finiteQuotientTuple
finiteR def: Finite-alphabet R-transform, with its prescribed value at zero. · OAI.InvariantIsing.finiteR
finiteRandomKernel def: A deterministic map with independent uniform finite auxiliary randomness. · OAI.TwoPointCorrelations.finiteRandomKernel
FiniteReflectionInput structure: Intelligent truncation into positive finite dimension. · OAI.Thomason.Construction.FiniteReflectionInput
FiniteRegularPath inductive: A finite expression made from actual compact regular smooth arcs. This records the geometric pieces even when their concatenation has corners. · OAI.ClosedSurfaceR4.FiniteOrderSmoothing.FiniteRegularPath
finiteRelations def: Two finite families of genuine evaluation-kernel relations. Completeness of these (plus the necessary tree-interchange and V relations) is NOT asserted. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.finiteRelations
finiteRepresentationEquivalence def: The presentation equivalence restricts in every finite dimension. · OAI.Thomason.Construction.finiteRepresentationEquivalence
finiteResidual def: The two true terms in the physical residual at truncation order eight. · OAI.ElasticityDistribution.finiteResidual
finiteResolvent def: The Cauchy transform of a finite spectral probability law. · OAI.InvariantIsing.finiteResolvent
finiteResolvent def: A finite resolvent contraction. The strictly positive denominator is retained also at the endpoint zero of the nonunital spectrum. · OAI.TraceConeClassification.ExtendedTrace.finiteResolvent
finiteRightAverage def: The elementary average x ↦ ∑ T(x mᵢ) mᵢ*. · OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage
finiteRightAverage def: Average a linear map by a finite row. · OAI.KadisonKastler.finiteRightAverage
FiniteRoleShape def: A finite ordered-role shape code with at most r children at every vertex. There are no numerical child labels in this type. · OAI.TraceReconstruction.OccupiedParityTree.FiniteRoleShape
finiteRootAction def: The positive contractive action of a finite trace square root. · OAI.TraceConeClassification.ExtendedTrace.finiteRootAction
finiteRowIsometry def: The normalized finite sum. · OAI.WeakPureInfiniteness.finiteRowIsometry
finiteRowRange def: The actual range projection of the finite isometry. · OAI.WeakPureInfiniteness.finiteRowRange
finiteRowShift def: The relative coefficient comparing two rows in a child. · OAI.TreeEdit.BinaryLower.FiniteTree.finiteRowShift
finiteRowWordSum def: The unnormalized sum ∑ |μ|≤m, s_μ r t_μ*. · OAI.WeakPureInfiniteness.finiteRowWordSum
FiniteRun def: The positive convention explicitly excludes a length-zero computation. · OAI.OneWayLiveness.FiniteRun
finiteSamplerBits abbrev: The exact number of independent input bits used by the initialized finite experiment. The physical simulation has additional operation cost. · OAI.ContingencyTables.SmallGraphProfiles.finiteSamplerBits
finiteSecondResolvent def: The second resolvent moment, which controls the derivative of the inverse. · OAI.InvariantIsing.finiteSecondResolvent
finiteSection def: The infimum over the full nested ℓ¹/ℓ² representation space. · OAI.DiamondDistortion.StartModel.finiteSection
finiteSeedDecode def: Total decoding, with an arbitrary fallback on codes outside the encoder range. · OAI.MatroidProphet.finiteSeedDecode
finiteSeedEncode def: A one-hot code retains the entire finite seed, including unused coordinates. · OAI.MatroidProphet.finiteSeedEncode
FiniteSelectionLaw structure: Finite probability coordinates and their retained subsets. · OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw
FiniteSeparatedAt def: Points and line parameters both use the Euclidean metric in this chart. · OAI.Falconer.FiniteSeparatedAt
finiteSet def: Four untwisted elements, together with the root and one half-copy of the acting group. This is an explicitly finitely generated subgroup when Γ is FG. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.finiteSet
finiteSign def: The coordinate signs on the uniform finite Boolean probability space. · OAI.KadisonKastler.finiteSign
finiteSignedGroup def: Its range is a finite subgroup of the ambient unitary group. · OAI.KadisonKastler.FullMatrixCorner.finiteSignedGroup
finiteSignedRepresentation def: The actual ambient representation of the finite signed-permutation group. · OAI.KadisonKastler.FullMatrixCorner.finiteSignedRepresentation
finiteSignLeftCovariance def: Left covariance of the coefficients. · OAI.KadisonKastler.finiteSignLeftCovariance
finiteSignRightCovariance def: Right covariance of the coefficients. · OAI.KadisonKastler.finiteSignRightCovariance
finiteSignSum def: The unnormalized random sum; normalization is introduced after expansion. · OAI.KadisonKastler.finiteSignSum
finiteSmooth def: The finite sum S + S(I-S) + ... + S(I-S)^(n-1). · OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth
finiteSourceLength def: Original word length before the quadratic-width binary conversion. · OAI.TreeEdit.BinaryLower.finiteSourceLength
finiteSquareLeftMul def: Left multiplication preserves the actual square-integrable trace ideal. · OAI.TraceConeClassification.ExtendedTrace.finiteSquareLeftMul
finiteSquareSet def: The two-sided square-integrable ideal, before taking its norm closure. · OAI.TraceConeClassification.ExtendedTrace.finiteSquareSet
finiteStreetNerve def: The same Street nerve on strict finite-dimensional categories. · OAI.Thomason.Construction.NormalizedSimplexIdentities.finiteStreetNerve
finiteSubelement def: A finite-weight subelement of a positive operator in the GNS weak closure. · OAI.TraceConeClassification.ExtendedTrace.finiteSubelement
finiteSubspaceRep def: The honest finite-dimensional subrepresentation on an invariant subspace. · OAI.NuclearUltrapower.finiteSubspaceRep
finiteSwitchRate def: The finite index may comprise a stage and its finite past-measurable pattern. Empty or simultaneous stages contribute zero. · OAI.SLEExactGauge.Multipoint.finiteSwitchRate
finiteTargetKernel def: The intersection only ranges over a finite type of homomorphisms. · OAI.PolycyclicRecognition.finiteTargetKernel
finiteTemperatureFunctional def: An everywhere-defined primitive; at nonnegative temperatures it is exactly the manuscript's finite-spectrum interaction functional. · OAI.InvariantIsing.finiteTemperatureFunctional
FiniteTensor structure: A set-sized presentation of any finite complex coefficient tensor. · OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor
finiteTensorHilbert def: Named bundled coordinates keep all tensor/Hilbert instances shared. · OAI.NuclearUltrapower.finiteTensorHilbert
finiteText def: The unique period-p text determined by the first p letters of v. Fallback values are never used in a valid rule, since there 0 < p < length v. · OAI.Superstring.Counts.finiteText
finiteThirdResolvent def: Third resolvent moment. · OAI.InvariantIsing.finiteThirdResolvent
FiniteTorusAnalyticMeasurability def: The specialization of Kechris, Theorem 21.10, actually needed for finite tuples of circle-valued levels. · OAI.CircleDomainRigidity.FiniteTorusAnalyticMeasurability
finiteTotal def: The signed total tensor complex on a finite interval of the right complex. · OAI.LittleFinitistic.ComplexTensor.finiteTotal
finiteTotalFunctor def: The actual signed finite tensor total is a functor on all input complexes. · OAI.LittleFinitistic.ComplexTensor.finiteTotalFunctor
finiteTotalMap def: Actual tensor total applied to an arbitrary chain map of input complexes. · OAI.LittleFinitistic.ComplexTensor.finiteTotalMap
finiteTotalVariation def: Total variation between two finite real mass functions. · OAI.TwoPointCorrelations.finiteTotalVariation
finiteTowerHilbert def: The finite retained tower embeds into the actual Hilbert direct sum. · OAI.Kaplansky.finiteTowerHilbert
FiniteTraceContraction abbrev: Finite-weight positive strict contractions, with their operator order. · OAI.TraceConeClassification.ExtendedTrace.FiniteTraceContraction
finiteTwirl def: The twirl associated to a finite unitary representation. Its inverse is written using the group, so no adjoint identities are hidden in this definition. · OAI.KadisonSimilarity.finiteTwirl
finiteTwoSplitKernel def: The two-split kernel, expressed without an assumed adjoint theorem. · OAI.JointDickman.finiteTwoSplitKernel
finiteUnderlyingComparison def: Both constructions of evaluation through Q agree by uniqueness of localization. · OAI.LittleFinitistic.QuadraticEncoding.finiteUnderlyingComparison
finiteUniformProbability def: Cardinal-ratio form of the uniform law on a finite sample space. · OAI.LowSpaceSubsetSum.finiteUniformProbability
finiteUnitaryAverage def: Average over the image of a finite unitary representation. · OAI.KadisonKastler.finiteUnitaryAverage
finiteUnitaryHomotopy def: The finite Haar average of the first-variable contracting homotopies. · OAI.BoundedHochschild.KadisonRingrose.finiteUnitaryHomotopy
FiniteUnitaryRep structure: A nonzero finite-dimensional unitary representation. · OAI.NuclearUltrapower.FiniteUnitaryRep
FiniteVector def: Exactly finite-head-supported vectors. For the coordinate models, these are the finite coordinate vectors on the allowed ancestral heads. · OAI.DiamondDistortion.Midpoint.Heads.FiniteVector
FiniteVectorDerived abbrev: The full subcategory of the canonical derived category represented by bounded finite-dimensional complexes. Over a field all its terms are projective. · OAI.LittleFinitistic.QuadraticEncoding.FiniteVectorDerived
FiniteVectorHomotopy abbrev: The concrete bounded homotopy category of finite-dimensional vector spaces. · OAI.LittleFinitistic.QuadraticEncoding.FiniteVectorHomotopy
FiniteVectorTrace def: A finite vector-functional formula, used below for the factor trace. · OAI.KadisonKastler.FiniteVectorTrace
FiniteVerifier structure: Finite test data, with no soundness or complexity assumption. · OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.FiniteVerifier
FiniteVerifier structure: Finite test data, with no soundness or complexity assumption. · OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.FiniteVerifier
FiniteVerticalOrder def: A finite-order bound restricted to a closed vertical strip. · OAI.CubicFirstMoment.FiniteVerticalOrder
finiteWord def: The concrete tree word at an arbitrary node. · OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord
finMatroid def: Relabel all elements, without restricting the matroid or dropping loops. · OAI.MatroidProphet.Labeling.finMatroid
finMean def: The equally weighted mean of a finite family. · OAI.ThompsonNonamenability.finMean
finPresentation def: A fixed presentation automorphism for each finite boundary permutation. · OAI.IntegralCharacterVarieties.SurfaceSurgery.Hurwitz.finPresentation
finSplitLinear def: Standard coordinate splitting, with explicit measure evidence. · OAI.PettyProjection.finSplitLinear
finWeights def: Transport each weight along the inverse of the chosen enumeration. · OAI.MatroidProphet.Labeling.finWeights
First def: A module supported on the first factor of the actual product algebra. · OAI.LittleFinitistic.BlockModule.First
first def: Canonical lower endpoint; no ordering is imposed on segment families. · OAI.DiamondDistortion.Ancestry.first
first def: Projection parses the actual prefix code and explicitly clears its tail. · OAI.ExactQuantumFactoring.BitStackProgram.Procedure.first
first def: Empty has its head on a blank. All other heads read the top. · OAI.Fifths.StOp.first
first def: The actual two core sides of a decoration. · OAI.HyperbolicObstruction.MasterGraph.first
first def: First successful element of a finite, linearly ordered search space. · OAI.KaplanskyCounterexample.Prescription.first
first def: The entire first arrow space inside the encoding algebra. · OAI.LittleFinitistic.EncodingGenerators.first
first def: The exact first endpoint of a comparison against a length-N window in uv. It also includes aligned different-word comparisons when t=0. · OAI.SmoothObstruction.ShiftComparisons.first
first def: A bounded first-admissible search. Its proof gives both success and order; it does not assume a choice primitive in the computational model. · OAI.Superstring.ThreadArray.first
first def: Each cut is the last occurrence of its run; the first occurrence is the partner of the final occurrence of the opposite run. · OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.first
firstAccept def: Read candidates in their given order and return the first eligible value. · OAI.LowSpaceSubsetSum.firstAccept
firstAcceptCoupling def: The bounded marginal ignores the independent eligible backup. The ideal completion uses it precisely on exhaustion of the fresh candidate tuple. · OAI.LowSpaceSubsetSum.firstAcceptCoupling
firstAccepted def: Return the first proposal accepted by the given test, or report exhaustion. · OAI.MaxCutGames.Foundations.CorrelatedSampling.firstAccepted
firstAccepted def: Return the first proposal accepted by the given test, or report exhaustion. · OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.firstAccepted
FirstBlock abbrev: Blocks for the first transfer: none is x, some none is t, and some (some j) is the j-th common product factor. · OAI.Problem346.FirstBlock
firstBlock def: The first ten coordinates in the standard orthogonal decomposition of R²⁰. · OAI.ProjectionCounterexample.firstBlock
firstBlockComparison def: The first actual tensor application is exactly ordinary O tensor Z on the second block. · OAI.LittleFinitistic.OrdinarySimulation.XResolution.firstBlockComparison
firstChild def: Choose one child deterministically from the actual nonempty child law. · OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstChild
firstCoefficientEquiv def: The first branch is literally the common automorphic-section space. · OAI.Nagata.Workers.W10.firstCoefficientEquiv
firstColumnFiberEquiv def: The first coefficient fiber has exactly the source's theta residue indices. · OAI.Nagata.Workers.W10.firstColumnFiberEquiv
firstComponent def: Source's distinguished component: the least prime divisor, not an arbitrary component for which the compiler would need extra advice. · OAI.ExactQuantumFactoring.UniversalSplit.firstComponent
firstCopiesInclusion def: Insert the first n coordinates, with zero in every later coordinate. · OAI.KadisonSimilarity.firstCopiesInclusion
firstCopiesIsometry def: The coordinate insertion preserves the Hilbert norm. · OAI.KadisonSimilarity.firstCopiesIsometry
firstCopiesProjection def: The orthogonal projection onto the first n copies. · OAI.KadisonSimilarity.firstCopiesProjection
firstCore def: The actual first 32 positions of the fixed anchor. · OAI.Problem348.AnchorRigidity.firstCore
firstCutChildTransport def: Child transport from the old negative end to the first vertex of the cut band. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.firstCutChildTransport
FirstCutColumnsCompatible def: Compatibility of column coordinates at the negative endpoint of the cut band. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstCutColumnsCompatible
FirstCutRowsCompatible def: Compatibility of row coordinates at the negative endpoint of the cut band. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstCutRowsCompatible
FirstDefaultAt def: The event that the first default occurs at a specified stage. · OAI.Problem310.CenterRouteExposure.FirstDefaultAt
firstExitSum def: A finite first-exit polynomial on conditionally independent coefficient blocks. · OAI.IndependentProducts.firstExitSum
firstFive def: Restriction to the first five points. · OAI.EuclideanRamsey.NineGeometry.firstFive
firstFrontTime def: First time a scalar progress coordinate reaches the front. · OAI.SLEExactGauge.FirstFrontPassage.firstFrontTime
firstFunctor def: The actual component functor, constructed on every module and map. · OAI.LittleFinitistic.ProductModules.firstFunctor
firstGapParity def: One parity class of the first-gap choices after a fixed offset. · OAI.Paper170.firstGapParity
firstHeightTime def: The first capacity time at which the trace reaches the specified height. · OAI.SLEExactGauge.FirstHeightSupport.firstHeightTime
firstHit def: Probability of a first visit to -1, starting at a nonnegative integer. · OAI.FKCRT.SimpleWalk.firstHit
firstHitWeight def: Probability transition for a finite first-acceptance process. A successful first trial contributes its own mass; a rejected first trial continues with one fewer trial. · OAI.MaxCutGames.Foundations.CorrelatedSampling.firstHitWeight
firstHitWeight def: Probability transition for a finite first-acceptance process. A successful first trial contributes its own mass; a rejected first trial continues with one fewer trial. · OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.firstHitWeight
firstIndex def: Totalized first index; on nonempty predicates this is the ordinary least index. · OAI.FKCRT.CutOutput.firstIndex
firstIndex abbrev: The zeroth index, avoiding modular reduction of a variable-sized Fin. · OAI.ForcedComputation.BoundedSpatialJets.firstIndex
firstInflationComponentEquiv def: Taking the first component of an inflated module recovers the original module. · OAI.LittleFinitistic.ProductModules.firstInflationComponentEquiv
firstInflationComponentIso def: This recovery is natural in every module and linear map. · OAI.LittleFinitistic.ProductModules.firstInflationComponentIso
firstIso def: The source's first-block localization is the actual selected exact inflation. · OAI.LittleFinitistic.SelectedOrdinaryOrbit.firstIso
firstJetSlot def: Slots of the two first and four ordered second coordinate derivatives. · OAI.ClosedSurfaceR4.JetPolynomial.firstJetSlot
firstLabel def: The slot labels after transferring the first k factors out of the t block. · OAI.Problem346.firstLabel
firstLabelCount def: Number of individual factors labelled by a given vector block. · OAI.Problem346.firstLabelCount
firstLetterProjection def: Projection onto the chosen first tensor coordinate and a tail subspace. · OAI.KadisonSimilarity.firstLetterProjection
firstList def: Original ordered labels after the first true boundary, without changing its phase or introducing a new pairing. · OAI.SmoothObstruction.WordHierarchy.firstList
FirstLocalFrameFlag def: The local frames at the first short seam determine the same graded flag. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstLocalFrameFlag
firstLower def: The first branch's lower interval endpoint. · OAI.Nagata.FiniteExponents.firstLower
firstMark def: First marked x-coordinate: k+1 on component zero and 1 on all others. · OAI.Nagata.W04.ReducibleSquare.firstMark
firstMatch def: The scan order is the fixed increasing finite-index order. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.firstMatch
firstMatch def: The scan order is the fixed increasing finite-index order. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.firstMatch
firstModeMass def: The three actual branches, including mode selection and uniform-label masses. · OAI.ExactQuantumFactoring.OrderTrial.firstModeMass
firstMoment def: The unnormalized Euclidean first moment. It is the barycenter for unit volume bodies, the only place where it is used below. · OAI.PettyProjection.firstMoment
firstMomentScaleDerivative def: The derivative of the scale appearing in the first moment. · OAI.CubicFirstMoment.firstMomentScaleDerivative
firstNeighbors def: `firstNeighbors r v` is the finite set of vertices `u` with an outgoing arc `r v u`. It is the manuscript's `N₁⁺(v)`, counting each reached vertex once. · OAI.SeymourSecondNeighborhood.firstNeighbors
FirstNewFrameCoordinates def: The first new port frame has the coordinates of the identified band. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstNewFrameCoordinates
firstOffset def: Offsets are computed in binary; the physical take/drop calls remain bounded by the supplied word on every malformed input. · OAI.ContingencyTables.CompanionMetropolisWordProgram.firstOffset
FirstOldFrameCoordinates def: The old negative port frame has the original named seam coordinates. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstOldFrameCoordinates
firstOnly def: A polynomial-size literal shape check, including the otherwise-unused last word. It does not construct the unknown canonical CRT residue. · OAI.ExactQuantumFactoring.TransitionWords.firstOnly
FirstOrderSplittingOn structure: The first-order conditions of Huang--Huang Definition 2.7, on actual Sobolev components with continuous pointwise representatives. The Hessian condition is obtained on a smaller ball by the published following remark. · OAI.RegularPointCoordinates.FirstOrderSplittingOn
firstPaperWeight def: The first manuscript's actual supported padded-completion weight, with its dimension allowance, padding, threshold and formal capacity. · OAI.ContingencyTables.CompletionCounts.firstPaperWeight
FirstPoint def: The first equation subspace is determined by its occurrence question alone. · OAI.MaxCutGames.Soundness.ZeroInformation.FirstPoint
FirstPoint def: The first equation subspace is determined by its occurrence question alone. · OAI.UniqueGamesTheorem.Soundness.ZeroInformation.FirstPoint
firstPolynomial def: The scalar polynomial at the k-th stage of the first transfer sequence. · OAI.Problem346.firstPolynomial
firstProjectionMap def: The first local Fourier substitution guesses the missing sector. · OAI.MatrixMultiplication.AuxiliarySeparation.firstProjectionMap
firstProjectionMap def: Collapsing the duplicated vertex is exactly the first prism projection. · OAI.Thomason.Construction.PrismBarycentric.firstProjectionMap
firstProper def: A guarded scan. Invalid proposals never change the arithmetic product invariant of the factoring controller. · OAI.ExactQuantumFactoring.firstProper
firstReferenceExpectation def: The first new path is retained along with every old path; all later paths are sampled and summed exactly as in the reference-history expansion. · OAI.DilutedSpinGlass.PrescribedTree.firstReferenceExpectation
firstReturnLevel def: The points of S whose first positive return occurs at time n+1. · OAI.DukePrimeDegree.firstReturnLevel
FirstRow abbrev: A raw row function on ambient first-question coordinates. Restricting it to the equation subspace gives the supplied map Z_B π. · OAI.MaxCutGames.Soundness.ZeroInformation.FirstRow
FirstRow abbrev: A raw row function on ambient first-question coordinates. Restricting it to the equation subspace gives the supplied map Z_B π. · OAI.UniqueGamesTheorem.Soundness.ZeroInformation.FirstRow
firstScaled def: Amplitude of a genuine first derivative, including the cutoff derivative. · OAI.ElasticityBoundaryCutoffParametrix.firstScaled
FirstSeamGrade def: The first short seam uses the grade of the original child index. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstSeamGrade
firstSeparation def: Exactly the source separating-first-hit event in chronological order. · OAI.KServer.PartitionProbabilities.firstSeparation
firstSeparationMap def: The first local Fourier map followed by its integer weight. · OAI.MatrixMultiplication.AuxiliarySeparation.firstSeparationMap
FirstShortSideValuesTrivial def: All side values at the first short seam are the identity. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstShortSideValuesTrivial
firstSourceThetaEquiv def: Low blocks use the exact centered theta multiplier, including the sign. · OAI.Nagata.Workers.W10.firstSourceThetaEquiv
firstSpace def: The actual first central-idempotent summand of an arbitrary product-ring module. · OAI.LittleFinitistic.ProductModules.firstSpace
FirstSpans def: The label is first spanned at this occurrence, and not before it. · OAI.MatroidProphet.MarkedPivots.FirstSpans
firstSuccessEquiv def: Each failed word is represented uniquely by its offset above N; the final accepted word is fixed. · OAI.EditApproximation.firstSuccessEquiv
firstSuccessEvent def: Finite traces with n failed words followed by the specified accepted integer. · OAI.EditApproximation.firstSuccessEvent
firstSumGraph def: Graph coefficient vector for the first block's sum facet. · OAI.ProjectionCounterexample.firstSumGraph
firstSwap def: Adjacent swaps in a fixed left-associated triple. · OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.firstSwap
firstTop def: Child one uses top blocks one and two. Child two uses the remaining top blocks, each once, exactly as in the manuscript's leaf layout. · OAI.LowSpaceSubsetSum.RepresentationSetup.firstTop
firstTor def: First Cartier Tor, as a functor to coherent sheaves ON the divisor. · OAI.ActualCartier.firstTor
firstTor_supported_iso def: The first Tor of a supported layer is its tensor by the conormal sheaf on the divisor. · OAI.ActualCartier.firstTor_supported_iso
firstTor_supported_pushforwardIso def: The first Tor of a supported layer is the ambient ideal line tensor after closed pushforward. Full faithfulness descends this identification to the divisor. · OAI.ActualCartier.firstTor_supported_pushforwardIso
firstTotalIso def: Actual tensor with the off-diagonal complex on a first-block input is the second-block O-total. · OAI.LittleFinitistic.OrdinarySimulation.BlockTensor.firstTotalIso
firstVectors def: Assign vector values to the three kinds of blocks in the first transfer. · OAI.Problem346.firstVectors
firstWeight def: Weight on the first tensor leg, which carries the guessed sector label. · OAI.MatrixMultiplication.AuxiliarySeparation.firstWeight
firstWeight def: No weight is assigned to the common first leg. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.firstWeight
fischer def: Fischer bilinear form on the actual polynomial coefficient module. · OAI.HarmonicCounterexample.Angular.fischer
fischerCore def: The actual polynomial norm is positive definite, not a formal assumed round-space inner product. Its restriction is rotation invariant. · OAI.HarmonicCounterexample.Angular.fischerCore
fischerSpan def: Algebraic span of radius powers times homogeneous harmonics of fixed total degree. · OAI.PettyProjection.Spherical.fischerSpan
Fits def: Every intermediate value fits, not merely the eventual answer. · OAI.ExactQuantumFactoring.NatExpr.Fits
Fits def: Bit length bound (all instances, same constant); not by itself a computability assertion. · OAI.Fifths.Fits
Fits def: The tag and sign checks for an actual normalized type. · OAI.PureTypeSystem.ObservationValues.Fits
Fits def: An explicit bound on all data consumed by an execution. Proving this invariant for an algorithm, rather than assuming its runtime, yields a cost. · OAI.WLIdentification.BoundedWords.Program.Fits
FitsStore def: Space for the contents of the port file itself (not input positions). · OAI.Fifths.FitsStore
fiveTensorMatrix def: Put the two contracted curvature slots into the row/column positions. · OAI.PositiveEinsteinFour.Geometry.fiveTensorMatrix
fiveTermSum def: Constant-length arithmetic formula for summing a degree-four expression. · OAI.ExactQuantumFactoring.OrderTrial.fiveTermSum
Fix abbrev: Ground pointwise stabilizer of a set of labels. · OAI.PartitionConsistency.SupportFilter.Fix
fixed def: Choose once, using the proved native finite-diagram theorem and actual theta. · OAI.LittleFinitistic.SelectedFixedDiagram.fixed
fixed def: The actual fixed submodule for a projector on the first tensor factor. · OAI.LittleFinitistic.TensorProjection.fixed
fixedAdviceSuccess def: The true weighted occurrence/position experiment at fixed visible advice. · OAI.MaxCutGames.Clean.UpperBound.fixedAdviceSuccess
fixedAdviceSuccess def: The true weighted occurrence/position experiment at fixed visible advice. · OAI.UniqueGamesTheorem.Clean.UpperBound.fixedAdviceSuccess
FixedAmplification def: Fixed-amplification proper infiniteness, including the zero element. · OAI.WeakPureInfiniteness.Campaign.FixedAmplification
FixedAngularPrimeExplicitEstimate def: Published fixed-type explicit prime estimate, before any logarithmic saving is deduced. This is the degree-two, nonexceptional case of Kaneko--Thorner Theorem 1.2 with Rajan's fixed-type zero-free region. The displayed second term retains … · OAI.CubicFirstMoment.FixedAngularPrimeExplicitEstimate
fixedBasis def: Replace the row's varying bases by the fixed maximizing cell basis. The original samples, profiles, law and supported affine pair are preserved. · OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow.fixedBasis
fixedBilinear def: Fixing the first factor of a pointwise bilinear product gives a bounded linear map. · OAI.ForcedComputation.BoundedSpatialJets.fixedBilinear
fixedChain def: These choices, too, are made once before any evaluation module Y. · OAI.LittleFinitistic.SelectedChainDiagram.fixedChain
fixedCost def: The fixed term in the layer inequality. · OAI.GeneralMahler.SCal.PA.fixedCost
fixedCycleLabelingsEquiv def: A new fixed point contributes an independent constant label. · OAI.KadisonSimilarity.fixedCycleLabelingsEquiv
fixedDefectClasses def: Morita classes represented by blocks with a defect group isomorphic to P. · OAI.Donovan.fixedDefectClasses
fixedEquiv def: The image of the original vertex projector after tensoring is the actual left vertex. · OAI.LittleFinitistic.BalancedVertexImage.fixedEquiv
fixedEquiv def: The fixed positions in the literal restricted comparison system are exactly this cluster's old fixed or lost-partner occurrences. · OAI.TorsionFreeZeroDivisors.ClusterLocalization.fixedEquiv
FixedFactorPublishedInputs structure: Every field refers to a separately documented published result. There is no stability, preparation or fixed-factor conclusion among these assumptions. · OAI.KadisonKastler.FixedFactorPublishedInputs
fixedFiberRepresentation def: A nonunital ambient field acts unitally on each fixed-coordinate range. · OAI.KadisonKastler.fixedFiberRepresentation
fixedFirst def: The first input is unchanged, including throughout the basis change. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.fixedFirst
fixedFrequencyEnergy def: Squared small Fourier coefficients whose image under a prescribed linear projection is the fixed partial frequency. · OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy
fixedFrequencyEnergy def: Squared small Fourier coefficients whose image under a prescribed linear projection is the fixed partial frequency. · OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy
fixedFunctionalEquivPairFiber def: Every pair in a fixed neighbor fiber has the same functional. · OAI.MaxCutGames.Inverse.KMSBasisComparison.fixedFunctionalEquivPairFiber
fixedFunctionalEquivPairFiber def: Every pair in a fixed neighbor fiber has the same functional. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fixedFunctionalEquivPairFiber
fixedFunctionalFiberMap def: The affine parametrization of a fixed-functional image fiber. · OAI.MaxCutGames.Inverse.KMSBasisComparison.fixedFunctionalFiberMap
fixedFunctionalFiberMap def: The affine parametrization of a fixed-functional image fiber. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fixedFunctionalFiberMap
FixedFunctionalNeighborFiber abbrev: Vectors external to the starting image which give the same updated image. · OAI.MaxCutGames.Inverse.KMSBasisComparison.FixedFunctionalNeighborFiber
FixedFunctionalNeighborFiber abbrev: Vectors external to the starting image which give the same updated image. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.FixedFunctionalNeighborFiber
fixedFunctionalNeighborFiberEquiv def: Exact constant-multiplicity fiber over an updated subspace. · OAI.MaxCutGames.Inverse.KMSBasisComparison.fixedFunctionalNeighborFiberEquiv
fixedFunctionalNeighborFiberEquiv def: Exact constant-multiplicity fiber over an updated subspace. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fixedFunctionalNeighborFiberEquiv
fixedImageEquivSurjection def: The full fixed-image fiber, with its canonical surjective coordinates. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.fixedImageEquivSurjection
fixedImageEquivSurjection def: The full fixed-image fiber, with its canonical surjective coordinates. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.fixedImageEquivSurjection
fixedInternalPathsLift def: A map of internal paths with constant endpoints lands in the actual fixed-endpoint subcomplex. · OAI.Thomason.Construction.fixedInternalPathsLift
fixedInternalPathSubcomplex def: The subcomplex of internal paths having the two specified constant endpoint simplices. · OAI.Thomason.Construction.fixedInternalPathSubcomplex
fixedKernelEquivInjection def: A fixed-kernel fiber is in explicit bijection with injections from the comparison space. This includes the zero-dimensional comparison space. · OAI.MaxCutGames.Inverse.KMSKernelFiberCard.fixedKernelEquivInjection
fixedKernelEquivInjection def: A fixed-kernel fiber is in explicit bijection with injections from the comparison space. This includes the zero-dimensional comparison space. · OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.fixedKernelEquivInjection
fixedKernelEquivQuotientInjection def: Every map with kernel K factors uniquely through an injective quotient map; the inverse sends that quotient map to its composition with K.mkQ. · OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.fixedKernelEquivQuotientInjection
fixedKernelEquivQuotientInjection def: Every map with kernel K factors uniquely through an injective quotient map; the inverse sends that quotient map to its composition with K.mkQ. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.fixedKernelEquivQuotientInjection
fixedLabelAt def: This lookup is fixed by the reduction parameters, not the input graph. · OAI.MaxCutGames.Foundations.PCP.PoweringRowData.fixedLabelAt
fixedLabelAt def: This lookup is fixed by the reduction parameters, not the input graph. · OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.fixedLabelAt
FixedLabels structure: Shared finite label data for a family of partitions. A representative is defined at every code, including unused codes, and preserves each realized label when applied to its encoding. · OAI.MetricEntropyDuality.FixedLabels
FixedLengthBinaryConversion def: Exact polynomial-width code endpoint, including the stronger deficit inequality. · OAI.TreeEdit.FixedLengthBinaryConversion
fixedMapSuccess def: Actual independent weighted occurrence/position draws, at a fixed genuine partner map. table is the product of the identical coordinate laws. · OAI.MaxCutGames.Clean.ActualAdviceBridge.fixedMapSuccess
fixedMapSuccess def: Two private finite answer draws, after receiving the respective actual question and linear row map. Acceptance is equality under the real projection. · OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.fixedMapSuccess
fixedMapSuccess def: Actual independent weighted occurrence/position draws, at a fixed genuine partner map. table is the product of the identical coordinate laws. · OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.fixedMapSuccess
fixedMapSuccess def: Two private finite answer draws, after receiving the respective actual question and linear row map. Acceptance is equality under the real projection. · OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.fixedMapSuccess
FixedMinimumLabelCertificate structure: Finite construction data for one label. The inner_bound field is exactly what the lower-dimensional induction supplies after restricting activity to the lifted family. All remaining fields concern finite choices or offset asymptotics. · OAI.Problem326.Affine.FixedMinimumLabelCertificate
FixedName def: Names literally fixed by one specified subgroup. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.FixedName
FixedPairOrbit abbrev: Third members reachable while fixing both members of the ordered pair. · OAI.SidorenkoCounterexample.FixedPairOrbit
fixedParams def: Ambient linear map, noise occurrence index, scalar linear functional, in exactly the original nested enumeration order. · OAI.MaxCutGames.Reduction.FixedOutcomes.fixedParams
fixedParams def: Ambient linear map, noise occurrence index, scalar linear functional, in exactly the original nested enumeration order. · OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.fixedParams
fixedPathInternalEquiv def: This is an isomorphism of hom sets, not merely a bijection of components. · OAI.Thomason.Construction.fixedPathInternalEquiv
fixedPathInternalIso def: The singular complex of the genuine fixed-endpoint path space is the actual fixed-endpoint subcomplex of the simplicial internal hom. · OAI.Thomason.Construction.fixedPathInternalIso
fixedPathRealization def: An evaluated cylinder with constant endpoints is a continuous family of paths with those endpoints. · OAI.Thomason.Construction.fixedPathRealization
fixedPathResidualPackets def: The residual subset is fixed by the path and stopping levels. It does not depend on the point at which the amplitude is evaluated. · OAI.LipschitzHilbert.AngularGrid.fixedPathResidualPackets
fixedPathToInternal def: Transposing a continuous family of fixed paths lands in the exact fixed-endpoint subcomplex of the singular internal hom. · OAI.Thomason.Construction.fixedPathToInternal
FixedPeriodTuple def: The fixed involved label is a genuine geometric fiber, not an extra analytic hypothesis on the rank kernel. · OAI.TraceReconstruction.FixedPeriodTuple
fixedPointAlgebra def: Fixed points inside M, expressed as the commutant of M' together with the given representation. · OAI.KadisonKastler.fixedPointAlgebra
fixedPointComplement def: A permutation fixing i preserves the complement of i. · OAI.KadisonSimilarity.fixedPointComplement
fixedPointRemainder def: The contraction over all slots except a distinguished fixed point. · OAI.KadisonSimilarity.fixedPointRemainder
fixedPowersProduct def: The fixed lambda product required by the absorption argument. · OAI.KadisonKastler.fixedPowersProduct
fixedScalarToInvariant def: Descending a fixed scalar class changes neither its values nor its norm. · OAI.KadisonKastler.fixedScalarToInvariant
fixedScaleEvent def: The fixed-scale smoothness event in the proof of the joint law. · OAI.JointDickman.fixedScaleEvent
fixedSlotFlatten def: Flatten the remaining rows after fixing the first slot to a pure power. · OAI.Problem346.fixedSlotFlatten
fixedSpareBlock def: A diagonal block sum in a row of partial isometries. · OAI.WeakPureInfiniteness.fixedSpareBlock
fixedSpareCopies def: The zeroth copy is the original corner; all other copies lie inside its fixed complement. No equality between the total range and one is used. · OAI.WeakPureInfiniteness.fixedSpareCopies
fixedSpareMesh def: Equal mesh on a cyclic index set, with its last point strictly below one. · OAI.WeakPureInfiniteness.fixedSpareMesh
fixedSpareProjection def: Complement of the fixed isometry's range. · OAI.WeakPureInfiniteness.fixedSpareProjection
fixedStepLists def: Includes every actual step list of length n, without a simplicity restriction. · OAI.GammaFPP.fixedStepLists
fixedSubsetList def: Fixed-size selections use the corresponding finite sublist generator. · OAI.LowSpaceSubsetSum.fixedSubsetList
fixedSumProgram def: Finite sums used by a fixed local matrix are bounded-depth compositions. · OAI.ContinuumCoulomb.QuantumAlgebraicScalar.fixedSumProgram
fixedSwap abbrev: Use one fixed equality decision so dependent comb induction does not change which decision procedure is stored in a transposition. The permutation is the usual Mathlib transposition. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.fixedSwap
fixedTensorFunctor def: Tensor by a fixed actual right module on every left module. · OAI.LittleFinitistic.BalancedTensor.fixedTensorFunctor
fixedTrailLists def: The probability bound uses only the subfamily with distinct undirected edges. · OAI.GammaFPP.fixedTrailLists
fixedTransportSet def: This actual finite subset of F is fixed before any averaging set. · OAI.ThompsonNonamenability.fixedTransportSet
fixedTrial def: The actual finite sequence depends only on the fixed mean operator. · OAI.ClosedSurfaceR4.FiniteMean.fixedTrial
fixedWalkParameter opaque: Initialized fixed data keep enormous constant powers symbolic in the kernel. The stored equality proves the exact requested parameter; no value is assumed. · OAI.MaxCutGames.Foundations.PCP.RoundTables.fixedWalkParameter
fixedWalkParameter opaque: Initialized fixed data keep enormous constant powers symbolic in the kernel. The stored equality proves the exact requested parameter; no value is assumed. · OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.fixedWalkParameter
FixedWLBound def: Using n+1 includes the zero-order input and is exactly O(n^r) on positive orders. The finite exceptional small orders can be absorbed in the constant. · OAI.ParityWL.Complexity.FixedWLBound
fixedWord def: A point-stabilizer relation: its root copy equals its two half-copies. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.fixedWord
fixSet def: Pointwise stabilizer of a named finite set of sites. · OAI.CoordinateSweeps.SparseDimension.fixSet
fixSetHom def: The complementary symmetric group onto the pointwise stabilizer. · OAI.CoordinateSweeps.SparseDimension.fixSetHom
fixTwo def: The pointwise stabilizer of two sites, used in the sparse dimension bridge. · OAI.CoordinateSweeps.fixTwo
fixTwoHom def: Permutations of the complementary sites, viewed in the two-point stabilizer. · OAI.CoordinateSweeps.SparseDimension.fixTwoHom
fixZeroPermutation def: Extend a permutation of the five noninitial coordinates by fixing zero. · OAI.MUB6.fixZeroPermutation
fkDet def: The invertible-case Fuglede--Kadison determinant. It is used below only for invertible regular operators. · OAI.GroupRingDeterminant.fkDet
fkEdgeWeight def: Independent bond part of the comparison FK weight; the cluster factor is supplied by summing compatible fair cluster colors. · OAI.BufferedIsing.fkEdgeWeight
fkWeight def: Zero-field FK weight with q=2 and p_e=1-exp(-2 K_e). Parallel edges may be retained: the measure after summing them is the measure for the summed parallel coupling. Loops created by contraction do not change components and cancel from … · OAI.BufferedIsing.fkWeight
fkWeight def: Exact decorated finite-map weight from eq:finite-law. · OAI.FKCRT.fkWeight
Flabby def: Extension of ordinary sections over ambient upper sets. · OAI.KLInvariance.MomentGraph.Sheaf.Flabby
Flag structure: A maximal flag in the barycentric subdivision of an integer cube. · OAI.SharpLiebThirring.CubeFlags.Flag
FlagComparison structure: One comparison of flags carrying their named graded fibers. · OAI.IntegralCharacterVarieties.FlagComparison
flagGridSum def: All blocks in a rectangular lower-left prefix. · OAI.IntegralCharacterVarieties.flagGridSum
flagLayer def: The new orthogonal layer appearing between two consecutive stages of a flag. · OAI.LeanBlast.GotsmanLinial.flagLayer
flagPosterior def: Exact orientation law after a report: only invisible bits remain random. · OAI.TraceReconstruction.FiniteLaw.flagPosterior
flagProjection def: The actual orthogonal projection onto a layer of a finite-dimensional flag. · OAI.LeanBlast.GotsmanLinial.flagProjection
flagProjectionMatrix def: Matrix of an actual flag-layer projection in an orthonormal basis. · OAI.LeanBlast.GotsmanLinial.flagProjectionMatrix
Flags abbrev: Self-loop flag, comparison mismatch flag, and second head register. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Flags
Flags abbrev: Self-loop flag, comparison mismatch flag, and second head register. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.Flags
flagWeights def: Flag weights associated to a nonincreasing finite list of coordinates. · OAI.Thomason.Construction.SubdivisionBarycentric.flagWeights
flash def: Avoid a coefficient zero test: uniform word for adding f*src. · OAI.PowerSaving.Slant.flash
Flat def: Flatness is a.e. equality of H¹ representatives. · OAI.Bernoulli.Flat
flat def: A plate distributes the free energy cost over a long range of factors. · OAI.FourierLLogL.Dyadic.Thermal.flat
flatAmplitude def: The manuscript's endpoint-discontinuous coefficient. · OAI.ThreeTorus.flatAmplitude
flatComplex def: The direct sum with its independently recursive signed differential. · OAI.DerivedBar.RecursiveTotal.flatComplex
flatExclusiveKernel def: The local-law profile is independent of the residue coordinate. · OAI.JointDickman.flatExclusiveKernel
flatLeadingMultibar def: Literal finite direct sums, equipped with the independently recursive bar faces. No count differential or derived comparison is used in this definition. · OAI.DerivedBar.flatLeadingMultibar
flatLeadingMultibarIso def: Chain isomorphism distributing all recursive X and leading-D totals. · OAI.DerivedBar.flatLeadingMultibarIso
flatNormalProjection def: Homogeneous extension of an actual test function off the affine normal chart. · OAI.AffineBernstein.flatNormalProjection
flatSamplePairs def: The first block holds first samples and the second block holds second samples. · OAI.PolycyclicRecognition.flatSamplePairs
flatten def: Interpret the split tree as a map from its ordered comb of leaves. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.flatten
flatten def: Flattening retains every original cell and does not change the terminal monoid or any of the limit unions. · OAI.PartitionConsistency.ConservativeMonoids.BlockTower.flatten
flattenBitBlocks def: Flatten bit blocks in the same order as the standard product equivalence Fin m × Fin B ≃ Fin (m*B). · OAI.TwoPointCorrelations.flattenBitBlocks
flattenChainIso def: An actual chain isomorphism flattening every recursive total, with both horizontal and signed vertical differential verified on literal summands. · OAI.DerivedBar.RecursiveTotal.flattenChainIso
flattenedForm abbrev: Compatibility API for the same flattened form, with inferred degrees. · OAI.Problem346.flattenedForm
flattenedSymmetricForm def: A form on symmetric powers, evaluated on products, is multilinear in all of the underlying vector factors. · OAI.Problem346.flattenedSymmetricForm
flattenIso def: Actual degreewise flattening into an ordinary direct sum of nested tensors. The universal property is proved for the recursive totals, not assumed. · OAI.DerivedBar.RecursiveTotal.flattenIso
flattenMatrix def: Flatten a rectangular matrix of blocks, with the block index first. · OAI.Release075.flattenMatrix
flattenOwnedReference def: The actual ownership-fiber union, preserving every original profile and integer site without repetition. · OAI.LipschitzHilbert.SourceLabeledLattice.flattenOwnedReference
flattenReference def: The common reference collection has the original profile bound. Its constant contains no factor counting the source tops. · OAI.LipschitzHilbert.SourceLabeledLattice.flattenReference
flattenTuple def: Flatten a rectangular array using the standard finite product equivalence. · OAI.TalagrandDiscreteConvexity.flattenTuple
flattenWords def: Only a fixed rearrangement of output wires, from tensor grouping to the source's consecutive n-bit fields. No factor search is present. · OAI.ExactQuantumFactoring.PhysicalTree.flattenWords
flatTubeFrame def: In a flat normal chart the final normal coordinate is one, and the transverse column is the fixed negative final basis vector. · OAI.AffineBernstein.flatTubeFrame
fleck def: natural address binary kernel · OAI.PowerSaving.Grove.fleck
flexibleClosing def: A fixed typed closing is flexible exactly when its type is the freshest burger still present. This is a property of the identified word, not of marks. · OAI.FKCRT.Inventory.flexibleClosing
flight def: Euclidean free transport, with the same velocity convention as GLPS. · OAI.BoltzmannNonuniqueness.EuclideanFlight.flight
FlightChain structure: A complete nonsingular billiard trajectory, indexed by its collisions. Flight zero contains the initial time strictly. Both ends of the collision time sequence are unbounded; collisions occur only in open sides, never vertices. These are … · OAI.TriangularBilliards.FlightChain
flip def: Reverse one coordinate of a cube vertex. · OAI.LeanBlast.GotsmanLinial.flip
flip def: Negate precisely the indices in F. · OAI.LowSpaceSubsetSum.flip
flip def: Flip exactly the coordinates belonging to the specified block. · OAI.Paper320.flip
flip def: Flipping any subset of the reference axes is still a count, not an added gate. · OAI.QAC.Count.flip
flip def: Toggle the endpoint chosen in coordinate i. · OAI.SharpLiebThirring.CubeFlags.Flag.flip
flipBit def: The measure-preserving involution that reverses one coordinate. · OAI.TwoPointCorrelations.flipBit
flipCoin def: Flipping one bit is a permutation of the uniform coin space. · OAI.CubeShuffle.QueryTree.flipCoin
flipLinear def: Interchanging a compact continuous-variable slot and a bounded linear slot. · OAI.ElasticityCompact.flipLinear
flipPairing def: Reverse a perfect pairing when the first module is reflexive. This turns the usual chart E' ≃ Dual E into the orientation needed by transpose. · OAI.Problem346.DualEmbedding.flipPairing
flipTables def: Negate exactly the whole tables on the fixed slice, and no other table. · OAI.OptimalMaxCut.TreeCode.flipTables
flipWord def: Complement selected computational bits. · OAI.QAC.flipWord
floorAt def: The literal geometric floor used throughout the source. · OAI.SmoothObstruction.GoodStationary.floorAt
Flow structure: Finite form of the posterior identity of the source. filtered t is the new pre-move posterior at step t+1; post t is the previous post-move measure. The test-function identity is over every old measurable function, not merely on an … · OAI.UniformKServer.PilotEdits.Flow
flow def: Flow to word-length height r, stopping part-way across its unique top shell. · OAI.EilenbergGanea.DescendingCube.Data.flow
flow def: A globally defined linear evolution, not restricted to small coefficients. · OAI.ElasticityODE.flow
FlowInput def: The positive-flow and trimming inputs, with their distinct coefficient B. · OAI.DiamondDistortion.PathApplications.FlowInput
flowLinear def: Actual initial-data linearity, later used for independence of harmonic columns. · OAI.HarmonicCounterexample.LinearODE.flowLinear
flowTimeSlice def: Evaluation at a fixed time is continuous in the topology of uniform convergence on compact sets. · OAI.PolycyclicRecognition.flowTimeSlice
FluidProperties def: Every clause refers to the named prescribed force and its actual Euclidean Navier--Stokes solution. · OAI.ForcedComputation.Balanced.FluidProperties
fluxCoordinates def: Coordinates in the positively oriented orthonormal frame already used by sphereFlux. · OAI.Mahler.fluxCoordinates
fluxPullback def: The actual real coordinate form, with the same ordered slots as eta. · OAI.Mahler.fluxPullback
Fock abbrev: The full, untruncated bosonic Fock space ℓ²(ℕⁿ, ℂ). · OAI.EntropyPhotonNumber.Fock
fockBasis def: The normalized monomials form a basis, by rescaling the monomial basis with nonzero coefficients. · OAI.Problem335.fockBasis
fockMonomial def: A factorial-normalized real monomial, the algebraic part of the Bargmann--Fock basis used in the moment calculation. · OAI.Problem335.fockMonomial
Focus structure: A focus with distinct arm colors. The arms have length k - 1, and adding their common next point would give a progression of length k. · OAI.QuantitativeVanDerWaerden.Focus
focus def: Inlining carries an inner tuple regenerated from q and the piece o. · OAI.ExactDerandomization.Relay.Cog.focus
focus def: Expose any literal word block while retaining all other blocks, in order. · OAI.TorsionFreeZeroDivisors.WordBlocks.focus
focusSize def: The inner recursion, with the bound for the preceding length supplied. · OAI.QuantitativeVanDerWaerden.focusSize
fold def: Tensor leaf decorations along the literal coloured tree. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.fold
foldAt def: Free boundary cancellation lands in a new actual genus-zero diagram, retaining every interior relator face, with all repeated side indices intact. · OAI.HyperbolicObstruction.WordPictures.WordPicture.foldAt
foldBits def: Fold a variable Boolean word. The bound covers every actual intermediate state; all pairing, data movement and loop iterations are charged. · OAI.ExactQuantumFactoring.BitStackProgram.Procedure.foldBits
foldedAnswer def: One stored bit and one explicit sign correction for every queried table. · OAI.MaxCutGames.Foundations.Hastad.foldedAnswer
foldedAnswer def: One stored bit and one explicit sign correction for every queried table. · OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer
Folk inductive: Arithmetic library with distinguished variable leaves · OAI.ExactDerandomization.Aurora.Folk
FollandMoments structure: Finite angular moment identities. · OAI.PositiveEinsteinFour.Angular.FollandMoments
followPath def: Query just the switches on one actual butterfly route, then pass its endpoint to a continuation. The index map permits parallel sub-butterflies. · OAI.CubeShuffle.QueryTree.followPath
Follows def: The listed distinct edges constitute a whole rotation cycle. · OAI.KaplanskyCounterexample.Planar.Follows
foot def: The initial spatial coordinate of the characteristic passing through (t,z). · OAI.BoltzmannNonuniqueness.AxialFlow.foot
footprint def: Forget only the local allocation/work certificates, preserving the exact trace. · OAI.EditApproximation.BitQuery.Heap.footprint
footprint def: A conservative flat-cell accounting for the two raw-leaf arrays and the mutable tournament, including its cached indexed occurrence and cursor. · OAI.LowSpaceSubsetSum.RepresentationPairData.footprint
footprint def: Two current readers, two replay snapshots, and a mutable tie buffer; dictionary masks and trie links are accounted for separately. · OAI.LowSpaceSubsetSum.RepresentationParentData.footprint
footprint def: Every cursor and cached front occupies a constant number of flat cells. · OAI.LowSpaceSubsetSum.SumReader.footprint
forbidden def: A compact forbidden set for a vertex disk: other vertices and the parts of every drawn edge that must stay outside that disk. · OAI.PlanarL1.Topology.Drawing.forbidden
forbidden def: Excluding an undirected edge means excluding both of its darts. · OAI.TorsionFreeZeroDivisors.ShortClosure.forbidden
ForbiddenConfiguration def: The finite-graph obstruction excluded by system-wide weak normalization. It is not an extra hypothesis on the normalization theorem. · OAI.PureTypeSystem.ForbiddenConfiguration
Force def: Formula-by-formula forcing: existential forcing is local density, NOT a maximum principle or selection of a single global witness name. · OAI.PartitionConsistency.ForcingQuotient.AtomicData.Force
Forced inductive: The actual binary selection sits inside an arbitrary occupied parity term, retaining its unselected children rather than assuming binary input. · OAI.TraceReconstruction.OccupiedParityTree.Forced
forcedAvailability def: The principal-filter availability ideal, built from the already proved intersection/descent calculus. Its definition assumes no stability. · OAI.PartitionConsistency.ProductForcing.forcedAvailability
ForcedAvailable def: Availability when only equality forced by d is used. Each witness is an actual normalized name on the required subdiagram. · OAI.PartitionConsistency.ProductForcing.ForcedAvailable
forcedMode def: All correction depths preserve the same compact support. · OAI.ClosedSurfaceR4.SmallModes.forcedMode
forcedWindowLabels def: A role-selected forced subtree remembers the actual complete-tree labels, not merely its abstract binary shape. · OAI.TraceReconstruction.forcedWindowLabels
ForceFormula def: Forcing in the full syntax of the statement is the previously defined Boolean/existential-basis forcing, with no change of quantifier domain. · OAI.PartitionConsistency.ForcingQuotient.AtomicData.ForceFormula
forceList def: Force a finite list of coin requirements; compatibility with previous ordinary or forced queries is handled by memo. · OAI.CubeShuffle.QueryTree.forceList
Forces abbrev: Named formula forcing in this symmetric system. Quantifiers range over all HS names; the existential clause remains density of local witnesses. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Forces
ForcesBits def: Fixing every bit in c to its value in x forces the event A. · OAI.PlanarFPP.ForcesBits
forcingPath def: The actual affine forcing path in the scalar variation-of-constants equation. · OAI.ForcedComputation.PlaneScalarMild.forcingPath
ford def: Recursively mixed-radix → one-dimensional index. · OAI.PowerSaving.Grove.ford
FordComparisonParameters def: The cutoff and size restrictions of Ford's published lemma. · OAI.TotientAsymptotic.FordComparisonParameters
FordLemma26Input def: The precise published exceptional-prime estimate, at integer endpoints. · OAI.TotientAsymptotic.FordLemma26Input
fordPositiveBandCondition def: Theorem 10 is used only on positive coordinates, where the indicated prime exists and its raw and clamped double logarithms agree. Missing or nonpositive coordinates are handled separately by Theorem 16. · OAI.TotientAsymptotic.fordPositiveBandCondition
fordPrime def: Prime factors with multiplicity, largest first, padded by 1. · OAI.TotientAsymptotic.fordPrime
FordScaleBounds def: Ford's counting-scale bounds, with constants independent of the endpoint. · OAI.TotientAsymptotic.FordScaleBounds
fordSimplexCondition def: The needed consequence of membership in Ford's S_L(xi). It retains the last adjacent inequality with coefficient 1 and coordinate ordering. · OAI.TotientAsymptotic.fordSimplexCondition
FordTheorem10Input def: Ford Theorem 10(a),(b), restricted to positive coordinates, the indices and the errors needed here. This does not assign a value to the raw double logarithm of a missing prime. The endpoint i=m is omitted because the application uses … · OAI.TotientAsymptotic.FordTheorem10Input
FordTheorem16Input def: Ford Theorem 16, with its uniform exp(-Psi^2/4) exceptional-value bound. · OAI.TotientAsymptotic.FordTheorem16Input
FordUpperSieveInput def: Ford 2023, Theorem 2.4, specialized to a finite nonnegative population. The constant is independent of the population, events, densities and bound. The parameter M is the main-term mass X in the source; its difference from the actual … · OAI.JointDickman.PublishedInputs.FordUpperSieveInput
forestBits def: Prefix encoding of a typed plane forest in binary-tree representation. · OAI.TwoPointCorrelations.forestBits
ForestCoord abbrev: Finite disjoint forest, one positive-height rooted tree per component. · OAI.DiamondDistortion.RecursiveModel.ForestCoord
forestCost def: Nonnegative forest aggregation, with components indexed by root-inclusive heights n+1. · OAI.BoundedTreePotentials.Segments.forestCost
forestEdges def: Kruskal's spanning forest, retaining literal paired-side indices. · OAI.HyperbolicObstruction.PictureSwitch.forestEdges
ForestHead def: Finite heads are componentwise ancestor closed; a used component includes its original root. There is no joined free root in this index type. · OAI.DiamondDistortion.RecursiveModel.ForestHead
forestIndexEquiv def: The finite index of a vertex is its first occurrence in preorder. · OAI.TwoPointCorrelations.forestIndexEquiv
ForestOrder def: Every ancestral cone is a chain, the order-theoretic forest condition. · OAI.ForestSpace.ForestOrder
ForestPathData structure: A finite realization of the regular segments in one column. · OAI.TwoPointCorrelations.ForestPathData
forestPathDataOfRepresentation def: Relabeling by Fin changes no forest index. The graph, walks, and non-reversal proofs are transported rather than postulated. · OAI.TwoPointCorrelations.forestPathDataOfRepresentation
forestPerfectName def: Omitted classes use bounded occurrence indices. Regular classes use exactly the line-vertex numbers shared across the path family. · OAI.TwoPointCorrelations.forestPerfectName
forestShapeEquiv def: This identification uses only the shape and the two preorder enumerations. · OAI.TwoPointCorrelations.forestShapeEquiv
forge def: local root and dimension table. · OAI.PowerSaving.RAM.Bench.forge
forget def: Forget deck coordinates but not a single dart or face. · OAI.HyperbolicObstruction.PictureSwitch.WalkCellCover.forget
forget def: Forget the degree bounds in the affine representation of binary forms. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget
forgetBimoduleComplex def: Forgetting the retained left action recovers the verified ordinary finite resolution. · OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetBimoduleComplex
forgetCompletion def: The literal source's forget-completion morphism. · OAI.SourceConeMorphism.forgetCompletion
forgetEquiv def: Forgetting the outside action gives exactly the previous balanced tensor term. · OAI.LittleFinitistic.BimoduleComplexTensor.forgetEquiv
forgetIntegerBimoduleComplex def: Every integer term and differential agrees after forgetting the left action. · OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetIntegerBimoduleComplex
forgetIso def: Forgetting the two outside actions gives the actual coordinate direct-sum complex. · OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.forgetIso
forgetLift def: Forgetting group coordinates keeps every dart, incidence, boundary and planar component. The metric labels can therefore be tracked through reduction. · OAI.Release075.TriangleFilling.forgetLift
forgetRight def: Restrict genuine bimodules to right B-modules. · OAI.ExternalTensor.Section4.forgetRight
forgetTotalFunctorIso def: The forgetful chain comparison is natural in all input complexes. · OAI.LittleFinitistic.BimoduleComplexTensor.forgetTotalFunctorIso
forgetTotalIso def: The genuine outside-action total forgets to the actual previously verified k-total. · OAI.LittleFinitistic.BimoduleComplexTensor.forgetTotalIso
Fork structure: Binary choices, left/right normalized. · OAI.FourierLLogL.Dyadic.Procedure.Fork
fork def: k paths with a common d-coordinate prefix, no contracted unary levels. · OAI.DilutedSpinGlass.PrescribedTree.fork
forkAt def: Two independent branches at the designated physical height; all other levels are unary. The height stays fixed, avoiding transports of spin paths. · OAI.DilutedSpinGlass.PrescribedTree.forkAt
forkLoop def: Drain one tape into two reverse-order accumulators. · OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkLoop
forkLoop def: Drain one tape into two reverse-order accumulators. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkLoop
forkOverlap def: The complete overlap in one of two conditionally independent descendants of an actually sampled stem. · OAI.DilutedSpinGlass.PrescribedTree.forkOverlap
Form abbrev: coefficient form. Throughout, nonnegativity of the coefficients means 0 ≤ A. · OAI.FourierLLogL.Dyadic.Thermal.Form
formalityIso def: Every bounded complex of vector spaces is isomorphic to its homology with zero differential. · OAI.LittleFinitistic.VectorComplexFormality.formalityIso
formalityMap def: Choose cycle representatives for each homology vector space. · OAI.LittleFinitistic.VectorComplexFormality.formalityMap
formCoordinateEquiv def: The coordinate action corresponding to a change of basis of a form. · OAI.SidorenkoCounterexample.formCoordinateEquiv
formDimension def: The number of multisets of j basis vectors chosen from r vectors. · OAI.MetricEntropyDuality.formDimension
Formed inductive: A path certificate retaining exactly its terminals, witness types and edge roles. Inclusion is a literal identity; there is no type-level cast. · OAI.PureTypeSystem.Labelled.ProofWrapper.Formed
formFlux def: The signed coordinate coefficient of an n-form in dimension n+1. · OAI.EilenbergGanea.formFlux
formGraph def: The graph over a subspace, with its free vertical annihilator retained. · OAI.SidorenkoCounterexample.formGraph
formGroundEnergy def: The same full fermionic bottom for real positions, prior to rationalization. · OAI.ContinuumCoulomb.formGroundEnergy
FormOrbit abbrev: The congruence orbit of the literal form, not merely its rank stratum. · OAI.SidorenkoCounterexample.FormOrbit
FormPair abbrev: Affine representatives of forms linear in the second pair of variables. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair
formRadicalEquiv def: Symmetric forms whose radical contains a prescribed subspace descend bijectively to the quotient. This keeps the actual radical condition. · OAI.SidorenkoCounterexample.formRadicalEquiv
formRootWeight def: The product of the weights of all forms vanishing at a residue. · OAI.JointDickman.formRootWeight
FormState abbrev: Every normalized state ranges over the full weak H¹ fermionic space. · OAI.ContinuumCoulomb.FormState
Formula structure: An ordinary conjunction of three-slot clauses with sparse variable names. Repeated names and repeated literals are permitted in every clause. · OAI.MaxCutGames.BinaryFormula.Formula
Formula structure: A finite conjunction of clauses with exactly three literal slots each. Repeated «variables» and repeated literals are allowed. · OAI.MaxCutGames.Foundations.Target.Formula
Formula inductive: Pure first-order membership syntax with equality. n variables are in scope. A quantifier binds the last variable in its body. There are no atoms/urelements, function symbols, constants, semantic predicates, or mathematical assumptions in … · OAI.PartitionConsistency.Formula
Formula abbrev: Exactly three literals per clause; repetitions are permitted. · OAI.UniformSparsestCut.Formula
Formula structure: An ordinary conjunction of three-slot clauses with sparse variable names. Repeated names and repeated literals are permitted in every clause. · OAI.UniqueGamesTheorem.BinaryFormula.Formula
Formula structure: A finite conjunction of clauses with exactly three literal slots each. Repeated variables and repeated literals are allowed. · OAI.UniqueGamesTheorem.Foundations.Target.Formula
formula def: The manuscript's recursive named formulas, on the whole metric component. · OAI.PlanarL1.Columns.Model.Point.RadialTree.formula
formulaInTime def: Formula headers supply the operand bounds for the actual transition count. · OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.formulaInTime
formulaInTime def: Formula headers supply the operand bounds for the actual transition count. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.formulaInTime
forNat def: Fold counting up. · OAI.ExactDerandomization.Counter.forNat
ForRank def: Additional conservation on the same concrete ranked program. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.ForRank
forward def: The actual forward associativity map of balanced tensors. · OAI.LittleFinitistic.BalancedAssociativity.forward
forward def: Quotient map from the detector tensor to the actual left D-linear bar quotient. · OAI.LittleFinitistic.PDBarQuotient.forward
forward def: Induced logical actions. · OAI.PowerSaving.Cluster.forward
forward def: The finite forward Green solution; no division by a spectral gap. · OAI.SmoothObstruction.FiniteShears.forward
forward def: Substitution F ↦ L, J ↦ N, fixing the other four generators. · OAI.StableCoordinate.Linearization.forward
forward def: Forward rotations carry the usual lexicographic order, not a coordinatewise order on streams. · OAI.Superstring.Hierarchical.forward
forwardAt def: Reassociate a fixed last input through the actual A-balanced quotient. · OAI.LittleFinitistic.BalancedAssociativity.forwardAt
ForwardDart def: Choosing only the forward dart avoids treating the two independently supplied oriented parametrizations as one geometric edge. · OAI.PlanarL1.Topology.ForwardDart
forwardDifference def: Iterated forward differences, with the shifts in list order. · OAI.Problem337.forwardDifference
forwardExit def: The rational definition makes joint measurability independent of coordinates on the direction-dependent transverse hyperplanes. · OAI.HenonLaneEmden.LineComponents.forwardExit
forwardIntegerHistory def: The actual node equations use the fixed nonbulk factor and the current giant on each child. The support includes both coefficient unit conditions. · OAI.Ostmann.forwardIntegerHistory
forwardMatrix def: The forward matrix before division by t-M. · OAI.DefocusingNLS.forwardMatrix
ForwardProhibited def: Exact numerical prohibition, with admissible tuple/padding pairs fixed. · OAI.TwoPointCorrelations.ForwardProhibited
forwardQuotient def: Forward difference quotient with step h. · OAI.Problem358.forwardQuotient
forwardRanks def: Reversal changes germ endpoint directions, not any fiber/refinement data. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.forwardRanks
forwardSpace def: Spaces of the genuine long-window gauge in its original endpoint chart. · OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.forwardSpace
foulkesIndexEquiv def: Reindex the slots in a transposed grid, allowing an independent permutation in each original row. · OAI.Problem346.foulkesIndexEquiv
foulkesMultilinear def: The canonical Foulkes--Howe expression is multilinear in its a * b individual vector arguments. · OAI.Problem346.foulkesMultilinear
foulkesOneEquiv def: The canonical Foulkes--Howe equivalence when the inner degree is one. · OAI.Problem346.foulkesOneEquiv
foulkesRowFormSpanning def: Hold all but a single input row of the Foulkes formula fixed. · OAI.Problem346.foulkesRowFormSpanning
foulkesSummandMultilinear def: A summand of the Foulkes--Howe formula, viewed as a multilinear map in all entries of the input grid. · OAI.Problem346.foulkesSummandMultilinear
Foundry structure: readiness via explicit finite tables · OAI.PowerSaving.RAM.Bench.Foundry
four def: The four ordered outer branches associated with two local families. · OAI.Problem356.CommonBranches.four
fourBoundedTree def: Shift by the fixed nonroot vertex [0], so the rootless row also starts at a nonzero path. No root coefficient is inserted in that row. · OAI.BoundedTreePotentials.TreeCalculus.fourBoundedTree
fourCoefficient def: One layer's four factors in the second trace. · OAI.Problem335.LocalMoments.fourCoefficient
fourCycle def: A nonnegative four-cycle is again a table with precisely the same margins. · OAI.ContingencyTables.fourCycle
fourCycleInt def: The signed four-cycle update, before converting back to natural entries. · OAI.ContingencyTables.fourCycleInt
fourFieldsInTime def: Four fields are separated by actual finite-stack transitions. The stated bound is exactly their serialized length plus four delimiter-seeding steps. · OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fourFieldsInTime
fourFieldsInTime def: Four fields are separated by actual finite-stack transitions. The stated bound is exactly their serialized length plus four delimiter-seeding steps. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fourFieldsInTime
fourfoldIndexEquiv def: The common enumeration of the three finite indices. · OAI.KadisonSimilarity.fourfoldIndexEquiv
fourfoldMatrixFlatten def: The four-by-four dilation's flattened matrix has size 4 * n. · OAI.KadisonSimilarity.fourfoldMatrixFlatten
fourier def: Fourier transformation with kernel exp (-2πi⟪x, ξ⟫). · OAI.SharpPlanar.fourier
fourierAbsolute def: Replace each ℓ² coordinate by its nonnegative norm, embedded in ℂ. · OAI.DefocusingNLS.fourierAbsolute
fourierCoeff def: Uniformly normalized complex Fourier coefficient. · OAI.MaxCutGames.Fourier.MatrixFourier.fourierCoeff
fourierCoeff def: Uniformly normalized complex Fourier coefficient. · OAI.UniqueGamesTheorem.Fourier.MatrixFourier.fourierCoeff
fourierConjugate def: Conjugating a torus function conjugates its coefficients and reverses frequency. · OAI.DefocusingNLS.fourierConjugate
fourierContraction def: A bounded Fourier multiplier of norm at most one. · OAI.DefocusingNLS.fourierContraction
fourierConvolution def: Discrete convolution, formed as an ℓ²-valued absolutely convergent series. · OAI.DefocusingNLS.fourierConvolution
fourierEuclideanSpace def: Fourier degree filtration in the Hilbert space with counting inner product. · OAI.LeanBlast.GotsmanLinial.fourierEuclideanSpace
fourierFlag def: Shift the degree filtration so that its zeroth member is bottom. · OAI.LeanBlast.GotsmanLinial.fourierFlag
fourierFrequencySet def: The positive frequencies required by the discrepancy stage. · OAI.Problem337.RandomProducts.fourierFrequencySet
FourierGap def: A measure with Fourier support in the open interval (-gap/4,gap/4) annihilates all the moments specified in this condition. · OAI.LipschitzHilbert.PhaseCombinatorics.FourierGap
fourierGaussianLaw def: The standard independent complex Gaussian Fourier coefficients. · OAI.DefocusingNLS.fourierGaussianLaw
fourierPolynomialFactor def: Concrete clipped factor for the Fourier weight on its declared M/X range. · OAI.Ostmann.fourierPolynomialFactor
fourierResponse def: Squared Fourier coefficients select a mask; a uniform support coordinate selects the actual answer. Both stages use only this player's private table. · OAI.MaxCutGames.Foundations.Hastad.fourierResponse
fourierResponse def: Squared Fourier coefficients select a mask; a uniform support coordinate selects the actual answer. Both stages use only this player's private table. · OAI.UniqueGamesTheorem.Foundations.Hastad.fourierResponse
fourierSpace def: Functions of Fourier degree at most k. · OAI.LeanBlast.GotsmanLinial.fourierSpace
fourierSpaceFrom def: Functions whose Walsh support starts in degree k. · OAI.LeanBlast.GotsmanLinial.fourierSpaceFrom
fourierSquare def: The nonnegative physical-space averaging density before normalization. · OAI.LipschitzHilbert.fourierSquare
fourierTranslateVector def: A Fourier vector with its indices shifted by m. · OAI.DefocusingNLS.fourierTranslateVector
fourierTranslation def: Translation of Fourier indices is a complex-linear isometry. · OAI.DefocusingNLS.fourierTranslation
fourShearPotential def: The four successive polynomial Hamiltonians have reciprocal-diagonal composition. This avoids logarithms in a finite effective force program. · OAI.ForcedComputation.PlanarHamiltonian.fourShearPotential
fourthMomentConstant def: The constant after the genuine mixed-energy estimate and A5 aggregation. · OAI.MaxCutGames.Inverse.KMSMomentConstants.fourthMomentConstant
fourthMomentConstant def: The constant after the genuine mixed-energy estimate and A5 aggregation. · OAI.UniqueGamesTheorem.Inverse.KMSMomentConstants.fourthMomentConstant
FourWordValid def: 0 is the outsider and 1,2 the two diagonal states. · OAI.EuclideanFiveColor.FourWordValid
fp def: A convenient rational-logarithmic expression for f'. · OAI.Bernoulli.DeSilvaJerison.fp
fractionalCut def: Expected cut weight under independent randomized rounding. · OAI.OptimalMaxCut.Unweighted.fractionalCut
fractionalMassFamily def: The actual normalized probability masses attached to family members. · OAI.TalagrandThreshold.fractionalMassFamily
fractionArith def: Extra work registers for retaining numerator and denominator through Euclid. · OAI.RationalHitting.StackLanguage.fractionArith
fractionChartAwayEquiv def: Each genuine section-fraction chart is unchanged over the source principal open where its selected section is invertible. · OAI.ReesProj.fractionChartAwayEquiv
fractionReduce def: Euclid followed by two binary divisions, destructively producing the coprime numerator and positive denominator magnitudes. · OAI.RationalHitting.StackLanguage.fractionReduce
fractionSign def: Registers 12 and 13 hold signed-magnitude signs; 15 stores the canonical result's sign and remains disjoint from the twelve arithmetic registers. · OAI.RationalHitting.StackLanguage.fractionSign
fractionValuation def: Extend a valuation that is finite on nonzero elements to the fraction field. · OAI.CartierSections.fractionValuation
Frag structure: Building block with bounded fourth-root Lipschitz norm and bounded sensitivity range. The constants here need not be the algorithmic clamp coefficients. · OAI.ExactDerandomization.Analysis.Frag
FragmentData structure: Per-fan normal link data, all indexed sides, and elementary side counts of an actual fragment. No filling or area inequality is a field of this structure. · OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData
Frame abbrev: The interval input together with accuracy and dimension allowances. · OAI.ContingencyTables.BinVectorProgram.Frame
Frame abbrev: Finite orthonormal frames; the zero-dimensional case is included. · OAI.SmoothObstruction.QR.Frame
Frame structure: A frame for the rank-one bundle underlying the determinant presentation. · OAI.StableCoordinate.FrameLift.Frame
frame def: `frame` encodes each payload bit as `false` followed by that bit, then terminates the framed list with `true`. · OAI.CurrentKS.frame
frame def: Escaped binary words. · OAI.CurrentKS.frame
frame def: Changing frames never alters the old edge transport. · OAI.IntegralCharacterVarieties.DiskGauge.frame
frame def: Binary framing: true,b for a payload bit and false as terminator. · OAI.LargeIndependentSets.frame
frame def: Prefix-free framing on the two-symbol input alphabet. · OAI.MaxCutGames.BinaryEncoding.frame
frame def: All permanent input fields and fixed Horner digits are explicit tape words. The argument is the forward-order emitted already emitted. · OAI.MaxCutGames.Explicit.MachineProductHeaders.frame
frame def: These are mathematical descriptions of the physical stacks at loop boundaries. They are never loaded into the machine's finite control. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.frame
frame def: The exact diagonal frame used to normalize triangular products. · OAI.PolycyclicRecognition.PositiveTriangular.frame
frame def: Basis independent frame from projection. · OAI.PowerSaving.Binary.frame
frame def: The selected anchor representatives use the same row/column seed in every anchor group. This correlation does not affect the cellwise sampling proof. · OAI.Problem348.Construction.SampledSelection.frame
frame def: One selected representative from each anchor group of a fixed mode. · OAI.Problem348.Construction.SelectedAnchor.frame
frame def: Prefix-free framing on the two-symbol input alphabet. · OAI.UniqueGamesTheorem.BinaryEncoding.frame
frame def: All permanent input fields and fixed Horner digits are explicit tape words. The argument is the forward-order emitted already emitted. · OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.frame
frame def: These are mathematical descriptions of the physical stacks at loop boundaries. They are never loaded into the machine's finite control. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.frame
frameAbove def: A choice of determinant-one frame above a quadric point. · OAI.StableCoordinate.QuadricFactorization.frameAbove
frameAt def: Use the same exact dyadic frames already furnished by the construction. · OAI.RegularPointCoordinates.RegularBilinearData.frameAt
FrameBound def: The synthesis operator bound on subfamily coordinate spaces, including the empty subfamily. · OAI.Dixmier.FiniteSynthesis.FrameBound
frameChartMatrix def: Components of an actual frame in the fixed chart at c. · OAI.PositiveEinsteinFour.Geometry.frameChartMatrix
FrameChosen structure: A selected anchor frame, considered only as a family of protected positions. · OAI.Problem348.Construction.HostSampling.FrameChosen
frameContents def: Complete explicit tape contents; all three scratch roles omitted here are empty. · OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frameContents
frameContents def: Complete explicit tape contents; all three scratch roles omitted here are empty. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frameContents
frameCurvature def: The Riemann tensor evaluated on an actual orthonormal frame. Its slots are <R(e_i,e_j)e_k,e_l>, matching sectionalNumerator. · OAI.PositiveEinsteinFour.Geometry.frameCurvature
framedConcat def: Literal unmarked concatenation of fixed windows with separately reported pure pre/post regions. Counts are in atoms, not surviving trace symbols. · OAI.TraceReconstruction.framedConcat
frameDimensionStratum def: Index zero is the infinite-rank stratum; index n + 1 is rank n. · OAI.KadisonKastler.frameDimensionStratum
framedPrefix def: A freely split flag with its named quotient identifications. · OAI.IntegralCharacterVarieties.framedPrefix
FramedSeamEquation def: The framed flag equation at a seam of a diagram. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FramedSeamEquation
framedSteps def: The increments seen in the diagonal frame at each prefix. · OAI.PolycyclicRecognition.PositiveTriangular.framedSteps
frameExecution def: Actual execution with the same step count, budget, and tapes. · OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameExecution
frameExecution def: Actual execution with the same step count, budget, and tapes. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameExecution
frameGradientLaplacian def: The actual rough Laplacian of the Weyl gradient, in the same frame. · OAI.PositiveEinsteinFour.Geometry.frameGradientLaplacian
frameIndexAvailable def: There are at least k + 1 indices satisfying the predicate. · OAI.KadisonKastler.frameIndexAvailable
frameIndexEquiv def: The ascending enumeration, restricted to its genuine indices, is a bijection. · OAI.KadisonKastler.frameIndexEquiv
FrameKey structure: A frame's key has the exact normalized domain and active target. · OAI.PureTypeSystem.ObservationValues.FrameKey
frameMatrix def: Matrix of a three-dimensional orthogonal change in the fixed Euclidean basis. · OAI.PositiveEinsteinFour.QuaternionFrame.frameMatrix
frameMomentumMap def: Lowering the initial frame vector in a fixed coordinate chart. · OAI.PositiveEinsteinFour.Geometry.frameMomentumMap
frameMul def: Change a finite frame by a matrix acting on its coefficient columns. · OAI.Kaplansky.frameMul
frameOfHom def: Each algebra map gives its frame of coordinate images. · OAI.StableCoordinate.FrameLift.frameOfHom
frameOperator def: Sum of the rank-one operators of a finite vector family. · OAI.MUB6.Weiner.frameOperator
FrameOrientation structure: An orientation is a clopen choice of determinant sign in every frame fiber. · OAI.PositiveEinsteinFour.Geometry.FrameOrientation
framePrefix def: Number of atoms strictly before the indicated padded unit. · OAI.TraceReconstruction.framePrefix
FrameReflectionData structure: The two elementary reflection compatibilities of uniform parallel frame flow. These are classical input, not a curvature estimate. · OAI.PositiveEinsteinFour.Geometry.FrameReflectionData
frameStatement def: Same code and stacks, with an untouched caller-register component. · OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameStatement
frameStatement def: Same code and stacks, with an untouched caller-register component. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameStatement
frameTensor def: Pull back every covariant slot by a single actual orthonormal frame. · OAI.PositiveEinsteinFour.Geometry.frameTensor
frameTensorPairing def: Pairing of all components of a covariant tensor in an orthonormal frame. · OAI.PositiveEinsteinFour.Geometry.frameTensorPairing
frameVariation def: First variation in the frame matrix, adding one covariant slot at a time. · OAI.PositiveEinsteinFour.Geometry.frameVariation
frameXX def: The normal components forced by the Gauss identity when the transverse second-form component is (S,0). · OAI.ClosedSurfaceR4.GeometryPreservation.frameXX
frankWolfeStep def: The conditional-gradient step size in the finite entropy optimizer. · OAI.EditApproximation.frankWolfeStep
Free abbrev: Slots not occupied by a pinned exceptional symbol. · OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.Free
Free abbrev: Coordinates are only the unpinned vertices; Lebesgue measure is on this space, not on the lower-dimensional subset of all-vertex height space. · OAI.TriangularSurface.FiniteModel.Free
freeBarObjIso def: Coherence between canonical categorical scalars and supplied compatible scalars. · OAI.DerivedBar.Multibar.freeBarObjIso
freeBarPatternIso def: Coherence of a free bar term with a literal leading block. · OAI.DerivedBar.Multibar.freeBarPatternIso
freeBarTensorIso def: The component comparison to the explicit two-sided bar. · OAI.DerivedBar.BimoduleTensor.freeBarTensorIso
freeBarTensorNatIso def: Natural comparison, preserving the exterior D-action. · OAI.DerivedBar.BimoduleTensor.freeBarTensorNatIso
freeCenter def: The affine center restricted to directions whose images already lie in W. · OAI.MaxCutGames.Inverse.KMSAffineRestriction.freeCenter
freeCenter def: The affine center restricted to directions whose images already lie in W. · OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.freeCenter
FreeChain abbrev: The free integral module on copies of the regular left group action. · OAI.Release075.FreeChain
freeColumn def: The actual free column at the split layer is the child's initial free set. · OAI.CoordinateSweeps.Grid.Holes.freeColumn
freeDiagonalModel_of_leadingProjections def: The only geometric construction still needed is a family of orthogonal leading-word projections whose complementary centered blocks vanish. · OAI.KadisonKastler.freeDiagonalModel_of_leadingProjections
freeEquiv def: The standard identification D ⊗_A (A ⊗_k W) ≅ D ⊗_k W for arbitrary algebras. · OAI.DerivedBar.Balanced.freeEquiv
freeEquiv def: Genuine X ⊗_D (D ⊗_k W) ≅ X ⊗_k W, with no flatness of X. · OAI.DerivedBar.BimoduleTensor.freeEquiv
freeFlow def: The free-flight shear on the whole plane, without any boundary. · OAI.TriangularBilliards.freeFlow
freeFormMap def: Positive free form ∫|u'|² + a∫|u|² on the full H¹ graph. · OAI.SharpLiebThirring.OperatorProof.freeFormMap
freeGlobalAmplitude def: The global complex amplitude retains the original compact support. · OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.freeGlobalAmplitude
freeGlobalPhase def: The outer cutoff makes the original local phase a globally smooth scalar. · OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.freeGlobalPhase
FreeHaarMoments structure: Standard alternating centered moments of a subalgebra free from a Haar unitary. Every interior exponent is nonzero; the final Haar letter is optional. · OAI.KadisonKastler.FreeHaarMoments
freeLetter def: The literal rose letters, with the fixed source inverse pairing. · OAI.TorsionFreeZeroDivisors.ConcreteGroup.freeLetter
freeMap def: Balanced tensor on a map of free modules, in the explicit field-tensor coordinates. · OAI.DerivedBar.BimoduleTensor.freeMap
freeMatchingDisk def: The exact disk in equation free:parameter-disk; terminating decimals are represented as rational numbers. · OAI.DefocusingNLS.freeMatchingDisk
freeMatrixExtensionHom def: The algebraic extension in the original algebra, using its faithful normal coordinates. · OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionHom
freePair def: A freely canceling pair is the boundary of a single thickened edge, with no interior cell. · OAI.HyperbolicObstruction.WordPictures.WordPicture.freePair
freeParameterRectangle def: A fixed rectangle containing the free-profile parameter disk. · OAI.DefocusingNLS.freeParameterRectangle
freePermEquiv def: The honest symmetric group on the unmarked sites, including empty sets. · OAI.CoordinateSweeps.Marked.freePermEquiv
freePresentation def: The finite free sheaf has the presentation with no relations. · OAI.CoherentLocality.freePresentation
freeRow def: The actual free row at the split layer is the child's terminal free set. · OAI.CoordinateSweeps.Grid.Holes.freeRow
freeS def: Free independent variable order: X,Y,T. · OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.freeS
freeSets def: Standard freeness: every nonempty alternating product of centered elements vanishes, starting with either algebra and with no restriction on length parity. · OAI.Generator.freeSets
freeTestFamily def: The defining free-root norm uses only genuine edges. It is a restriction of the rooted-sibling test family, NOT the anchored rootless sibling family. · OAI.BoundedTreePotentials.FreeRoot.freeTestFamily
freeTorusEvolution def: The free evolution, represented by continuous functions on the torus. · OAI.DefocusingNLS.freeTorusEvolution
freeTracialHeadCoordinates def: The raw head coordinates of the reduced product, with their actual left multiplication action. · OAI.KadisonSimilarity.freeTracialHeadCoordinates
freeTwistedLayerQuotient def: The quotient map from the jth conormal twist of O_D^N to the jth quotient layer. · OAI.ActualCartier.freeTwistedLayerQuotient
freeUltrafilter def: The actual free ultrafilter used for the bounded-sequence quotient. · OAI.Tingley.freeUltrafilter
freeWordThreshold def: A convenient integral threshold, larger than the one displayed in the manuscript, that keeps the distinct-label constant equal to seven. · OAI.KadisonKastler.freeWordThreshold
frequency def: The loss frequency in the paper's normal parametrization. · OAI.BoltzmannNonuniqueness.frequency
frequency def: Collision frequency of a particle in the two unit-strength reference beams. · OAI.BoltzmannNonuniqueness.ReferenceGeometry.frequency
frequency def: Canonical frequencies of the dyadic restrictions. · OAI.PlaneFiveColor.ContinuousCharacters.frequency
frequencyBlockEquiv def: Splitting the fixed and free frequency blocks is an exact bijection. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.frequencyBlockEquiv
frequencyBlockEquiv def: Splitting the fixed and free frequency blocks is an exact bijection. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.frequencyBlockEquiv
frequencyChange def: The contragredient reindexing used in the trace pairing. · OAI.MaxCutGames.Inverse.KMSBasisInvariant.frequencyChange
frequencyChange def: The contragredient reindexing used in the trace pairing. · OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.frequencyChange
frequencyCoordinates def: Integer coordinates in the standard Euclidean Fourier lattice. · OAI.DefocusingNLS.frequencyCoordinates
frequencyCoset def: Frequencies in the affine target's annihilator coset. With q = Q.mkQ, this is exactly θ + Hom(H,Q) in the ambient reverse-map space. · OAI.MaxCutGames.Decoder.PrivateFourier.frequencyCoset
frequencyCoset def: Frequencies in the affine target's annihilator coset. With q = Q.mkQ, this is exactly θ + Hom(H,Q) in the ambient reverse-map space. · OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyCoset
frequencyEquiv def: Natural frequency coordinates for an earlier pair inside a fixed final pair. This is a change of domain and codomain separately. · OAI.MaxCutGames.Appendix.A5ReverseIndex.frequencyEquiv
frequencyEquiv def: Natural frequency coordinates for an earlier pair inside a fixed final pair. This is a change of domain and codomain separately. · OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.frequencyEquiv
frequencyImage def: The image classification of an exact-rank frequency. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.frequencyImage
frequencyImage def: The image classification of an exact-rank frequency. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.frequencyImage
frequencyImageFiberEquiv def: Removing the redundant rank certificate from a fixed-image fiber. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.frequencyImageFiberEquiv
frequencyImageFiberEquiv def: Removing the redundant rank certificate from a fixed-image fiber. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.frequencyImageFiberEquiv
frequencyLattice def: The standard Fourier frequency lattice in twelve dimensions. · OAI.DefocusingNLS.frequencyLattice
frequencyProdEquiv def: Splitting the last frequency row is an exact bijection. · OAI.MaxCutGames.Inverse.KMSAnalytic.frequencyProdEquiv
frequencyProdEquiv def: Splitting the last frequency row is an exact bijection. · OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.frequencyProdEquiv
frequencyProduct def: The product records every frequency at or below this state. · OAI.Ostmann.MovingSlotData.frequencyProduct
frequencyRank def: The actual rank of a Fourier index S : F → E. · OAI.MaxCutGames.Appendix.LevelInequality.frequencyRank
frequencyRank def: The degree is the rank of the actual dual linear map. · OAI.MaxCutGames.Inverse.KMSBasisInvariant.frequencyRank
frequencyRank def: The actual rank of a Fourier index S : F → E. · OAI.UniqueGamesTheorem.Appendix.LevelInequality.frequencyRank
frequencyRank def: The degree is the rank of the actual dual linear map. · OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.frequencyRank
FrequencySmoothing structure: The precise output of frequency-nest approximation for a contraction field. The approximation is on the common original Hilbert space. · OAI.KadisonKastler.FrequencySmoothing
frequencySumEquiv def: The additive shear used to collect terms of a double Fourier series. · OAI.DefocusingNLS.frequencySumEquiv
frequencyWeight def: The actual probability assigned to a reverse-map frequency. · OAI.MaxCutGames.Decoder.PrivateFourier.frequencyWeight
frequencyWeight def: The actual probability assigned to a reverse-map frequency. · OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyWeight
Fresh def: No coin is requested twice along any branch of the experiment. · OAI.CubeShuffle.QueryTree.Fresh
Fresh def: Genuine secondary-name witnesses at every vertex of the walk. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.Fresh
Fresh def: A property of an actual ranked program, not an assumed property of a band chosen from its weaker original specification. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.Fresh
Fresh def: No coordinate is queried twice along any branch. · OAI.MatroidProphet.MarkedQueryProgram.Fresh
Fresh def: A new clause has no old subclause, including no equal old clause. · OAI.Sparsification.Fresh
fresh def: Actual next fresh registers depend only on the completed list output, including its rare guessing branch. Previous outcomes remain in the record. · OAI.ExactQuantumFactoring.CompletedSplit.fresh
fresh def: Actual next fresh registers depend only on the completed list output, including its rare guessing branch. Previous outcomes remain in the record. · OAI.ExactQuantumFactoring.FixedSplit.fresh
fresh def: Every quantum preparation below is the same physical fixed-width program (on the runtime input word). Hard/easy tests affect the deferred predicate only. · OAI.ExactQuantumFactoring.UniversalSplit.fresh
fresh def: A fresh relayer fixes layer zero, so the ensuing straight homotopies are based. Positive layers move above every old layer under consideration. · OAI.GroupRingTopology.Milnor.fresh
freshAbsolute def: Sum of their absolute values. · OAI.DilutedSpinGlass.PrescribedTree.freshAbsolute
FreshAt def: Only the actually followed branch must query each available label at most once. This makes no assertion about branches impossible under the chosen bit law. · OAI.MatroidProphet.MarkedQueryProgram.FreshAt
freshAt def: refresh test. Ignore when breaching the cap. · OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.freshAt
freshCharge def: Forced bits counted only when fresh; ordinary path queries insert their bits into the same record, so subsequent closures cannot charge them twice. · OAI.CubeShuffle.QueryTree.freshCharge
freshEval def: Conditional expectation on a completely new path below the chosen vertex. Old sampled descendants are NOT reused, even if their values happen to agree. · OAI.DilutedSpinGlass.PrescribedTree.freshEval
FreshGallery def: A finite genuine ranked gallery with a verified fresh-parent decoration at every vertex. This is constructed below, not included as a main hypothesis. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.FreshGallery
freshLength def: The short fresh-product length, with the constants used in the random residue construction. · OAI.Problem337.RandomProducts.freshLength
freshPatternLaw def: The finite law of spin patterns induced by one fresh message label on all replica leaves. The message label, including its root, is shared across leaves; only the final spin draws are conditionally independent. · OAI.DilutedSpinGlass.freshPatternLaw
freshRank def: The main parent has its own occurrence label. All secondary facet labels remain available without any distinctness requirement. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.freshRank
freshSplitDepth def: Positional split depth of a genuinely fresh branch from an old reference. · OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth
FreshStrip abbrev: These, and not cell-rank values, label the newly created disk facets. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.FreshStrip
freshTotal def: Sum of the fresh-extension coefficients gamma_beta. · OAI.DilutedSpinGlass.PrescribedTree.freshTotal
friendlyQuartetFiberEquiv def: The held coordinates and the inverse first free coordinate parametrize one quartet product fiber without changing its uniform measure. · OAI.Ostmann.friendlyQuartetFiberEquiv
fringe def: composition of sector metadata under extension of an axis. · OAI.PowerSaving.Grove.Shard.fringe
frobenius def: Actual Hilbert--Schmidt coordinates, not the operator norm silently endowed with a Hilbert inner product. · OAI.HarmonicCounterexample.LinearODE.frobenius
frobeniusDistance def: Frobenius distance, with the unnormalized matrix-coordinate convention. · OAI.InvariantIsing.frobeniusDistance
from_kernels def: The kernel and cokernel functors supply the universal properties used in from_resolution. · OAI.CartierConnecting.from_kernels
from_resolution def: The divisor-valued boundary obtained from an invertible-ideal resolution, retaining its morphisms and exactness rather than just Euler classes. · OAI.CartierConnecting.from_resolution
fromArrays def: The initializer takes array values, so every row closure shares right. · OAI.LowSpaceSubsetSum.PreparedReaderContext.fromArrays
fromBarUnbalanced def: The reverse unbalanced tensor map is B-linear before passing to the quotient. · OAI.LittleFinitistic.BimoduleBarComparison.fromBarUnbalanced
fromBase def: A fixed coherent base maps to a directed union independently of the stage used to define the map. · OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.fromBase
fromBase def: Each stage has the same specified conservative map from the round's base. · OAI.PartitionConsistency.MonoidConstruction.Round.fromBase
fromBinary def: Package an independently proved two-input clean register routine as a serialized procedure. Its polynomial bound is not an operation oracle: the actual Eval proof is required. · OAI.RationalHitting.StackLanguage.Procedure.fromBinary
fromCompletion def: Compatible vertex-adic residues determine each homogeneous coefficient. · OAI.SectionCompletion.fromCompletion
fromDecoration def: Every corner-color equation follows from vertex tables and wiring. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.fromDecoration
fromFiniteOmega def: The inverse conversion also preserves the same finite dimension bound. · OAI.Thomason.Construction.fromFiniteOmega
fromFinsupp def: Reassemble a chain from its finite basis coefficients. · OAI.Thomason.Construction.PastingGlobeCylinderBasis.fromFinsupp
fromGlobe def: The actual positive-table realization of the free globe receives its canonical strict cell map, with no Gray input. · OAI.Thomason.Construction.DirectedGlobeComplex.fromGlobe
fromGraph def: The original graph-loop group maps to the nonredundant cone group. · OAI.TorsionFreeZeroDivisors.GraphConePresentation.fromGraph
fromLog def: The exact side regularizers obtained from the stored log size. · OAI.KServer.SideFamilies.fromLog
fromOmega def: The cell-preserving conversion to Boolean-indexed boundaries. · OAI.Thomason.Construction.fromOmega
fromPasting def: The actual strict map from the pasted globes to its ordered chain model. · OAI.Thomason.Construction.PastingGlobeBasis.fromPasting
fromPhase def: The inverse is Borel by Lusin--Souslin, not by choice of arbitrary unmeasurable representatives. It agrees with every exact chain at its initial state. · OAI.TriangularBilliards.CodedChain.fromPhase
fromPolynomial def: Evaluate the polynomial quotient at the actual cyclic group-ring generator. · OAI.CirculantHadamard.CyclicPolynomial.fromPolynomial
fromPolynomial def: The inverse polynomial presentation uses the forward matrix coordinates upstairs. · OAI.StableCoordinate.Presentation.fromPolynomial
fromPorts def: Construct every boundary circle from the oriented corner involution. In particular no boundary-coverage or cyclic-closure premise is imposed on a new rank-reduction diagram. Facet labels may repeat, and closed facets have zero cycles. · OAI.IntegralCharacterVarieties.SurfacePresentation.fromPorts
fromPowers def: Newton reconstruction from the entire sequence of power sums. · OAI.EuclideanFiveColor.PhaseEncoding.fromPowers
fromPrimePowers def: Multiply local factors over the positive exponents in the prime factorization. · OAI.TwoPointCorrelations.fromPrimePowers
fromPrimeSet def: A canonical finite label model, using the actual prime factors of each whole tuple inside one finite prime pool. · OAI.TwoPointCorrelations.LabeledPrimeWord.fromPrimeSet
fromRealization def: The actual geometric realization has canonical coordinates in the geometric horn. · OAI.Thomason.Construction.HornBarycentric.fromRealization
fromRoot def: The unique contraction from the initial vertex to a chain vertex. · OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.fromRoot
fromSimplexChains def: Differential compatibility follows from injectivity of the evaluated chains; the basis construction already gives both inverse equations. · OAI.Thomason.Construction.SimplexAtomsInput.fromSimplexChains
fromUnit def: Undo affine unit-interval coordinates. · OAI.Problem358.KernelQuantile.fromUnit
frontier def: The literal full-column frontier of a column cell in the active graph. · OAI.PlanarL1.Columns.Model.Point.frontier
FrontierExtension structure: One concrete finite successor level. Its parentwise positive weights are supplied only after the corresponding adaptive selections stop. · OAI.ReflexiveFixedPoints.FrontierExtension
FrontierTower structure: A coherent sequence of actual finite extensions, beginning with the root. · OAI.ReflexiveFixedPoints.FrontierTower
frontPassageProbability def: Probability of the concrete full-prefix front success and its physical sausage mass. The index records an admissible physical configuration. · OAI.SLEExactGauge.PassageSuccess.frontPassageProbability
FrontSuccess def: Concrete success of the first front stop, including the full preceding path and the required terminal offset. · OAI.SLEExactGauge.PassageSuccess.FrontSuccess
frontTime def: Finite-valued representative; it agrees with the actual first-front hitting time whenever a retained endpoint witnesses a crossing. · OAI.SLEExactGauge.FirstFrontPassage.frontTime
frozen def: D + attack directions. · OAI.HadwigerCounterexample.Volley.frozen
frozenAt def: Freeze at the heat scale two dyadic steps below the pinching mean radius. · OAI.RegularPointCoordinates.RegularBilinearData.frozenAt
FrozenCell abbrev: Actual non-top cells; these faces must not be split during macro surgery. · OAI.HyperbolicObstruction.ConeSkeleton.FrozenCell
frozenConjugate def: A covariant positive form in frozen Euclidean coordinates. · OAI.RegularPointCoordinates.frozenConjugate
FrozenInitialSpectatorData structure: This packages consequences of the selected support, without selecting another family. · OAI.Ostmann.FrozenInitialSpectatorData
FrozenMapped def: Frozen source faces use one complete indexed side cycle, without wrapping. This property is imposed on raw cellular face maps, not on their reducedness. · OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.FrozenMapped
frozenOffset def: Cell lift coordinate at a frozen side, measured from its indexed first vertex. Reversing orientation changes the initial point but not the cell lift. · OAI.HyperbolicObstruction.ConeSkeleton.frozenOffset
frozenSiteMass def: Sampled coordinates are fixed; every other coordinate keeps its law. · OAI.JointDickman.frozenSiteMass
frozenSource def: Affine coordinates frozen at a point and a scale. · OAI.RegularPointCoordinates.frozenSource
FrozenTarget structure: Additional literal boundary indexing for the cells which are not free macro walks. No normalization property is packaged into this data. · OAI.HyperbolicObstruction.PictureSwitch.FrozenTarget
Fuel structure: semantic call responses · OAI.ExactDerandomization.Mint.Mill.Fuel
Full def: A separated completion in the supremum over all unitary models. · OAI.NuclearUltrapower.FullGroupModel.Full
full def: Integer computation of the exact expanded Taylor-reversal matrix at t. · OAI.RationalHitting.IntegralTest.full
full def: The reverse-Taylor test matrix over the univariate polynomial ring in t. Summation over all M Taylor coordinates appends only zero terms. · OAI.RationalHitting.TestPolynomial.full
full abbrev: Discarding components disjoint from the outer face makes an ordinary filling into a full filling, with no exceptional faces. · OAI.Release075.TriangleFilling.full
full def: No vertex or dart names survive, but all actual graph incidence does. · OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.full
FullAdmissible def: Exact upper-array constraints: nonnegative values, coordinate difference v, and each of the two arrays dominating the countable ℓp norm of its children. At leaves the child norm is zero. · OAI.DiamondDistortion.RecursiveModel.FullAdmissible
FullAdvice structure: The first prover's entire information; no singleton-choice or private matrix field is present. · OAI.MaxCutGames.Decoder.AdviceExperiment.FullAdvice
FullAdvice structure: The first prover's entire information; no singleton-choice or private matrix field is present. · OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.FullAdvice
fullAlternatingProduct def: The full prime-index product, using all subsets of the finite index type. · OAI.CirculantHadamard.fullAlternatingProduct
FullApprox structure: A global graph approximation, with actual small exceptional disks. All fields will be constructed, not postulated as coloring hypotheses. · OAI.EuclideanFiveColor.FullApprox
fullArray def: The complete least upper arrays, including every non-root coordinate. · OAI.DiamondDistortion.RecursiveModel.fullArray
FullCell def: All cells whose two object boundaries lie in the specified set. · OAI.Thomason.Construction.StrictOmegaCategory.FullCell
FullCertificate structure: The conclusion of the affine approximation lemma in one dimension d. The label set and its slopes are fixed before a small parameter is chosen. · OAI.Problem326.Affine.FullCertificate
fullCertificate_zero def: Harmless dimension-zero base for strong induction. It is not used as a positive-dimensional fixed-minimum family. · OAI.Problem326.Affine.fullCertificate_zero
FullClaim def: The same witness has a proper strongly closed unital complex commutant. · OAI.Hyperinvariant.FullClaim
FullColumnCoordinates structure: The finite matrix-unit coordinates of a full column and its corner. The two action identities say that full left multiplication has the usual corner matrix entries. They assert no existence of an intertwiner. · OAI.KadisonSimilarity.FullColumnCoordinates
fullColumnCoordinates def: Both coordinate unitaries and every entry in the full-column theorem are now constructed from the same finite family in the tracial algebra. · OAI.KadisonSimilarity.TracialCornerGeometry.fullColumnCoordinates
fullColumnCoordinatesOfColumns def: Realize the full-column coordinates from the actual corner inclusion operators and their common matrix of algebra entries. · OAI.KadisonSimilarity.fullColumnCoordinatesOfColumns
FullComponent abbrev: The complete infimal-cost space of all finite-cost coordinate outputs, modulo representations with zero output. · OAI.DiamondDistortion.StartModel.FullComponent
fullCoordinates def: The small frequency map before its last coordinate is embedded into D. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.fullCoordinates
fullCoordinates def: The small frequency map before its last coordinate is embedded into D. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.fullCoordinates
fullCost def: The hypothetical full tree includes a sibling skipped after early YES. · OAI.LowSpaceSubsetSum.CountedPrefixSearch.fullCost
FullCubicSymmetry def: Every row permutation of the cubic matrix extends using column permutations, unit phases and optional conjugation, and its Fourier norm is invariant under signed permutations of balanced charges. · OAI.HadamardSix.CubicSymmetry.FullCubicSymmetry
fullDifference def: The complete six-difference product in the source's stated order. · OAI.Paper170.fullDifference
FullDual abbrev: The full continuous dual, used for the finite-height forest example. · OAI.ForestSpace.FullDual
fullD₂ def: Full oriented boundary in edge coordinates. The internal factors are, respectively, radial, collar diagonal, outer and apex edges. Their indices include the entire independent polygon index; no deck augmentation occurs. The graph factor … · OAI.HyperbolicObstruction.CyclicTriangleBoundary.fullD₂
fullFaceIso def: The smaller oriental is the full strict subcategory on a convex split face. · OAI.Thomason.Construction.SimplexComplex.fullFaceIso
fullFaceMap def: Any ordinal face lands in the actual full subcategory on its image vertices. · OAI.Thomason.Construction.SimplexComplex.fullFaceMap
fullFiberEquivFixedKernel def: The kernel condition already forces surjectivity onto the comparison space. · OAI.MaxCutGames.Inverse.KMSKernelFiberCard.fullFiberEquivFixedKernel
fullFiberEquivFixedKernel def: The kernel condition already forces surjectivity onto the comparison space. · OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.fullFiberEquivFixedKernel
FullFilling structure: Unlike an ordinary filling, this records every connected component. The only nontriangular interior faces allowed are isolated two-dart spheres, created when an exterior cancellable pair is folded. · OAI.Release075.FullFilling
fullGraph def: The underlying connectivity graph with every bond retained. · OAI.CriticalPercolation.BondGraph.fullGraph
fullIdealBall def: All nonzero ideals of norm at most Y, including ideals above three. · OAI.CubicFirstMoment.fullIdealBall
fullInclusion def: The inclusion preserves all strict compositions and faces. · OAI.Thomason.Construction.StrictOmegaCategory.fullInclusion
fullInput def: Decode only the data visible to the first player. · OAI.MaxCutGames.Decoder.ActualAdviceUpper.fullInput
fullInput def: Decode only the data visible to the first player. · OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.fullInput
FullLabel abbrev: A full label retains the literal first and second interval labels. · OAI.QuantitativeVanDerWaerden.FullLabel
fullLabel def: Actual full labels of actual cyclic points. This specializes the generic literal-label definition also used in the heavy-label return proof. · OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabel
fullLabelsEquiv def: The combined exact split into forced, extra-leaf and extra-interior labels. · OAI.TraceReconstruction.OccupiedParityTree.Forced.fullLabelsEquiv
fullLabelWord def: The actual label word of an ordered cyclic progression. No nonzero-step condition is needed to define the word; event families impose it separately. · OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabelWord
FullLattice structure: The lattice data appearing in Theorem 1.1, before choosing an ordering of the real embeddings. · OAI.DukePrimeDegree.FullLattice
FullLine def: Affine lines are identified by their actual point sets. · OAI.KaplanskyCounterexample.FiniteGeometry.FullLine
fullLines def: Full incidences among the six lines AB, AC, AD, BC, BD, CD at A,B,C,D. These are exactly the doubled fans of the source. · OAI.HyperbolicObstruction.fullLines
fullMap def: Restrict a strict functor that sends the selected objects to selected objects. · OAI.Thomason.Construction.StrictOmegaCategory.fullMap
FullMatrixCorner structure: Actual countable matrix units with initial corner E and strong sum one. · OAI.KadisonKastler.FullMatrixCorner
fullMatrixCorner def: The actual countable matrix units after rebasing to the first final projection. · OAI.KadisonKastler.CountableProjectionCopies.fullMatrixCorner
FullMatrixFrame structure: A full matrix system for a concrete algebra, with a finite nonempty index. · OAI.KadisonKastler.FullMatrixFrame
FullNagata def: The strict, simultaneous Nagata inequality in homogeneous coordinates, equivalent to the effective-cycle formulation FullNagataEffectiveCurves. · OAI.Nagata.FullNagata
FullNagataClassOrdinary def: The equivalent numerical formulation for projective classes of nonzero homogeneous equations. Classes identify only nonzero scalar multiples, not zero loci or radicals; reducible and nonreduced equations remain represented. · OAI.Nagata.W13.FullNagataClassOrdinary
FullNagataCurves def: Full strict simultaneous target on genuine nonzero effective curve cycles. No square-only, equal-multiplicity, degree, or reducedness restriction is added. · OAI.Nagata.Workers.W10.FullNagataCurves
FullNagataEffectiveCurves def: One exceptional union handles every genuine effective curve and every unequal nonnegative multiplicity vector. All positive degrees, reducible curves and repeated components remain quantified. · OAI.Nagata.Workers.W10.FullNagataEffectiveCurves
FullNagataOrdinary def: The unchanged full baseline quantifier pattern, with each multiplicity lower bound written as an inequality between actual natural numbers. · OAI.Nagata.W13.FullNagataOrdinary
fullOn def: The full strict omega-subcategory on a set of object cells. · OAI.Thomason.Construction.StrictOmegaCategory.fullOn
FullOnVertices def: An actual cell whose two object boundaries are in the selected vertices. · OAI.Thomason.Construction.SimplexComplex.FullOnVertices
FullOperatorAlgebra def: An actual presentation as a full algebra of Hilbert-space operators. · OAI.BoundedHochschild.KadisonRingrose.FullOperatorAlgebra
fullOperatorAlgebra def: The full concrete operator algebra. · OAI.KadisonKastler.WeakOperatorRepresentative.fullOperatorAlgebra
FullPairing structure: The full inverse-letter pairing of the original boundary words, retaining actual graph lifts. Planarity is additional data, not asserted here. · OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing
fullParity def: Full parity, with values in the reals. · OAI.LeanBlast.GotsmanLinial.fullParity
fullPrefixBucket def: The bucket reached by following a designated entry's complete prefix. · OAI.LowSpaceSubsetSum.fullPrefixBucket
fullPrimeProductPolynomial def: The product before imposing squarefreeness. The prime supports and weights are independent, exactly as required by the structured coefficients. · OAI.CubicFirstMoment.fullPrimeProductPolynomial
fullReplacement def: The literal clamped proposal, extended by the old comparison on the rest of the old band. This is the extension whose finite maximum is required for simultaneous overlapping secondary groups. · OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullReplacement
fullRunInTime def: Literal init-to-halt execution, with every non-output tape empty at halt. · OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.fullRunInTime
fullRunInTime def: Literal initialization to literal clean halting configuration, with exact semantic subdivision output. No execution or runtime premise is assumed. · OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.fullRunInTime
fullRunInTime def: Literal initList to literal haltList, including all private tape and finite-state cleanup. This theorem has no runtime premise. · OAI.MaxCutGames.Reduction.MachineAddressGame.fullRunInTime
fullRunInTime def: Literal init-to-halt execution, with every non-output tape empty at halt. · OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.fullRunInTime
fullRunInTime def: Literal initialization to literal clean halting configuration, with exact semantic subdivision output. No execution or runtime premise is assumed. · OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.fullRunInTime
fullRunInTime def: Literal initList to literal haltList, including all private tape and finite-state cleanup. This theorem has no runtime premise. · OAI.UniqueGamesTheorem.Reduction.MachineAddressGame.fullRunInTime
fullSeedCoordinatesEquiv def: A global bijection retains all actual visible data, with exactly one uniform kernel-valued matrix left after conditioning. · OAI.MaxCutGames.Decoder.AdviceLaw.fullSeedCoordinatesEquiv
fullSeedCoordinatesEquiv def: A global bijection retains all actual visible data, with exactly one uniform kernel-valued matrix left after conditioning. · OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeedCoordinatesEquiv
fullSeedLaw def: A finite hidden sample whose actual Draw is seedToActualDraw. · OAI.MaxCutGames.Decoder.AdviceLaw.fullSeedLaw
fullSeedLaw def: A finite hidden sample whose actual Draw is seedToActualDraw. · OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeedLaw
fullSelectedError def: The literal unnormalised score error from pert:error, with the quenched center under the entire same-law reservoir disorder. · OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedError
FullShapeControl structure: The full signed identity, retained for marker anchors as well as spin anchors. This is the literal output of the analytic perturbation selector. · OAI.DilutedSpinGlass.UniversalDictionary.FullShapeControl
fullSide def: Extra endpoint stutters allow either orientation to be trimmed while retaining both endpoints. This ensures exact shared-edge parametrizations. · OAI.ArtinCAT0.WordDiagram.fullSide
fullSolutionFormula def: The concrete full correction uses the genuine slow derivative of the normalized primitive in its transverse datum. · OAI.ClosedSurfaceR4.PeriodicCorrector.fullSolutionFormula
FullSpace abbrev: All countable finite-cost start outputs, componentwise quotient, outer ℓ². · OAI.DiamondDistortion.StartModel.FullSpace
fullStepRetention def: The complete rank-one update experiment at a specified starting map. · OAI.MaxCutGames.Inverse.KMSBasisComparison.fullStepRetention
fullStepRetention def: The complete rank-one update experiment at a specified starting map. · OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fullStepRetention
fullStreetCarrierHomeomorph def: The actual full Street nerve realizes to its intrinsic carrier subspace. · OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetCarrierHomeomorph
fullStreetCellComplex def: A strict full inclusion has an actual relative barycentric cell presentation on Street realizations. · OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetCellComplex
fullStreetIso def: The nerve of a full subcategory is isomorphic to this actual subcomplex. · OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetIso
fullStreetPreimageHomeomorph def: Realizing a strict full inverse image gives the actual inverse image of the corresponding closed Street carrier subspace. · OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetPreimageHomeomorph
fullStreetSubcomplex def: A simplex is in the full subcomplex when all its cells are in the full subcategory. · OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetSubcomplex
fullSubposetComplex def: The full subcomplex of the ordinary nerve on a set of vertices. · OAI.Thomason.Construction.fullSubposetComplex
fullSubposetInclusion def: The ordinary functor including the full induced subposet. · OAI.Thomason.Construction.fullSubposetInclusion
fullSupport def: The barycentric interior, expressed by its nonzero coordinates. · OAI.Thomason.Construction.RealizationPrism.fullSupport
fullTable def: No hidden matrix is an input to this fixed table function. · OAI.MaxCutGames.Decoder.SelectedPolicies.fullTable
fullTable def: Full forward and inverse tables of an explicit finite permutation. · OAI.MaxCutGames.Explicit.ProductTarget.fullTable
fullTable def: No hidden matrix is an input to this fixed table function. · OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.fullTable
fullTable def: Full forward and inverse tables of an explicit finite permutation. · OAI.UniqueGamesTheorem.Explicit.ProductTarget.fullTable
fullTableEquiv def: A bijection merely rearranges the full sampled table and changes its matrix coordinates. It never appends the hidden projection to this law. · OAI.MaxCutGames.Decoder.ActualEvents.fullTableEquiv
fullTableEquiv def: A bijection merely rearranges the full sampled table and changes its matrix coordinates. It never appends the hidden projection to this law. · OAI.UniqueGamesTheorem.Decoder.ActualEvents.fullTableEquiv
FullTensorTerm abbrev: Every degree of Q_T tensor_BC O, carrying the actual outside B-actions. · OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm
FullTestBundle abbrev: A single coherent presentation of the finite stages on full Y. · OAI.Kaplansky.FullTestBundle
fullUpperData def: Least upper values on the original full ℓp component, not on a finite-support substitute. All child sequences are genuine countable ℓp vectors. · OAI.DiamondDistortion.RecursiveModel.fullUpperData
fullVectorEquiv def: Exact full-model identification, preserving every finite coordinate. · OAI.DiamondDistortion.RecursiveModel.fullVectorEquiv
fullWord def: The actual full label word of two independent D-coordinate progressions. · OAI.QuantitativeVanDerWaerden.CirclePartition.fullWord
fullyProtected def: All sampled terminal leaves are canceled, with no diagonal contraction. · OAI.DilutedSpinGlass.PrescribedTree.fullyProtected
FullyReduced def: No adjacent sides are oppositely indexed pieces of the same target cell, including both the free top occurrences and all genuine frozen cells. · OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.FullyReduced
funBuild def: Ordinary data abstraction on the single bundle, before even wrapping. · OAI.PureTypeSystem.Labelled.ProbeCode.funBuild
function def: The ordinary function represented by the zeroth jet. · OAI.ForcedComputation.BoundedSpatialJets.function
function def: Function coordinate zero is the least significant radix digit. · OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.function
function def: Function coordinate zero is the least significant radix digit. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.function
functional def: The exact finite-depth cavity functional B_r. · OAI.DilutedSpinGlass.functional
functionalAt def: Extend the actual nonroot functionals by the zero functional at the root. · OAI.ReflexiveFixedPoints.SwitchingTreeData.functionalAt
FunctionalEdges structure: Oriented edges of a finite functional graph. Loops and distinct parallel edges are permitted a priori; the source map nevertheless is injective. · OAI.OneWayLiveness.FunctionalEdges
functionalRow def: The coordinate row of a binary linear functional. · OAI.MaxCutGames.Inverse.Shortcode.functionalRow
functionalRow def: The coordinate row of a binary linear functional. · OAI.UniqueGamesTheorem.Inverse.Shortcode.functionalRow
functionEvaluation def: Evaluation at a genuine punctured-plane point is a unital ring map. · OAI.Nagata.Workers.W17.functionEvaluation
functionMap def: Bounded linear extraction of the represented function. · OAI.ForcedComputation.BoundedSpatialJets.functionMap
functionOn def: f is a set graph of a function whose domain is exactly d. The first conjunct excludes non-pairs and graph entries outside the domain; the second conjunct asserts totality and single-valuedness. · OAI.PartitionConsistency.SetLanguage.functionOn
functions def: Exhaustive finite-function enumeration with a specified value list. · OAI.MaxCutGames.Reduction.ActualEnumeration.functions
functions def: Exhaustive finite-function enumeration with a specified value list. · OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.functions
functionShift def: The right translation action on a group-valued function space. · OAI.EilenbergGanea.functionShift
functor def: The actual left vertex of the balanced tensor, with its original induced maps. · OAI.LittleFinitistic.BalancedVertexFunctor.functor
functor def: The actual balanced tensor functor from bimodules to left modules. · OAI.LittleFinitistic.BimoduleBalancedTensor.functor
functor def: Tensoring with the fixed bimodule complex acts on every left-module complex. · OAI.LittleFinitistic.BimoduleTotal.functor
functor abbrev: The original left vertex action, with the right B-module structure retained. · OAI.LittleFinitistic.BimoduleVertex.functor
functor def: The actual vertex-component functor; it retains the original right action. · OAI.LittleFinitistic.VertexFunctor.functor
functor def: The actual colimit construction, as an endofunctor on simplicial sets. · OAI.Thomason.Construction.InfiniteExtension.functor
functor def: The concrete strict abelianization functor. · OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.functor
functorObjectIteration def: An actual natural isomorphism identifies every objectwise iterate. · OAI.LittleFinitistic.functorObjectIteration
FundamentalCross def: Symmetric fundamental-cut incidence. For distinct edges of a planar tree tour this is precisely alternation of their two darts. · OAI.FKCRT.FundamentalCross
fundamentalCube def: One unit-volume fundamental domain; its boundary is immaterial to integration. · OAI.CubicTorus.fundamentalCube
FundamentalGroup abbrev: Path-order multiplication is the opposite of Mathlib's End multiplication. · OAI.Release075.BlockPresentation.FundamentalGroup
fundamentalHom def: Traversal-order labels are a homomorphism to the opposite, because Mathlib's fundamental group multiplication is categorical (right path first). · OAI.EilenbergGanea.PathTransport.Local.fundamentalHom
fundamentalKernelEquiv def: This is an equivalence with the actual kernel, not an assumed presentation. · OAI.EilenbergGanea.CoverKernel.fundamentalKernelEquiv
fundG def: Conditional entropy of total sum. · OAI.FourierLLogL.Compress.fundG
fundI def: Conditional exact cost. · OAI.FourierLLogL.Compress.fundI
fundK def: Conditional m-block noisy cost. · OAI.FourierLLogL.Compress.fundK
future def: The original cut, followed by all its selected future cells. · OAI.PartitionConsistency.ConservativeMonoids.CellTower.future
futureAmbientKernel def: Push a time-coordinate kernel to the actual right root orbits. · OAI.DukePrimeDegree.EliminationChain.futureAmbientKernel
f₀ def: First generator of the pulled-back distinguished ideal. · OAI.StableCoordinate.Bundle.f₀