Glossary: M

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

M def: Both blocks of the exact 2N-dimensional interpolation space. · OAI.CriticalHoneycomb.FiniteFunctional.M
M def: Normal-form connection matrix on the finite chart; q is the bottom-left row in this frame and T the original scalar coefficient. · OAI.ElasticityRigidity.M
M def: The last level containing a giant. · OAI.WeakPinned.Hierarchy.Depth.M
m def: Number of distinct edges in a residual tuple. · OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.m
Machine structure: `Machine` records finite numbers of stacks and states, an initial state, designated input and output stacks, and a finite instruction table. · OAI.CurrentKS.Machine
Machine structure: A deterministic left-ended one-tape machine. none is halt, recognized only while the head is at a workspace cell. · OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine
Machine structure: A deterministic automaton on an arbitrary state type. · OAI.OneWayLiveness.Machine
Machine structure: Blank is 0, input bits are 1 and 2. Every work alphabet, state space and collection of tapes is finite. Tapes are two-way infinite. · OAI.ParityWL.Complexity.Machine
machine def: Concrete finite machine; exit labels 0, 1, 2 mean equal, different, malformed. · OAI.MaxCutGames.BinaryNameCompare.machine
machine def: One concrete machine with two Boolean stacks and finite control. The two exit labels expose acceptance to a caller; the scanner leaves them unexecuted. · OAI.MaxCutGames.BinaryNameMachine.machine
machine def: Concrete finite-control instantiation; the counter is its designated output. · OAI.MaxCutGames.BinaryNameSearch.machine
machine def: A fixed finite machine. Its control stores only the fixed port position; vertex and reverse-index values reside on the tapes. · OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.machine
machine def: The fixed block map is also a concrete machine with two Boolean tapes and a finite register, independently of any ambient placement. · OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.machine
machine def: A concrete machine for this stored-field phase, with nine Boolean tapes and a finite residue register. It does not assume a whole-row runtime. · OAI.MaxCutGames.Foundations.Complexity.MachineLazyRows.machine
machine def: A concrete finite machine using exactly three binary stacks. Its table and unary index may be supplied in a caller configuration; no list oracle is used. · OAI.MaxCutGames.Foundations.Complexity.MachineLookup.machine
machine def: The complete construction has five Boolean tapes, nine control labels, and one optional-bit register. No table data appears in its finite state. · OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.machine
machine def: Three Boolean stacks, three labels, and one optional Boolean register. · OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.machine
machine def: A canonical finite machine over six Boolean stacks. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.machine
machine def: A fixed nine-label six-stack finite machine implementing the routine. Its inputs may be supplied in a caller's distributed tape configuration. · OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.machine
machine def: Finite packaging of the concrete control program. Callers supply a fixed finite body; no input-dependent collection of labels or states is introduced. · OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.machine
machine def: All state and control spaces are explicit finite types; only the tapes hold variable-size data. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.machine
machine def: Its finite description depends on the fixed degree and selected port; the vertex count and graph table are runtime tape data. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.machine
machine def: A closed finite-control instance. Embedded uses instantiate instruction on the caller's common tapes and preserve its larger ambient register. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.machine
machine def: A finite machine realizing the header phase on prepared operand registers. · OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.machine
machine def: Finiteness of tape addresses and registers constructs an actual TM2; its execution bound is established above by the concrete transitions. · OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.machine
machine def: A bundled finite machine. Its input/output tapes are designated explicitly. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.machine
machine def: Every state component is finite; the q-dependent relation register is enumerated by the explicit vector/function equivalence of the parser. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.machine
machine def: Bundling makes the fixed finite tape, control-label, and register sets explicit. Neither the label type nor the state type contains a natural input. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.machine
machine def: A concrete finite machine instance, with input-dependent unary values located only on its three tapes. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.machine
machine def: This stage itself has only seven tapes and nine control labels. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.machine
machine def: All alphabets and registers are finite. Counts live solely on Bool stacks. · OAI.MaxCutGames.Reduction.AddressMachineProgram.machine
machine def: No semantic atomic arithmetic operation is being charged unit time: only unary increment/decrement, one input/output bit, and finite jumps are atomic. · OAI.OptimalMaxCut.CounterMachine.machine
machine def: Concrete finite machine; exit labels 0, 1, 2 mean equal, different, malformed. · OAI.UniqueGamesTheorem.BinaryNameCompare.machine
machine def: One concrete machine with two Boolean stacks and finite control. The two exit labels expose acceptance to a caller; the scanner leaves them unexecuted. · OAI.UniqueGamesTheorem.BinaryNameMachine.machine
machine def: Concrete finite-control instantiation; the counter is its designated output. · OAI.UniqueGamesTheorem.BinaryNameSearch.machine
machine def: A fixed finite machine. Its control stores only the fixed port position; vertex and reverse-index values reside on the tapes. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.machine
machine def: The fixed block map is also a concrete machine with two Boolean tapes and a finite register, independently of any ambient placement. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.machine
machine def: A concrete machine for this stored-field phase, with nine Boolean tapes and a finite residue register. It does not assume a whole-row runtime. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.machine
machine def: A concrete finite machine using exactly three binary stacks. Its table and unary index may be supplied in a caller configuration; no list oracle is used. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.machine
machine def: The complete construction has five Boolean tapes, nine control labels, and one optional-bit register. No table data appears in its finite state. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.machine
machine def: Three Boolean stacks, three labels, and one optional Boolean register. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.machine
machine def: A canonical finite machine over six Boolean stacks. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.machine
machine def: A fixed nine-label six-stack finite machine implementing the routine. Its inputs may be supplied in a caller's distributed tape configuration. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.machine
machine def: Finite packaging of the concrete control program. Callers supply a fixed finite body; no input-dependent collection of labels or states is introduced. · OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.machine
machine def: All state and control spaces are explicit finite types; only the tapes hold variable-size data. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.machine
machine def: Its finite description depends on the fixed degree and selected port; the vertex count and graph table are runtime tape data. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.machine
machine def: A closed finite-control instance. Embedded uses instantiate instruction on the caller's common tapes and preserve its larger ambient register. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.machine
machine def: A finite machine realizing the header phase on prepared operand registers. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.machine
machine def: Finiteness of tape addresses and registers constructs an actual TM2; its execution bound is established above by the concrete transitions. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.machine
machine def: A bundled finite machine. Its input/output tapes are designated explicitly. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.machine
machine def: Every state component is finite; the q-dependent relation register is enumerated by the explicit vector/function equivalence of the parser. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.machine
machine def: Bundling makes the fixed finite tape, control-label, and register sets explicit. Neither the label type nor the state type contains a natural input. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.machine
machine def: A concrete finite machine instance, with input-dependent unary values located only on its three tapes. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.machine
machine def: This stage itself has only seven tapes and nine control labels. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Setup.machine
machine def: All alphabets and registers are finite. Counts live solely on Bool stacks. · OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.machine
machine_run def: Every derived structured evaluation is an actual finite-alphabet execution, including the final halt transition. No arithmetic oracle is added. · OAI.OptimalMaxCut.CounterMachine.Command.machine_run
machineCost def: The machine's literal finite expected movement, prior to forgetting its private state. Physical configurations are determined by visible histories. · OAI.KServer.HiddenMachine.machineCost
machineDummyInTime def: The same actual machine on the padding invariant e = d * v, with its exact existing-codec graph-row output. · OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.machineDummyInTime
machineDummyInTime def: The same actual machine on the padding invariant e = d * v, with its exact existing-codec graph-row output. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.machineDummyInTime
machineHaltInTime def: Full cleanup reaches haltList, with all nonoutput stacks empty and the machine's actual initial finite state restored. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.machineHaltInTime
machineHaltInTime def: Full cleanup reaches haltList, with all nonoutput stacks empty and the machine's actual initial finite state restored. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.machineHaltInTime
machineInTime def: Genuine staged execution of the concrete four-label finite machine. · OAI.MaxCutGames.BinaryHeaderMachine.machineInTime
machineInTime def: The bounded run instantiated with the displayed finite machine, including its actual entry and two actual exit labels. · OAI.MaxCutGames.BinaryNameMachine.machineInTime
machineInTime def: A concrete finite-machine certificate, with neither a runtime nor a selection oracle among its hypotheses. · OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.machineInTime
machineInTime def: The full actual finite-machine execution, including initialization and all rows. No body trace or runtime hypothesis is an input to this certificate. · OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.machineInTime
machineInTime def: A full actual finite-machine execution with a fixed-degree polynomial budget, the exact lazy-table output, preserved original input, and clean work. · OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.machineInTime
machineInTime def: The same exact computation as a certificate for the concrete finite three-stack machine. Both valid and invalid indices terminate with reset local state, retaining the zero index delimiter and all other stated tape contents. · OAI.MaxCutGames.Foundations.Complexity.MachineLookup.machineInTime
machineInTime def: The generic trace instantiates the concrete finite machine, with the same linear bound and completely cleaned working copy. · OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.machineInTime
machineInTime def: Exact inherited-row emission with all working tapes restored to empty. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.machineInTime
machineInTime def: Concrete finite-machine execution for the actual regularized input row. · OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.machineInTime
machineInTime def: The input predicate/match block is consumed. The exact unary predicate row is prepended; the remaining input, old output, and ambient register are accounted for in the actual transition witness. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.machineInTime
machineInTime def: The same proved run stated directly for the concrete finite machine. · OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.machineInTime
machineInTime def: The same proved run stated directly for the concrete finite machine. · OAI.MaxCutGames.Reduction.SourceEquationLookup.machineInTime
machineInTime def: Genuine staged execution of the concrete four-label finite machine. · OAI.UniqueGamesTheorem.BinaryHeaderMachine.machineInTime
machineInTime def: The bounded run instantiated with the displayed finite machine, including its actual entry and two actual exit labels. · OAI.UniqueGamesTheorem.BinaryNameMachine.machineInTime
machineInTime def: A concrete finite-machine certificate, with neither a runtime nor a selection oracle among its hypotheses. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.machineInTime
machineInTime def: The full actual finite-machine execution, including initialization and all rows. No body trace or runtime hypothesis is an input to this certificate. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.machineInTime
machineInTime def: A full actual finite-machine execution with a fixed-degree polynomial budget, the exact lazy-table output, preserved original input, and clean work. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.machineInTime
machineInTime def: The same exact computation as a certificate for the concrete finite three-stack machine. Both valid and invalid indices terminate with reset local state, retaining the zero index delimiter and all other stated tape contents. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.machineInTime
machineInTime def: The generic trace instantiates the concrete finite machine, with the same linear bound and completely cleaned working copy. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.machineInTime
machineInTime def: Exact inherited-row emission with all working tapes restored to empty. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.machineInTime
machineInTime def: Concrete finite-machine execution for the actual regularized input row. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.machineInTime
machineInTime def: The input predicate/match block is consumed. The exact unary predicate row is prepended; the remaining input, old output, and ambient register are accounted for in the actual transition witness. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.machineInTime
machineInTime def: The same proved run stated directly for the concrete finite machine. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.machineInTime
machineInTime def: The same proved run stated directly for the concrete finite machine. · OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.machineInTime
machineInTime_inputBound def: The same actual execution has a linear bound measured in the complete input stack, including its unread suffix. · OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.machineInTime_inputBound
machineInTime_inputBound def: The same actual execution has a linear bound measured in the complete input stack, including its unread suffix. · OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.machineInTime_inputBound
machineProgram def: The compiler outputs two finite rational instruction tables. The body is computed from the machine alone; only the one-period loader uses the input. · OAI.ForcedComputation.machineProgram
machineRowInTime def: Direct execution of the concrete finite machine on caller-supplied unary fields. This instantiates all program equations; no execution premise remains. · OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.machineRowInTime
machineRowInTime def: Direct execution of the concrete finite machine on caller-supplied unary fields. This instantiates all program equations; no execution premise remains. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.machineRowInTime
MacroCell abbrev: One (unoriented) elementary top triangle per actual macro edge. The finite vertex numbering only chooses signs; it does not identify different edges. · OAI.HyperbolicObstruction.ConeSkeleton.MacroCell
macroCellDart def: A canonical positive orientation, with exactly ONE elementary triangle per unoriented macro edge. No redundant simple-cycle disks are introduced. · OAI.HyperbolicObstruction.ConeSkeleton.macroCellDart
MacroMachine structure: A finite control-flow chart whose nodes are verified stack routines. · OAI.ParityWL.Complexity.MacroMachine
macroRoute def: Send apex i to its fixed actual fan base and expand radial edges by fixed fan paths. The exceptional two-step incidence uses the genuine loose letter, not a fictitious eighth fan. · OAI.HyperbolicObstruction.ConeSkeleton.macroRoute
macroStep def: The literal map of the subdivided incidence graph from source02:72--79. The exceptional two-edge path is radial X_D followed by the loose letter. · OAI.HyperbolicObstruction.ConeSkeleton.macroStep
magneticBiasObjective def: The finite canonical field value with the magnetization constraint. · OAI.InvariantIsing.magneticBiasObjective
magneticHeightBias def: The unique interior minimizing bias for the actual literal height vector. · OAI.InvariantIsing.magneticHeightBias
main def: Initialization first clones the input's live vertex-count field. · OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.main
main def: Initialization first clones the input's live vertex-count field. · OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.main
MainAsymptotic def: Uniform O(ε⁴), with exactly twice the ceiling of 2/ε² cylinders. · OAI.TriangularCovering.MainAsymptotic
MainBatch structure: A finite family of the actual main-cell proposals. Distinct cells may meet at unchanged boundary points; no disjointness of their closed domains is assumed. · OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch
MainBounds def: The upper-bound constant is chosen independently of epsilon. · OAI.SharpLogRamsey.MainBounds
MainClaim def: Uniform two-sided bounds with common positive constants and threshold. · OAI.EditDistortion.MainClaim
MainClaim def: The manuscript's unconditional main existence claim. · OAI.HarmonicCounterexample.MainClaim
MainClaim def: Nonzero, norm-quasinilpotent, and with no nontrivial closed hyperinvariant subspace. · OAI.Hyperinvariant.MainClaim
MainClaim def: A group algebra over a finite field of characteristic 2, of a finitely generated group, can contain elements a, b with a*b = 1 but b*a different from 1. · OAI.KaplanskyCounterexample.MainClaim
MainClaim def: Every positive real power is eventually smaller than the PSD rank, uniformly over all even vertex counts. The exponentiation is real rpow. · OAI.PerfectMatchingPSD.MainClaim
MainClaim def: The full spectral bound, optimal constants, and attainment at the explicit potential. · OAI.SharpLiebThirring.MainClaim
MainClaim def: Existence of a complete normal local domain over ℂ with no small Cohen–Macaulay module. · OAI.SmallCM.MainClaim
MainConclusion def: Complete simple Lebesgue spectrum, including the stated consequences. · OAI.ThreeTorus.MainConclusion
MainConclusion def: The main conclusion, together with the geometric/nonvacuity guarantees needed by the concrete definition of the actual two-sided billiard. · OAI.TriangularBilliards.MainConclusion
mainHamiltonianPath def: A complete smooth Hamiltonian path on the actual normalized Fubini--Study quadric. · OAI.ArnoldCounterexample.Construction.mainHamiltonianPath
mainInstruction def: Fixed degree control, including two actual independent working streams. · OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.mainInstruction
mainInstruction def: Fixed degree control, including two actual independent working streams. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.mainInstruction
mainIx def: Index depth i denotes b=2^{-i}; b₀=h^{-16}. · OAI.FourierLLogL.Dyadic.Thermal.mainIx
MainLimit def: The logarithmic exponent converges along all natural orders. · OAI.SharpLogRamsey.MainLimit
mainRevealRate def: Probability that a label is sacrificed in the main branch. · OAI.MatroidProphet.Secretary.mainRevealRate
MainRuleFeasibility def: Core and hidden prefix feasibility, measurability after masking the initial observations, complete accepted-set nonanticipation, irrevocability, and literal rejection of sacrificed labels. The mask depends only on the initial seed by the … · OAI.MatroidProphet.MainRuleFeasibility
MainStatement def: Cubic bipartite three-vertex-connected plane graphs have a Hamiltonian cycle. · OAI.Barnette.MainStatement
MainStatement def: Both constants are uniform over the sequence, all degrees below d, and all cochains. · OAI.CoboundaryExpanders.MainStatement
MainStatement def: The complete main assertion thm:main. Both constants are chosen outside all three quantifiers m, i, and f. Vertex growth is convergence to infinity, not mere existence of one arbitrarily large complex. · OAI.CoboundaryExpanders.MainStatement
MainStatement def: Constant-factor directed feedback vertex set hardness for all NP languages. · OAI.DirectedFeedback.MainStatement
MainStatement def: The precise quantified formulation of source theorem thm:main. · OAI.ExactFourier.MainStatement
MainStatement def: thm:main. The quantifiers over Brownian realizations express that the limit is the standard excursion-tree law, not a coupling-specific object. · OAI.FKCRT.MainStatement
MainStatement def: An integral group-ring matrix with rational and bounded inverses and determinant in (0, 1). · OAI.GroupRingDeterminant.MainStatement
MainStatement def: A finite aspherical complex with hyperbolic fundamental group, no geometric CAT(0) action, and no homotopy equivalent finite complex admitting a locally CAT(-1) metric. · OAI.HyperbolicObstruction.MainStatement
MainStatement def: This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content. · OAI.KServer.MainStatement
MainStatement def: The positive universal constant strengthens ReductionStatement. · OAI.KServer.MainStatement
MainStatement def: A uniform approximation scheme using independent fair bits. All tapes halt within the fixed polynomial bound and return a nonnegative rational. A zero count always produces encoded zero. · OAI.MatchingFPRAS.MainStatement
MainStatement def: Exact main obligation, using an existential representative of the universal C*-algebra. Proving this includes existence of C*(G), not just an implication from an assumed universal model, and includes its separability. The nonembedding … · OAI.NuclearUltrapower.MainStatement
MainStatement def: One universal distortion bound for finite connected planar graphs with arbitrary symmetric positive edge lengths, realized in a real L¹ space. · OAI.PlanarL1.MainStatement
MainStatement def: Literal universal-distortion target. A graph is indexed by Fin n only to express finite vertex sets without an extraneous universe for the target space. No bound depending on n, edge lengths, or number of scales is permitted. · OAI.PlanarL1.MainStatement
MainStatement def: A fixed polynomial bound on bit time, full binary output length, and common positive dimension. · OAI.RationalHitting.MainStatement
MainStatement def: Single-fold representation with positive input and witness lengths. · OAI.SingleFold.MainStatement
MainStatement def: Uniform multiplicity and pinned-distance convergence statements. · OAI.WeakPinned.MainStatement
MainStatementWithCuntzCorollary def: The manuscript's main statement including its explicitly stated O_2 corollary. Both universal C*-algebras must be constructed to prove this. · OAI.NuclearUltrapower.MainStatementWithCuntzCorollary
MainStep structure: Literal deterministic data of a kept eligible main cell. Fresh signs are label coordinates, not assumptions of independence between existing labels. · OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep
MainTarget def: The Falconer distance conjecture in every ambient dimension at least two. · OAI.Falconer.MainTarget
MainTarget def: The single-generation proposition for nonzero finite diffuse factors with separable Banach preduals. · OAI.Generator.MainTarget
MainTarget def: Every irreducible inclusion of concrete type II₁ factors with separable predual of the larger factor has a dense Gδ full relative-generator locus in the normalized trace two-topology. The normalized faithful normal trace is asserted to … · OAI.RelativeGeneration.MainTarget
MainTheorem def: Every countable discrete nonamenable group has a bounded nonunitarizable witness. · OAI.Dixmier.MainTheorem
MainTheorem def: Literal main endpoint: one length-uniform family, exact output for EVERY binary integer N≥2, and worst-case polynomial gates AND qubits. · OAI.ExactQuantumFactoring.MainTheorem
MainTheorem def: The entire main theorem, including its "Moreover" clause. · OAI.TorsionFreeZeroDivisors.MainTheorem
majorant def: Literal majorant from (majorant-construction), retaining Q and B as arguments. · OAI.ExactQuantumFactoring.OrderTrial.majorant
majorantE def: Actual constant-depth arithmetic for U, including dynamic quarter selection. No residue loop and no polynomial-valued oracle occurs in this expression. · OAI.ExactQuantumFactoring.OrderTrial.Expressions.majorantE
majorants def: Continuous nonnegative functions majorizing one on the compact set. · OAI.Kaplansky.PositiveDimensionFunctional.majorants
majorantSum def: Source half-sum, initially a mathematical sum; bounded-piece evaluation follows. · OAI.ExactQuantumFactoring.OrderTrial.majorantSum
majorArcs def: The major arcs complementary to the proved logarithmic minor arcs. · OAI.Problem337.MangoldtMajorArcReduction.majorArcs
majorArcs def: The union of major arcs with reduced denominator at most Q. The rational parameter retains coprimality without a separate hypothesis. · OAI.Problem337.MinorArc.majorArcs
majorArcUnion def: All rational neighborhoods with positive denominator at most Q and centers in [0,1]. Including nonreduced fractions only enlarges the set. · OAI.Problem337.ThreePrimeAnalysis.majorArcUnion
majorIntegral def: The actual major-arc contribution, not a model exponential sum. · OAI.Problem337.MangoldtMajorArcReduction.majorIntegral
majorityBit def: A deterministic majority, resolving a zero bias to false. · OAI.MaxCutGames.Outer.Clone100Counting.majorityBit
majorityBit def: A deterministic majority, resolving a zero bias to false. · OAI.UniqueGamesTheorem.Outer.Clone100Counting.majorityBit
makeData def: empirical input-and-image law · OAI.HadwigerCounterexample.Program.makeData
mandatoryArrayLaw def: The coordinate choices are independent; the rows need not be independent. · OAI.TalagrandDiscreteConvexity.mandatoryArrayLaw
MandatoryColumn abbrev: A coordinate chooses one compulsory row, together with independent marks. The mark in the compulsory row may be sampled and then ignored. · OAI.TalagrandDiscreteConvexity.MandatoryColumn
mandatoryColumnLaw def: Uniform mandatory label, independent of all the extra row marks. · OAI.TalagrandDiscreteConvexity.mandatoryColumnLaw
mandatoryParameter def: The extra inclusion probability after the uniformly chosen mandatory row. · OAI.TalagrandDiscreteConvexity.mandatoryParameter
mandatoryRows def: Read the sets in all rows of a coordinate array. · OAI.TalagrandDiscreteConvexity.mandatoryRows
Mane inductive: The clock argument is in b. q is the immutable tuple seen by the inline recipe (may be virtual, i.e. regenerated via an inline frame). · OAI.ExactDerandomization.Relay.Lot.Mane
mangoldtPhaseSum def: The actual positive-frequency Mangoldt polynomial on the unit circle. · OAI.Problem337.ThreePrimeContinuousFourier.mangoldtPhaseSum
mangoldtTripleSum def: The weighted ternary convolution used in the analytic three-prime theorem. · OAI.Problem337.mangoldtTripleSum
ManifoldFreeChart structure: Coordinate data for one supported free mode. The representative model is a genuine smooth extension of the immersed map in these coordinates. · OAI.ClosedSurfaceR4.ManifoldFreeChart
manufacturedOrbitalSquaredError def: The seventy-second-moment tail keeps the residual compatible with the physical mesh scale even for high-aspect slabs. · OAI.ContinuumCoulomb.manufacturedOrbitalSquaredError
ManufacturedPlanarGroundGap def: The single well-specific consequence actually used by the construction. · OAI.ContinuumCoulomb.PlanarSobolev.ManufacturedPlanarGroundGap
manyMarkedPoints def: The finite set of k² original marks and n distinct extra points. · OAI.Nagata.W06.LineArrangement.manyMarkedPoints
map def: Push forward a law; the sample space need not map injectively. · OAI.CoordinateSweeps.FiniteLaw.map
map def: Scalar extension of a morphism between explicitly free A-modules. · OAI.DerivedBar.FreeBaseChange.map
map def: Tensor of a left-module map and a right-module map is enveloping-linear. · OAI.ExternalTensor.map
map def: Zero-preserving unital monoid maps induce unital maps of contracted algebras. · OAI.FiniteAlgebraicEnvelopes.Contracted.map
map def: The determinant of the linear part is ε * c. · OAI.ForcedComputation.PlanarConjugacy.map
map def: Replacing names uniformly preserves all corner incidences, so a local recipe may be used when several of its named old facets coincide globally. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.map
map def: Transport all averaging unitaries by a star automorphism. · OAI.KadisonKastler.FiniteInnerAverage.map
map def: Apply the given inclusion to a partial unitary. · OAI.KadisonSimilarity.SourcePartialUnitary.map
map def: A genuine bimodule map induces a map preserving the full left B action after tensoring. · OAI.LittleFinitistic.BimoduleBalancedTensor.map
map def: Both actual term maps with the outside left action retained. · OAI.LittleFinitistic.BimoduleComplexTensor.map
map def: The balanced map for actual maps between terms of the two input complexes. · OAI.LittleFinitistic.ComplexTensor.map
map def: Actual component maps of the off-diagonal right product-ring module. · OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.map
map def: Functoriality of the actual tensor with both outside actions retained. · OAI.LittleFinitistic.TwoSidedTensor.map
map def: Module maps restrict to the actual vertex fixed submodules. · OAI.LittleFinitistic.VertexFunctor.map
map def: The induced operator on the completed Hilbert ultraproduct. · OAI.NuclearUltrapower.HilbertUltraproduct.map
map def: Transport the actual overlap starts along a base homomorphism. The pair relation remains the given one-step relation, not its transitive closure. · OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.map
map def: Transport parameters, not profile conclusions, from the starting stage. · OAI.PartitionConsistency.MonoidConstruction.ProbeData.map
map def: The same countable probe presentation over the larger base. · OAI.PartitionConsistency.ProbeAlgebra.Path.map
map def: Extend a kernel homomorphism compatible with both action and cocycle. · OAI.PolycyclicRecognition.FactorExtension.map
map def: The actual linear change from frame coordinates to chart coordinates. · OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.map
map def: Extend each coordinate of a frame by a ring homomorphism. · OAI.StableCoordinate.FrameLift.Frame.map
map def: Pushforward by summing the source weights in each fiber. · OAI.TalagrandDiscreteConvexity.FiniteLaw.map
map def: Pushforward by summing the source weights in each fiber. · OAI.TalagrandThreshold.FiniteLaw.map
map def: The ordinal map encoding a chain inclusion under the chosen enumerations. · OAI.Thomason.Construction.ChainOrdinal.map
map def: The boundary map with p at time zero, q at time one, and value x on every lateral face. · OAI.Thomason.Construction.CubeBoundaryValues.map
map def: Applying a positive chain map in every degree preserves the full table equations, including the boundary data below any vanishing top chain. · OAI.Thomason.Construction.DirectedComplex.Cell.map
map def: Tensor a positive augmented chain map with the identity of the interval. · OAI.Thomason.Construction.DirectedComplex.RightCylinder.map
map def: Actual face-poset last vertex, with codomain the original simplicial set. · OAI.Thomason.Construction.NonsingularLastVertex.map
map def: Postcomposition is continuous on path spaces. · OAI.Thomason.Construction.PathSpace.map
map def: The chain map induced by an arbitrary strict functor. · OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.map
map def: Postcompose every finite globe map by an actual strict functor. · OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.map
map def: A monotone map induces the unique functor on the associated thin categories. · OAI.Thomason.Construction.StrictPoset.map
map def: The affine barycentric map is continuous on the actual realization. · OAI.Thomason.Construction.SubdivisionBarycentric.map
map def: Homotope an actual map on the whole presentation complex so that EVERY vertex goes to one basepoint. Both cell layers are extended, not collapsed by an unproved quotient/homotopy-equivalence assertion. · OAI.TorsionFreeZeroDivisors.VertexCollapse.map
mapAction def: A linear functor transports an algebra action on endomorphisms. · OAI.LittleFinitistic.FormalSummandAction.mapAction
mapAmbient def: Enlarge the finite ambient registers by reading a projection of them. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Command.mapAmbient
mapAmbient def: Enlarge the finite ambient registers by reading a projection of them. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Command.mapAmbient
mapBasis def: A monotone vertex map takes a nondegenerate simplex to its image if that image is nondegenerate, and to zero otherwise. · OAI.Thomason.Construction.SimplexComplex.mapBasis
mapCoefficient def: The genuine rooted-map coefficient, with the stipulated trivial map. · OAI.FKCRT.mapCoefficient
mapCoefficients def: Pure coefficient relabeling; no algebraic properties are needed for syntactic homogeneity. · OAI.Problem335.Depth5Circuit.mapCoefficients
MapConditions def: Labelled connected orientable genus-zero rotation systems. · OAI.FKCRT.MapConditions
mapConditions def: Recursive transport of names by a map on condition codes. · OAI.PartitionConsistency.SetForcingNames.mapConditions
mapCopies def: Coordinatewise amplification of a bounded operator between different spaces. · OAI.KadisonSimilarity.mapCopies
mapCoproductOfHomBijections def: A coproduct's full Hom universal property transfers through an essentially surjective functor when Hom is bijective on its summands and its point. · OAI.DerivedBar.mapCoproductOfHomBijections
MapData structure: Morphisms preserve both degree-zero maps and the specified relation homotopy, which is part of the three-column input data. · OAI.LittleFinitistic.RectificationTotal.MapData
mapDictionary def: Erase bounded-list records while keeping the same trie and array order. · OAI.LowSpaceSubsetSum.StoredEntry.mapDictionary
mapEquation def: Rename the three occurrences without merging or dropping any occurrence. · OAI.MaxCutGames.Foundations.Hastad.mapEquation
mapEquation def: Rename the three occurrences without merging or dropping any occurrence. · OAI.UniqueGamesTheorem.Foundations.Hastad.mapEquation
mapEquiv def: Arbitrary independent raw coefficients bijectively specify an actual linear map. · OAI.MaxCutGames.Soundness.PartnerMapCoordinates.mapEquiv
mapEquiv def: Arbitrary independent raw coefficients bijectively specify an actual linear map. · OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.mapEquiv
mapFaceFunctor def: The actual map of face-simplex categories underlying the resolution. · OAI.Thomason.Construction.FaceSimplexResolution.mapFaceFunctor
mapFirst def: A map of the first right module retains the middle bimodule's right B-action. · OAI.LittleFinitistic.RightTensor.mapFirst
mapHistory def: Relabeling requests, leaving server labels unchanged. · OAI.KServer.mapHistory
MapIso def: Root-preserving isomorphism of oriented maps (both dart permutations intertwine). · OAI.FKCRT.MapIso
mapL2Dist def: The formalization proves one-third Hölder stability of Brenier maps from the uniform measure on a compact convex body with nonempty interior in $\mathbb R^d$, for every $d\ge2$. For targets supported in one fixed nonempty compact set, the … · OAI.Problem358.mapL2Dist
mapLast def: A map of the last left module retains the middle bimodule's left A-action. · OAI.LittleFinitistic.LeftTensor.mapLast
mapLeft def: Tensor an actual right-module homomorphism with the identity. · OAI.LittleFinitistic.BalancedTensor.mapLeft
mapLinear def: Uniformly bounded operator families act on bounded vector families. · OAI.NuclearUltrapower.UltraPreHilbert.mapLinear
mapNullHomotopy def: Apply the functor to the supplied null-homotopy, transporting only functorial composition and zero equalities. · OAI.LittleFinitistic.RectificationTotal.mapNullHomotopy
mapObjectIteration def: Transport an object isomorphism through an actual repeated functor. · OAI.LittleFinitistic.mapObjectIteration
mappedMacroPolygon def: The actual simple macro polygon carried by one free source face. Its vertices are the original TEMPLATE vertices in their original cyclic order, not the possibly identified letter-bouquet vertices. This supplies the finite macro-cycle … · OAI.HyperbolicObstruction.ConeSkeleton.mappedMacroPolygon
mappedMacroPolygon def: The actual simple macro polygon carried by one free source face. Its vertices are the original TEMPLATE vertices in their original cyclic order, not the possibly identified letter-bouquet vertices. This supplies the finite macro-cycle … · OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.mappedMacroPolygon
mappedTotalIso def: Taking an additive image that kills the relation column leaves precisely the ordinary cone. · OAI.LittleFinitistic.ZeroLastColumn.mappedTotalIso
mapPerm def: Untwisted chart bijection between any two equally sized dyadic partitions. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.mapPerm
mappingPathContraction def: Shrinking a path to its initial point leaves its point over p fixed. · OAI.Thomason.Construction.mappingPathContraction
mappingPathEquiv def: The mapping-path inclusion is an actual homotopy equivalence. · OAI.Thomason.Construction.mappingPathEquiv
mappingSpace def: Compact-open maps out of the fixed parameter space. · OAI.Thomason.Construction.TopologicalProduct.mappingSpace
mapPlane def: An ambient automorphism permutes the plane sample space. · OAI.KaplanskyCounterexample.FiniteGeometry.mapPlane
mapPoint def: Applying a group homomorphism only to the initial vertices of cubes. · OAI.EilenbergGanea.CubeRealization.mapPoint
mapRank def: The natural-number rank of a linear map. Its use below always has a finite-dimensional source, or an explicit finite-dimensional factorization. · OAI.Problem335.RankMeasure.mapRank
mapRight def: Tensor an actual left-module homomorphism with the identity. · OAI.LittleFinitistic.BalancedTensor.mapRight
mapRight def: The actual tensor differential, with the original right B-action. · OAI.LittleFinitistic.TensorComplex.mapRight
mapRightTo def: The actual covariant map in the left-module factor of a balanced tensor. · OAI.LittleFinitistic.BalancedTensor.mapRightTo
mapSpace def: Root and decoration are not included in the metric probability space. · OAI.FKCRT.mapSpace
mapsTo def: Internal set function f : d → r. · OAI.PartitionConsistency.SetLanguage.mapsTo
mapSwitchParameters def: Apply the prescribed sampling map in each of the two independent slots. · OAI.PolycyclicRecognition.mapSwitchParameters
mapTarget def: Apply an actual homomorphism to the target of every scale index. · OAI.CoarseAssembly.Analytic.CompatibleIndexFamily.mapTarget
mapUnit def: Ring change on an GL transport. · OAI.IntegralCharacterVarieties.MatrixExpression.mapUnit
MarchenkoPasturInput structure: The fixed-aspect-ratio Gaussian specialization of MP1967, Theorem1. · OAI.InvariantIsing.MarchenkoPasturInput
marginal def: The actual finite-state label marginal, with its scale-dependent spatial rows. This definition introduces no geometric or probabilistic hypothesis. · OAI.ActualLabels.marginal
marginal def: Pushforward mass at a point, for a finite real nonnegative measure. · OAI.BoundedTreewidthL1.marginal
marginal def: The first of the four triple-coordinate subprobability weights. · OAI.LipschitzHilbert.PhaseCombinatorics.marginal
marginal def: The actual finite-state label marginal, with its scale-dependent spatial rows. This definition introduces no geometric or probabilistic hypothesis. · OAI.SignedDisk.ActualLabels.marginal
marginal def: The unconditioned one-coordinate law; the complete path is summed out. · OAI.SmoothObstruction.SequentialLaw.marginal
marginLists def: The first two natural numbers give the lengths of the two margins. · OAI.ContingencyTables.GreedyFeasibleTable.marginLists
marginSource def: Preserve a positive gap by moving both thresholds inward by the proved simulation error, before removing the exact scalar matrix offset. · OAI.ContinuumCoulomb.QMAPortRouteData.marginSource
Mark inductive: Left endmarker at 0, then the word, then right endmarker. · OAI.Fifths.Mark
mark def: The path of the q-th realized mark, in that mark's own finite space. · OAI.DilutedSpinGlass.HeterogeneousMarks.mark
markAnnulus def: Adding a zero-sign marked corner just inserts a bivalent boundary point. · OAI.KervaireRibbon.markAnnulus
Marked def: An oriented image of a seed edge under an admissible map. · OAI.FiniteCongruence.Marked
marked def: All labels at one endpoint. · OAI.HadwigerCounterexample.Volley.marked
marked def: The marked base point is exactly one; no value with u=0 is accepted. · OAI.KServer.SimplexFamilies.marked
marked def: Index the outer identity paths touched by a specified set of interface edges. The definition is made once, independently of a replacement diagram. · OAI.OneWayLiveness.Pairing.marked
markedColumn def: Retain labels at perfect positions only. · OAI.TwoPointCorrelations.markedColumn
markedCoordinate def: Positive x-coordinate of mark s, where U=-x. The first mark of line zero is moved from 1 to k+1; every other first mark remains 1. · OAI.Nagata.W06.LineArrangement.markedCoordinate
markedCost def: Only the first crossing from the most recent marked direction is counted; a crossing resets the anchor before descending further. · OAI.IntrinsicMarks.markedCost
markedCost def: Only the first crossing from the most recent marked direction is counted; a crossing resets the anchor before descending further. · OAI.SignedDisk.IntrinsicMarks.markedCost
MarkedCutFirstSeam def: The first marked original seam satisfies its framed flag equation. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutFirstSeam
MarkedCutInheritedSeams def: Inherited old seams satisfy their framed flag equations. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutInheritedSeams
MarkedCutLastMirrorSeam def: The last marked mirror seam satisfies its framed flag equation. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutLastMirrorSeam
MarkedCutMirrorInternalSeams def: The internal marked mirror seams satisfy their framed flag equations. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutMirrorInternalSeams
MarkedCutNegativeSeams def: The negative seam family satisfies its framed flag equations. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutNegativeSeams
MarkedCutOriginalInternalSeams def: The internal marked original seams satisfy their framed flag equations. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutOriginalInternalSeams
MarkedCutPositiveSeams def: The positive seam family satisfies its framed flag equations. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutPositiveSeams
MarkedCutSeamEquations def: All seam equations of a marked cut follow from the original named seam flags. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutSeamEquations
MarkedCutSeamFlag abbrev: The framed flag equation at a seam of the marked cut. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutSeamFlag
MarkedCutSelectedSeam def: The selected old seam satisfies its framed flag equation. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutSelectedSeam
markedExponent def: Exponents for the nine marked points in the manuscript. · OAI.Nagata.W06.markedExponent
MarkedFirstShortFlag def: The first short seam inherits the old negative framed flag for every handle value. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedFirstShortFlag
markedGap def: The actual finite minimum δ_P used in the manuscript. · OAI.Nagata.Workers.W05.markedGap
MarkedGeneratorValues def: Invertible matrix values on the generators of a marked cut. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedGeneratorValues
MarkedGreedySteps inductive: A finite trace of unreduced marked greedy steps. · OAI.Problem337.MarkedGreedySteps
MarkedInheritedSeamFlags def: A framed flag equation on an uncut seam is retained in the marked cut diagram. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedInheritedSeamFlags
markedLastShortColumns def: Child coordinates for the marked positive short seam. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedLastShortColumns
MarkedLastShortFlag def: The positive short seam preserves the framed flag equation of the original seam. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedLastShortFlag
markedLastShortRows def: Parent coordinates for the marked positive short seam. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedLastShortRows
MarkedLiftFreshSurface def: The surface equation on a fresh strip of a marked lift. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedLiftFreshSurface
MarkedLineData structure: Exact finite data fixed once for all before any finite quotient is chosen. No geometric or group-theoretic conclusion is part of these data. · OAI.Release075.MarkedLineData
markedLog def: All k selected factors at a terminal leaf, tilting the complete base log weight. · OAI.DilutedSpinGlass.markedLog
markedMapTest def: Evaluate precisely the original all-edge metric and degree measure of an actual compatible marked core tree. Incompatible marks have probability zero, and are assigned zero only to totalize an observable. · OAI.FKCRT.markedMapTest
markedMirrorColumns def: Column coordinates of the marked short mirror seam. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedMirrorColumns
MarkedMirrorGrade def: The marked short mirror seam has the original child-index grading. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedMirrorGrade
markedMirrorRows def: Row coordinates of the marked short mirror seam. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedMirrorRows
MarkedMirrorSeams def: The reflected internal seams satisfy their framed flag equations for every handle value. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedMirrorSeams
MarkedMirrorShortFlags def: The short mirror seam satisfies the framed flag equation. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedMirrorShortFlags
MarkedNegativeBranchSeams def: The negative transverse seams satisfy their framed flag equations for every handle value. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedNegativeBranchSeams
markedNormalBase def: The actual nine marked lifts followed by the moving base lifts. · OAI.Nagata.CoefficientSpaces.markedNormalBase
markedNormalFibre def: Zero normal displacements at the nine marks and Pi-scaled moving displacements. · OAI.Nagata.CoefficientSpaces.markedNormalFibre
MarkedOriginalSeams def: The original internal seams satisfy their framed flag equations for every handle value. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedOriginalSeams
markedPi def: The actual finite product of the nine actual infinite theta products. · OAI.Nagata.W06.TorusConfiguration.markedPi
markedPi def: The product Π in the local covering frame, with offsets aᵢ=x₀−xᵢ. · OAI.Nagata.W22.markedPi
markedPoint def: The k marked points of component i, in actual affine coordinates (U,Y). · OAI.Nagata.W06.LineArrangement.markedPoint
markedPoints def: The actual finite set of marked affine points. · OAI.Nagata.W06.LineArrangement.markedPoints
MarkedPositiveBranchSeams def: The positive transverse seams satisfy their framed flag equations for every handle value. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedPositiveBranchSeams
MarkedQueryProgram inductive: A finite adaptive program with optional success declarations. · OAI.MatroidProphet.MarkedQueryProgram
markedRoot def: The actual quenched root free energy of the marked model. · OAI.DilutedSpinGlass.markedRoot
markedSupplyMultiplier def: The supply multiplier from the marked-denominator construction, with the prime count already simplified using log (m^4) = 4 log m. · OAI.Problem337.markedSupplyMultiplier
markedSymEquiv def: Removing one marked label identifies marked multisets with a label and a multiset of one smaller cardinality. The mark has no multiplicity. · OAI.KadisonKastler.markedSymEquiv
markedThetaSection def: The actual marked divisor product as a genuine section of degree card ι. · OAI.Nagata.W08.markedThetaSection
markedTower def: The literal product-prior tower for k independent copies of a mark process. The physical tower includes every other type in the reservoir. · OAI.DilutedSpinGlass.markedTower
markedTreeScore def: The actual tree score of a specified selected-type term, with an arbitrary old physical replica test. The terminal numerator includes the spin-or-marker anchor from the manuscript, and the factor is its original denominator. · OAI.DilutedSpinGlass.markedTreeScore
markIndicator def: Intrinsic marks as an actual function on prefixes, with first-crossing reset. Prefixes outside the tree have zero charge. · OAI.IntrinsicMarks.markIndicator
markIndicator def: Intrinsic marks as an actual function on prefixes, with first-crossing reset. Prefixes outside the tree have zero charge. · OAI.SignedDisk.IntrinsicMarks.markIndicator
markInterface def: Split off ONE genuine short-end from an exhaustive interface; all other ports remain explicitly enumerated, never silently thrown away. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.markInterface
markLaw def: Actual conditional root-core marks. The arbitrary probability at an unattainable arity is never used by the offspring distribution. · OAI.FKCRT.Inventory.CoreLabel.markLaw
markPath def: Read one complete independent mark process from a latent path. · OAI.DilutedSpinGlass.markPath
markPerm def: Permute selected-type mark labels without permuting spins or other types. · OAI.DilutedSpinGlass.markPerm
markPolynomial def: Actual polynomial vanishing at the k chosen marks on component i. · OAI.Nagata.W04.ReducibleSquare.markPolynomial
markPrior def: An independent mark prior with no physical state. · OAI.DilutedSpinGlass.markPrior
marks def: Mark all irregular vertices and the specified start/end vertices. · OAI.TorsionFreeZeroDivisors.MarkedChainBound.marks
markTail def: The common marks with affine x-coordinates 2,...,k, in the parameter U=-x. · OAI.Nagata.W04.ReducibleSquare.markTail
Martingale def: Fair one-step conditional expectations. Iterating gives W_i=E(W_m|F_i). · OAI.DiamondDistortion.SignCube.Protocol.Martingale
mask def: Fix all occupied edges of a frontier, without fixing their orientations. · OAI.CriticalHoneycomb.Transfer.PlanarNormalization.mask
mask def: Canonical full-cube proof address: every illegal coordinate is false. · OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.mask
mask def: Canonical full-cube proof address: every illegal coordinate is false. · OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.mask
MaskBits abbrev: Labels of the successive mask bits, in the fixed processing order. · OAI.LowSpaceSubsetSum.MaskBits
maskCount def: The exact mask, including the empty mask at k = 0. · OAI.MaxCutGames.Clean.maskCount
maskCount def: The exact mask, including the empty mask at k = 0. · OAI.UniqueGamesTheorem.Clean.maskCount
maskedAngleCos def: The two diagonal coefficients of the finite angular profile. · OAI.WeakPureInfiniteness.maskedAngleCos
MaskedGate structure: A fully resolved occupancy history. Summation now remains only over orientations; it is not a sum over different unoriented configurations. · OAI.CriticalHoneycomb.Transfer.PlanarNormalization.MaskedGate
maskedMixedReferenceBand def: The exact physical band, with the original analyzing coefficient, the physical top mask, and the original alternate synthesis packet. · OAI.LipschitzHilbert.SourceLatticePacket.maskedMixedReferenceBand
maskedMixedReferenceLine def: The actual top mask is applied only to the synthesis wave. · OAI.LipschitzHilbert.SourceLatticePacket.maskedMixedReferenceLine
maskedRotationModel def: Polynomial comparison expression, also defined for uncorrected rows. · OAI.WeakPureInfiniteness.maskedRotationModel
maskedRotationPiece def: The partial isometry between the two copies of a retained cell. · OAI.WeakPureInfiniteness.maskedRotationPiece
maskedRotationUnitary def: A finite family of the corrected cell rotations is an actual unitary. · OAI.WeakPureInfiniteness.maskedRotationUnitary
maskLeafOccurrence def: The top and local mask components are chosen by the representation; the background component is the fixed solution restricted to its leaf. · OAI.LowSpaceSubsetSum.RepresentationSetup.maskLeafOccurrence
maskParentSet def: The union of every component of a raw parent. · OAI.LowSpaceSubsetSum.RepresentationSetup.maskParentSet
maskSlotChoice def: Full positions discard their auxiliary slot; singleton positions retain it. · OAI.MaxCutGames.Decoder.AdviceLaw.maskSlotChoice
maskSlotChoice def: Full positions discard their auxiliary slot; singleton positions retain it. · OAI.UniqueGamesTheorem.Decoder.AdviceLaw.maskSlotChoice
maskWeight def: The deletion-mask probability, with deletion probability q. · OAI.TraceReconstruction.maskWeight
mass def: Maximal initial-segment mass of a test inside the cone at g. · OAI.ForestSpace.mass
mass def: The mass of a finite set of columns. · OAI.MetricEntropyDuality.GreedyPivots.mass
mass def: Frame mass. · OAI.PowerSaving.Binary.mass
mass def: The squared normalized coefficient of one squarefree path. · OAI.Problem335.FirstMoment.mass
mass def: Squared local Fock coefficient, with true denoting differentiation. · OAI.Problem335.LocalMoments.mass
mass def: The mass of a vertical section of a set. · OAI.Problem358.SectionMass.mass
mass def: The smallest coordinate away from the cone vertex. · OAI.Thomason.Construction.HornBarycentric.mass
mass def: The total mass of a finitely supported real function. · OAI.ThompsonNonamenability.mass
mass def: Probability of a finite subset; the fiber weights used below will be the exact uniform probabilities on the original retained distance fibers. · OAI.WeakPinned.SmallFiber.mass
massDensity def: The density n! det(tau_{z_k bar z_l}) for the complex Hessian convention. · OAI.Mahler.massDensity
masses def: The actual closed-cell mass vector, without a choice of maximizing selector. · OAI.Problem358.FixedMassIntercepts.masses
MassFamily structure: A probability mass for each actual member of the family. · OAI.TalagrandThreshold.Selector.MassFamily
MassHypotheses structure: The hypotheses for the isolated-zero mass inequality. This structure records hypotheses; it does not assert the inequality. · OAI.Mahler.MassHypotheses
massIntegral def: The extended nonnegative integral allows infinite mass. This definition does not assert its equality to an exterior-form integral. · OAI.Mahler.massIntegral
massLift def: massLift true-recursion accumulator pays post costs selected at Jump nodes · OAI.FourierLLogL.Dyadic.Procedure.Thread.massLift
massLinearMap def: The actual mass derivative as a bounded linear map in sites and intercepts. · OAI.Problem358.CellGeometry.massLinearMap
massResidual def: The mass residual for an ordinary coordinate-valued mass map. · OAI.Problem358.CellLaplacian.massResidual
massSphereFlux def: Dimension-indexed surface flux, including an irrelevant zero-dimensional branch. · OAI.Mahler.massSphereFlux
massTail def: The mass and energy scalar remainder after the first N annuli. · OAI.BoltzmannNonuniqueness.DatumBounds.massTail
MassTest structure: Smooth local mass tests have no velocity cutoff, since their velocity dependence is introduced only by the transport derivative. · OAI.BoltzmannNonuniqueness.MassTest
Master abbrev: Pair coordinates and all elementary mixed nodes share one ambient space. The numerical certificate is reindexed into this space separately. · OAI.MUB6.Certificate.MixedSemantics.Master
Mat3 abbrev: Flat 3-by-3 integer matrices, used only as kernel-computable labels. · OAI.NuclearUltrapower.SOS.Mat3
matchCount def: The number of master matches for the given finite table instance. · OAI.HyperbolicObstruction.TableModel.matchCount
MatchedPair def: A pair with its actual lower-dimensional matching equation. · OAI.Thomason.Construction.StrictOmegaCategory.MatchedPair
Matches def: Direct second-factor convention. Conjugating all irreducibles gives an equivalent convention with the same quantification over representation classes. · OAI.NuclearUltrapower.Matches
Matches def: Two representatives agree when compared at a common contraction. · OAI.PartitionConsistency.LocalDiagramSystem.System.Matches
Matches def: Exact heat parameters, dimensionless regularizer, and curvature smallness for the normalized harmonic data. · OAI.RegularPointCoordinates.RegularHeatConstants.Matches
Matches def: Agreement with a template at origin zero, as in every count rule. · OAI.Superstring.Counts.Matches
matchesOldProfile def: Shared-prefix equations determine the same allowed old-or-fresh set as references; this positional definition does not examine any spin values. · OAI.DilutedSpinGlass.PrescribedTree.matchesOldProfile
Matching abbrev: A matching on the signed labelled port set; inverse labels have no fixed points. Keeping the origin function separate fixes the vertex types. · OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching
Matching structure: A full inverse-letter matching on the separate literal word boundaries, with actual combinatorial genus zero. This is not a PL-picture assertion. · OAI.TorsionFreeZeroDivisors.WordBlocks.Matching
matchingCanonical def: The canonical inverse word has the literal, uniquely determined stack matching edge and vertex permutations. · OAI.FKCRT.matchingCanonical
matchingClassEquiv def: Each matching orbit has exactly one lower-ranked representative. · OAI.KadisonSimilarity.matchingClassEquiv
matchingEdges def: Edges of the first colour, in the edge-orbit quotient of the complete matching. · OAI.FKCRT.matchingEdges
matchingFacePairs def: Pairs of face points whose nondegenerate coordinate descriptions agree. · OAI.Thomason.Construction.RealizationPrism.matchingFacePairs
matchingKeys def: Proof-only list of keys reported by a complete Cartesian-match join. · OAI.LowSpaceSubsetSum.BinaryTrie.matchingKeys
matchingNormalized def: Normalized matching directions on exactly the positive edge support. · OAI.MatchingEntropy.matchingNormalized
matchingRecords def: A proof view; the runtime never constructs this Cartesian list. · OAI.LowSpaceSubsetSum.RecordedDictionary.matchingRecords
MatchingRepresentatives abbrev: Choose the lower-ranked vertex in each pair. · OAI.KadisonSimilarity.MatchingRepresentatives
MatchingSectors def: The three retained blocks have matching sector labels. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MatchingSectors
matchingSpan def: The integer interval hull of the positions bearing one matching label. The empty fiber has empty span. · OAI.TreeEdit.BinaryLower.matchingSpan
matchingSplitEquiv def: The vertices split into a representative and its partner, once per pair. · OAI.KadisonSimilarity.matchingSplitEquiv
MatchingTuple def: Each inverse pair receives a bijection between its two carrier sets. · OAI.TorsionFreeZeroDivisors.Types.MatchingTuple
matchingTupleEquiv def: An ordered tuple of distinct primes lies in a matching set exactly when it is an embedding into that set. · OAI.Ostmann.matchingTupleEquiv
matchingUniverse def: Raw matching occurrences include those rejected by the validity callback. · OAI.LowSpaceSubsetSum.RepresentationParentData.matchingUniverse
matchingVisits def: A proof view of all matching occurrences visited if YES checks are ignored. The runtime does not build this tree or its list of occurrences. · OAI.LowSpaceSubsetSum.RepresentationParentData.matchingVisits
matchingWord def: The actual two-colour opening/closing word in canonical rooted tour order. · OAI.FKCRT.Inventory.matchingWord
mateEdge def: A canonically normalized mate: every simple graph occurs among these masks, while diagonal/asymmetric mask bits do not admit malformed graphs. · OAI.WLIdentification.NumericGraph.mateEdge
MaterialEvent def: The designated particle of the prescribed fluid enters the open set. · OAI.ForcedComputation.MaterialEvent
materialize def: Materialize explicitly supplied pair-dart semantics in numbered port coordinates. The executable rotation only conjugates G.reverse by ports. The hypothesis about reversal affects proofs, not stored data. · OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.materialize
materialize def: Materialize explicitly supplied pair-dart semantics in numbered port coordinates. The executable rotation only conjugates G.reverse by ports. The hypothesis about reversal affects proofs, not stored data. · OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.materialize
materializedSelectionWithWork def: The final scan retains the original action label, so equal vectors and tied scores do not change which listed action is returned. · OAI.EditApproximation.materializedSelectionWithWork
materializeInTime def: Actual table materialization consumes the level produced by the preceding phase while retaining the original request and its computed padded size. · OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.materializeInTime
materializeInTime def: Actual table materialization consumes the level produced by the preceding phase while retaining the original request and its computed padded size. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.materializeInTime
MatForm abbrev: Matrix forms use the topology of the chosen operator norm. The orthogonal group retains its original (definitionally distinct) product topology. · OAI.ArnoldCounterexample.CriticalBound.MatForm
matrix def: Literal placement-by-fiber block matrix of the induced unitary action. · OAI.CoordinateSweeps.PlacementInduction.Chart.matrix
matrix def: Matrix of the exact parity-signed action in the tensor word basis. · OAI.CoordinateSweeps.SignedTensor.matrix
matrix def: Direct multiplication: this construction will be used only for the fixed spatial matrices in the coefficient-boundary comparison, not as a purported FFT saving. · OAI.ExactFourier.LinearDAG.matrix
matrix def: Matrix entries are indexed by lists in wire order (row first, column second). Entries on ill-sized lists are irrelevant and set to zero. · OAI.ExactQuantumFactoring.Primitive.matrix
matrix def: Depth of a sequence (no missing jumps within plateau) · OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.matrix
matrix def: The entrywise quotient is itself a tracial quotient of finite matrix algebras. · OAI.KadisonKastler.TraceQuotientMap.matrix
matrix def: The genuine dihedral matrix attached to the canonical plane endpoints. · OAI.KLInvariance.TitsSpace.PlaneBasis.matrix
matrix def: The actual finite horizontal tensor differential, on the sum of all selected columns. · OAI.LittleFinitistic.ComplexTensor.matrix
matrix def: Independent reindexings of the exact canonical raw host. · OAI.Problem348.Construction.SelectedAnchor.matrix
Matrix2 structure: A computational four-entry matrix, avoiding dependent finite-index evaluation. · OAI.DefocusingNLS.ProfileCertificate.Matrix2
matrixAction def: The actual real-matrix action on C5, jointly continuous bilinear. · OAI.ArnoldCounterexample.CriticalBound.matrixAction
matrixAlgebraCore def: A concrete finite-algebra Hilbert--Schmidt core, not the operator norm. · OAI.RowColumn.MatrixState.matrixAlgebraCore
matrixAmplification def: The entrywise amplification of a bounded map is a bounded linear map on each fixed finite matrix algebra. · OAI.BoundedHochschild.KadisonRingrose.matrixAmplification
matrixAutomorphismOfReducedWords def: Existence of the ambient matrix-conjugation automorphism follows from the published two-factor extension and the actual reduced-word density. · OAI.KadisonSimilarity.TracialCornerGeometry.matrixAutomorphismOfReducedWords
matrixBilinearDifferential def: The degree-two Hochschild differential, already amplified to matrices. · OAI.KadisonKastler.matrixBilinearDifferential
matrixBlockSwap def: Swap the finite amplification index and the two-by-two block index. · OAI.KadisonKastler.matrixBlockSwap
matrixChart def: The finite matrix chart in the Grassmann vertex type. · OAI.MaxCutGames.Inverse.MatrixChart.matrixChart
matrixChart def: The finite matrix chart in the Grassmann vertex type. · OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrixChart
matrixClass def: Square matrix multiplication as an element of the tensor semiring. · OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass
matrixClosureVectorTrace def: The trace on the closure is the restriction of the given faithful vector state. · OAI.KadisonKastler.matrixClosureVectorTrace
matrixCommutator def: The entrywise spatial commutator, also for rectangular matrices. · OAI.KadisonKastler.matrixCommutator
matrixConjugatedEmbedding def: The conjugate of the fixed source factor, diagonal in the matrix subfactor before passing to the tracial ultrapower. · OAI.KadisonSimilarity.matrixConjugatedEmbedding
matrixConjugateLetter def: Algebraic conjugation of a letter in the other factor. · OAI.KadisonSimilarity.TracialCornerGeometry.matrixConjugateLetter
MatrixConjugationExtensionInput def: The two-factor specialization of Blanchard--Dykema, Embeddings of reduced free products of operator algebras, Pacific J. Math. 199 (2001), 1--19, Theorem 3.7 (arXiv:math/9911012, p. 13). Applied to a tracial reduced free product, the … · OAI.KadisonSimilarity.TracialCornerGeometry.MatrixConjugationExtensionInput
matrixCoords def: Lower-coordinate restriction is faithful on symmetric matrices. · OAI.SharpLiebThirring.PathTopology.matrixCoords
matrixCornerCommutantEquiv def: The matrix coefficient map identifies a diagonal corner with the full matrix commutant. Its inverse is multiplication by that diagonal projection. · OAI.BoundedHochschild.KadisonRingrose.matrixCornerCommutantEquiv
matrixCornerError def: The displacement from the injective embedding followed by the finite corner conjugacy. · OAI.KadisonKastler.matrixCornerError
matrixCornerProjection def: A diagonal scalar matrix unit in the actual C-star matrix algebra. · OAI.KadisonSimilarity.matrixCornerProjection
matrixCurvatureTensor def: The uncompressed matrix-slot operator, specialized to the diagonal curvature block v * S.s. · OAI.PositiveEinsteinFour.Bianchi.matrixCurvatureTensor
matrixDenominator def: The denominator includes the proposal word and its padded completion word. · OAI.ContingencyTables.ProfilePrograms.matrixDenominator
MatrixDepth def: Vanishing on all diagonals strictly below the k-th upper diagonal. · OAI.PolycyclicRecognition.MatrixDepth
matrixDiagonalCut def: The projection onto a finite subset of the matrix diagonal. · OAI.KadisonKastler.matrixDiagonalCut
matrixDiagonalHom def: The unital diagonal embedding into a finite C-star matrix algebra. · OAI.KadisonSimilarity.matrixDiagonalHom
matrixDiagonalProjection def: The actual coordinate projections in the represented matrix algebra. · OAI.KadisonKastler.matrixDiagonalProjection
matrixDirDeriv def: Entrywise derivative of a genuine smooth matrix field. · OAI.AffineBernstein.matrixDirDeriv
matrixEntry def: Invalid source vectors are stationary. Invalid target vectors have zero weight from every valid source. · OAI.ContingencyTables.ProfilePrograms.matrixEntry
matrixEntry def: A single entry in a rectangular C⋆-matrix. · OAI.KadisonKastler.matrixEntry
matrixEntry def: One entry of a bounded family of matrices is a bounded family. · OAI.NuclearUltrapower.VariableUltra.matrixEntry
matrixEntryCompression def: An off-diagonal block of an operator on finite Hilbert arrays. · OAI.KadisonSimilarity.matrixEntryCompression
matrixEntryHom def: The entrywise amplification of the actual subfactor embedding. · OAI.KadisonSimilarity.matrixEntryHom
matrixEntryPaths def: All labelled paths through a nonempty sequence of matrix layers. The empty sequence uses the usual identity-matrix path convention. · OAI.Problem335.matrixEntryPaths
matrixEntrySequence def: A matrix entry of a bounded sequence is itself a bounded sequence. · OAI.KadisonKastler.matrixEntrySequence
matrixEquiv def: The source's inverse matrix substitution, regarded as an algebra automorphism. It carries the original hypersurface equation to -J-u. · OAI.StableCoordinate.Presentation.matrixEquiv
matrixEval def: Entrywise evaluation is an honest matrix ring homomorphism. · OAI.ElasticityAugmented.matrixEval
matrixEvaluation def: Evaluation retains every occurrence's forward and backward transport. · OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.matrixEvaluation
matrixExtensionAction def: The ambient extensions form a genuine group action, by uniqueness on the tracially dense generated algebra. · OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionAction
matrixExtensionAutomorphism def: The actual ambient automorphism is derived from the two inverse published factor embeddings. · OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionAutomorphism
matrixExtensionUnitaryRepresentation def: The actual Hilbert-space unitary representation induced by the derived free-product automorphisms. · OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionUnitaryRepresentation
matrixFamily def: Assemble a finite matrix of bounded families. There is no bound on the dimension of any of the entry algebras. · OAI.NuclearUltrapower.VariableUltra.matrixFamily
matrixField def: The symmetric-cutoff limit, whose convergence and local regularity are proved below. · OAI.SharpLiebThirring.matrixField
matrixForcing def: The outer-product forcing, viewed in the supremum-norm space on the time interval. · OAI.SharpLiebThirring.MatrixFlow.matrixForcing
MatrixFreeCornerLocalInput abbrev: The exact local published bundle on the canonical matrix free-product model. This abbreviation only fixes the generated geometry and transported frame; it does not assert the existence of any of its fields. · OAI.KadisonSimilarity.MatrixFreeCornerLocalInput
matrixFrobeniusPair def: The real, unnormalized Frobenius bilinear form. · OAI.InvariantIsing.matrixFrobeniusPair
MatrixGNSArray abbrev: Square arrays use the ordinary Hilbert sum norm in both coordinates. · OAI.KadisonSimilarity.MatrixGNSArray
matrixGNSArrayLinear def: The unscaled array of represented matrix entries. · OAI.KadisonSimilarity.matrixGNSArrayLinear
matrixGNSIsometry def: The completed matrix GNS space embeds isometrically in its entry array. · OAI.KadisonSimilarity.matrixGNSIsometry
matrixGNSLiftOperator def: The amplified standard-copy operator transported to matrix GNS. · OAI.KadisonSimilarity.matrixGNSLiftOperator
matrixGNSScale def: Normalization converting the array norm into normalized tracial L² norm. · OAI.KadisonSimilarity.matrixGNSScale
matrixGNSUnitary def: The completed normalized matrix GNS space is exactly the square Hilbert array. · OAI.KadisonSimilarity.matrixGNSUnitary
matrixGNSVector def: Normalized represented matrix vectors. · OAI.KadisonSimilarity.matrixGNSVector
matrixGrading def: The real-valued spectral multiplier defined by the projection family. · OAI.LeanBlast.GotsmanLinial.matrixGrading
matrixGraphRow def: The concrete row of independently sampled left matrix translates. · OAI.KadisonKastler.matrixGraphRow
MatrixHilbertStage structure: Local geometric data of one full matrix stage in a tracial Hilbert space. The maps and identities describe its normalized Hilbert--Schmidt realization; no coefficient expansion or intertwiner classification is included. · OAI.KadisonSimilarity.MatrixHilbertStage
matrixHistory def: The constant-observable component of the analytic COMPLETE-matrix history. It is the original old-erase/fresh-grow recursion, not the reference recursion. · OAI.DilutedSpinGlass.PrescribedTree.matrixHistory
matrixHomCore def: Construct the actual Hom-tuple vector bundle from transition matrices and their verified cocycle. There is no bundle-realization hypothesis. · OAI.Kaplansky.matrixHomCore
matrixInnerAverage def: The finite signed matrix group, considered as inner automorphisms of M. · OAI.KadisonKastler.matrixInnerAverage
MatrixIso structure: A genuinely invertible rectangular coordinate matrix; source and target fiber labels can differ, even if both occur on a single facet. · OAI.IntegralCharacterVarieties.MatrixIso
matrixLeftArray def: The ordinary matrix action on the row coordinate, with a standard copy in each column coordinate. · OAI.KadisonSimilarity.matrixLeftArray
MatrixLieDifferentialInput def: The matrix derivative supplied by the precisely cited Lee results. No injectivity, triangularity or spectral consequence is assumed. · OAI.PolycyclicRecognition.MatrixLieDifferentialInput
matrixLiftUnitaryAt def: The coordinate unitary of a bounded unitary sequence. · OAI.KadisonKastler.matrixLiftUnitaryAt
matrixLinearEquiv def: Entrywise application of a linear equivalence is an equivalence at every rectangular matrix size. · OAI.KadisonKastler.matrixLinearEquiv
matrixMap def: The matrix action of the presented Steinberg group. Its codomain here is all matrix units rather than the equal image subgroup E_n(R). · OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap
matrixMap def: Entrywise amplification of a unital star homomorphism. · OAI.NuclearUltrapower.matrixMap
MatrixNearInclusion def: One direction of matrix unit-ball proximity, uniformly in the matrix size. · OAI.KadisonKastler.MatrixNearInclusion
matrixNonunitalMap def: Entrywise extension before adjoining the unchanged identity. · OAI.FiniteAlgebraicEnvelopes.matrixNonunitalMap
matrixOfOperator def: The bounded coordinate blocks, packaged as an actual matrix. · OAI.KadisonSimilarity.matrixOfOperator
matrixOperator def: An operator matrix acts by matrix-vector multiplication on the Hilbert sum. · OAI.KadisonSimilarity.matrixOperator
matrixOperatorAlgebra def: The same finite matrices acting on the finite Hilbert sum. · OAI.KadisonKastler.matrixOperatorAlgebra
MatrixOrbitIndex abbrev: The actual finite sample space for one left and one right unitary. · OAI.KadisonKastler.MatrixOrbitIndex
matrixOrbitSample def: An operator sampled from the finite two-sided matrix orbit. · OAI.KadisonKastler.matrixOrbitSample
matrixPairing def: Matrix-slot Frobenius pairing. · OAI.PositiveEinsteinFour.TraceHessian.matrixPairing
matrixPath def: A finite matrix path expansion, used only for the actual physical column kernels below. All intermediate states are summed once. · OAI.CriticalHoneycomb.Transfer.RasterGrid.matrixPath
matrixPathFunctionEquiv def: Transpose four vertex functions into four labels at each vertex. · OAI.Problem335.Pairings.matrixPathFunctionEquiv
matrixPathLabelsEquiv def: Apply a representation equivalence independently to the four paths. · OAI.Problem335.Pairings.matrixPathLabelsEquiv
matrixPathLabelsProdEquiv def: The four-field record is a nested Cartesian product. · OAI.Problem335.Pairings.matrixPathLabelsProdEquiv
matrixPermutationUnitary def: The finite permutation sum is an actual unitary. · OAI.KadisonKastler.matrixPermutationUnitary
matrixPermutationValue def: The permutation matrix in an actual system of matrix units. · OAI.KadisonKastler.matrixPermutationValue
matrixPolynomialAction def: Direct evaluated matrix action on Hilbert vectors, with every term placed in its specified row and applied to its specified input column. · OAI.Kaplansky.matrixPolynomialAction
matrixPolynomialDerivation def: Differentiate a matrix polynomial along the vector field U ↦ A U. · OAI.InvariantIsing.matrixPolynomialDerivation
matrixPolynomialTerm def: The common positive degree bound and the actual terms of a finite rectangular polynomial matrix are produced from its entries. · OAI.Kaplansky.matrixPolynomialTerm
matrixPositiveTrace def: The ordinary (unnormalized) matrix trace, restricted to its real part. · OAI.NuclearUltrapower.matrixPositiveTrace
matrixQuotient def: Pass to the ultraproduct in every matrix entry. · OAI.NuclearUltrapower.VariableUltra.matrixQuotient
matrixQuotientEquiv def: This is the norm-ultrafilter version of the fixed-size amplification identity in the tensor-norm formulation. · OAI.NuclearUltrapower.VariableUltra.matrixQuotientEquiv
matrixRelativeAverage def: The actual algebra element obtained by finite matrix averaging. · OAI.KadisonKastler.matrixRelativeAverage
matrixRepresentation def: Operator matrices act as a star algebra homomorphism on the Hilbert sum. · OAI.KadisonSimilarity.matrixRepresentation
matrixRepresentationEquiv def: Amplify a concrete representation by a finite matrix algebra. · OAI.KadisonKastler.matrixRepresentationEquiv
matrixRotation def: An orthogonal matrix acts as a linear isometry in the pressure model. · OAI.InvariantIsing.matrixRotation
matrixRotation def: Matrix-slot rotation, retaining the actual tangent four-vectors. · OAI.PositiveEinsteinFour.Bianchi.matrixRotation
matrixScalarHom def: The unital diagonal embedding into a finite matrix algebra. · OAI.BoundedHochschild.KadisonRingrose.matrixScalarHom
matrixScalarHom def: The constant diagonal copy of the coefficient algebra. · OAI.KadisonKastler.matrixScalarHom
matrixSequenceOfEntries def: Assemble finitely many bounded entries into a bounded matrix sequence. · OAI.KadisonKastler.matrixSequenceOfEntries
matrixSequenceQuotient def: Apply a tracial quotient to each finite matrix entry. · OAI.KadisonKastler.matrixSequenceQuotient
matrixSignedGroup def: The finite subgroup actually represented by the matrix units. · OAI.KadisonKastler.matrixSignedGroup
matrixSlot def: Continuous linear dependence on the matrix coefficient. · OAI.PositiveEinsteinFour.Geometry.matrixSlot
matrixSlotAction def: The uncompressed trace-free anticommutator on a matrix. · OAI.PositiveEinsteinFour.Geometry.matrixSlotAction
matrixSlotForm def: The coefficient of the diagonal matrix-slot curvature form. · OAI.PositiveEinsteinFour.HighestHessian.matrixSlotForm
matrixSlotOperator def: The bounded operator that acts on every matrix slice of the Weyl gradient. · OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator
matrixSource def: Present the concrete matrix quotient as a quotient of abstract C⋆-matrices. · OAI.KadisonKastler.TraceQuotientMap.matrixSource
MatrixSplitData structure: The five split-sequence identities, proved from each principal matrix chart below. They are preserved under arbitrary base change. · OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData
matrixStageConcreteUnits def: The ambient matrix units of a finite stage. · OAI.KadisonKastler.matrixStageConcreteUnits
matrixStageUnitaryInclusion def: A nested matrix star embedding maps the compact unitary groups. · OAI.KadisonSimilarity.TracialCornerGeometry.matrixStageUnitaryInclusion
matrixStateRetraction def: A minimal matrix column gives a concrete contractive retraction. · OAI.KadisonKastler.matrixStateRetraction
matrixSystemOfUnits def: The same concrete matrix units in the signed-group construction. · OAI.KadisonKastler.matrixSystemOfUnits
matrixTable def: The table at a fixed actual occurrence question and complement map. · OAI.MaxCutGames.Decoder.SelectedPolicies.matrixTable
matrixTable def: The table at a fixed actual occurrence question and complement map. · OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.matrixTable
matrixTrace def: The canonical normalized faithful tracial state on finite square matrices. · OAI.KadisonKastler.matrixTrace
matrixTrace def: The matrix trace obtained by applying the canonical trace to each diagonal entry. · OAI.TorsionFreeBass.matrixTrace
matrixTraceAmbientRetraction def: The finite matrix retraction, with codomain viewed in ambient operators. · OAI.KadisonKastler.matrixTraceAmbientRetraction
matrixTraceRetraction def: Ambient compression based at the specified diagonal trace vector. · OAI.KadisonKastler.matrixTraceRetraction
matrixTransferEquiv def: The given isomorphism restricted to the concrete finite matrix images. · OAI.KadisonKastler.matrixTransferEquiv
matrixUltrapowerEquiv def: The represented quotient of matrices is the matrix algebra over the scalar represented quotient, with its normalized matrix trace. · OAI.KadisonKastler.matrixUltrapowerEquiv
matrixUnit def: The scalar matrix unit, continuously acting on all (possibly uncountable) group coordinates. · OAI.KervaireMatrix.matrixUnit
matrixUnitaryAction def: Restriction of a matrix representation to its unitary group. · OAI.KadisonSimilarity.matrixUnitaryAction
matrixUnitAverage def: The actual finite-matrix average of an arbitrary ambient operator. · OAI.KadisonKastler.matrixUnitAverage
matrixUnitBall def: The concrete matrix unit ball uses the C*-matrix norm. · OAI.KadisonKastler.CuntzFamily.matrixUnitBall
MatrixUnitColumnFamily structure: The precise finite-frame data consumed by full-column coordinates. · OAI.KadisonSimilarity.MatrixUnitColumnFamily
matrixUnitColumnFamilyOfEmbedding def: Taking a single column of embedded matrix units supplies the full frame. · OAI.KadisonSimilarity.matrixUnitColumnFamilyOfEmbedding
matrixUnitConcreteAlgebra def: The concrete finite matrix image, with its proved weak closedness. · OAI.KadisonKastler.matrixUnitConcreteAlgebra
matrixUnitDiagonalProjection def: A specified diagonal matrix unit, as an algebra projection. · OAI.KadisonKastler.matrixUnitDiagonalProjection
matrixUnitEquiv def: Linear equivalence defined by a transport and its inverse. · OAI.IntegralCharacterVarieties.HomTransport.matrixUnitEquiv
matrixUnits def: A partition of the identity yields a unital full matrix-unit system. · OAI.Generator.Tracial.EquivalentPartition.matrixUnits
matrixUnitsEmbedding def: The existing algebraic matrix-unit representation with the C⋆-matrix domain. · OAI.KadisonKastler.matrixUnitsEmbedding
matrixUnitSignedRepresentation def: The signed permutations of a given concrete matrix-unit system. · OAI.KadisonKastler.matrixUnitSignedRepresentation
matrixUnitsInAlgebra def: Restriction of a concrete matrix-unit system to a von Neumann algebra that contains each of its entries. · OAI.KadisonKastler.matrixUnitsInAlgebra
matrixUnitsPauliX def: The off-diagonal Pauli matrix in the given matrix units. · OAI.KadisonKastler.matrixUnitsPauliX
matrixUnitsPauliXUnitary def: The off-diagonal Pauli unitary. · OAI.KadisonKastler.matrixUnitsPauliXUnitary
matrixUnitsPauliZ def: The diagonal Pauli matrix in the given matrix units. · OAI.KadisonKastler.matrixUnitsPauliZ
matrixUnitsPauliZUnitary def: The diagonal Pauli unitary. · OAI.KadisonKastler.matrixUnitsPauliZUnitary
matrixUpperGap def: Matrices whose entries vanish below the kth upper diagonal. · OAI.PolycyclicRecognition.matrixUpperGap
MatrixValid def: Coordinate form of the requirement τ ∘ T ≠ 0. · OAI.MaxCutGames.Fourier.MatrixParity.MatrixValid
MatrixValid def: Coordinate form of the requirement τ ∘ T ≠ 0. · OAI.UniqueGamesTheorem.Fourier.MatrixParity.MatrixValid
matrixVector def: Entry coordinates preserve the Frobenius norm exactly. · OAI.PositiveEinsteinFour.Jacobi.matrixVector
matrixVectorCoordinate def: Coordinate evaluation of matrix-vector multiplication as a continuous linear functional, with the Frobenius norm used only for the exponential. · OAI.InvariantIsing.matrixVectorCoordinate
matrixVectorFunctional def: An actual finite sum of bounded vector functionals. · OAI.Generator.Tracial.EquivalentPartition.matrixVectorFunctional
matrixVelocitySpace def: The finite-dimensional real subspace comes from actual subgroup curves. In particular, it is not an arbitrary assigned frame. · OAI.DukePrimeDegree.matrixVelocitySpace
matrixVertex def: A matrix as an actual Grassmann vertex on ell + m binary coordinates. · OAI.MaxCutGames.Inverse.MatrixChart.matrixVertex
matrixVertex def: A matrix as an actual Grassmann vertex on ell + m binary coordinates. · OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrixVertex
MatrixVertexChartNeighbors abbrev: Actual Grassmann vertices adjacent to matrixVertex M and remaining inside the finite matrix chart. · OAI.MaxCutGames.Inverse.MatrixChart.MatrixVertexChartNeighbors
MatrixVertexChartNeighbors abbrev: Actual Grassmann vertices adjacent to matrixVertex M and remaining inside the finite matrix chart. · OAI.UniqueGamesTheorem.Inverse.MatrixChart.MatrixVertexChartNeighbors
matrixVonNeumann def: Finite matrices over P, constructed as an actual double-commutant algebra. · OAI.KadisonSimilarity.matrixVonNeumann
matrixVonNeumannEquiv def: The usual C-star matrix algebra over P is star-isomorphic to its constructed concrete von Neumann realization. · OAI.KadisonSimilarity.matrixVonNeumannEquiv
MatrixWordCovariance structure: Isometric simultaneous-conjugation covariance on source and test words. These are local actions on the realized tensor words, not coefficient formulas. · OAI.KadisonSimilarity.MatrixWordCovariance
matrixZeroPadding def: A square matrix with zero entries outside the embedded index set. · OAI.KadisonSimilarity.matrixZeroPadding
matrixZeroPaddingHom def: The algebraic zero-padding map, before assigning the C-star matrix norm. · OAI.KadisonSimilarity.matrixZeroPaddingHom
maxCut def: The maximum over all Boolean cuts of the finite vertex set. · OAI.OptimalMaxCut.Graph.maxCut
maxEmission def: The fixed maximum word length bounds pushes in each emitted statement. · OAI.MaxCutGames.Reduction.MachineSubstitution.maxEmission
maxEmission def: A finite maximum depending only on the fixed emission table. · OAI.MaxCutGames.Reduction.MachineTransducer.maxEmission
maxEmission def: The fixed maximum word length bounds pushes in each emitted statement. · OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.maxEmission
maxEmission def: A finite maximum depending only on the fixed emission table. · OAI.UniqueGamesTheorem.Reduction.MachineTransducer.maxEmission
maximal def: The actual centered disk maximal function, over every positive real radius. · OAI.CenteredDiskEndpoint.maximal
maximal def: The actual centered disk maximal function, over every positive real radius. · OAI.SignedDisk.CenteredDiskEndpoint.maximal
maximalCell def: The closed weak-maximizer cell of a continuous finite family. · OAI.Problem358.ClosedCoverConnectivity.maximalCell
MaximalCentralPartition structure: A maximal family satisfying P, together with its actual central complement. · OAI.BoundedHochschild.KadisonRingrose.MaximalCentralPartition
maximalOrderSpan def: The maximal-order span of an integer lattice. · OAI.DukePrimeDegree.maximalOrderSpan
maximalPatchNet def: A concrete finite maximal-cardinality net. · OAI.RegularPointCoordinates.maximalPatchNet
maximalReal def: Real representative; the endpoint also asserts that maximal f is finite a.e. · OAI.CenteredDiskEndpoint.maximalReal
maximalReal def: Real representative; the endpoint also asserts that maximal f is finite a.e. · OAI.SignedDisk.CenteredDiskEndpoint.maximalReal
maximalSobolevInteractionDomain def: The union of every classical solution interval through the prescribed datum. · OAI.DefocusingNLS.maximalSobolevInteractionDomain
maximalSobolevInteractionFlow def: The unique value supplied by any classical solution patch containing the time. · OAI.DefocusingNLS.maximalSobolevInteractionFlow
maximalSobolevSchrodingerFlow def: Return the maximal interaction solution to the physical Schrödinger variable. · OAI.DefocusingNLS.maximalSobolevSchrodingerFlow
Maximizes def: An index is active when its affine form dominates every other form. · OAI.Problem358.FiniteAffine.Maximizes
maximizingPredecessor def: The actual maximizing predecessor; the finite choice includes the empty set. · OAI.LeanBlast.SecondKahnKalai.maximizingPredecessor
maximizingSubset def: A deterministic classical choice of a maximizer over all subsets of I. The empty set is included, so this definition also applies to empty I. · OAI.LeanBlast.SecondKahnKalai.maximizingSubset
maximum def: A finite upper bound for every generator occurrence. · OAI.Thomason.Construction.StrictOmegaCategory.ExpressionDegree.maximum
maximum def: The maximum multiplicity is present exactly in the active components. · OAI.TorsionFreeZeroDivisors.LinkComponents.maximum
maxLabel def: Combine the two ordered endpoint labels by maximum. · OAI.Thomason.Construction.StrictOmegaCategory.maxLabel
maxLabelFiberIso def: The joint zero-fibre is the original full intersection. · OAI.Thomason.Construction.StrictOmegaCategory.maxLabelFiberIso
MaxOrthogonal abbrev: MaxOrthogonals are self-orthogonal subspaces, equivalently isotropic subspaces of half the ambient dimension. · OAI.SidorenkoCounterexample.MaxOrthogonal
maxRepresentative def: A maximum-weight representative of each nonempty unsigned class. · OAI.HyperbolicObstruction.Coincidence.maxRepresentative
maxSatisfied def: The maximum number of satisfied occurrences among all vertex labelings. · OAI.MaxCutGames.Integration.InstanceValue.maxSatisfied
maxSatisfied def: The maximum number of satisfied occurrences among all vertex labelings. · OAI.UniqueGamesTheorem.Integration.InstanceValue.maxSatisfied
maxScale def: The largest admissible scale; its irrelevant nonpositive-density value is zero. · OAI.TalagrandThreshold.maxScale
maxSum def: The nonnegative running maximum of the partial sums of a stationary observable. · OAI.FKCRT.Stationary.maxSum
maxTensorNorm def: The maximal C*-tensor norm: supremum over commuting representations. · OAI.NuclearUltrapower.maxTensorNorm
maxValue def: The maximum of a nonempty finite family of real-valued functions. · OAI.Problem358.FiniteMaxDerivative.maxValue
mayerVietoris_equiv def: No cellular theorem is assumed: this is the comparison for actual open sets in an actually contractible space, proved by finite singular subdivision. · OAI.EilenbergGanea.CubicalSingular.mayerVietoris_equiv
Mean structure: A normalized positive translation-invariant real functional. · OAI.EuclideanFiveColor.Amenable.Mean
mean def: Expectation for the uniform sign probability, written as iterated fair averages. · OAI.DiamondDistortion.SignCube.mean
mean def: Spherical means in the probability normalization. · OAI.PettyProjection.Spherical.mean
mean def: The invariant mean, as the limit of the multiplicity-preserving averages. · OAI.PlaneFiveColor.InvariantMean.mean
meanAt def: The invariant meanAt b, as the limit of the multiplicity-preserving averages. · OAI.EuclideanFiveColor.MovingMean.meanAt
meanAt def: The actual dyadic mean Gram, using an already constructed exact frame only to certify its invertibility. · OAI.RegularPointCoordinates.RegularBilinearData.meanAt
meanCLM def: A normalized positive shift-invariant continuous real linear functional. · OAI.EuclideanFiveColor.MovingMean.meanCLM
meanCLM def: A normalized positive shift-invariant continuous real linear functional. · OAI.PlaneFiveColor.InvariantMean.meanCLM
meanCoefficient def: Apply the scalar expectation to the actual coefficient family. · OAI.KadisonKastler.UniformMeasurableOperators.meanCoefficient
meanCorrection def: Averaging the bounded increments gives an additive homomorphism. · OAI.PolycyclicRecognition.meanCorrection
meanDeficiency def: Mean deficiency of a uniform size-v subset of U. · OAI.LowSpaceSubsetSum.meanDeficiency
meanExponent def: The mean of the character's three singleton-leg exponents. · OAI.MatrixMultiplication.AuxiliarySeparation.Character.meanExponent
meanGradientVector def: The vector of mean gradient pairings with the coordinate columns. It is defined using the canonical Sobolev Gram, not chosen coefficients. · OAI.RegularPointCoordinates.meanGradientVector
meanGramEquiv def: The mean Gram itself, with the inverse supplied by its proved nondegeneracy. This is independent of which exact normalizer witnesses it. · OAI.RegularPointCoordinates.meanGramEquiv
meanKernel def: The scalar boundary mean supplies all data of the bounded operator kernel. · OAI.KadisonKastler.UniformMeasurableOperators.meanKernel
meanL2 def: Integration is the continuous L2 pairing with the constant one. · OAI.DukePrimeDegree.meanL2
meanMass def: The unconditional spin-pattern distribution, not a conditional law. · OAI.DilutedSpinGlass.Pattern.meanMass
meanPassageSequence def: Mean passage time along an integer lattice direction, indexed by natural steps. · OAI.GammaFPP.meanPassageSequence
meanStabilizer def: The left translations preserving a linear averaging functional form a subgroup. · OAI.PolycyclicRecognition.meanStabilizer
meanZero def: The full complex subspace defined by zero Lebesgue integral. · OAI.ThreeTorus.meanZero
measurableOperatorSubalgebra def: Measurable operator fields form a star subalgebra. · OAI.KadisonKastler.measurableOperatorSubalgebra
MeasurablePartition structure: A finite measurable partition, allowing empty atoms. · OAI.DukePrimeDegree.MeasurablePartition
measurableProjectionFrame def: The normalized Gram-Schmidt vectors of a measurable projection field. · OAI.KadisonKastler.measurableProjectionFrame
measurableProjectionOperator def: An actual orthogonal projection from a strongly measurable projection field; no separate uniform-bound hypothesis is required. · OAI.KadisonSimilarity.measurableProjectionOperator
measurableUnitaryRepresentative def: Bundle an everywhere unitary field from measurable evaluations. · OAI.KadisonKastler.measurableUnitaryRepresentative
measure def: A strictly decreasing validator measure, valid for every dirty sector. · OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.measure
measure def: The Borel measure furnished by the proved compact content. · OAI.Kaplansky.PositiveDimensionFunctional.measure
measure def: The probability measure represented by the finite coordinates. · OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.measure
measure def: A rank measure associated with a linear family of linear maps. · OAI.Problem335.RankMeasure.measure
measure def: The probability law obtained by normalizing the restriction to a positive finite cell. · OAI.Problem358.NormalizedCell.measure
measure def: Every diagonal signed measure is converted to an actual positive finite measure, rather than replaced by a density with respect to volume. · OAI.RegularPointCoordinates.PositiveBilinearMeasure.measure
MeasuredCone structure: The concrete groups, maps and compatible measures for one cone. · OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone
measuredFront def: Initialize and read one padded row, directly from the shared arrays. · OAI.LowSpaceSubsetSum.FilteredStream.measuredFront
measuredIndex def: Little-endian binary evaluation. The cost includes access to a bit in a path built by at most d nested Fin.cons nodes. · OAI.LowSpaceSubsetSum.PaddedRows.measuredIndex
measureDistance def: Convergence-in-measure distance on L1 equivalence classes. · OAI.ExactModuli.measureDistance
MeasuredProbeRegions structure: One section and three containing regions, with their actual measure bounds. The ideal exponent is fixed while the loss is subexponential. · OAI.PolycyclicRecognition.MeasuredProbeRegions
measuredRun def: The accumulator makes the search loop tail recursive. · OAI.LowSpaceSubsetSum.BinaryPivot.measuredRun
MeasuredTransportData structure: Bounded source measures, optimal transport plans, compression estimates, and convergence of their Euclidean pushforwards. · OAI.RegularPointCoordinates.MeasuredTransportData
measureFamilyModulus def: Pointwise admissibility, including infinite values on reference-null sets. · OAI.CircleDomainRigidity.measureFamilyModulus
MeasureImageDuality def: The measure-image conclusion of ADMS Theorem 5.1 and Corollary 5.2(b). · OAI.CircleDomainRigidity.MeasureImageDuality
measurement def: Apply the real matrix whose rows encode the strip constraints. · OAI.SymmetricMahler.measurement
measurePair def: The genuine unpolarized cosine pairing of two (not necessarily even) measures. · OAI.PettyProjection.measurePair
MeasurePlanLifting def: The probability-lifting consequence of the cited measurable selector. · OAI.CircleDomainRigidity.MeasurePlanLifting
MeasurePrecompactBall def: Finite covers of the entire unit ball in convergence-in-measure distance. · OAI.ExactModuli.MeasurePrecompactBall
medianEstimatorBits def: Each complete estimator uses constant confidence; the requested failure probability changes only the number of independent medians. · OAI.ContingencyTables.CompanionOracleDensity.medianEstimatorBits
mediatorCompression def: Restriction to original spins tensored with all mediator singlets. · OAI.ContinuumCoulomb.mediatorCompression
mediatorContraction def: Compression of the square of the two-spoke coupling to the normalized mediator singlet. The first matrix factors act on the external pair; the matrix elements contract the mediator pair. · OAI.ContinuumCoulomb.mediatorContraction
mediatorEdgeSpoke def: The two physical spokes incident to one original edge. The left spoke uses the first mediator member; the right can use either member. · OAI.ContinuumCoulomb.mediatorEdgeSpoke
mediatorInverseWeight def: Full inverse on the triplet complement and zero on the singlet kernel. · OAI.ContinuumCoulomb.mediatorInverseWeight
mediatorLocal def: An operator acting on one actual fresh pair, with identity on all others. · OAI.ContinuumCoulomb.mediatorLocal
mediatorSecondOrder def: The inverse of the unit mediator penalty is 1/4 on the excited space, and every spoke takes the singlet there. The contraction hence has the negative second-order prefactor -v²/4. · OAI.ContinuumCoulomb.mediatorSecondOrder
mediatorTensor def: Tensor product over the actual four-state mediator pairs. · OAI.ContinuumCoulomb.mediatorTensor
Meet def: The bounded intersection makes the empty meet the typed top. · OAI.PureTypeSystem.Candidates.Meet
meet def: Intersection is again one brick: take the longer prefix at each coordinate. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.meet
mellinCoefficient def: Probability-normalized Mellin coefficient on the nonzero field elements. · OAI.Ostmann.mellinCoefficient
mellinPacket def: A smoothed logarithmic window, retaining the literal coefficients. · OAI.JointDickman.mellinPacket
mellinPolynomial def: The reciprocal-weighted Dirichlet polynomial in Fourier normalization. · OAI.JointDickman.mellinPolynomial
member def: Freeze the equality implementation at the abstract element type. Nested lists may otherwise elaborate different, extensionally equal BEq instances. · OAI.Superstring.BitCode.member
memberDecisions def: Conditions which either contain an atomic membership witness or exclude membership at every strengthening. · OAI.PartitionConsistency.SetForcingNames.AtomicForcing.memberDecisions
Membership def: Membership on the quotient is independent of both representatives. · OAI.PartitionConsistency.ForcingQuotient.AtomicData.Membership
membershipLabel def: The sieve membership label in every positive finite dimension. · OAI.Thomason.Construction.FiniteReflectionInput.membershipLabel
membershipLabel def: The actual strict walking-arrow label associated to a poset sieve. · OAI.Thomason.Construction.NormalizedSimplexIdentities.membershipLabel
membershipLinear def: Membership is an internal strict linear order on a. · OAI.PartitionConsistency.SetLanguage.membershipLinear
membershipWellFounded def: Every nonempty internal subset of a has a membership-minimal element. This does NOT assert external well-foundedness of the relation. · OAI.PartitionConsistency.SetLanguage.membershipWellFounded
MemG def: Membership before descent to equivalence classes. · OAI.PartitionConsistency.ForcingQuotient.AtomicData.MemG
memo def: Eliminate repeated queries against an explicit exposure record. Repeated forced bits test compatibility but acquire no likelihood-ratio factor. · OAI.CubeShuffle.QueryTree.memo
Memory abbrev: Finite private memory, sufficient for a fixed local experiment. The final policy is extended to all requests; compactness below removes this bound. · OAI.KServer.BoundedSimulation.Memory
memory def: Every unnamed work tape is empty at these phase boundaries. · OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory
memory def: The archives, family count, and level residue are the only retained non-output stacks. Work stacks, including unused duplicate slots, are empty. · OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.memory
memory def: All unnamed work stacks are empty at the phase boundaries below. · OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.memory
memory def: Every unnamed work tape is empty at these phase boundaries. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory
memory def: The archives, family count, and level residue are the only retained non-output stacks. Work stacks, including unused duplicate slots, are empty. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.memory
memory def: All unnamed work stacks are empty at the phase boundaries below. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.memory
merge def: Flatten (comb (m+1), comb (n+1)) to the right comb. As every nonempty object is positive, the value only depends on the size of the left block. · OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.merge
merge def: One literal recursive step: every separator vertex becomes a singleton, while the two nonadjacent sides retain their recursively constructed parts. · OAI.HyperbolicObstruction.PlanarRecursion.CutPartition.merge
merge def: Reversal retains the same three whole ports, with all their orientations reversed according to the source merge convention. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep.merge
merge def: The merge retains its input tails, one continuation per selected head, and the newly constructed result spine. · OAI.LowSpaceSubsetSum.MeasuredSortSpace.merge
mergeBlack def: The color-reversed local surgery. · OAI.KaplanskyCounterexample.Planar.Ribbon.mergeBlack
mergeClass def: Identify two classes of a partition, by redirecting the second to the first. · OAI.KaplanskyCounterexample.Planar.mergeClass
mergeColumnRuns def: A true bit consumes a regular segment; a false bit consumes one omitted run. Unused trailing bits have no effect. · OAI.TwoPointCorrelations.mergeColumnRuns
mergeCycleEquiv def: Joining two different cycles deletes exactly one vertex. · OAI.KaplanskyCounterexample.Planar.mergeCycleEquiv
mergedClass def: The quotient of the old vertex set that identifies precisely the two vertices joined by the transposition. · OAI.KaplanskyCounterexample.Planar.mergedClass
mergedCoefficient def: A finite merged coefficient. phase can incorporate a translation character and the indicator of one restriction fiber. · OAI.MaxCutGames.Appendix.Level.mergedCoefficient
mergedCoefficient def: A finite merged coefficient. phase can incorporate a translation character and the indicator of one restriction fiber. · OAI.UniqueGamesTheorem.Appendix.Level.mergedCoefficient
mergeEdge def: Delete the paired sides and join the remaining oriented boundaries. Unlike cancellation of an entire equal pair of cells, this works when the remaining boundaries differ. · OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge
mergeLabelings def: Two independently chosen side labelings give one total labeling because every vertex has exactly one Boolean side. Isolated vertices cause no exception. · OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.mergeLabelings
mergeLabelings def: Two independently chosen side labelings give one total labeling because every vertex has exactly one Boolean side. Isolated vertices cause no exception. · OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.mergeLabelings
Merger abbrev: The extension is constructed, not postulated: its elements are the normal forms over the actual prescribed quotient. · OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Merger
mergerHeightCost def: The height and cost extension for the literal finite nonempty merger, not an assumed extension and not merely a margin on the adjoined roots. · OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.mergerHeightCost
mergerSimulation def: Simulate exactly the smaller merger presentation in the larger base, using the same prescribed overlap starts. · OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.mergerSimulation
MergeSide structure: The common side of two distinct, non-monogon faces. These are local incidence hypotheses, not any normalization or genus conclusion. · OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide
mergeWhite def: Local surgery merging two white vertices along consecutive black edges. The newly created digon is a one-cycle of the face permutation. · OAI.KaplanskyCounterexample.Planar.Ribbon.mergeWhite
MertensHarmonicEstimate def: Precise published Mertens-second input, weaker than its convergent-error form and sufficient for the favorable-prime harmonic mass. · OAI.Ostmann.MertensHarmonicEstimate
MertensLowerBound def: The precise one-sided consequence of Mertens' first theorem needed by the collision argument. C is fixed independently of the cutoff. · OAI.Ostmann.MertensLowerBound
mesh def: Lattice mesh and actual sampled heights, not a reference density. · OAI.FKCRT.SimpleWalk.mesh
mesh def: The actual exponential second-system mesh, using the selected base. · OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh
meshContractionMatrix def: The contraction coefficient is the positive square root used in the essential-path representation of the mesh algebra. · OAI.HarmonicArtin.ParabolicIntersections.meshContractionMatrix
meshEdgeFlip def: Reversal of an oriented edge exchanges the two endpoint sums. · OAI.HarmonicArtin.ParabolicIntersections.meshEdgeFlip
meshExtendMatrix def: Extending a prefix operator by one edge, without changing that edge. · OAI.HarmonicArtin.ParabolicIntersections.meshExtendMatrix
meshInsertBacktrack def: Attach the last two edges v,u,v to a path ending at v. · OAI.HarmonicArtin.ParabolicIntersections.meshInsertBacktrack
MeshNilpotent def: Exact abstract algebra input: sufficiently long positive words lie in the two-sided ideal generated by the mesh relations. · OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent
MeshPaths def: Paths of length n, indexed by their final vertex. The recursive presentation makes extension of prefix operators a block-diagonal map. · OAI.HarmonicArtin.ParabolicIntersections.MeshPaths
meshProjection def: The correction formula removes precisely the final contraction from the already projected prefix. Only positive-index quantum integers occur as denominators before the cutoff. · OAI.HarmonicArtin.ParabolicIntersections.meshProjection
meshQuantum def: Quantum integers as a real recurrence, with no trigonometric choices. · OAI.HarmonicArtin.ParabolicIntersections.meshQuantum
MetadataBinomialCaps def: Numerical binomial caps extracted from the literal known/hidden metadata. In applications these are proved using the source hidden-trial lower bounds. · OAI.TraceReconstruction.MetadataBinomialCaps
MetadataSmoothingCap def: A purely numerical typical-metadata condition on every local collection. It includes unoccupied vertices and is fixed before a coefficient is chosen. · OAI.TraceReconstruction.MetadataSmoothingCap
MetaplecticCoefficientBounds def: Support read from (5.79), avoiding the repeated ramified exponent in the printed (5.67). The coefficient bound follows from (5.7), (5.13), (5.14). The two supported factors may have arbitrarily large exponents. · OAI.CubicFirstMoment.MetaplecticCoefficientBounds
metaplecticCompletionWeight def: The precise inverse-completion weight, including the norm phase created by replacing the length by U / (Nc)^3. · OAI.CubicFirstMoment.metaplecticCompletionWeight
MetaplecticContinuation def: The needed continuation/residue consequence of DR2024 Proposition 5.2, after the nonvanishing Euler factor in Re s>1/2 is removed. · OAI.CubicFirstMoment.MetaplecticContinuation
metaplecticIdealLocalWeight def: The absolute supported-prime factor in terms of genuine ideal exponents. The first ideal is squarefree; the second carries the cubes. · OAI.CubicFirstMoment.metaplecticIdealLocalWeight
metaplecticLocalCoefficient def: Equation (5.68), written as its exact squarefree Euler product. · OAI.CubicFirstMoment.metaplecticLocalCoefficient
MetaplecticMeanSquare def: HB2000 §3 Lemma 3, angular index zero, with only its actual vertical mean-square bound as the published hypothesis. · OAI.CubicFirstMoment.MetaplecticMeanSquare
metaplecticPrimalCoefficient def: The literal primal summand before its norm-phase, as in the published completed sum. · OAI.CubicFirstMoment.metaplecticPrimalCoefficient
metaplecticTransform def: Equation (5.81), parameterized on the vertical line Re s = -sigma. · OAI.CubicFirstMoment.metaplecticTransform
MetaplecticVoronoiInput def: The only new analytic identity assumed here is DR Proposition 5.3. Its absolute convergence is part of the published proof of (5.80). The input retains the actual transform, frequency lattice, local Euler coefficients and global … · OAI.CubicFirstMoment.MetaplecticVoronoiInput
Meter structure: A convenience for the different integrated-error sums. · OAI.ExactDerandomization.Analysis.Meter
metric def: The canonical word metric agrees with WordDistance. · OAI.HyperbolicObstruction.WordDistance.metric
metric def: On metrics with linear chains and finite balls, an actual discrete coarse equivalence is a metric quasi-equivalence. · OAI.PolycyclicRecognition.GroupCoarseEquivalence.metric
metricBad def: All and only the three exceptional events needed for the original map comparison: impossible marks (a null set), a macroscopic core, and a large uniform ancestral distance error. · OAI.FKCRT.Inventory.metricBad
metricBasis def: An ordinary linear basis supplies the complete orthonormal basis; no orthonormal-frame existence hypothesis is used. · OAI.Kaplansky.metricBasis
metricCoefficients def: Metric coefficients in a chart. Only values in the chart target are used. · OAI.YauCounterexamples.metricCoefficients
metricConnectionAt def: The three symmetric Christoffel slots, with values in the coordinate tangent plane, computed from the metric and its first derivatives. · OAI.ClosedSurfaceR4.PhaseGeometry.metricConnectionAt
MetricCore structure: Exactly the core path distances in Proposition configuration (i). The third condition uses distinct fields and the actual fan quota; the exceptional loose edge is not charged to the D fan. · OAI.HyperbolicObstruction.CoreGeometry.MetricCore
metricCount def: Counting measure of a labeled configuration; repetitions contribute separately. · OAI.KServer.FiniteExperiment.metricCount
MetricDoubleCover structure: Raw data of a Riemannian two-sheeted cover. distance_lift is the endpoint of a lift of a minimizing base geodesic from the specified point; the other distance inequality is length preservation under projection. · OAI.PositiveEinsteinFour.MetricDoubleCover
metricEnergy def: Sum of the two coordinate energy contributions in an eigenframe. · OAI.CircleDomainRigidity.FiniteTransfer.metricEnergy
metricEntropy def: Kolmogorov--Sinai entropy, as the supremum over finite measurable partitions. · OAI.DukePrimeDegree.metricEntropy
MetricFirstJet abbrev: A metric value together with its first coordinate derivative. · OAI.ClosedSurfaceR4.PhaseGeometry.MetricFirstJet
MetricFrameMoments structure: The actual frame moments in the normalization of balanced_moments: its volume variable is twice the round-sphere volume ratio. · OAI.PositiveEinsteinFour.Geometry.MetricFrameMoments
MetricGreenData structure: Petersen's tensor commutators and ordinary differentiation in parallel frames, with Brin--Karcher measure-preserving flows. Ricci is normalized to 3g; the last two curvature entries are reversed for the covector action. The normalization … · OAI.PositiveEinsteinFour.Geometry.MetricGreenData
MetricHexagon structure: Six cyclic vertices, with exactly the path information obtained from the square decorations and admissible three-edge paths. · OAI.HyperbolicObstruction.MetricHexagon
metricIterate def: The actual coordinate iteration, starting from the identity. · OAI.RegularPointCoordinates.metricIterate
metricMean def: The source block-distance mean; finiteness uses only offspring variance. · OAI.FKCRT.Inventory.metricMean
MetricMeasureData structure: Unbundled presentation of a measured metric space; validity is specified below. · OAI.FKCRT.MetricMeasureData
MetricQuasiEquivalence structure: Actual coarse inverse maps with affine metric bounds in both directions. · OAI.PolycyclicRecognition.MetricQuasiEquivalence
metricSpace def: The exact source graph metric, on the original vertex type. · OAI.PlanarL1.Weighted.metricSpace
metricSpeed def: Metric speed. Limsup agrees a.e. with the metric derivative on AC² curves. · OAI.WeakHessian.metricSpeed
MetricSquare structure: Squared metric data for the unit square, in cyclic order. · OAI.HyperbolicObstruction.MetricSquare
metricVolume def: Riemannian volume calibrated to Lebesgue measure in Euclidean space. · OAI.WeakMTWTransport.metricVolume
mid def: Metric midpoint, available without completeness or properness. · OAI.HyperbolicObstruction.CATZero.mid
Middle abbrev: Block-entry gates: block number and two matrix indices. · OAI.Problem335.BlockData.Middle
middle def: These two finite programs are independent of dimensions and margins. · OAI.ContingencyTables.ExactPublicPrefix.middle
MiddleBranch def: Parametrization of the middle copy with the second and third legs exchanged. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch
middleLeftComplex def: The genuine left tensor complex, with its left A-action. · OAI.LittleFinitistic.middleLeftComplex
middleLeftFunctor def: Tensor by the fixed middle bimodule, retaining its actual left action. · OAI.LittleFinitistic.middleLeftFunctor
middleLevel def: Positive integers in the open-closed interval between adjacent cutoffs. · OAI.Problem337.GeometricRandomRanges.middleLevel
middleMap def: The second local map assigns weight one to the middle interval. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleMap
middleMomentError def: A_i is zero for an empty middle segment, since its sole coefficient is centered. · OAI.Generator.Tracial.middleMomentError
middleObstacle def: Obstacles for the middle of an edge: all vertices and the radial heads of every other unoriented edge. · OAI.PlanarL1.Topology.Drawing.middleObstacle
middleRightComplex def: The genuine right tensor complex, with its right B-action. · OAI.LittleFinitistic.middleRightComplex
middleRightFunctor def: Tensor a right module by the middle bimodule, retaining its actual right action. · OAI.LittleFinitistic.middleRightFunctor
middleSwap def: The four-leaf middle transposition, expressed only in associator, symmetry and binary tensor; its naturality is needed in the colour-orbit reduction. · OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.middleSwap
middleTensor def: The middle retained branch; its first leg is the actual shared first leg. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor
middleTests def: Only levels whose denominator factor is one need a random block. · OAI.Problem337.GeometricRandomRanges.middleTests
middleValue def: Value of a middle sum gate before relabelling the gate types. · OAI.Problem335.IndexedDepth5Circuit.middleValue
middleWordFamily def: The uncompressed middle coefficient between the first two patch letters. Every coefficient here is internal to the original word. · OAI.Generator.Tracial.middleWordFamily
MiddleY def: The middle interval on the second tensor leg. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleY
middleY def: Embed the middle second-leg interval, which carries the convolution output. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleY
MiddleZ def: The middle interval on the third tensor leg. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleZ
middleZ def: Embed the middle third-leg interval, which carries the second input. · OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleZ
midpoint def: The coupled midpoint of two samplers driven by the same parameter tuple. · OAI.Problem358.TriangularRecursion.midpoint
MidpointComparisonData structure: Geometric data sufficient for one symmetric cell-moment comparison. In particular, midpoint_dominated records the difficult geometric input. · OAI.Problem358.StationaryMoment.MidpointComparisonData
midpointComparisonData_of_normalized_cells def: Actual normalized couplings of three cell partitions supply the moment comparison data. All measure-scaling, partition, boundedness and raw-moment identities follow from their definitions; midpoint domination remains the explicit geometric … · OAI.Problem358.StationaryMoment.midpointComparisonData_of_normalized_cells
midpointComparisonData_of_pair_couplings def: Construct the abstract moment witness directly from genuine pair couplings of the three finite cell partitions. Squared-integrability and the moment identity are consequences, rather than extra assumptions. · OAI.Problem358.StationaryMoment.midpointComparisonData_of_pair_couplings
midpointFiber def: The last-coordinate midpoint fibre, with the original input prefix as parameter. · OAI.Problem358.TriangularRecursion.midpointFiber
midpointRootRaw def: Equalize the selected two coordinates while keeping all other coordinates at their original ordered values. · OAI.DukePrimeDegree.midpointRootRaw
midpointSet def: The exact midpoint image, without a convexity assumption. · OAI.RegularPointCoordinates.midpointSet
midpointSupportFactor def: The volume factor from the two separately bounded endpoint densities. · OAI.RegularPointCoordinates.midpointSupportFactor
Mild def: Known large first values don't cross the capped thresholds when relative prefix errors are small. Keep track of the discrepancy from the raw prefix at such locations. · OAI.ExactDerandomization.Buf.Run.Mild
MildAE def: The mild identity on every time slice, with spatial null sets allowed to depend on time. · OAI.BoltzmannNonuniqueness.WeightedLocal.MildAE
MildCollisionSolution structure: The characteristic identity uses the full physical collision terms and the prescribed initial density. The spacetime identity determines a continuous-time representative through the Bochner integral of the collision source. · OAI.BoltzmannNonuniqueness.MildCollisionSolution
mildSolution def: The uniquely determined continuous solution at a fixed finite jet order. · OAI.ForcedComputation.PlaneScalarMild.mildSolution
minimalCyclicRetraction def: The concrete ambient-to-algebra retraction supplied by a minimal projection. · OAI.KadisonKastler.minimalCyclicRetraction
MinimalInvariant def: Minimality concerns genuine norm-closed convex invariant subsets. · OAI.ReflexiveFixedPoints.MinimalInvariant
MinimalInvariantData structure: Structural conclusions obtained from a genuine fixed-point-free map. · OAI.ReflexiveFixedPoints.MinimalInvariantData
minimalSpatialEvaluation def: Evaluation at one of the spatial representations defining the norm. · OAI.WeakPureInfiniteness.minimalSpatialEvaluation
MinimalWord def: Minimality refers to numerical words and permits reversing every shorter contiguous subword. · OAI.TwoPointCorrelations.MinimalWord
minimizer def: A canonical tie-break using choice is legitimate on the finite input tree. · OAI.KServer.Pilot.minimizer
minimizingFiniteLabel def: Fix one minimizing label at every parameter value. · OAI.PolycyclicRecognition.minimizingFiniteLabel
minimum def: Finite minimum of the clipped ramps, with value 1 for an empty roster. · OAI.KServer.RosterExpectation.minimum
minimum def: A positive augmented chain contraction, requiring no abstract Gray input. · OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimum
minimumCoordinate def: The least coordinate in a positive-dimensional exponent vector. · OAI.Problem326.Affine.minimumCoordinate
minimumDistance def: The minimum squared distance over the frequency interval [-X, X]. · OAI.JointDickman.PublishedInputs.minimumDistance
minimumMap def: The chain map induced by minimum on the two right interval factors. · OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimumMap
minimumNet def: Pair costly subnets ONCE before comparing; the recursive minimum is not copied into each arm of the mux. This gives a linear, not exponential, scan. · OAI.ExactQuantumFactoring.OrderTrial.minimumNet
minimumRoot def: The bin-minimizing root need not be present at a given stage. · OAI.TorsionFreeZeroDivisors.LinkComponents.minimumRoot
minLabel def: Minimum combines membership in two full one fibres. · OAI.Thomason.Construction.StrictOmegaCategory.minLabel
minNamed def: Minima and maxima both resolve ties toward the earliest atom name. · OAI.PlanarL1.Interpolation.minNamed
minorantGap def: Explicit gap from the finite-time minorant; its value depends only on the finite group law, not on the dimension of any represented space. · OAI.CubeShuffle.UnitaryFinite.minorantGap
minorArcGeometricBound def: The resonant case is kept explicit, rather than assigning an infinite value to a reciprocal at zero. · OAI.TwoPointCorrelations.minorArcGeometricBound
minorArcs def: The logarithmic minor arcs, with the denominator cutoff needed to save D powers of the logarithm in the actual Mangoldt exponential sum. · OAI.Problem337.MangoldtMinorArcActual.minorArcs
minorArcWindowInterval def: The upper cofactor cutoff is exclusive. · OAI.TwoPointCorrelations.minorArcWindowInterval
minorityCutEmbedding def: The tail label determines the forgotten minority color. · OAI.MaxCutGames.Foundations.PCP.CloudRounding.minorityCutEmbedding
minorityCutEmbedding def: The tail label determines the forgotten minority color. · OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.minorityCutEmbedding
minorPolynomial def: Full-column-size minor polynomial, with rows selected by s. Repeated row selections cause no problem and require no artificial ordering of the finite column set. · OAI.Nagata.W27.minorPolynomial
minted def: number born before cap breach; representatives from these births may be retained for delayed estimates on further jumps · OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.minted
minTensorNorm def: The minimal C*-tensor norm: supremum over spatial representations. · OAI.NuclearUltrapower.minTensorNorm
minTraceTV def: The real infimum is a minimum for n>0 (a nonempty finite set). · OAI.TraceReconstruction.minTraceTV
MintV structure: Scalar prices determined before unfolding predecessor calls. · OAI.ExactDerandomization.SiteX.MintV
minusDerivativeCurvatureForm def: The anti-self-dual curvature term, with the normalization of equation (11). · OAI.PositiveEinsteinFour.HighestHessian.minusDerivativeCurvatureForm
minusI def: Integer arithmetic at grid points. The only root of unity is -i. · OAI.ExactQuantumFactoring.OrderTrial.minusI
minusPos def: The minus class, identified with the plus class exactly at the leaf. · OAI.Problem348.TreePositions.minusPos
minusShear def: Subtract the transformed remainder from the independent new variable. · OAI.StableCoordinate.Linearization.minusShear
minusWeyl def: The anti-self-dual Weyl block in the same concrete frame. · OAI.PositiveEinsteinFour.Geometry.minusWeyl
minusWeylGradient def: The opposite block is differentiated in the same actual coordinate connection, before the orthonormal frame and Hodge basis are applied. · OAI.PositiveEinsteinFour.Geometry.minusWeylGradient
mirror def: Reversal of all child orders, without imposing any symmetry on marks. · OAI.FKCRT.TreeCoding.PlaneTree.mirror
mirror def: Reflection reverses every face orientation; side pairs are unchanged. · OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mirror
mirror def: Mirror all internal sewing, without losing any transverse branch port. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.mirror
mirror def: The mirror uses the same color on the same literal occurrence. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.mirror
mirror def: The orientation reverse is again one of the literal allowed vertices. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.mirror
mirror def: Reverse the orientation of the whole filling, not just its boundary word. · OAI.Release075.TriangleFilling.mirror
MirrorAdjacentSeamsAgree def: Adjacent reflected ports attach to the same seam. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorAdjacentSeamsAgree
mirrorAlignedFrame def: The mirror frame in the coordinate labels of the original port. · OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorAlignedFrame
MirrorChildCoordinates def: The inverse child word of the mirror short seam acts as the identity. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorChildCoordinates
MirrorChildrenMatch def: The child identifications across every reflected internal seam. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorChildrenMatch
mirrorColorGauge def: The mirror gauge changes only the principal rank fiber; lower strip fibers retain their named gauges. · OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorColorGauge
mirrorEntry def: Actual positive traversal of the new principal circle of the graft. · OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorEntry
MirrorFirstFrameCoordinates def: The initial mirror frame has the first coordinates of the identified band. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorFirstFrameCoordinates
MirrorFrameMatch def: Compatibility of the transported frames across a reflected internal seam. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorFrameMatch
MirrorFrameValuesAgree def: Equality of the two frame values on a reflected internal seam. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorFrameValuesAgree
MirrorInputAttached def: The attachment of each reflected input port. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorInputAttached
MirrorInternalFlagsHold def: The framed flag equations on every reflected internal seam. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorInternalFlagsHold
MirrorInternalSideValuesTrivial def: The side values on every reflected internal seam are trivial. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorInternalSideValuesTrivial
MirrorLastFrameCoordinates def: The terminal mirror frame has the last coordinates of the identified band. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorLastFrameCoordinates
MirrorLeftWordCoordinates def: Coordinates of the complete left word of the short mirror seam. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorLeftWordCoordinates
MirrorOutputAttached def: The attachment of each reflected output port. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorOutputAttached
MirrorParentCoordinates def: The mirror parent word has the coordinates of the conjugated cut transport. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorParentCoordinates
mirrorReflect def: Action on x=k, y=k, x+y=k for the three side reflections of the triangle x≥0, y≥0, x+y≤1 in equilateral coordinates. · OAI.ArtinCAT0.mirrorReflect
MirrorRightWordCoordinates def: Coordinates of the complete right word of the short mirror seam. · OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorRightWordCoordinates
mismatch def: Specification-only outcome, also recording an earlier mismatch. · OAI.MaxCutGames.Foundations.Complexity.MachineCompare.mismatch
mismatch def: Same-label mismatch, not a minimum matching; repetitions are allowed. · OAI.UniformKServer.mismatch
mismatch def: Specification-only outcome, also recording an earlier mismatch. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.mismatch
mismatchFiberEquiv def: Every changed dart belongs to precisely one tail fiber. · OAI.MaxCutGames.Foundations.PCP.CloudRounding.mismatchFiberEquiv
mismatchFiberEquiv def: Every changed dart belongs to precisely one tail fiber. · OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.mismatchFiberEquiv
mismatchSlots def: Exceptional slots of a vectorized commuting matrix. · OAI.CoordinateSweeps.SignedTensor.mismatchSlots
missedSup def: The amount reserved by the margin at an ordered pair. · OAI.PartitionConsistency.MonoidConstruction.missedSup
missing def: Classes whose recurrent loops are absent after replacement by z. · OAI.TwoWayComplementation.Diagram.missing
mix def: Mixture of two laws, with the real probability range explicit. · OAI.CoordinateSweeps.FiniteLaw.mix
mix def: Convex combinations preserve all density and support bounds. · OAI.DiskKernels.mix
mix def: A coherent or antichain mixture. Coherence is a property proved separately; the present construction itself is just the unrestricted union of active names. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mix
mix def: Retain the sampled leaf's node but choose the within-node offset from u. · OAI.Problem348.SampledPath.mix
mix def: Replace the within-block coordinate of a leaf by that of a second seed. · OAI.Problem348.TreeSampling.mix
mix def: Convex combinations preserve all density and support bounds. · OAI.SignedDisk.DiskKernels.mix
mixCast def: Transport the mixer to a size presented by an equality rather than a product. · OAI.Problem348.TreeSampling.mixCast
mixed def: First variable rapid (the tail layer), second moderate (Gaussian). · OAI.GeneralMahler.mixed
mixedAtom def: The mixed tensor generator is the top chain of the explicit prism atom. · OAI.Thomason.Construction.PastingGlobeBasis.mixedAtom
mixedBlock def: Mixed block of the regularized Hessian. · OAI.Problem356.LocalHessian.mixedBlock
mixedBochnerTest def: The scalar mixed Bochner test expression, before finite-span assembly. · OAI.RegularPointCoordinates.mixedBochnerTest
mixedCubic def: The primitive cubic characters occurring after cancelling common factors of two squarefree conductors. · OAI.CubicFirstMoment.mixedCubic
MixedCubicNonprincipal def: Excludes the principal character on ideals prime to the conductor. · OAI.CubicFirstMoment.MixedCubicNonprincipal
mixedDerivative def: Take Y-derivatives first, and then X-derivatives, at an ordinary affine point. · OAI.Nagata.Workers.W30.mixedDerivative
mixedGram def: Explicit mixed-moment expansion of a pair of integer linear forms. · OAI.MUB6.Certificate.GramFunctions.LinearForm.mixedGram
mixedJetAtZero def: First take b derivatives in y, then ell derivatives in x, at the origin, exactly as in the source's jet rows. · OAI.Nagata.Workers.W11.mixedJetAtZero
mixedMapFintype def: A consistent finite enumeration of actual binary linear maps, built from the finite vertex spaces. This is the enumeration used by the mixed theorem. · OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.mixedMapFintype
mixedMapFintype def: A consistent finite enumeration of actual binary linear maps, built from the finite vertex spaces. This is the enumeration used by the mixed theorem. · OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.mixedMapFintype
mixedMoment def: The real mixed moment with uniform reference, row injection, and injection of the distinct matrix labels into the six nonreference bases. · OAI.MUB6.mixedMoment
mixedMonomialMatrix def: The coefficient matrix in arbitrary selected source and target monomials. When the selections enumerate bidegree fibers, this is the restricted operator matrix in the unnormalized monomial bases. · OAI.Problem335.mixedMonomialMatrix
mixedOperator def: Substitution of derivatives on V and multiplication on its complement. This is the full operator, before taking a bidegree component or restricting to finite-dimensional homogeneous source and target spaces. · OAI.Problem335.mixedOperator
mixedPoint def: A direct index type for the ordered original and additional points. · OAI.Nagata.W06.LineArrangement.mixedPoint
mixedPosteriorKernel def: The mixed posterior keeps every unselected coordinate fixed. · OAI.FiniteFactor.CouplingParameters.mixedPosteriorKernel
mixedProb def: Mixed cell probability, including B=P without an undefined outside branch. The outside column formula is never used when B=P. · OAI.WeakPinned.Variance.mixedProb
mixedRankConstant def: A single uniform constant for all fixed-point dimensions at rank at most R. · OAI.MaxCutGames.Inverse.KMSFourthMoment.mixedRankConstant
mixedRankConstant def: A single uniform constant for all fixed-point dimensions at rank at most R. · OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixedRankConstant
mixedReferenceBand def: The actual mixed synthesis band, with the original integral coefficient and no repeated frozen selector in the synthesis profile. · OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceBand
mixedReferenceJetBand def: Actual unmasked synthesis with the original frozen analyzing coefficient and the requested covariant jet. · OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceJetBand
mixedResidueChar def: This character is defined at composite conductors, rather than supplied as an abstract character agreeing with the desired cubic symbol. · OAI.CubicFirstMoment.mixedResidueChar
mixedRootIncrement def: The actual root energy difference on appending a fresh independent block, with the ordinary physical energy held fixed. · OAI.DilutedSpinGlass.PrescribedTree.mixedRootIncrement
mixedSquarefreePrimePolynomial def: This is the actual squarefree mixed-character polynomial appearing after the independent prime factors have been expanded. · OAI.CubicFirstMoment.mixedSquarefreePrimePolynomial
mixedStepFactor def: A deliberately generous rank-dependent cost for one fixed point. · OAI.MaxCutGames.Inverse.KMSFourthMoment.mixedStepFactor
mixedStepFactor def: A deliberately generous rank-dependent cost for one fixed point. · OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixedStepFactor
mixedTensorOperator def: The finite-rank operator represented by a rectangular Hilbert tensor. · OAI.NuclearUltrapower.mixedTensorOperator
mixedVertexEvaluation def: Extend vertex values on the free orbits while retaining the prescribed orbits. · OAI.SharpLiebThirring.PLParity.mixedVertexEvaluation
mixedWordIdeal def: The span of mixed words is an actual Lie ideal, rather than an assumed quotient datum. · OAI.PolycyclicRecognition.mixedWordIdeal
MixEntries abbrev: Index the literal children of a small family, with no uniform bound on the ranks of the family's members. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.MixEntries
mixerColor def: The index of a mixer containing an input position, or the outside category. · OAI.LowSpaceSubsetSum.mixerColor
mixerCount def: This function is determined entirely by the input and the permuted mixer domain; a designated solution is not an argument. · OAI.LowSpaceSubsetSum.MixerParameterCount.mixerCount
mixerOrderFromCounts def: Sort by decreasing distinct-sum count, with the same index tie rule as the deficiency ordering in the analysis. · OAI.LowSpaceSubsetSum.mixerOrderFromCounts
mixerSize def: The block size is divisible by eight; n counts indices, not input bits. · OAI.LowSpaceSubsetSum.mixerSize
mixerSpreadTest def: The exact pairwise integer spread test; it also bounds the largest list by the smallest list times the displayed factor. · OAI.LowSpaceSubsetSum.mixerSpreadTest
mixingMatrix def: The scalar mixing involution; no group coefficients occur in it. · OAI.KervaireMixing.mixingMatrix
MixingOfOrder def: Rokhlin's multiple-mixing problem asks whether ordinary mixing of one invertible probability-preserving transformation implies mixing of every finite order. The formalization proves this implication. For each $k\ge3$ and every $k$ … · OAI.Rokhlin.MixingOfOrder
mixingTime def: First physical time with TV at most 1/4. The main conclusion proves this set nonempty for every sufficiently large d. · OAI.CubeShuffle.mixingTime
mixture def: Binary mixture; real probability t for the first option. · OAI.FourierLLogL.Law.mixture
mixture def: Literal mixture of names, with no fixed name-rank cutoff. · OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.mixture
MixtureEdges def: The index set for the mixture in the support-descent argument. Both the trigger and the original member condition are respected. · OAI.PartitionConsistency.SetForcingNames.ConditionAction.MixtureEdges
mixtureName def: A set name formed from all translates with active triggers. Using all common strengthenings is essential: a selected meet need not exist. · OAI.PartitionConsistency.SetForcingNames.ConditionAction.mixtureName
mixturePolicy def: The posterior distribution over the private mixture index is normalized only at reached histories; all null histories receive the same fixed pure rule. · OAI.KServer.mixturePolicy
mixtureProb def: Any probability mixture of source prescriptions. Full configurations index the mixture, but only their restrictions to J are used. Thus this is exactly the class of all mixtures on {-1,+1}^J. · OAI.BufferedIsing.mixtureProb
mixtureSampler def: Common direction kernel for all block-invariant spherical laws. · OAI.SubsphereCurrent.Mixture.mixtureSampler
mk def: Bundle any uniformly bounded measurable operator field. · OAI.KadisonKastler.WeakOperatorRepresentative.mk
mk def: Quotient projection for the source hypersurface. · OAI.StableCoordinate.Presentation.mk
mkEdge def: Convert a nonempty bounded path into the finite edge type. · OAI.Problem310.TreePreorder.mkEdge
modAEquivResidual def: Setting a=0 gives the domain presentation k[d,b,c,u]/(bd+1). · OAI.StableCoordinate.DeterminantPrimeA.modAEquivResidual
mode def: The positive resolvent mode belongs to the closed H¹ graph. · OAI.ContinuumCoulomb.PlanarSobolev.mode
mode def: The mode classifier used by the abstract rigidity theorem. · OAI.Problem348.Construction.SelectedAnchors.mode
mode def: Encode the mode at the edge from depth i to depth i+1. · OAI.Problem348.HostSampledPath.mode
mode def: The closed Fourier eigenspace, presented as the fixed space of the proved bounded projection rather than an assumed orthogonal decomposition. · OAI.TriangularBilliards.Analysis.CircleAction.mode
ModeBody def: One of the four mode bodies encountered at the edge from level i to level i + 1 of the selected path. · OAI.Problem348.PathPropagation.ModeBody
modeCoeff def: Downward dyadic ratio rounding, as in (mode-coefficient). · OAI.ExactQuantumFactoring.OrderTrial.modeCoeff
modeCons def: Modes are a separate syntax discipline on the labelled PTS. This keeps metatheory independent of mode well-formedness and proves preservation below. · OAI.PureTypeSystem.Labelled.modeCons
Model structure: The data and standing hypotheses of a column model. Only the actual prescribed switch heights identify columns. · OAI.PlanarL1.Columns.Model
Model structure: A concrete finite rotation map, with its exact Euler equality and an isomorphism to the represented simple graph. Loops and parallel darts are allowed; no abstract planar-minor or separator hypotheses are used. · OAI.TorsionFreeZeroDivisors.PlanarMap.Model
model def: Only initialization changes the seed; the potential and coefficient are the exact source primitives already proved affine in the raw ranks. · OAI.KServer.CausalSimplex.model
model def: One fixed genuine derived tensor functor, chosen before any test module. · OAI.LittleFinitistic.SelectedDerivedFunctor.model
model def: Choose only the concrete measured cone required by the application. · OAI.PolycyclicRecognition.CartanWordModel.PolarConeModelInputs.model
model def: The classical input constructs Mathlib's full model-category interface. The weak-equivalence class is defined by geometric realization. · OAI.Thomason.Construction.KanQuillenPublishedInput.model
model def: Assemble the genuine model-category structure with the prescribed classes. · OAI.Thomason.Construction.ProperCombinatorialAxioms.model
model def: The chain-cylinder model before extension from the finite parameters. · OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.model
model def: The conditional result supplies a genuine Mathlib model category. · OAI.Thomason.Construction.ThomasonModelResult.model
modeLabel def: The mode label of an anchor, and none for a non-anchor. · OAI.Problem348.HostAnchorRigidity.modeLabel
modelCollapse def: Collapse the interval in the global chain model. · OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.modelCollapse
modelCurry def: A concrete chain-model map gives a strict map into the actual internal hom. · OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.modelCurry
modelEndpoint def: The actual endpoint into the chain model, using the constructed unit. · OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.modelEndpoint
modelFiber def: The transverse fiber, including lower-dimensional and boundary fibers. · OAI.AffineBernstein.modelFiber
modelIso def: Literal positive-table comparison for the full pasted-globe cylinder. · OAI.Thomason.Construction.PastingGlobeCylinderBasis.modelIso
ModelIsUnimodular def: Unimodularity for the canonical Borel Haar measure of the Lie group. · OAI.PolycyclicRecognition.ModelIsUnimodular
ModelIsUnimodular def: Unimodularity of the actual Lie model, using its canonical Borel Haar measure. · OAI.PolycyclicRecognition.ModelIsUnimodular
modelLift def: Universal evaluation of the finite presentation in any proved seed data. · OAI.LittleFinitistic.FinitePresentation.modelLift
modelMap def: Extension to every model, not merely to Hilbert-space models. · OAI.NuclearUltrapower.FullGroupModel.modelMap
modelNilradicalLinearAction def: The transported linear representation. · OAI.PolycyclicRecognition.modelNilradicalLinearAction
modelNilradicalRotation def: The compact rotation on the chosen nilpotent model's tangent algebra. · OAI.PolycyclicRecognition.modelNilradicalRotation
modelNormSet def: The possible operator norms in all unital models of the Cuntz relations. · OAI.NuclearUltrapower.CuntzPolynomial.modelNormSet
modelNormSet def: The possible operator norms in all unital C*-models of the group. · OAI.NuclearUltrapower.GroupStarAlgebra.modelNormSet
ModelOrientedInputs def: The Derdzinski--Hitchin special case applies after establishing Weyl vanishing. · OAI.PositiveEinsteinFour.ModelOrientedInputs
modelPushforwardFreeIso def: The required source framing, obtained from CM freeness and the puncture isomorphisms of both models. · OAI.SourceConeMorphism.modelPushforwardFreeIso
modelPushforwardOverFreeIso def: The slice-site framing for the generic lattice construction. · OAI.SourceConeMorphism.modelPushforwardOverFreeIso
Models def: A model here is an arbitrary membership structure. This definition places no external well-foundedness, transitivity, or cardinal assumptions on the model. · OAI.PartitionConsistency.Models
modelVolumeBasis def: The determinant volume is normalized by the base point's horizontal frame. · OAI.KervaireIncidenceCurrent.modelVolumeBasis
modeRetentionNet def: The three actual source retentions. Each net is total also at malformed labels; the separately compiled label guard suppresses those outputs. · OAI.ExactQuantumFactoring.OrderTrial.Expressions.modeRetentionNet
modeSum def: Regroup a literal weighted family by its actual nonzero angular mode. Only algebra is used: no cross-family orthogonality is asserted. · OAI.ThreeTorus.PassagePackets.modeSum
modFiveHurwitzCombination def: An explicit analytic function for each of the three parameters. · OAI.TwoPointCorrelations.modFiveHurwitzCombination
modFiveMangoldtTwist def: The Dirichlet-series coefficients whose partial sums are required. · OAI.TwoPointCorrelations.modFiveMangoldtTwist
ModFiveThetaInput def: The precise published input: a fixed-modulus consequence of Koukoulopoulos, Theorem 12.1, before any application-dependent exclusions. · OAI.TwoPointCorrelations.ModFiveThetaInput
modification def: The Laurent subalgebra generated by T and r/T for r ∈ I. · OAI.StableCoordinate.ModificationPieces.modification
modificationComplex def: The sequence firstTor(layer) → restriction(modification) → kernel(restriction(E) → layer), before suppressing the harmless zero terms. · OAI.CartierConnecting.Boundary.modificationComplex
modificationKernelIso def: The right-hand kernel after restriction is the kernel of the last-factor quotient. · OAI.ActualCartier.modificationKernelIso
modificationMap def: The ambient quotient map for an elementary transform. · OAI.ActualCartier.modificationMap
modificationSequence def: A coherent elementary modification is the kernel along the divisor. · OAI.ActualCartier.modificationSequence
modificationToRotationalExtension def: The actual modification has the other proper cocompact inclusion. · OAI.PolycyclicRecognition.ComplexWeightFactorModel.modificationToRotationalExtension
modifiedBoundary def: In an exceptional block the input map equals its output map, so the central permutation is exactly identity. Elsewhere its inverse is uniform. · OAI.CubeShuffle.modifiedBoundary
modifiedReverseCoins def: A measure-preserving reversal of the actual modified coin experiment. At a leaf the redundant output butterfly is kept, while its uniform seed is inverted and conjugated. At higher nodes the two outer fair fields are swapped. · OAI.CubeShuffle.modifiedReverseCoins
modularAdaptiveCoefficients def: Choose any valid completion of the exposed prefix. The precision theorem below proves that the required reduced coefficients do not depend on it. · OAI.Ostmann.modularAdaptiveCoefficients
modularCompensatedEquations def: The equation of the moving construction, keeping its compensation product instead of replacing the new giant by a composite pivot. · OAI.Ostmann.PivotDependencyScheme.modularCompensatedEquations
modularCompressedTracialState def: The constructed state is selected through its proved specification, so GNS instance reduction does not unfold the entire modular weight construction. · OAI.WeakPureInfiniteness.modularCompressedTracialState
ModularCorePublishedInputs structure: The modular representation and source-core type are explicit hypotheses for descent through the regular core. · OAI.KadisonKastler.ModularCorePublishedInputs
modularFourierCompression def: Scalar compression after Fourier diagonalization. · OAI.WeakPureInfiniteness.modularFourierCompression
modularFourierInclusion def: The scalar inclusion in Fourier coordinates is an actual Hilbert-space isometry, rather than a formal change of spectral variables. · OAI.WeakPureInfiniteness.modularFourierInclusion
modularHalfGaussian def: A bounded regularization of the half-exponential. · OAI.WeakPureInfiniteness.modularHalfGaussian
modularLpRepresentation def: The actual modularly twisted coefficient representation. · OAI.WeakPureInfiniteness.modularLpRepresentation
modularPositiveOperator def: The positive part of the closed Tomita operator. · OAI.KadisonKastler.modularPositiveOperator
modularPower def: The complete bounded binary-power network. Inputs remain available for copying; the result is a separate output word. · OAI.ExactQuantumFactoring.BitArithmetic.modularPower
ModularSpectralResolution structure: The part of modular spectral theory used by the application. All operators retained here are bounded, including the restricted inverse. · OAI.KadisonKastler.ModularSpectralResolution
modularStrongUnitary def: The limiting group consists of actual unitaries, with inverse at negative time. · OAI.KadisonKastler.modularStrongUnitary
modularTranslationCalculus def: Functional calculus for regular translation, in the Fourier convention fixed by fourier_modularLpTranslate. · OAI.WeakPureInfiniteness.modularTranslationCalculus
module def: The ordinary C-module constructed from the complex equation. · OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.module
moduleBlockEquiv def: Exact module-input indexing by the manuscript's tuples of r+1 block lengths. · OAI.DerivedBar.RecursiveTotal.moduleBlockEquiv
moduleBlocks def: Remove the zero input degree from the list of bar lengths. · OAI.DerivedBar.RecursiveTotal.moduleBlocks
ModuleData structure: Actual finite nonnegatively graded modules; no character or duality property is folded into this data. · OAI.KLInvariance.Graded.ModuleData
moduleEvaluation abbrev: The native degree-zero-module evaluation, retaining its original B action and differential. · OAI.LittleFinitistic.BimoduleTotal.moduleEvaluation
moduleEvaluation abbrev: Actual tensor evaluation on projectives. · OAI.LittleFinitistic.ConcreteTensorEvaluation.moduleEvaluation
moduleExtendLeft def: Extension by zero into the left summand of a finite Hilbert C⋆-module. · OAI.KadisonKastler.moduleExtendLeft
moduleExtendRight def: Extension by zero into the right summand. · OAI.KadisonKastler.moduleExtendRight
moduleFlatCoordinates def: All recursive-total terms are identified with the manuscript's exact finite sum of tensor blocks. This includes discarding only proved zero input-degree terms. · OAI.DerivedBar.RecursiveTotal.moduleFlatCoordinates
moduleIndex def: The recursive total index attached to a block tuple, with input degree zero. · OAI.DerivedBar.RecursiveTotal.moduleIndex
moduleIso def: The coordinate-ring base-change isomorphism, with the restriction and extension of scalars in both corners. · OAI.AffineClosedBaseChange.moduleIso
moduleIso def: This is the original selected input, with precisely its constructed D-action. · OAI.LittleFinitistic.SelectedFirstBlockFamily.moduleIso
moduleK def: Name the generic residue scalar structure so concrete square-zero algebras need not unfold their entire construction during typeclass search. · OAI.LittleFinitistic.PDResidueScalar.moduleK
moduleMap def: Comparison as a morphism over the structure sheaf. · OAI.AffineExterior.moduleMap
moduleRestrictLeft def: Restriction to the left summand. · OAI.KadisonKastler.moduleRestrictLeft
moduleShapeEquiv def: Exact full-degree shape index, including the shift by the number of X slots. · OAI.DerivedBar.RecursiveTotal.moduleShapeEquiv
moduleSumCocone def: The native algebraic direct sum, with its actual coproduct maps. · OAI.DerivedBar.moduleSumCocone
moduleSummandIso def: Each surviving recursive-total summand is the exact previously indexed block tensor in degree r+n; the input is the original D-module. · OAI.DerivedBar.RecursiveTotal.moduleSummandIso
ModuliBound def: Leaf moduli obey the bound forced by the giant and sum-bin cutoffs. Internal cutoff factors are at most one in modulus. · OAI.Ostmann.HistorySmoothData.ModuliBound
modulusIterates def: Exact integer in rigidity.tex: N(r)=max(0,ceil(log_beta(R*/r))). The natural-number ceiling incorporates max with zero. · OAI.AffineBernstein.modulusIterates
mollifier def: A concrete normalized smooth approximate identity; all integrals retain the ambient Haar measure, rather than changing normalization. · OAI.WeakSobolev.mollifier
moment def: Oriented-plane coordinates of a unit isotropic vector. · OAI.ArnoldCounterexample.Factors.moment
moment def: Moments include all replica subsets, not only pair overlaps. · OAI.DilutedSpinGlass.Pattern.moment
moment def: The interpretation is the actual injective moment defined in Section 2. · OAI.MUB6.Certificate.ExponentCode.moment
moment def: isD denotes the nonzero-difference pairing. same is relevant only in its complementary pairing, where the two selected coordinates may coincide. · OAI.Problem335.LocalMomentWeights.moment
momentBase def: The exponent remains the literal 1/1000 fixed by the manuscript. · OAI.CubeShuffle.momentBase
MomentBound def: Real exponential version of the exact conditional main estimate, used only as the induction predicate; its equivalence to logMoment includes zero moments. · OAI.CoordinateSweeps.MomentBound
MomentF def: integrable densities with polynomial weights · OAI.GeneralMahler.MomentF
momentFrame def: The finite moment matrix which will be realized by actual radial Gamma variables and root phases rather than an assumed de Finetti density. · OAI.CoordinateSweeps.OrdinaryTensor.momentFrame
momentLocalFactor def: Before discarding U-coincidence factors, a normal U layer may have weight 1+B. The Boolean coincides records the relevant equality event. · OAI.Problem335.WordLocalProduct.momentLocalFactor
momentMatrix def: The moment matrix I + BC, expressed without choosing coordinates. · OAI.StationaryNS.momentMatrix
moments def: Target, constant and identity coordinates, all in the normalized local L² space. Their finite moments are the compactness output needed. · OAI.RegularPointCoordinates.EuclideanHarmonicModel.moments
momentSix def: The fifteen pairings of six indices, grouped by the partner of i. · OAI.PositiveEinsteinFour.Angular.momentSix
momentum def: Absolute angular momentum about a fixed point. · OAI.TriangularBilliards.Admissible.momentum
monochromaticEvent def: Either target bit is bad. · OAI.QuantitativeVanDerWaerden.SparsePerturbation.monochromaticEvent
monoError def: Only the allowed mass and energy budget changes; all constructed patches, operators and frozen frames are retained exactly. · OAI.RegularPointCoordinates.PatchIterationGeometry.monoError
monogenousPoint def: The parameter map onto the entire subcomplex generated by one simplex. · OAI.Thomason.Construction.RealizationPrism.monogenousPoint
monoid def: The manuscript's auxiliary monoid is generated by the six actual partial affine maps. none is an undefined value; composition is right first. · OAI.FiniteAlgebraicEnvelopes.PartialAffine.monoid
monoidLift def: The same direct limit has its universal property for all monoid maps, not only maps which preserve divisions and joins. · OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.monoidLift
monoidLift def: Evaluation of a directed union in an arbitrary target monoid. · OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.monoidLift
monoidMap def: The literal map of direct limits induced by a coherent map of stages. · OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.monoidMap
monomial def: The exact scalar weighted permutation attached to the oriented bands. · OAI.KervaireMatrix.monomial
monomialElement def: A monomial as a member of its assigned image-filtration piece. · OAI.StableCoordinate.GradedPresentationMap.monomialElement
monomialFunctional def: A functional on a symmetric power induces a symmetric multilinear form. · OAI.Problem346.monomialFunctional
MonomialMatrix def: Literal permutation-times-invertible-diagonal form on a finite index type. · OAI.ExactFourier.MonomialMatrix
monomialWeight def: The source weight (-1,0,0,1,1) on exponent vectors. · OAI.StableCoordinate.Filtration.monomialWeight
MontgomeryVaughanBound def: Precise published input: the constant is independent of the interval, length, coefficients, and any later translation of the height. · OAI.CubicFirstMoment.MontgomeryVaughanBound
MooreSphereDecomposition def: The precise topological published input. Singleton classes are allowed; every other class is connected and has connected nonempty complement. · OAI.CircleDomainRigidity.MooreSphereDecomposition
more def: Enlarge a machine's collection of hidden stacks. · OAI.Fifths.SM.more
MoritaClass def: Morita classes of all finite-group blocks over the fixed field K. · OAI.Donovan.MoritaClass
moritaClass def: The Morita class represented by a block. · OAI.Donovan.moritaClass
moritaSetoid def: The equivalence relation is linear Morita equivalence, not ring isomorphism or equivalence of the underlying un-enriched categories. · OAI.Donovan.FiniteGroupBlock.moritaSetoid
MostowSolvableLatticeUniformInput def: The connected-solvable specialization of Mostow's uniformity theorem. · OAI.PolycyclicRecognition.MostowSolvableLatticeUniformInput
motifChildSign def: A motif's actual outgoing type, allowing every integer displacement. · OAI.TraceReconstruction.motifChildSign
motifDifferenceWeight def: Coefficients of 1 + χ V + τ β D. · OAI.TraceReconstruction.motifDifferenceWeight
motifIndicator def: The literal support indicator of the length-2^s signed block. · OAI.TraceReconstruction.motifIndicator
motifOffset def: The actual displaced primitive slot in a period. · OAI.TraceReconstruction.motifOffset
motifPatternMultiplier def: A kernel-pattern multiplier averaged over the actual finitely supported anchor law. No independence of its involved positions is asserted. · OAI.TraceReconstruction.motifPatternMultiplier
motifShift def: The sign-dependent displacement in {-1,0,1}, represented by Fin 3. · OAI.TraceReconstruction.motifShift
Move structure: A complete chart change between coloured splitting trees, already lying in the proposed finite-generator subgroup. Leaf order is not imposed. · OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move
Move inductive: The deterministic local machine model is explicit; no oracle or arbitrary state-transition on whole inputs is included. Both alphabets are fixed finite types for each machine. Extra symbols and states allow arbitrary finite tables. · OAI.WLIdentification.Move
move def: Frequency moves · OAI.ExactDerandomization.Analysis.Square.move
move def: The formalization proves $\mathsf L=\mathsf{RL}=\mathsf{BPL}$ for binary languages in an explicit Turing-machine model with logarithmic workspace. The randomized classes use polynomial time: $\mathsf{RL}$ never accepts a no-instance and … · OAI.ExactDerandomization.Direction.move
move def: The membership branch totalizes the mathematical rule off its admitted rank/parameter domain. The ordinary regular/marked lemmas below prove it is never used on genuine source data. Wholesale steps use the canonical base. · OAI.KServer.CausalSimplex.move
move def: Transport of a filter along an order automorphism. It transports the filter, not the interpretation of all names in a single fixed extension. · OAI.PartitionConsistency.ForcingQuotient.GenericFilter.move
move def: Coordinate transport preserves the entire contraction, not merely a relation between ranges. · OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow.move
move def: Automorphisms of the poset obtained from its coded action. · OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.move
move def: Order-preserving transfer, implemented using two stack reversals. · OAI.RationalHitting.StackLanguage.move
move def: Relocate a single encoded value without reversing its bit order. · OAI.Superstring.BitCode.Block.move
moveAux def: Move the auxiliary from the front to position i, preserving the order of all physical sites. This is only a permutation, not a trace. · OAI.CriticalHoneycomb.Transfer.PlanarNormalization.moveAux
moveInput def: The formalization proves $\mathsf L=\mathsf{RL}=\mathsf{BPL}$ for binary languages in an explicit Turing-machine model with logarithmic workspace. The randomized classes use polynomial time: $\mathsf{RL}$ never accepts a no-instance and … · OAI.ExactDerandomization.Direction.moveInput
moveLast def: Move one selected row to the end, preserving the order of the rest. · OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.moveLast
moveMatches def: Conjugating the reversal while keeping port origins fixed is a matching switch, not a relabeling of the original graph. · OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.moveMatches
movement def: Pointwise membership movement; component labels are deliberately not moved. · OAI.PlanarL1.Columns.Model.Activity.movement
mover def: Current designated occurrence in the selected optimum; it is not observed. · OAI.KServer.FiniteExperiment.mover
moveRows def: This is transport of the row data, not an automorphism of one fixed universe of evaluated symmetric names. · OAI.PartitionConsistency.TailSelector.TailData.moveRows
moveWord def: Move an entire word without reversing its order. Each symbol is pushed and popped twice; this is not an atomic bulk-copy instruction. · OAI.ExactQuantumFactoring.BitStackProgram.moveWord
movingArithmeticCellValue def: A cell is accepted precisely when it contains an original supported integer in the prescribed progression. Invariance supplies the converse. · OAI.Ostmann.movingArithmeticCellValue
movingArithmeticModuli def: One frequency block, one square for each distinct internal prime, and one field for each spectator. · OAI.Ostmann.movingArithmeticModuli
movingArithmeticPrimePageFactor def: Both Page factors stay in the frequency block; the other blocks have exactly their uniform two-unit laws. · OAI.Ostmann.movingArithmeticPrimePageFactor
movingBulkProducts def: The two child bulk products in the same root-to-node order. · OAI.Ostmann.movingBulkProducts
movingCompactLeaf def: The zero frequency is removed and all live bottom frequencies are retained. · OAI.Ostmann.movingCompactLeaf
movingCompensationTargets def: The entries are ordered from the first removed type to the last. · OAI.Ostmann.movingCompensationTargets
movingCutoffExponent def: The square-root reserve agrees with the proved bottom cutoff at 4m. · OAI.Ostmann.movingCutoffExponent
MovingDescendantFrequencyIndex def: The root frequency is fixed by the amplitude; only its descendants are summed here, each under its own level cutoff. · OAI.Ostmann.MovingDescendantFrequencyIndex
movingEvent def: The moving-threshold event in the main theorem. · OAI.JointDickman.movingEvent
movingExternalDiagonalWeight def: The common regular multiplier depends only on the external draws. · OAI.Ostmann.movingExternalDiagonalWeight
movingFourierPolynomialFactors def: Exactly one clipped Fourier polynomial per terminal leaf, with the conjugation imposed by its actual left/right path. · OAI.Ostmann.movingFourierPolynomialFactors
movingFrameConstants def: These factors are computed from the fixed small and internal samples; no bulk coordinate or giant value is used. · OAI.Ostmann.movingFrameConstants
movingFrequencyCoefficient def: This is the current coefficient after the original internal prime samples and all descendant frequencies have been summed. Root guards remain in each term and are never turned into a conditioned probability law. · OAI.Ostmann.movingFrequencyCoefficient
movingFrequencyRate def: One unit of reserve is left for the root-frequency count. · OAI.Ostmann.movingFrequencyRate
movingFrequencySkeleton def: Discard descendant prime data, keeping all their frequencies. Root cutoffs may still impose the cross-branch frequency tests of Section 7.4. · OAI.Ostmann.movingFrequencySkeleton
movingFullOutsidePairwise def: Literal pairwise support at every current state, including the fixed outside list from the manuscript's recursive average. · OAI.Ostmann.movingFullOutsidePairwise
movingFullResidueSupport def: All terms here are periodic; the mutual top-giant gcd is kept outside. · OAI.Ostmann.movingFullResidueSupport
movingGiantAmplitude def: Ordinary integral evaluation, including the inserted-giant zero convention. All additional smooth and range factors can multiply this spectator factor. · OAI.Ostmann.movingGiantAmplitude
movingGiantAncestorRows def: The full path retains the same determinant invariant in the source order. · OAI.Ostmann.movingGiantAncestorRows
movingGiantOffDiagonal def: The inserted giant is N / (s * U). The compensation product U is retained, so the reconstructed integer is the giant and not the whole pivot. · OAI.Ostmann.movingGiantOffDiagonal
movingGiantPhase def: The two giant factors of Section 7.4, evaluated at their exact cofactors. The definition also applies to the integer giant in a transfer diagonal. · OAI.Ostmann.movingGiantPhase
MovingGiantSamples inductive: The four actual compensation positions per child leaf at a reversal. · OAI.Ostmann.MovingGiantSamples
movingGiantUnitPeriod def: A period for precisely the current unit tests and their descendant Euclidean divisions. No real inequalities are used in this definition. · OAI.Ostmann.movingGiantUnitPeriod
movingInternalLocalSupport def: All occurrences of a fixed internal prime impose their line modulo p and exclude its zero lift modulo p². Repeated occurrences remain simultaneous. · OAI.Ostmann.movingInternalLocalSupport
movingLocalExtra def: Original node factors depend on the current prime lists, two giants and complete frequency tree, not on prime samples which will be made later. · OAI.Ostmann.movingLocalExtra
movingLocalGiantUnits def: Tests the two giants against every subtree frequency, every current regular slot, and the fixed outside list. Mutual coprimality of the two current giants is deliberately separate. · OAI.Ostmann.movingLocalGiantUnits
movingNodeArithmeticGuard def: The original nine arithmetic tests at a node, in terms of its products. · OAI.Ostmann.movingNodeArithmeticGuard
movingNodeGuard def: The two word entries are the complete current child products, including all regular factors. The reconstructed pivot here is the composite u*p. · OAI.Ostmann.movingNodeGuard
movingOriginalDiagonalMean def: Both history averages and the external law are the original ones. · OAI.Ostmann.movingOriginalDiagonalMean
movingOriginalMatchedMean def: Both history averages and the external law are the original ones. · OAI.Ostmann.movingOriginalMatchedMean
movingOriginalPairPrimeKernel def: The fixed-sample prime integral before choosing any equality pattern. · OAI.Ostmann.movingOriginalPairPrimeKernel
movingOriginalPatternPrimeObservable def: The same actual prime integral in the full finite pattern coordinates. · OAI.Ostmann.movingOriginalPatternPrimeObservable
movingOriginalPrimePairMean def: The original external average of two sampled histories. The external weights may in particular be the unchanged product of harmonic prime priors. · OAI.Ostmann.movingOriginalPrimePairMean
movingOriginalSampleAverage def: The sampled Fourier coefficient, with all original support and all original internal probabilities. · OAI.Ostmann.movingOriginalSampleAverage
movingOriginalSupportedPair def: The literal product in the original sampled coefficient square. · OAI.Ostmann.movingOriginalSupportedPair
movingPatternFinRepresentative def: The base row is selected from a proved original occurrence, then mapped into the finite coordinate system used by polynomial comparison. · OAI.Ostmann.movingPatternFinRepresentative
movingPatternLogPrimeBulkHaar def: This is the original real kernel and its original Page and spectator averages, evaluated after inserting the selected prime draws. · OAI.Ostmann.movingPatternLogPrimeBulkHaar
movingPatternLogPrimeObservable def: The coefficient before selecting or conditioning any of its bulk coordinates. All original frequency and coprimality gates are retained. · OAI.Ostmann.movingPatternLogPrimeObservable
movingPatternLogTwoPrimeBulkHaar def: This is the original real kernel and its original Page and spectator averages, evaluated after inserting the selected prime draws. · OAI.Ostmann.movingPatternLogTwoPrimeBulkHaar
movingPatternLogTwoPrimeObservable def: The coefficient before selecting or conditioning any of its bulk coordinates. All original frequency and coprimality gates are retained. · OAI.Ostmann.movingPatternLogTwoPrimeObservable
movingPatternPrimeBulkHaar def: This is the original real kernel and its original Page and spectator averages, evaluated after inserting the selected prime draws. · OAI.Ostmann.movingPatternPrimeBulkHaar
movingPatternPrimeObservable def: The coefficient before selecting or conditioning any of its bulk coordinates. All original frequency and coprimality gates are retained. · OAI.Ostmann.movingPatternPrimeObservable
movingPatternRegularSlots def: The common top list, before its primes are drawn. · OAI.Ostmann.movingPatternRegularSlots
movingPatternSamples def: Fixed external labels and internal equality classes are kept separate. The latter number depends only on depth, not on the bulk length. · OAI.Ostmann.movingPatternSamples
movingPatternSupportedPrimeTerm def: The supported prime term of the original pattern, with its values pulled back along the finite assignment. · OAI.Ostmann.movingPatternSupportedPrimeTerm
movingPatternTwoPrimeBulkHaar def: This is the original real kernel and its original Page and spectator averages, evaluated after inserting the selected prime draws. · OAI.Ostmann.movingPatternTwoPrimeBulkHaar
movingPatternTwoPrimeObservable def: The coefficient before selecting or conditioning any of its bulk coordinates. All original frequency and coprimality gates are retained. · OAI.Ostmann.movingPatternTwoPrimeObservable
movingPrimeNodeFactor def: This factor uses only the current lists and three root frequencies. Descendant support is retained in the two child coefficients. · OAI.Ostmann.movingPrimeNodeFactor
movingProductExponent def: The logarithmic product budget left after each common pivot is removed. · OAI.Ostmann.movingProductExponent
movingProductFrequencyExponent def: Centering at the measured terminal product avoids charging its rounding error again at each subsequent transfer. · OAI.Ostmann.movingProductFrequencyExponent
movingRealWeight def: Real evaluation of the very same moving recursion, before arithmetic indicators. The reciprocal compensation product remains in every pivot. · OAI.Ostmann.movingRealWeight
movingRegularOther def: The denominator left after removing one regular prime and both giants. · OAI.Ostmann.movingRegularOther
movingRegularOutsidePairwise def: The outside list is fixed while the current regular slots change. These small-slot tests are independent of both top giant values. · OAI.Ostmann.movingRegularOutsidePairwise
MovingRegularSlot abbrev: Each surviving leaf has its remaining small slots and its original bulk. · OAI.Ostmann.MovingRegularSlot
movingRegularTransform def: Product of the actual local transforms, with their CRT cofactors. · OAI.Ostmann.movingRegularTransform
movingRepresentativeIndex def: Indices outside a representative's system repeat its selected base row. Thus every representative uses the same finite index without changing any test. · OAI.Ostmann.movingRepresentativeIndex
MovingRescalingNetFamily structure: Every radius and accuracy has a fixed finite label type across the whole sequence. The point at infinity is not introduced at this stage. · OAI.RegularPointCoordinates.MovingRescalingNetFamily
movingRestoredActive def: The extracted compensation primes retain their places in every cofactor, but the Cauchy step leaves no Fourier factor at those places. · OAI.Ostmann.movingRestoredActive
movingReverse def: Both source children order their giants as (new, retained). · OAI.Ostmann.GiantRows.movingReverse
movingReverseTemplate def: Restoring a removed type puts its four sampled compensation primes back before the surviving small slots. Bulk labels retain their identity. · OAI.Ostmann.movingReverseTemplate
movingSampledWeight def: The finite expansion keeps every internal sample's original prior. · OAI.Ostmann.movingSampledWeight
MovingSampleSlots inductive: The same sampler as MovingGiantSamples, before the prime labels have been evaluated. Four actual positions are used at each child leaf. · OAI.Ostmann.MovingSampleSlots
movingSignedGiantUnits def: Signed evaluation uses exact Euclidean division and hence is defined on all residue representatives, including representatives off the real support. · OAI.Ostmann.movingSignedGiantUnits
movingSlotCutoff def: The extra support test is literal divisibility of the composite pivot by its sampled compensation product. All smooth and other support factors stay in extra. · OAI.Ostmann.movingSlotCutoff
MovingSlotData inductive: At a node, the two regular lists exclude its moving giants. The compensation list is inserted in both children by the sampler. · OAI.Ostmann.MovingSlotData
movingSlotNaturalPath def: A path is written with its newest reversal first, matching the cleared row recursion. Each step is performed over the integers before reduction. · OAI.Ostmann.movingSlotNaturalPath
MovingSlotReversal structure: The products multiplying the current two giants, together with the actual compensation product in the denominator. Giants themselves are excluded. · OAI.Ostmann.MovingSlotReversal
movingSmallCellCenters def: A compensation type occurs four times in the full initial list. · OAI.Ostmann.movingSmallCellCenters
movingSubgroup def: Elements whose actual linear displacement lies in P. This is a subgroup even when the invariant bilinear form restricted to P is singular. · OAI.KLInvariance.TitsSpace.movingSubgroup
movingSumFactors def: The dependent disjoint union of two families, with its motive explicit. · OAI.Ostmann.movingSumFactors
movingSupportedWeight def: Multiplying by this mask retains all current-state coprimality and all subtree-frequency unit tests, including the fixed outside list. · OAI.Ostmann.movingSupportedWeight
movingTaggedTransform def: A common formula for regular factors and the two marked giant phases. Using the modulus as an explicit argument makes reindexing independent of presentation of the dependent residue types. · OAI.Ostmann.movingTaggedTransform
movingTemplateCompensationEquiv def: The compensation block is sampled once, in precisely the coordinates of movingCompensationPrior; the two child histories will share this block. · OAI.Ostmann.movingTemplateCompensationEquiv
movingTemplatePrimeAmplitude def: The finite prime amplitude, with both giants and every regular slot sampled from their original laws. The root frequency is not renormalized. · OAI.Ostmann.movingTemplatePrimeAmplitude
movingTopPeriod def: The period depends only on the fixed small data and frequencies. · OAI.Ostmann.movingTopPeriod
movingTransferSlotEquiv def: The first block is the removed giant and compensation. The second is one surviving giant and its remaining regular slots. · OAI.Ostmann.movingTransferSlotEquiv
movingUnrestrictedWeight def: Evaluation along the forced integer pivots with just the arithmetic indicators removed. The same leaf and node factors remain. · OAI.Ostmann.movingUnrestrictedWeight
movingWeightedDiagonalMean def: Both history averages and the external law are the original ones. · OAI.Ostmann.movingWeightedDiagonalMean
movingWeightedMatchedMean def: Both history averages and the external law are the original ones. · OAI.Ostmann.movingWeightedMatchedMean
Mrec def: Z=ξ^i Mk · OAI.GeneralMahler.SCal.Tail.JT.Mrec
MRTDistanceLowerBound def: The exact range of lower bounds required by corrected MRT Theorem 1.7. · OAI.TwoPointCorrelations.MRTDistanceLowerBound
MRTLiouvilleShortInput def: Natural-cutoff Liouville specialization of MRT Theorem 1.3. Endpoint conventions differ only at a measure-zero set of interval origins. · OAI.TwoPointCorrelations.MRTLiouvilleShortInput
mrtMeanSquareKernel def: The integrable exponential time weight, with angular frequency ω. · OAI.TwoPointCorrelations.mrtMeanSquareKernel
mrtModulusCutoff def: The character-modulus cutoff in corrected MRT Theorem 1.7. · OAI.TwoPointCorrelations.mrtModulusCutoff
mrtShortError def: The error shared by MRT Theorems 1.3 and 1.7. · OAI.TwoPointCorrelations.mrtShortError
MRTShortExponentialInput def: Natural-cutoff specialization of corrected MRT Theorem 1.7, with an explicit lower bound M in place of the infimum of squared distances. · OAI.TwoPointCorrelations.MRTShortExponentialInput
MRTWeakHurwitzGrowthInput def: A polynomial logarithmic bound on the shrinking VK disk. Removing the first Hurwitz term makes the bound uniform down to a = 0. · OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput
mtw def: The Ma–Trudinger–Wang fourth derivative with factor -3/2. · OAI.WeakMTWTransport.mtw
mu def: The true-metric posterior after t requests, independent of algorithmic tapes. · OAI.KServer.FiniteExperiment.mu
muBefore def: Old counting measure filtered through the new true request. · OAI.KServer.FiniteExperiment.muBefore
mul def: Gluing the marked outside disks along a zero-sign corner concatenates their words. The second potential is gauged to agree at the glued marker. · OAI.KervaireRibbon.OuterRibbon.mul
mul def: Multiplying equations adds degrees and preserves nonzeroness. · OAI.Nagata.W16.NonzeroHomogeneousForm.mul
mul def: Products of four-frame lifts induce the corresponding product of three-dimensional coefficient changes. · OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.mul
mul def: A disjoint-coordinate product has the product of the local coefficients. · OAI.Problem335.FactorialExpansion.mul
mul def: Composition of actual finite dyadic PL witnesses, using the sorted union of the inner breakpoints and pulled-back outer breakpoints. · OAI.ThompsonNonamenability.DyadicPLWitness.mul
mulAccWord def: Shift-and-add on explicit little-endian words. · OAI.RationalHitting.StackLanguage.mulAccWord
mulBody def: Registers: 0 multiplicand, 1 multiplier, 2 accumulator, 3 copied addend, 4/5/6 addition scratch, 7 copy scratch. · OAI.RationalHitting.StackLanguage.mulBody
mulEquiv def: No splitting is assumed: the section factor supplies the full group law. · OAI.PolycyclicRecognition.GroupExtensionSection.mulEquiv
mulExponent def: Exponents of the variables acting by multiplication. · OAI.Problem335.mulExponent
mulI def: Multiplication by i as an endomorphism of the countable core. · OAI.KadisonKastler.RationalComplexCore.mulI
mulLinear def: Multiplication by the linear polynomial a + scale * X. · OAI.DefocusingNLS.SeparatorArithmetic.mulLinear
mulMod def: Full double-width product followed by full double-width remainder, with no word overflow. The narrow remainder is valid because the modulus is a word. · OAI.ExactQuantumFactoring.BitArithmetic.mulMod
mulModGridEquiv def: Multiplication by a coprime natural number permutes the finite residues. · OAI.QuantitativeVanDerWaerden.mulModGridEquiv
multibarAugmentedDifferential def: Explicit bar faces with a sign change on crossing a D slot and no sign change on crossing an X slot. This is defined independently of count transport. · OAI.DerivedBar.SquareZero.multibarAugmentedDifferential
multibarCountDifferential def: Restriction of the independently defined literal faces to count r. · OAI.DerivedBar.SquareZero.multibarCountDifferential
multibarTwoSidedDifferential def: The independent two-sided differential. The first face uses D's right A-action by projection. All remaining faces use the explicit slot parity recursion. · OAI.DerivedBar.SquareZero.multibarTwoSidedDifferential
multiFactorial def: The product of coordinate factorials of an exponent vector. · OAI.Problem335.multiFactorial
MultiGraph structure: `MultiGraph n m` has vertices `Fin n` and edge copies `Fin m`. Each edge copy has a left and right endpoint, and `loopless` rules out an edge whose two endpoints coincide. · OAI.StrongThinTree.MultiGraph
MultihomogeneousEquation structure: An equation homogeneous separately in each block of three coordinates. The support condition is the ordinary definition of multihomogeneity. · OAI.Nagata.ProjectiveGeometry.MultihomogeneousEquation
multilinearDescend def: A multilinear map constant on the fibers of coordinatewise surjections descends. · OAI.Problem346.multilinearDescend
multilinearPolynomial def: The scalar polynomial obtained by feeding a multilinear form vector variables, with block i specifying which vector variable occurs in its ith argument. · OAI.Problem346.multilinearPolynomial
multiple def: The ideal multiple, defined as the image of the ideal action. · OAI.CartierImageFiltration.multiple
multiplication def: Multiplication by a bounded scalar jet, as a bounded linear operator on the unknown jet. · OAI.ForcedComputation.PlaneScalarMild.multiplication
multiplicationDiagonalTerm def: The multiplying diagonal term, extended by zero when its backward shift is invalid. · OAI.Problem335.LocalMoments.multiplicationDiagonalTerm
Multiplicative def: Ordinary multiplicativity is required only for coprime positive arguments; this also permits the identically zero function, as does the manuscript. · OAI.TwoPointCorrelations.Multiplicative
multiplicativeCell def: The multiplicative cell with positive center s, exactly the cell of bounds.tex:219: no choice of transverse normalization occurs in this set. · OAI.AffineBernstein.multiplicativeCell
MultiplicativeExponentialInput def: The finite partial-sum specialization of Montgomery--Vaughan Cor. 1. · OAI.JointDickman.PublishedInputs.MultiplicativeExponentialInput
MultiplicativeLineCover abbrev: The total space before taking the multiplicative-period quotient. · OAI.Nagata.W21.MultiplicativeLineCover
multiplicity def: Full-word multiplicity of a label. · OAI.QuantitativeVanDerWaerden.OuterWordTests.multiplicity
multiplicity def: Constant traversal multiplicity on each original marked chain. · OAI.TorsionFreeZeroDivisors.ChainSubdivision.multiplicity
multiplicity def: Largest-remainder multiplicities computed from the exact input weights. · OAI.UniqueGamesTheorem.Explicit.RationalWeights.multiplicity
multiplicityAtLeast def: Local multiplicity lower bounds are membership in powers of the point ideal. · OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast
multiplicityAtLeast def: Algebraic vanishing order in every chart containing the point, using powers of the genuine maximal ideal in the affine coordinate ring. · OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast
multiplicityCompression def: Compression to a chosen unit vector in the non-multiplicity factor. · OAI.KadisonSimilarity.multiplicityCompression
MultiplicityMatrixCovariance structure: Word covariance before taking scalar multiplicity slices. · OAI.KadisonSimilarity.MultiplicityMatrixCovariance
multiplicitySlice def: A scalar matrix coefficient in the multiplicity space. · OAI.KadisonSimilarity.multiplicitySlice
multiplicityWordInclusion def: A unit vector in the centered tensor power inserts the base Hilbert space isometrically into the corresponding multiplicity space. · OAI.KadisonSimilarity.multiplicityWordInclusion
MultiplicityWordSpace abbrev: The actual space of one word level, including its degree-dependent multiplicity. · OAI.KadisonSimilarity.MultiplicityWordSpace
multipliedThetaCoefficient def: The exact second-branch scalar coefficient. · OAI.Nagata.W22.multipliedThetaCoefficient
multiplier def: Two powers allow the bilinear products and two powers allow stripping all small-prime factors of a cube-free modulus. · OAI.Problem337.CompositeSupply.multiplier
multiplierBound def: The bound b_(k+2)(ε), indexed by the excess clique size. · OAI.CliqueFreeIndependence.WeightedGraph.multiplierBound
multiplierChart def: The source formulas into the genuine multiplier-bundle set quotient. · OAI.Nagata.Workers.W05.multiplierChart
MultiplierCritical def: The constrained critical equations of the polynomial. · OAI.ArnoldCounterexample.ThreePoints.MultiplierCritical
multiplierDiscriminant def: The absolute order discriminant in the index convention. · OAI.DukePrimeDegree.multiplierDiscriminant
multiplierFibreChart def: An actual quotient local homeomorphism whose image covers every fibre above the base slice, rather than a bounded portion of each fibre. · OAI.Nagata.W21.multiplierFibreChart
MultiplierHypotheses structure: Positivity, nonconstancy, mean one, and finite second moment of the multiplier law. · OAI.IndependentProducts.MultiplierHypotheses
multiplierIndex def: Index of the multiplier order inside the maximal order. · OAI.DukePrimeDegree.multiplierIndex
multiplierIterate def: Every integer iterate exists because the generator has a proved inverse. · OAI.Nagata.W21.multiplierIterate
multiplierLocalChart def: An injective open subset of the covering surface yields an actual local homeomorphism of the total multiplier quotient. · OAI.Nagata.W21.multiplierLocalChart
multiplierOrbitSetoid def: Orbit relation of the explicit integer iterates. · OAI.Nagata.W21.multiplierOrbitSetoid
multiplierOrder def: Elements of the field preserving the given integer lattice. · OAI.DukePrimeDegree.multiplierOrder
multiplierPhase def: Unit-norm phase, defined directly from the original multiplier. · OAI.Nagata.W02.multiplierPhase
multiplierQuotientMk def: Canonical projection from the covering surface to its multiplier orbit quotient. · OAI.Nagata.W21.multiplierQuotientMk
multiplierQuotientProjection def: Quotienting the scalar multiplier action preserves its projection to the base period quotient; this is not an asserted bundle structure. · OAI.Nagata.W21.multiplierQuotientProjection
multiplierSigma def: Real exponent carrying the absolute value of the multiplier. · OAI.Nagata.W02.multiplierSigma
multiplierStep def: The manuscript's generator (z,t) ↦ (τz, γz⁻ⁿt) as an actual equivalence. Units supply the inverse multiplier; invertibility is not assumed as a field. · OAI.Nagata.W21.multiplierStep
multiply def: Multiply both coefficients by a first-input polynomial. · OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply
multiply def: The normalized multiplication instruction; the accumulator starts at zero. After execution register 2 is the canonical binary product. · OAI.RationalHitting.StackLanguage.multiply
multiplyClean def: Clean multiplication interface used by the finite rising-product loop. · OAI.RationalHitting.StackLanguage.multiplyClean
multiplyInTime def: A time witness with the exact transition count, including restoration of the operand delimiter and removal of the counter delimiter. · OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.multiplyInTime
multiplyInTime def: A time witness with the exact transition count, including restoration of the operand delimiter and removal of the counter delimiter. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.multiplyInTime
multiplyPackets def: Actual spectral multiplication of every retained angular coefficient. · OAI.ThreeTorus.multiplyPackets
multiplyPower def: Multiplication by a fixed function power is a linear map on actual functions. · OAI.Nagata.CoefficientSpaces.multiplyPower
multiplySection def: The literal multiplication map restricted to actual automorphic sections. · OAI.Nagata.CoefficientSpaces.multiplySection
multiplySlots def: Multiplication uses radix, accumulator, output, counter, and scratch, skipping the independently preserved digit stack. · OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.multiplySlots
multiplySlots def: Multiplication uses radix, accumulator, output, counter, and scratch, skipping the independently preserved digit stack. · OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.multiplySlots
mulVecAddHom def: Left multiplication of columns, viewed purely additively. · OAI.FiniteAlgebraicEnvelopes.Steinberg.mulVecAddHom